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 pre1_1 pre2_2 val_3 i_4) (return val_3) :guard (and (not (<= i_4 n_0)) (not (< val_3 0))) :vars ((n_0 Int) (pre1_1 Int) (pre2_2 Int) (val_3 Int) (i_4 Int)))
(rule (v n_5 pre1_6 pre2_7 val_8 i_9) (return -1) :guard (and (not (<= i_9 n_5)) (< val_8 0)) :vars ((n_5 Int) (pre1_6 Int) (pre2_7 Int) (val_8 Int) (i_9 Int)))
(rule (v n_10 pre1_11 pre2_12 val_13 i_14) (v n_10 (+ pre1_11 pre2_12) pre1_11 (+ pre1_11 pre2_12) (+ i_14 1)) :guard (<= i_14 n_10) :vars ((n_10 Int) (pre1_11 Int) (pre2_12 Int) (val_13 Int) (i_14 Int)))
(rule (u n_15 pre1_16 pre2_17 val_18 i_19) (v n_15 pre1_16 pre2_17 val_18 2) :guard (and (not (<= n_15 0)) (not (= n_15 1))) :vars ((n_15 Int) (pre1_16 Int) (pre2_17 Int) (val_18 Int) (i_19 Int)))
(rule (u n_20 pre1_21 pre2_22 val_23 i_24) (return 1) :guard (and (not (<= n_20 0)) (= n_20 1)) :vars ((n_20 Int) (pre1_21 Int) (pre2_22 Int) (val_23 Int) (i_24 Int)))
(rule (u n_25 pre1_26 pre2_27 val_28 i_29) (return 0) :guard (<= n_25 0) :vars ((n_25 Int) (pre1_26 Int) (pre2_27 Int) (val_28 Int) (i_29 Int)))
(rule (fastfib n_30) (u n_30 1 0 0 rnd_31) :vars ((n_30 Int) (rnd_31 Int)))

Confluence could not be determined.

Elapsed Time:  27.10 ms