YES (format LCTRS :logic QF_LIA) (fun sum1 1 :sort (Int Int)) (rule (sum1 x_0) (+ x_0 (sum1 (- x_0 1))) :guard (<= 0 (- x_0 1)) :vars ((x_0 Int))) (rule (sum1 x_1) 0 :guard (<= x_1 0) :vars ((x_1 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 11.58 ms