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 fb_2 p_3 q_4) (return fb_2) :guard (not (<= i_1 n_0)) :vars ((n_0 Int) (i_1 Int) (fb_2 Int) (p_3 Int) (q_4 Int)))
(rule (v n_5 i_6 fb_7 p_8 q_9) (v n_5 (+ i_6 1) (+ p_8 q_9) (+ p_8 q_9) p_8) :guard (<= i_6 n_5) :vars ((n_5 Int) (i_6 Int) (fb_7 Int) (p_8 Int) (q_9 Int)))
(rule (u n_10 i_11 fb_12 p_13 q_14) (v n_10 2 fb_12 p_13 q_14) :guard (and (not (< n_10 1)) (not (= n_10 1))) :vars ((n_10 Int) (i_11 Int) (fb_12 Int) (p_13 Int) (q_14 Int)))
(rule (u n_15 i_16 fb_17 p_18 q_19) (return 1) :guard (and (not (< n_15 1)) (= n_15 1)) :vars ((n_15 Int) (i_16 Int) (fb_17 Int) (p_18 Int) (q_19 Int)))
(rule (u n_20 i_21 fb_22 p_23 q_24) (return 0) :guard (< n_20 1) :vars ((n_20 Int) (i_21 Int) (fb_22 Int) (p_23 Int) (q_24 Int)))
(rule (fastfib n_25) (u n_25 rnd1_26 rnd2_27 1 0) :vars ((n_25 Int) (rnd1_26 Int) (rnd2_27 Int)))

Confluence could not be determined.

Elapsed Time:  16.33 ms