YES
LCTRS
  Theories
    Core, Ints
  Signature
    return: Int -> Int
    sum2: (Int, Int) -> Int
    u: (Int, Int, Int, Int) -> Int
  Rules
    sum2(?20, ?21) -> u(?20, ?21, ?20, 0)
    u(?22, ?23, ?24, ?25) -> return(?25) [not(<=(?24, ?23))]
    u(?26, ?27, ?28, ?29) -> u(?26, ?27, +(?28, 1), +(?29, ?28)) [<=(?28, ?27)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  41.29 ms