MAYBE

(format LCTRS :logic QF_NIA)
(fun / 2 :sort (Int Int Int))
(fun lif 3 :sort (Bool Int Int Int))
(fun log 2 :sort (Int Int Int))

(rule (log x_0 y_1) (lif (and (>= x_0 y_1) (> y_1 1)) x_0 y_1) :vars ((x_0 Int) (y_1 Int)))
(rule (lif true x_2 y_3) (+ 1 (log (/ x_2 y_3) y_3)) :vars ((x_2 Int) (y_3 Int)))
(rule (lif false x_4 y_5) 0 :vars ((x_4 Int) (y_5 Int)))
(rule (/ x_6 y_7) z_8 :guard (= x_6 (* y_7 z_8)) :vars ((x_6 Int) (y_7 Int) (z_8 Int)))

Confluence could not be determined.

Elapsed Time:  13.59 ms