YES
LCTRS
  Theories
    Core, Ints
  Signature
    sum: Int -> Int
  Rules
    sum(!x) -> 0 [>=(0, !x)]
    sum(!x) -> +(!x, sum(+(!x, -1))) [not(>=(0, !x))]
DPGraph with indexed dependency pairs
  {1: sum#(!x) -> sum#(+(!x, -1)) [not(>=(0, !x))]}
and edges
  1 -> {1}
with 1 SCC(s)
  SCC:
    {sum#(!x) -> sum#(+(!x, -1)) [not(>=(0, !x))]}
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)) [not(>=(0, !x))]}

Elapsed Time:  32.20 ms