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