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

Elapsed Time:  55.42 ms