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:  29.54 ms