MAYBE

(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))

(rule (sum x_0) 0 :guard (>= 0 x_0) :vars ((x_0 Int)))
(rule (sum x_1) (+ x_1 (sum (+ x_1 (- 1)))) :guard (not (>= 0 x_1)) :vars ((x_1 Int)))

Confluence could not be determined.

Elapsed Time:   4.66 ms