YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Result
  Signature
    return: Int -> Result
    sum: Int -> Result
    w: (Int, Result) -> Result
  Rules
    sum(?14) -> return(0) [<=(?14, 0)]
    sum(?15) -> w(?15, sum(-(?15, 1))) [<=(0, -(?15, 1))]
    w(?16, return(?17)) -> return(+(?16, ?17))
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  45.00 ms