(format LCTRS :logic QF_LIA)

(fun insert 2 :sort (Int List List))
(fun sort 1 :sort (List List))
(fun cons 2 :sort (Int List List))
(fun nil 0 :sort (List))
(fun rev 1 :sort (List List))
(fun app 2 :sort (List List List))
(fun tsort 1 :sort (List List))
(fun flatten 1 :sort (List List))
(fun leaf 1 :sort (Int List))
(fun node 2 :sort (List List List))

(rule (app nil xs) xs)
(rule (app (cons x xs) ys) (cons x (app xs ys)))
(rule (insert x nil) (cons x nil))
(rule (insert x (cons y nil)) (cons x (cons y nil)) :guard (< x y))
(rule (insert x (cons y ys)) (cons y (insert x ys)) :guard (>= x y))
(rule (sort nil) nil)
(rule (sort (cons x xs)) (insert x (sort xs)))
(rule (flatten (leaf x)) (cons x nil))
(rule (flatten (node x y)) (app (flatten x) (flatten y)))
(rule (node x y) (node y x))
(rule (tsort x) (sort (flatten x)))