MAYBE

(format LCTRS :logic QF_LIA)
(fun eval1 2 :sort (Int Int Unit))
(fun eval2 2 :sort (Int Int Unit))
(fun eval3 2 :sort (Int Int Unit))

(rule (eval3 x_0 y_1) (eval2 (- x_0 1) (+ y_1 1)) :guard (> x_0 0) :vars ((x_0 Int) (y_1 Int)))
(rule (eval3 x_2 y_3) (eval3 (+ x_2 1) (- y_3 1)) :guard (> x_2 0) :vars ((x_2 Int) (y_3 Int)))
(rule (eval2 x_4 y_5) (eval1 x_4 y_5) :guard (not (> x_4 0)) :vars ((x_4 Int) (y_5 Int)))
(rule (eval2 x_6 y_7) (eval2 (- x_6 1) (+ y_7 1)) :guard (and (> x_6 0) (>= x_6 0)) :vars ((x_6 Int) (y_7 Int)))
(rule (eval1 x_8 y_9) (eval3 x_8 y_9) :guard (>= y_9 x_8) :vars ((x_8 Int) (y_9 Int)))
(rule (eval1 x_10 y_11) (eval2 x_10 y_11) :guard (and (> x_10 y_11) (>= x_10 0)) :vars ((x_10 Int) (y_11 Int)))

Confluence could not be determined.

Elapsed Time: 186.75 ms