YES (format LCTRS :logic QF_LIA) (fun badfib 1 :sort (Int Unit)) (fun return 1 :sort (Int Unit)) (fun w 2 :sort (Unit Unit Unit)) (rule (badfib x_0) (w (badfib (- x_0 1)) (badfib (- x_0 2))) :guard (> x_0 3) :vars ((x_0 Int))) (rule (badfib x_1) (return 1) :guard (<= x_1 3) :vars ((x_1 Int))) (rule (w (return x_2) (return y_3)) (return (+ x_2 y_3)) :vars ((x_2 Int) (y_3 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 14.40 ms