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

Elapsed Time:  49.74 ms