MAYBE (format LCTRS :logic QF_LIA) (fun f 1 :sort (Int Int)) (fun g 2 :sort (Int Int Int)) (fun h 1 :sort (Int Int)) (rule (f x_0) (g x_0 x_0) :guard (<= x_0 0) :vars ((x_0 Int))) (rule (h (f x_1)) (h x_1) :guard (>= x_1 0) :vars ((x_1 Int))) (rule (g (f x_2) y_3) (g x_2 z_4) :guard (and (> x_2 0) (> z_4 x_2)) :vars ((x_2 Int) (y_3 Int) (z_4 Int))) (rule (g x_5 (+ x_5 y_6)) (f y_6) :guard (and (> x_5 0) (> y_6 0)) :vars ((x_5 Int) (y_6 Int))) Confluence could not be determined. Elapsed Time: 12.06 ms