MAYBE (format LCTRS :logic QF_LIA) (fun end 0 :sort (Unit)) (fun f 1 :sort (Int Unit)) (fun g 1 :sort (Int Unit)) (fun h 1 :sort (Int Unit)) (fun h' 1 :sort (Int Unit)) (fun i 1 :sort (Int Unit)) (fun i' 1 :sort (Int Unit)) (fun start 0 :sort (Unit)) (rule (i' x_0) (f x_0) :vars ((x_0 Int))) (rule (i x_1) (i' (+ x_1 1)) :vars ((x_1 Int))) (rule (h' x_2) (f x_2) :vars ((x_2 Int))) (rule (h x_3) (h' (- x_3 12)) :vars ((x_3 Int))) (rule (g x_4) (i x_4) :guard (not (> x_4 2)) :vars ((x_4 Int))) (rule (g x_5) (h x_5) :guard (> x_5 2) :vars ((x_5 Int))) (rule (f x_6) end :guard (not (> x_6 0)) :vars ((x_6 Int))) (rule (f x_7) (g x_7) :guard (> x_7 0) :vars ((x_7 Int))) (rule start (f input_8) :vars ((input_8 Int))) Confluence could not be determined. Elapsed Time: 18.42 ms