YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    return: Int -> Unit
    sum1: Int -> Unit
    u: (Int, Int, Int) -> Unit
  Rules
    sum1(?14) -> u(?14, 0, 0)
    u(?15, ?16, ?17) -> return(?16) [not(<=(?17, ?15))]
    u(?18, ?19, ?20) -> u(?18, +(?19, ?20), +(?20, 1)) [<=(?20, ?18)]
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  42.40 ms