MAYBE

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

(rule (app nil xs_0) xs_0 :vars ((xs_0 List)))
(rule (app (cons x_1 xs_2) ys_3) (cons x_1 (app xs_2 ys_3)) :vars ((x_1 Int) (xs_2 List) (ys_3 List)))
(rule (insert x_4 nil) (cons x_4 nil) :vars ((x_4 Int)))
(rule (insert x_5 (cons y_6 nil)) (cons x_5 (cons y_6 nil)) :guard (< x_5 y_6) :vars ((x_5 Int) (y_6 Int)))
(rule (insert x_7 (cons y_8 ys_9)) (cons y_8 (insert x_7 ys_9)) :guard (>= x_7 y_8) :vars ((x_7 Int) (y_8 Int) (ys_9 List)))
(rule (sort nil) nil)
(rule (sort (cons x_10 xs_11)) (insert x_10 (sort xs_11)) :vars ((x_10 Int) (xs_11 List)))
(rule (flatten (leaf x_12)) (cons x_12 nil) :vars ((x_12 Int)))
(rule (flatten (node x_13 y_14)) (app (flatten x_13) (flatten y_14)) :vars ((x_13 List) (y_14 List)))
(rule (node x_15 y_16) (node y_16 x_15) :vars ((x_15 List) (y_16 List)))
(rule (tsort x_17) (sort (flatten x_17)) :vars ((x_17 List)))

Confluence could not be determined.

Elapsed Time:  27.13 ms