MAYBE

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

(rule (@ Nil xs_0) xs_0 :vars ((xs_0 List)))
(rule (add x_1 Nil) (singleton x_1) :vars ((x_1 Int)))
(rule (add x_2 (cons y_3 ys_4)) (cons y_3 (add x_2 ys_4)) :guard (>= x_2 y_3) :vars ((x_2 Int) (y_3 Int) (ys_4 List)))
(rule (sort (cons x_5 xs_6)) (add x_5 (sort xs_6)) :vars ((x_5 Int) (xs_6 List)))
(rule (flatten (N x_7 y_8)) (@ (flatten x_7) (flatten y_8)) :vars ((x_7 Tree) (y_8 Tree)))
(rule (tsort t_9) (toTree (sort (flatten t_9))) :vars ((t_9 Tree)))
(rule (@ (cons x_10 xs_11) ys_12) (cons x_10 (@ xs_11 ys_12)) :vars ((x_10 Int) (xs_11 List) (ys_12 List)))
(rule (add x_13 (cons y_14 ys_15)) (cons x_13 (cons y_14 ys_15)) :guard (< x_13 y_14) :vars ((x_13 Int) (y_14 Int) (ys_15 List)))
(rule (sort Nil) Nil)
(rule (flatten (L x_16)) (singleton x_16) :vars ((x_16 Int)))
(rule (N x_17 y_18) (N y_18 x_17) :vars ((x_17 Tree) (y_18 Tree)))

Confluence could not be determined.

Elapsed Time:  16.97 ms