YES (format LCTRS :logic QF_LRA) (fun lif 3 :sort (Bool Real Real Real)) (fun log 2 :sort (Real Real Real)) (rule (log x_0 y_1) (lif (and (>= x_0 y_1) (> y_1 1)) x_0 y_1) :vars ((x_0 Real) (y_1 Real))) (rule (lif true x_2 y_3) (+ 1 (log (/ x_2 y_3) y_3)) :vars ((x_2 Real) (y_3 Real))) (rule (lif false x_4 y_5) 0 :vars ((x_4 Real) (y_5 Real))) Confluent by Weak Orthogonality with proof: no critical pairs Elapsed Time: 8.23 ms