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 fi_1 fp_2 fn_3 i_4) (return fi_1) :guard (not (< i_4 n_0)) :vars ((n_0 Int) (fi_1 Int) (fp_2 Int) (fn_3 Int) (i_4 Int)))
(rule (v n_5 fi_6 fp_7 fn_8 i_9) (v n_5 (+ fi_6 fp_7) fi_6 (+ fi_6 fp_7) (+ i_9 1)) :guard (< i_9 n_5) :vars ((n_5 Int) (fi_6 Int) (fp_7 Int) (fn_8 Int) (i_9 Int)))
(rule (u n_10 fi_11 fp_12 fn_13 i_14) (v n_10 fi_11 fp_12 fn_13 1) :guard (not (<= n_10 0)) :vars ((n_10 Int) (fi_11 Int) (fp_12 Int) (fn_13 Int) (i_14 Int)))
(rule (u n_15 fi_16 fp_17 fn_18 i_19) (return 0) :guard (<= n_15 0) :vars ((n_15 Int) (fi_16 Int) (fp_17 Int) (fn_18 Int) (i_19 Int)))
(rule (fastfib n_20) (u n_20 1 0 rnd1_21 rnd2_22) :vars ((n_20 Int) (rnd1_21 Int) (rnd2_22 Int)))

Confluence could not be determined.

Elapsed Time:  23.57 ms