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 i_1 r_2 o_3 t_4) (return r_2) :guard (not (<= i_1 n_0)) :vars ((n_0 Int) (i_1 Int) (r_2 Int) (o_3 Int) (t_4 Int)))
(rule (v n_5 i_6 r_7 o_8 t_9) (v n_5 (+ i_6 1) (+ r_7 o_8) r_7 r_7) :guard (<= i_6 n_5) :vars ((n_5 Int) (i_6 Int) (r_7 Int) (o_8 Int) (t_9 Int)))
(rule (u n_10 i_11 r_12 o_13 t_14) (v n_10 2 1 0 t_14) :guard (distinct n_10 0) :vars ((n_10 Int) (i_11 Int) (r_12 Int) (o_13 Int) (t_14 Int)))
(rule (u 0 i_15 r_16 o_17 t_18) (return 0) :vars ((i_15 Int) (r_16 Int) (o_17 Int) (t_18 Int)))
(rule (fastfib n_19) (u n_19 rnd0_20 rnd1_21 rn2_22 rnd3_23) :vars ((n_19 Int) (rnd0_20 Int) (rnd1_21 Int) (rn2_22 Int) (rnd3_23 Int)))

Confluence could not be determined.

Elapsed Time:  22.52 ms