MAYBE

(format LCTRS :logic QF_LRA)
(fun lif 2 :sort (Real Real Real))
(fun log 2 :sort (Real Real Real))

(rule (log x_0 y_1) (lif x_0 y_1) :vars ((x_0 Real) (y_1 Real)))
(rule (lif x_2 y_3) (+ 1 (log (/ x_2 y_3) y_3)) :guard (and (>= x_2 y_3) (> y_3 1)) :vars ((x_2 Real) (y_3 Real)))
(rule (lif x_4 y_5) 0 :guard (not (and (>= x_4 y_5) (> y_5 1))) :vars ((x_4 Real) (y_5 Real)))

Confluence could not be determined.

Elapsed Time:   2.62 ms