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
  Rules
    sum2(?31, ?32) -> u(?31, ?32, 0)
    u(?33, ?34, ?35) -> return(?35) [not(<(?33, ?34))]
    u(?36, ?37, ?38) -> v(?36, ?37, ?38) [<(?36, ?37)]
    v(?39, ?40, ?41) -> return(?41) [not(>=(?40, ?39))]
    v(?42, ?43, ?44) -> v(?42, -(?43, 1), +(?44, ?43)) [>=(?43, ?42)]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  80.98 ms