MAYBE (format LCTRS :logic QF_LIA) (fun f 2 :sort (Int Int Unit)) (fun g 1 :sort (Int Unit)) (rule (f x4_0 (+ x4_0 y4_1)) (g y4_1) :guard (> x4_0 0) :vars ((x4_0 Int) (y4_1 Int))) (rule (f x3_2 y3_3) (g y3_3) :guard (< x3_2 y3_3) :vars ((x3_2 Int) (y3_3 Int))) (rule (f x2_4 y2_5) (g x2_4) :guard (<= x2_4 y2_5) :vars ((x2_4 Int) (y2_5 Int))) (rule (f x1_6 y1_7) (g (+ x1_6 y1_7)) :guard (>= x1_6 y1_7) :vars ((x1_6 Int) (y1_7 Int))) Confluence could not be determined. Elapsed Time: 2.62 ms