MAYBE

(format LCTRS :logic QF_LIA)
(fun geq 2 :sort (Int Int Bool))
(fun geq2 4 :sort (Int Int Int Int Bool))
(fun p 1 :sort (Int Int))
(fun plus 2 :sort (Int Int Int))
(fun s 1 :sort (Int Int))
(fun sum 1 :sort (Int Int))
(fun sum2 2 :sort (Bool Int Int))

(rule (sum x_0) (sum2 (geq 0 x_0) x_0) :vars ((x_0 Int)))
(rule (sum2 true x_1) 0 :vars ((x_1 Int)))
(rule (sum2 false (s x_2)) (plus (s x_2) (sum x_2)) :vars ((x_2 Int)))
(rule (plus (p x_3) y_4) (p (plus x_3 y_4)) :vars ((x_3 Int) (y_4 Int)))
(rule (plus (s x_5) y_6) (s (plus x_5 y_6)) :vars ((x_5 Int) (y_6 Int)))
(rule (plus 0 y_7) y_7 :vars ((y_7 Int)))
(rule (s (p x_8)) x_8 :vars ((x_8 Int)))
(rule (p (s x_9)) x_9 :vars ((x_9 Int)))
(rule (geq x_10 y_11) (geq2 x_10 y_11 0 0) :vars ((x_10 Int) (y_11 Int)))
(rule (geq2 (s x_12) y_13 z_14 u_15) (geq2 x_12 y_13 (s z_14) u_15) :vars ((x_12 Int) (y_13 Int) (z_14 Int) (u_15 Int)))
(rule (geq2 (p x_16) y_17 z_18 u_19) (geq2 x_16 y_17 z_18 (s u_19)) :vars ((x_16 Int) (y_17 Int) (z_18 Int) (u_19 Int)))
(rule (geq2 0 (s x_20) y_21 z_22) (geq2 0 x_20 y_21 (s z_22)) :vars ((x_20 Int) (y_21 Int) (z_22 Int)))
(rule (geq2 0 (p x_23) y_24 z_25) (geq2 0 x_23 (s y_24) z_25) :vars ((x_23 Int) (y_24 Int) (z_25 Int)))
(rule (geq2 0 0 (s x_26) (s y_27)) (geq2 0 0 x_26 y_27) :vars ((x_26 Int) (y_27 Int)))
(rule (geq2 0 0 x_28 0) true :vars ((x_28 Int)))
(rule (geq2 0 0 0 (s x_29)) false :vars ((x_29 Int)))

Confluence could not be determined.

Elapsed Time: 171.58 ms