YES (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Int)) (fun sum1 1 :sort (Int Int)) (fun u 3 :sort (Int Int Int Int)) (rule (sum1 n_0) (u n_0 1 0) :vars ((n_0 Int))) (rule (u n_1 i_2 k_3) (u n_1 (+ i_2 1) (+ k_3 i_2)) :guard (<= i_2 n_1) :vars ((n_1 Int) (i_2 Int) (k_3 Int))) (rule (u n_4 i_5 k_6) (return k_6) :guard (not (<= i_5 n_4)) :vars ((n_4 Int) (i_5 Int) (k_6 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 15.44 ms