MAYBE

(format LCTRS :logic QF_LIA)
(fun f 2 :sort (Int Int Int))
(fun g 2 :sort (Int Int Int))
(fun h 1 :sort (Int Int))

(rule (f x_0 y_1) (+ (f z_2 y_1) 1) :guard (and (>= x_0 1) (= z_2 (- x_0 1))) :vars ((x_0 Int) (y_1 Int) (z_2 Int)))
(rule (g 0 y_3) y_3 :guard (<= x_4 0) :vars ((y_3 Int) (x_4 Int)))
(rule (f x_5 0) (g 1 x_5) :guard (<= x_5 1) :vars ((x_5 Int)))
(rule (g 1 1) (+ (g 1 0) 1))
(rule (h x_6) (+ (g 1 x_6) 1) :guard (<= x_6 1) :vars ((x_6 Int)))
(rule (h x_7) (+ (f (- x_7 1) 0) 2) :guard (>= x_7 1) :vars ((x_7 Int)))

Confluence could not be determined.

Elapsed Time:  75.69 ms