YES
LCTRS
  Theories
    Core, Reals
  Signature
    lif: (Real, Real) -> Real
    log: (Real, Real) -> Real
  Rules
    lif(?12, ?13) -> +(1.0, log(/(?12, ?13), ?13)) [and(>=(?12, ?13), >(?13, 1.0))]
    lif(?14, ?15) -> 0.0 [not(and(>=(?14, ?15), >(?15, 1.0)))]
    log(?16, ?17) -> lif(?16, ?17)
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  49.62 ms