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))
(fun w 3 :sort (Int Int Int Result))

(rule (w n_0 i_1 s_2) (return s_2) :guard (not (< s_2 0)) :vars ((n_0 Int) (i_1 Int) (s_2 Int)))
(rule (w n_3 i_4 s_5) (return -1) :guard (< s_5 0) :vars ((n_3 Int) (i_4 Int) (s_5 Int)))
(rule (v n_6 i_7 s_8) (w n_6 i_7 s_8) :guard (not (and (<= i_7 n_6) (>= s_8 0))) :vars ((n_6 Int) (i_7 Int) (s_8 Int)))
(rule (v n_9 i_10 s_11) (v n_9 (+ i_10 1) (+ s_11 i_10)) :guard (and (<= i_10 n_9) (>= s_11 0)) :vars ((n_9 Int) (i_10 Int) (s_11 Int)))
(rule (u n_12 i_13 s_14) (v n_12 0 s_14) :guard (not (< n_12 0)) :vars ((n_12 Int) (i_13 Int) (s_14 Int)))
(rule (u n_15 i_16 s_17) (return 0) :guard (< n_15 0) :vars ((n_15 Int) (i_16 Int) (s_17 Int)))
(rule (sum1 n_18) (u n_18 rnd_19 0) :vars ((n_18 Int) (rnd_19 Int)))

Confluence could not be determined.

Elapsed Time:  25.37 ms