YES
LCTRS
  Theories
    Core, Ints
  Signature
    f1: Int -> Int
    u_1: Int -> Int
    u_6: Int -> Int
  Rules
    u_6(!x) -> !x [>=(!x, 0)]
    u_6(!x) -> 0 [<(!x, 0)]
    f1(!x) -> u_6(!x) [<=(!x, 0)]
    u_1(!w_1) -> u_6(+(!w_1, 1))
    f1(!x) -> u_1(f1(-(!x, 1))) [>(!x, 0)]
* DPGraph approximation on the DP problem
  dependency pairs:
    {f1#(!x) -> u_6#(!x) [<=(!x, 0)]
    , u_1#(!w_1) -> u_6#(+(!w_1, 1))
    , f1#(!x) -> u_1#(f1(-(!x, 1))) [>(!x, 0)]
    , f1#(!x) -> f1#(-(!x, 1)) [>(!x, 0)]}
  rules:
    {u_6(!x) -> !x [>=(!x, 0)]
    , u_6(!x) -> 0 [<(!x, 0)]
    , f1(!x) -> u_6(!x) [<=(!x, 0)]
    , u_1(!w_1) -> u_6(+(!w_1, 1))
    , f1(!x) -> u_1(f1(-(!x, 1))) [>(!x, 0)]}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: f1#(!x) -> u_6#(!x) [<=(!x, 0)]
    , 2: u_1#(!w_1) -> u_6#(+(!w_1, 1))
    , 3: f1#(!x) -> u_1#(f1(-(!x, 1))) [>(!x, 0)]
    , 4: f1#(!x) -> f1#(-(!x, 1)) [>(!x, 0)]}
  and edges
    1 -> {}
    2 -> {}
    3 -> {2}
    4 -> {1, 3, 4}
with 1 SCC(s)
  SCC:
    {f1#(!x) -> f1#(-(!x, 1)) [>(!x, 0)]}
* Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(f1#) = 1
    removing the rule(s):
      {f1#(!x) -> f1#(-(!x, 1)) [>(!x, 0)]}

Elapsed Time:  25.08 ms