YES (format LCTRS :logic QF_LIA) (fun sum 1 :sort (Int Int)) (fun test 1 :sort (Int Unit)) (rule (test x_0) (test y_1) :guard (and (> x_0 0) (= x_0 (+ y_1 1))) :vars ((x_0 Int) (y_1 Int))) (rule (sum x_2) (+ x_2 (sum (- x_2 1))) :guard (< 0 x_2) :vars ((x_2 Int))) (rule (sum 0) 0) (rule (sum x_3) 0 :guard (< x_3 0) :vars ((x_3 Int))) Confluent by Newmans Lemma with proof: terminating and no critical pairs Elapsed Time: 15.51 ms