YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    return: Int -> Unit
    sum1: Int -> Unit
  Rules
    sum1(?4) -> return(0) [<(?4, 0)]
    sum1(?5) -> return(div(*(?5, +(?5, 1)), 2)) [not(<(?5, 0))]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  42.07 ms