MAYBE

(format LCTRS :logic QF_LIA)
(fun a 0 :sort (Int))
(fun b 0 :sort (Int))
(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) (g a (+ y_1 y_1)) :guard (and (>= y_1 x_0) (= y_1 1)) :vars ((x_0 Int) (y_1 Int)))
(rule (h (f x_2 y_3)) (h (g b 2)) :guard (>= x_2 y_3) :vars ((x_2 Int) (y_3 Int)))
(rule a b)
(rule (g x_4 y_5) (g y_5 x_4) :vars ((x_4 Int) (y_5 Int)))

Confluence could not be determined.

Elapsed Time:   6.26 ms