MAYBE

(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Result))
(fun sum1 1 :sort (Int Result))
(fun u 3 :sort (Int Int Int Result))
(fun v 3 :sort (Int Int Int Result))

(rule (v n_0 i_1 s_2) (return s_2) :guard (not (> (- n_0 i_1) 0)) :vars ((n_0 Int) (i_1 Int) (s_2 Int)))
(rule (v n_3 i_4 s_5) (v n_3 (+ i_4 1) (+ s_5 (- n_3 i_4))) :guard (> (- n_3 i_4) 0) :vars ((n_3 Int) (i_4 Int) (s_5 Int)))
(rule (u n_6 i_7 s_8) (v n_6 0 s_8) :guard (> n_6 0) :vars ((n_6 Int) (i_7 Int) (s_8 Int)))
(rule (u n_9 i_10 s_11) (return 0) :guard (<= n_9 0) :vars ((n_9 Int) (i_10 Int) (s_11 Int)))
(rule (sum1 n_12) (u n_12 rnd_13 0) :vars ((n_12 Int) (rnd_13 Int)))

Confluence could not be determined.

Elapsed Time:  14.82 ms