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

Elapsed Time:  45.35 ms