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

Elapsed Time:  50.79 ms