YES
LCTRS
  Theories
    Core, Ints
  Signature
    eval1: (Int, Int) -> Int
    eval2: (Int, Int) -> Int
    eval3: (Int, Int) -> Int
  Rules
    eval1(!x, !y) -> eval2(!x, !y) [and(and(>(!x, 0), >(!y, 0)), >(!x, !y))]
    eval1(!x, !y) -> eval3(!x, !y) [and(and(>(!x, 0), >(!y, 0)), not(>(!x, !y)))]
    eval2(!x, !y) -> eval2(+(!x, -1), +(!y, 1)) [>(!x, 0)]
    eval2(!x, !y) -> eval1(!x, !y) [not(>(!x, 0))]
    eval3(!x, !y) -> eval3(+(!x, 1), +(!y, -1)) [>(!y, 0)]
    eval3(!x, !y) -> eval1(!x, !y) [not(>(!y, 0))]
DPGraph with indexed dependency pairs
  {1: eval1#(!x, !y) -> eval2#(!x, !y) [and(and(>(!x, 0), >(!y, 0)), >(!x, !y))]
  , 2: eval1#(!x, !y) -> eval3#(!x, !y) [and(and(>(!x, 0), >(!y, 0)), not(>(!x, !y)))]
  , 3: eval2#(!x, !y) -> eval2#(+(!x, -1), +(!y, 1)) [>(!x, 0)]
  , 4: eval2#(!x, !y) -> eval1#(!x, !y) [not(>(!x, 0))]
  , 5: eval3#(!x, !y) -> eval3#(+(!x, 1), +(!y, -1)) [>(!y, 0)]
  , 6: eval3#(!x, !y) -> eval1#(!x, !y) [not(>(!y, 0))]}
and edges
  1 -> {3}
  2 -> {5}
  3 -> {3, 4}
  4 -> {}
  5 -> {5, 6}
  6 -> {}
with 2 SCC(s)
  SCC:
    {eval3#(!x, !y) -> eval3#(+(!x, 1), +(!y, -1)) [>(!y, 0)]}
  SCC:
    {eval2#(!x, !y) -> eval2#(+(!x, -1), +(!y, 1)) [>(!x, 0)]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(eval3#) = 2
    removing the rule(s):
      {eval3#(!x, !y) -> eval3#(+(!x, 1), +(!y, -1)) [>(!y, 0)]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(eval2#) = 1
    removing the rule(s):
      {eval2#(!x, !y) -> eval2#(+(!x, -1), +(!y, 1)) [>(!x, 0)]}

Elapsed Time:  41.92 ms