YES
LCTRS
  Theories
    Core, Ints
  Signature
    A: (Int, Int) -> Int
  Rules
    A(?19, ?20) -> +(?20, 1) [?19 = 0]
    A(?21, ?22) -> A(-(?21, 1), A(?21, -(?22, 1))) [and(not(?21 = 0), not(?22 = 0))]
    A(?23, ?24) -> A(-(?23, 1), 1) [?24 = 0, not(?23 = 0)]
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  45.93 ms