YES (format LCTRS :logic QF_LIA) (fun fib 1 :sort (Int Int)) (rule (fib x_0) (+ (fib (- x_0 1)) (fib (- x_0 2))) :guard (>= (- x_0 2) 0) :vars ((x_0 Int))) (rule (fib 1) 1) (rule (fib x_1) 0 :guard (<= x_1 0) :vars ((x_1 Int))) Confluent by Orthogonality with proof: no critical pairs Elapsed Time: 15.97 ms