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

Elapsed Time:  33.26 ms