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

Elapsed Time:  33.21 ms