MAYBE

(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))
(fun sum3 2 :sort (Int Int Int))
(fun sum_decl 1 :sort (Int Int))
(fun u_3 2 :sort (Int Int Int))

(rule (sum3 x_0 n_1) (+ n_1 (sum3 x_0 (+ n_1 1))) :guard (>= x_0 n_1) :vars ((x_0 Int) (n_1 Int)))
(rule (sum3 x_2 n_3) 0 :guard (< x_2 n_3) :vars ((x_2 Int) (n_3 Int)))
(rule (u_3 z_4 i_5) z_4 :guard (<= i_5 0) :vars ((z_4 Int) (i_5 Int)))
(rule (u_3 z_6 i_7) (u_3 (+ z_6 i_7) (- i_7 1)) :guard (> i_7 0) :vars ((z_6 Int) (i_7 Int)))
(rule (sum_decl x_8) (u_3 0 x_8) :vars ((x_8 Int)))
(rule (sum x_9) (+ x_9 (sum (- x_9 1))) :guard (<= 0 (- x_9 1)) :vars ((x_9 Int)))
(rule (sum x_10) 0 :guard (<= x_10 0) :vars ((x_10 Int)))

Confluence could not be determined.

Elapsed Time:   6.34 ms