MAYBE

(format LCTRS :logic QF_LIA)
(fun fastfib 1 :sort (Int Unit))
(fun return 1 :sort (Int Unit))
(fun u 4 :sort (Int Int Int Int Unit))

(rule (u num_0 f0_1 f1_2 f2_3) (return f1_2) :guard (not (>= num_0 2)) :vars ((num_0 Int) (f0_1 Int) (f1_2 Int) (f2_3 Int)))
(rule (u num_4 f0_5 f1_6 f2_7) (u (- num_4 1) f1_6 (+ f1_6 f0_5) (+ f1_6 f0_5)) :guard (>= num_4 2) :vars ((num_4 Int) (f0_5 Int) (f1_6 Int) (f2_7 Int)))
(rule (fastfib num_8) (u num_8 1 1 rnd_9) :vars ((num_8 Int) (rnd_9 Int)))

Confluence could not be determined.

Elapsed Time:  14.17 ms