MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    /: (Int, Int) -> Int
    lif: (Bool, Int, Int) -> Int
    log: (Int, Int) -> Int
  Rules
    log(!x, !y) -> lif(and(>=(!x, !y), >(!y, 1)), !x, !y)
    lif(true, !x, !y) -> +(1, log(/(!x, !y), !y))
    lif(false, !x, !y) -> 0
    /(!x, !y) -> !z [!x = *(!y, !z)]
No termination info given.

Elapsed Time:  35.15 ms