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))
(fun w 5 :sort (Int Int Int Int Int Unit))

(rule (w n_0 p1_1 p2_2 p_3 i_4) (v n_0 p_3 p1_1 p_3 (+ i_4 1)) :guard (not (< p_3 p1_1)) :vars ((n_0 Int) (p1_1 Int) (p2_2 Int) (p_3 Int) (i_4 Int)))
(rule (w n_5 p1_6 p2_7 p_8 i_9) (return -2) :guard (< p_8 p1_6) :vars ((n_5 Int) (p1_6 Int) (p2_7 Int) (p_8 Int) (i_9 Int)))
(rule (v n_10 p1_11 p2_12 p_13 i_14) (return p_13) :guard (not (< i_14 n_10)) :vars ((n_10 Int) (p1_11 Int) (p2_12 Int) (p_13 Int) (i_14 Int)))
(rule (v n_15 p1_16 p2_17 p_18 i_19) (w n_15 p1_16 p2_17 (+ p1_16 p2_17) i_19) :guard (< i_19 n_15) :vars ((n_15 Int) (p1_16 Int) (p2_17 Int) (p_18 Int) (i_19 Int)))
(rule (u n_20 p1_21 p2_22 p_23 i_24) (v n_20 p1_21 p2_22 p_23 1) :guard (and (and (not (< n_20 0)) (not (= n_20 0))) (not (= n_20 1))) :vars ((n_20 Int) (p1_21 Int) (p2_22 Int) (p_23 Int) (i_24 Int)))
(rule (u n_25 p1_26 p2_27 p_28 i_29) (return 1) :guard (and (and (not (< n_25 0)) (not (= n_25 0))) (= n_25 1)) :vars ((n_25 Int) (p1_26 Int) (p2_27 Int) (p_28 Int) (i_29 Int)))
(rule (u n_30 p1_31 p2_32 p_33 i_34) (return 0) :guard (and (not (< n_30 0)) (= n_30 0)) :vars ((n_30 Int) (p1_31 Int) (p2_32 Int) (p_33 Int) (i_34 Int)))
(rule (u n_35 p1_36 p2_37 p_38 i_39) (return -1) :guard (< n_35 0) :vars ((n_35 Int) (p1_36 Int) (p2_37 Int) (p_38 Int) (i_39 Int)))
(rule (fastfib x_40) (u x_40 1 0 rnd1_41 rnd2_42) :vars ((x_40 Int) (rnd1_41 Int) (rnd2_42 Int)))

Confluence could not be determined.

Elapsed Time:  30.15 ms