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 now_1 next_2 i_3 tmp_4) (return next_2) :guard (not (<= i_3 n_0)) :vars ((n_0 Int) (now_1 Int) (next_2 Int) (i_3 Int) (tmp_4 Int)))
(rule (v n_5 now_6 next_7 i_8 tmp_9) (v n_5 next_7 (+ next_7 now_6) (+ i_8 1) now_6) :guard (<= i_8 n_5) :vars ((n_5 Int) (now_6 Int) (next_7 Int) (i_8 Int) (tmp_9 Int)))
(rule (u n_10 now_11 next_12 i_13 tmp_14) (v n_10 1 1 3 tmp_14) :guard (and (not (<= n_10 0)) (not (= n_10 1))) :vars ((n_10 Int) (now_11 Int) (next_12 Int) (i_13 Int) (tmp_14 Int)))
(rule (u n_15 now_16 next_17 i_18 tmp_19) (return 1) :guard (and (not (<= n_15 0)) (= n_15 1)) :vars ((n_15 Int) (now_16 Int) (next_17 Int) (i_18 Int) (tmp_19 Int)))
(rule (u n_20 now_21 next_22 i_23 tmp_24) (return 0) :guard (<= n_20 0) :vars ((n_20 Int) (now_21 Int) (next_22 Int) (i_23 Int) (tmp_24 Int)))
(rule (fastfib n_25) (u n_25 rnd1_26 rnd2_27 rnd3_28 rnd4_29) :vars ((n_25 Int) (rnd1_26 Int) (rnd2_27 Int) (rnd3_28 Int) (rnd4_29 Int)))

Confluence could not be determined.

Elapsed Time:  20.20 ms