YES (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))) Confluent by Almost Parallel Closedness with proof: no critical pairs Elapsed Time: 15.81 ms