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