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))
(fun v 4 :sort (Int Int Int Int Unit))

(rule (v x_0 i_1 p_2 q_3) (return q_3) :guard (not (< i_1 x_0)) :vars ((x_0 Int) (i_1 Int) (p_2 Int) (q_3 Int)))
(rule (v x_4 i_5 p_6 q_7) (v x_4 (+ i_5 1) (+ p_6 q_7) p_6) :guard (< i_5 x_4) :vars ((x_4 Int) (i_5 Int) (p_6 Int) (q_7 Int)))
(rule (u x_8 i_9 p_10 q_11) (v x_8 1 p_10 q_11) :guard (and (not (= x_8 0)) (not (= x_8 1))) :vars ((x_8 Int) (i_9 Int) (p_10 Int) (q_11 Int)))
(rule (u x_12 i_13 p_14 q_15) (return 1) :guard (and (not (= x_12 0)) (= x_12 1)) :vars ((x_12 Int) (i_13 Int) (p_14 Int) (q_15 Int)))
(rule (u x_16 i_17 p_18 q_19) (return 0) :guard (= x_16 0) :vars ((x_16 Int) (i_17 Int) (p_18 Int) (q_19 Int)))
(rule (fastfib x_20) (u x_20 rnd_21 1 0) :vars ((x_20 Int) (rnd_21 Int)))

Confluence could not be determined.

Elapsed Time:  21.27 ms