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

Elapsed Time:  43.70 ms