YES (format LCTRS :logic QF_LIA) (fun ditch_globals 1 :sort (Unit Result)) (fun return 3 :sort (Int Int Int Unit)) (fun return1 1 :sort (Int Result)) (fun sum1 3 :sort (Int Int Int Unit)) (fun u 3 :sort (Int Int Int Unit)) (rule (ditch_globals (return x_0 y_1 z_2)) (return1 z_2) :vars ((x_0 Int) (y_1 Int) (z_2 Int))) (rule (u num_3 i_4 answer_5) (return i_4 answer_5 answer_5) :guard (not (<= i_4 num_3)) :vars ((num_3 Int) (i_4 Int) (answer_5 Int))) (rule (u num_6 i_7 answer_8) (u num_6 (+ i_7 1) (+ answer_8 i_7)) :guard (<= i_7 num_6) :vars ((num_6 Int) (i_7 Int) (answer_8 Int))) (rule (sum1 num_9 i_10 answer_11) (u num_9 0 0) :guard (not (< num_9 0)) :vars ((num_9 Int) (i_10 Int) (answer_11 Int))) (rule (sum1 num_12 i_13 answer_14) (return i_13 answer_14 0) :guard (< num_12 0) :vars ((num_12 Int) (i_13 Int) (answer_14 Int))) Confluent by Orthogonality with proof: no critical pairs Elapsed Time: 40.61 ms