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

Elapsed Time:  33.84 ms