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

Elapsed Time:  37.12 ms