NO
LCTRS
  Theories
    Core, Ints
  Signature
    /: (Int, Int) -> Int
    lif: (Bool, Int, Int) -> Int
    log: (Int, Int) -> Int
  Rules
    /(?20, ?21) -> ?22 [?20 = *(?21, ?22)]
    lif(?23, ?24, ?25) -> +(1, log(/(?24, ?25), ?25)) [?23 = true]
    lif(?26, ?27, ?28) -> 0 [?26 = false]
    log(?29, ?30) -> lif(and(>=(?29, ?30), >(?30, 1)), ?29, ?30)
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      /(?20', ?21') -> ?22' [=(?20', *(?21', ?22'))]
    Outer Rule
      /(?20", ?21") -> ?22" [=(?20", *(?21", ?22"))]
    Pair
      ?22' ≈ ?22" [=(?20", *(?21", ?22')), =(?20", *(?21", ?22"))]
  reaches the non-trivial normal form
    ?22' ≈ ?22" [?20" = *(?21", ?22'), ?20" = *(?21", ?22")]

Elapsed Time:  95.18 ms