YES
LCTRS
  Theories
    Core, Ints
  Signature
    f: (Int, Int) -> Int
  Rules
    f(!x, !y) -> 0 [or(or(>=(-(!x, 1), !y), <(-(!x, 1), 0)), <(!y, 0))]
    f(!x, !y) -> 0 [or(<(!x, 0), <=(!y, 0))]
    f(0, !y) -> 0 [>=(!y, 0)]
    f(!x, !y) -> f(-(!x, 1), !y) [and(and(<(-(!x, 1), !y), >=(-(!x, 1), 0)), >=(!y, 0))]
DPGraph with indexed dependency pairs
  {1: f#(!x, !y) -> f#(-(!x, 1), !y) [and(and(<(-(!x, 1), !y), >=(-(!x, 1), 0)), >=(!y, 0))]}
and edges
  1 -> {1}
with 1 SCC(s)
  SCC:
    {f#(!x, !y) -> f#(-(!x, 1), !y) [and(and(<(-(!x, 1), !y), >=(-(!x, 1), 0)), >=(!y, 0))]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(f#) = 1
    removing the rule(s):
      {f#(!x, !y) -> f#(-(!x, 1), !y) [and(and(<(-(!x, 1), !y), >=(-(!x, 1), 0)), >=(!y, 0))]}

Elapsed Time:  43.34 ms