YES (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Unit)) (fun sum1 1 :sort (Int Unit)) (rule (sum1 n_0) (return (div (* n_0 (+ n_0 1)) 2)) :guard (not (< n_0 0)) :vars ((n_0 Int))) (rule (sum1 n_1) (return 0) :guard (< n_1 0) :vars ((n_1 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 9.65 ms