MAYBE
LCTRS
  Theories
    Core, Reals
  Signature
    lif: (Real, Real) -> Real
    log: (Real, Real) -> Real
  Rules
    log(!x, !y) -> lif(!x, !y)
    lif(!x, !y) -> +(1.0, log(/(!x, !y), !y)) [and(>=(!x, !y), >(!y, 1.0))]
    lif(!x, !y) -> 0.0 [not(and(>=(!x, !y), >(!y, 1.0)))]
No termination info given.

Elapsed Time:  55.53 ms