YES
LCTRS
  Theories
    Core, Ints
  Signature
    sum: Int -> Int
    sum3: (Int, Int) -> Int
    sum_decl: Int -> Int
    u_3: (Int, Int) -> Int
  Rules
    sum(?31) -> +(?31, sum(-(?31, 1))) [<=(0, -(?31, 1))]
    sum(?32) -> 0 [<=(?32, 0)]
    sum3(?33, ?34) -> +(?34, sum3(?33, +(?34, 1))) [>=(?33, ?34)]
    sum3(?35, ?36) -> 0 [<(?35, ?36)]
    sum_decl(?37) -> u_3(0, ?37)
    u_3(?38, ?39) -> ?38 [<=(?39, 0)]
    u_3(?40, ?41) -> u_3(+(?40, ?41), -(?41, 1)) [>(?41, 0)]
Confluent by Almost Parallel Closedness with proof:
  no critical pairs

Elapsed Time:  76.78 ms