(meta-info (comment "Example 37 Winkler et al. 2018"))
(meta-info (comment "Modified as we need a conversion toTree such that it type checks and is a valid LCTRS"))
(format LCTRS :logic QF_LIA)

(fun add 2 :sort (Int List List))
(fun cons 2 :sort (Int List List))
(fun @ 2 :sort (List List List))
(fun sort 1 :sort (List List))
(fun flatten 1 :sort (Tree List))
(fun tsort 1 :sort (Tree Tree))
(fun N 2 :sort (Tree Tree Tree))
(fun L 1 :sort (Int Tree))
(fun Nil 0 :sort (List))
(fun singleton 1 :sort (Int List))
(fun toTree 1 :sort (List Tree))

(rule (@ Nil xs) xs)
(rule (add x Nil) (singleton x))
(rule (add x (cons y ys)) (cons y (add x ys)) :guard (>= x y))
(rule (sort (cons x xs)) (add x (sort xs)))
(rule (flatten (N x y)) (@ (flatten x) (flatten y)))
(rule (tsort t) (toTree (sort (flatten t))))
(rule (@ (cons x xs) ys) (cons x (@ xs ys)))
(rule (add x (cons y ys)) (cons x (cons y ys)) :guard (< x y))
(rule (sort Nil) Nil)
(rule (flatten (L x)) (singleton x))
(rule (N x y) (N y x))