MAYBE

(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)))

Confluence could not be determined.

Elapsed Time:   4.77 ms