MAYBE

(format LCTRS :logic QF_LIA)
(fun plus 2 :sort (Int Int Int))
(fun sum 1 :sort (Int Int))
(fun sumsum 1 :sort (Int Int))
(fun sumsum1 1 :sort (Int Int))
(fun u0 4 :sort (Int Int Int Int Int))
(fun u1 4 :sort (Int Int Int Int Int))

(rule (plus x_0 y_1) (+ x_0 y_1) :vars ((x_0 Int) (y_1 Int)))
(rule (u0 x_2 i_3 j_4 z_5) (u1 x_2 i_3 0 z_5) :guard (>= x_2 i_3) :vars ((x_2 Int) (i_3 Int) (j_4 Int) (z_5 Int)))
(rule (u0 x_6 i_7 j_8 z_9) z_9 :guard (not (>= x_6 i_7)) :vars ((x_6 Int) (i_7 Int) (j_8 Int) (z_9 Int)))
(rule (u1 x_10 i_11 j_12 z_13) (u1 x_10 i_11 (+ j_12 1) (+ z_13 j_12)) :guard (>= i_11 j_12) :vars ((x_10 Int) (i_11 Int) (j_12 Int) (z_13 Int)))
(rule (u1 x_14 i_15 j_16 z_17) (u0 x_14 (+ i_15 1) j_16 z_17) :guard (not (>= i_15 j_16)) :vars ((x_14 Int) (i_15 Int) (j_16 Int) (z_17 Int)))
(rule (sumsum1 x_18) (u0 x_18 0 0 0) :vars ((x_18 Int)))
(rule (sumsum x_19) 0 :guard (<= x_19 0) :vars ((x_19 Int)))
(rule (sumsum x_20) (plus (sumsum (- x_20 1)) (sum x_20)) :guard (>= (- x_20 1) 0) :vars ((x_20 Int)))
(rule (sum x_21) (plus (sum (- x_21 1)) x_21) :guard (>= (- x_21 1) 0) :vars ((x_21 Int)))
(rule (sum x_22) 0 :guard (<= x_22 0) :vars ((x_22 Int)))

Confluence could not be determined.

Elapsed Time:   6.37 ms