YES (format LCTRS :logic QF_LIA) (fun fastfib 1 :sort (Int Int)) (fun g 1 :sort (Int Int)) (fun u 5 :sort (Int Int Int Int Int Int)) (fun v 5 :sort (Int Int Int Int Int Int)) (rule (g x_0) (g x_0) :vars ((x_0 Int))) (rule (v x_1 i_2 p_3 q_4 z_5) p_3 :guard (>= i_2 x_1) :vars ((x_1 Int) (i_2 Int) (p_3 Int) (q_4 Int) (z_5 Int))) (rule (v x_6 i_7 p_8 q_9 z_10) (v x_6 (+ i_7 1) (+ p_8 q_9) p_8 z_10) :guard (< i_7 x_6) :vars ((x_6 Int) (i_7 Int) (p_8 Int) (q_9 Int) (z_10 Int))) (rule (u x_11 i_12 p_13 q_14 z_15) (v x_11 i_12 p_13 q_14 (g 0)) :guard (> x_11 1) :vars ((x_11 Int) (i_12 Int) (p_13 Int) (q_14 Int) (z_15 Int))) (rule (u x_16 i_17 p_18 q_19 z_20) 1 :guard (= x_16 1) :vars ((x_16 Int) (i_17 Int) (p_18 Int) (q_19 Int) (z_20 Int))) (rule (u x_21 i_22 p_23 q_24 z_25) 0 :guard (<= x_21 0) :vars ((x_21 Int) (i_22 Int) (p_23 Int) (q_24 Int) (z_25 Int))) (rule (fastfib x_26) (u x_26 0 1 0 0) :vars ((x_26 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 14.38 ms