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

Elapsed Time:  32.47 ms