YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    return: Int -> Unit
    sum1: Int -> Unit
    u: (Int, Int) -> Unit
    v: (Int, Int) -> Unit
  Rules
    sum1(?21) -> u(?21, 0)
    u(?22, ?23) -> return(0) [<(?22, 0)]
    u(?24, ?25) -> v(?24, ?25) [not(<(?24, 0))]
    v(?26, ?27) -> return(?27) [not(>=(?26, 0))]
    v(?28, ?29) -> v(-(?28, 1), +(?29, ?28)) [>=(?28, 0)]
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  49.89 ms