YES (format LCTRS :logic QF_LIA) (fun badfib 1 :sort (Int Unit)) (fun return 1 :sort (Int Unit)) (fun w2 2 :sort (Unit Unit Unit)) (rule (w2 (return x_0) (return y_1)) (return (+ x_0 y_1)) :vars ((x_0 Int) (y_1 Int))) (rule (badfib x_2) (w2 (badfib (- x_2 1)) (badfib (- x_2 2))) :guard (> x_2 1) :vars ((x_2 Int))) (rule (badfib x_3) (return 1) :guard (= x_3 1) :vars ((x_3 Int))) (rule (badfib x_4) (return 1) :guard (<= x_4 0) :vars ((x_4 Int))) Confluent by Orthogonality with proof: no critical pairs Elapsed Time: 16.31 ms