YES (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))) Confluent by Parallel Closedness with proof: no critical pairs Elapsed Time: 12.06 ms