YES
LCTRS
  Theories
    Core, Ints
  Signature
    sum: (Int, Int) -> Int
  Rules
    sum(?11, ?12) -> +(?11, sum(-(?11, 1), ?12)) [>=(?11, ?12)]
    sum(?13, ?14) -> 0 [<(?13, ?14)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  44.00 ms