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

Elapsed Time:  68.56 ms