YES
LCTRS
  Theories
    Core, Ints
  Signature
    f: (Int, Int) -> Int
  Rules
    f(?30, ?31) -> f(-(?30, 1), ?31) [and(and(<(-(?30, 1), ?31), >=(-(?30, 1), 0)), >=(?31, 0))]
    f(?32, ?33) -> 0 [or(and(?32 = 0, >=(?33, 0)), or(or(<(?32, 0), <=(?33, 0)), or(or(>=(-(?32, 1), ?33), <(-(?32, 1), 0)), <(?33, 0))))]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  49.14 ms