MAYBE

(format LCTRS :logic QF_LIA)
(fun fastfib 1 :sort (Int Unit))
(fun return 1 :sort (Int Unit))
(fun u 5 :sort (Int Int Int Int Int Unit))
(fun v 5 :sort (Int Int Int Int Int Unit))

(rule (v n_0 a1_1 a2_2 sum_3 i_4) (return sum_3) :guard (not (< i_4 n_0)) :vars ((n_0 Int) (a1_1 Int) (a2_2 Int) (sum_3 Int) (i_4 Int)))
(rule (v n_5 a1_6 a2_7 sum_8 i_9) (v n_5 (+ a1_6 a2_7) a1_6 (+ a1_6 a2_7) (+ i_9 1)) :guard (< i_9 n_5) :vars ((n_5 Int) (a1_6 Int) (a2_7 Int) (sum_8 Int) (i_9 Int)))
(rule (u n_10 a1_11 a2_12 sum_13 i_14) (return sum_13) :guard (not (and (> n_10 0) (< n_10 47))) :vars ((n_10 Int) (a1_11 Int) (a2_12 Int) (sum_13 Int) (i_14 Int)))
(rule (u n_15 a1_16 a2_17 sum_18 i_19) (v n_15 a1_16 a2_17 1 1) :guard (and (> n_15 0) (< n_15 47)) :vars ((n_15 Int) (a1_16 Int) (a2_17 Int) (sum_18 Int) (i_19 Int)))
(rule (fastfib n_20) (u n_20 1 0 0 rnd_21) :vars ((n_20 Int) (rnd_21 Int)))

Confluence could not be determined.

Elapsed Time:   6.00 ms