YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Result
  Signature
    return: Int -> Result
    sum: Int -> Result
    w: (Int, Result) -> Result
  Rules
    w(!x, return(!y)) -> return(+(!x, !y))
    sum(!x) -> w(!x, sum(-(!x, 1))) [<=(0, -(!x, 1))]
    sum(!x) -> return(0) [<=(!x, 0)]
DPGraph with indexed dependency pairs
  {1: sum#(!x) -> w#(!x, sum(-(!x, 1))) [<=(0, -(!x, 1))]
  , 2: sum#(!x) -> sum#(-(!x, 1)) [<=(0, -(!x, 1))]}
and edges
  1 -> {}
  2 -> {1, 2}
with 1 SCC(s)
  SCC:
    {sum#(!x) -> sum#(-(!x, 1)) [<=(0, -(!x, 1))]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(sum#) = 1
    removing the rule(s):
      {sum#(!x) -> sum#(-(!x, 1)) [<=(0, -(!x, 1))]}

Elapsed Time:  33.49 ms