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

Elapsed Time:  78.21 ms