MAYBE

(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)))

Confluence could not be determined.

Elapsed Time:   6.05 ms