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

Elapsed Time:  64.17 ms