YES
LCTRS
  Theories
    Core, Ints
  Signature
    sum: Int -> Int
    sum2: Int -> Int
    u1: (Int, Int, Int) -> Int
    u2: (Int, Int, Int, Int) -> Int
  Rules
    sum(?37) -> +(?37, sum(-(?37, 1))) [<(0, ?37)]
    sum(?38) -> 0 [<=(?38, 0)]
    sum2(?39) -> u1(?39, 0, 0)
    u1(?40, ?41, ?42) -> ?42 [not(<=(?41, ?40))]
    u1(?43, ?44, ?45) -> u2(?43, ?44, 0, ?45) [<=(?44, ?43)]
    u2(?46, ?47, ?48, ?49) -> u1(?46, +(?47, 1), ?49) [not(<(?48, ?47))]
    u2(?50, ?51, ?52, ?53) -> u2(?50, ?51, +(?52, 1), +(?53, 1)) [<(?52, ?51)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  75.53 ms