MAYBE

(format LCTRS :logic QF_LIA)
(fun fastfib 1 :sort (Int Unit))
(fun p 5 :sort (Int Int Int Int 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 (p n_0 x_1 y_2 z_3 i_4) (return x_1) :guard (not (< i_4 n_0)) :vars ((n_0 Int) (x_1 Int) (y_2 Int) (z_3 Int) (i_4 Int)))
(rule (p n_5 x_6 y_7 z_8 i_9) (p n_5 (+ x_6 y_7) x_6 x_6 (+ i_9 1)) :guard (< i_9 n_5) :vars ((n_5 Int) (x_6 Int) (y_7 Int) (z_8 Int) (i_9 Int)))
(rule (w n_10 x_11 y_12 z_13 i_14) (p n_10 x_11 y_12 z_13 1) :guard (not (> n_10 46)) :vars ((n_10 Int) (x_11 Int) (y_12 Int) (z_13 Int) (i_14 Int)))
(rule (w n_15 x_16 y_17 z_18 i_19) (return -1) :guard (> n_15 46) :vars ((n_15 Int) (x_16 Int) (y_17 Int) (z_18 Int) (i_19 Int)))
(rule (v n_20 x_21 y_22 z_23 i_24) (return n_20) :guard (not (< n_20 0)) :vars ((n_20 Int) (x_21 Int) (y_22 Int) (z_23 Int) (i_24 Int)))
(rule (v n_25 x_26 y_27 z_28 i_29) (return 0) :guard (< n_25 0) :vars ((n_25 Int) (x_26 Int) (y_27 Int) (z_28 Int) (i_29 Int)))
(rule (u n_30 x_31 y_32 z_33 i_34) (w n_30 x_31 y_32 z_33 i_34) :guard (not (<= n_30 1)) :vars ((n_30 Int) (x_31 Int) (y_32 Int) (z_33 Int) (i_34 Int)))
(rule (u n_35 x_36 y_37 z_38 i_39) (v n_35 x_36 y_37 z_38 i_39) :guard (<= n_35 1) :vars ((n_35 Int) (x_36 Int) (y_37 Int) (z_38 Int) (i_39 Int)))
(rule (fastfib n_40) (u n_40 1 0 rnd3_41 rnd4_42) :vars ((n_40 Int) (rnd3_41 Int) (rnd4_42 Int)))

Confluence could not be determined.

Elapsed Time:   6.14 ms