YES (format LCTRS :logic QF_LIA) (fun fib 1 :sort (Int Unit)) (fun return 1 :sort (Int Unit)) (fun tmp 2 :sort (Unit Unit Unit)) (rule (tmp (return x_0) (return y_1)) (return (+ x_0 y_1)) :vars ((x_0 Int) (y_1 Int))) (rule (fib x_2) (tmp (fib (- x_2 1)) (fib (- x_2 2))) :guard (>= (- x_2 2) 0) :vars ((x_2 Int))) (rule (fib 1) (return 1)) (rule (fib x_3) (return 0) :guard (<= x_3 0) :vars ((x_3 Int))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 17.07 ms