YES
LCTRS
  Theories
    Core, Ints
  Signature
    g2: (Int, Int) -> Int
    triangle2: Int -> Int
    u_16: Int -> Int
    u_23: Int -> Int
  Rules
    u_23(!w_8) -> !w_8
    g2(!n, !s) -> u_23(g2(-(!n, 1), +(!n, !s))) [>(!n, 0)]
    g2(!n, !s) -> !s [<=(!n, 0)]
    u_16(!w_6) -> !w_6
    triangle2(!n) -> u_16(g2(!n, 0))
DPGraph with indexed dependency pairs
  {1: g2#(!n, !s) -> u_23#(g2(-(!n, 1), +(!n, !s))) [>(!n, 0)]
  , 2: g2#(!n, !s) -> g2#(-(!n, 1), +(!n, !s)) [>(!n, 0)]
  , 3: triangle2#(!n) -> u_16#(g2(!n, 0))
  , 4: triangle2#(!n) -> g2#(!n, 0)}
and edges
  1 -> {}
  2 -> {1, 2}
  3 -> {}
  4 -> {1, 2}
with 1 SCC(s)
  SCC:
    {g2#(!n, !s) -> g2#(-(!n, 1), +(!n, !s)) [>(!n, 0)]}
Reduction Pair with dependency pairs:
    dependency pairs:
      {g2#(!n, !s) -> g2#(-(!n, 1), +(!n, !s)) [>(!n, 0)]}
    rules:
      {u_23(!w_8) -> !w_8
      , g2(!n, !s) -> u_23(g2(-(!n, 1), +(!n, !s))) [>(!n, 0)]
      , g2(!n, !s) -> !s [<=(!n, 0)]
      , u_16(!w_6) -> !w_6
      , triangle2(!n) -> u_16(g2(!n, 0))}
    Value criterion after 1 iteration(s) with the projections:
      Iteration 1:
        projection(s):
          v(g2#) = 1
        removing the rule(s):
          {g2#(!n, !s) -> g2#(-(!n, 1), +(!n, !s)) [>(!n, 0)]}

Elapsed Time:  34.10 ms