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 approximation on the DP problem
  dependency pairs:
    {v#(!n, !s) -> v#(-(!n, 1), +(!s, !n)) [>(!n, 0)]
    , u#(!n, !s) -> v#(!n, 0) [not(<(!n, 0))]
    , sum1#(!n) -> u#(!n, !rnd)}
  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)}
resulting in the DP graph
  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:  24.17 ms