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 num_0 a_1 b_2 c_3 i_4) (return c_3) :guard (not (< i_4 num_0)) :vars ((num_0 Int) (a_1 Int) (b_2 Int) (c_3 Int) (i_4 Int)))
(rule (v num_5 a_6 b_7 c_8 i_9) (v num_5 b_7 (+ a_6 b_7) (+ a_6 b_7) (+ i_9 1)) :guard (< i_9 num_5) :vars ((num_5 Int) (a_6 Int) (b_7 Int) (c_8 Int) (i_9 Int)))
(rule (u num_10 a_11 b_12 c_13 i_14) (v num_10 a_11 b_12 c_13 0) :guard (and (not (= num_10 1)) (not (= num_10 2))) :vars ((num_10 Int) (a_11 Int) (b_12 Int) (c_13 Int) (i_14 Int)))
(rule (u num_15 a_16 b_17 c_18 i_19) (return 1) :guard (and (not (= num_15 1)) (= num_15 2)) :vars ((num_15 Int) (a_16 Int) (b_17 Int) (c_18 Int) (i_19 Int)))
(rule (u num_20 a_21 b_22 c_23 i_24) (return 1) :guard (= num_20 1) :vars ((num_20 Int) (a_21 Int) (b_22 Int) (c_23 Int) (i_24 Int)))
(rule (fastfib num_25) (u num_25 1 1 0 rnd_26) :vars ((num_25 Int) (rnd_26 Int)))

Confluence could not be determined.

Elapsed Time:  12.76 ms