YES (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Unit)) (fun sum1 1 :sort (Int Unit)) (fun u 3 :sort (Int Int Int Unit)) (rule (u n_0 s_1 i_2) (return s_1) :guard (not (<= i_2 n_0)) :vars ((n_0 Int) (s_1 Int) (i_2 Int))) (rule (u n_3 s_4 i_5) (u n_3 (+ s_4 i_5) (+ i_5 1)) :guard (<= i_5 n_3) :vars ((n_3 Int) (s_4 Int) (i_5 Int))) (rule (sum1 n_6) (u n_6 0 0) :vars ((n_6 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 9.27 ms