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

Elapsed Time:  39.16 ms