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 a_1 b_2 c_3 d_4) (return d_4) :guard (not (<= c_3 n_0)) :vars ((n_0 Int) (a_1 Int) (b_2 Int) (c_3 Int) (d_4 Int)))
(rule (v n_5 a_6 b_7 c_8 d_9) (v n_5 b_7 (+ a_6 b_7) (+ c_8 1) (+ a_6 b_7)) :guard (<= c_8 n_5) :vars ((n_5 Int) (a_6 Int) (b_7 Int) (c_8 Int) (d_9 Int)))
(rule (u n_10 a_11 b_12 c_13 d_14) (v n_10 a_11 b_12 2 d_14) :guard (and (not (< n_10 0)) (not (= n_10 1))) :vars ((n_10 Int) (a_11 Int) (b_12 Int) (c_13 Int) (d_14 Int)))
(rule (u n_15 a_16 b_17 c_18 d_19) (return 1) :guard (and (not (< n_15 0)) (= n_15 1)) :vars ((n_15 Int) (a_16 Int) (b_17 Int) (c_18 Int) (d_19 Int)))
(rule (u n_20 a_21 b_22 c_23 d_24) (return 0) :guard (< n_20 0) :vars ((n_20 Int) (a_21 Int) (b_22 Int) (c_23 Int) (d_24 Int)))
(rule (fastfib n_25) (u n_25 0 1 rnd3_26 rnd4_27) :vars ((n_25 Int) (rnd3_26 Int) (rnd4_27 Int)))

Confluence could not be determined.

Elapsed Time:  18.77 ms