YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { U11(tt(), N) -> activate(N) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__isNat(X)) -> isNat(X) , activate(n__s(X)) -> s(X) , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N) , plus(N, 0()) -> U11(isNat(N), N) , and(tt(), X) -> activate(X) , isNat(X) -> n__isNat(X) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> and(isNat(activate(V1)), n__isNat(activate(V2))) , isNat(n__s(V1)) -> isNat(activate(V1)) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Arguments of following rules are not normal-forms: { plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N) , plus(N, 0()) -> U11(isNat(N), N) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { U11(tt(), N) -> activate(N) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__isNat(X)) -> isNat(X) , activate(n__s(X)) -> s(X) , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , and(tt(), X) -> activate(X) , isNat(X) -> n__isNat(X) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> and(isNat(activate(V1)), n__isNat(activate(V2))) , isNat(n__s(V1)) -> isNat(activate(V1)) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 5. The enriched problem is compatible with the following automaton. { U11_0(2, 2) -> 1 , U11_0(2, 9) -> 1 , U11_0(2, 10) -> 1 , U11_0(2, 11) -> 1 , U11_0(2, 12) -> 1 , U11_0(9, 2) -> 1 , U11_0(9, 9) -> 1 , U11_0(9, 10) -> 1 , U11_0(9, 11) -> 1 , U11_0(9, 12) -> 1 , U11_0(10, 2) -> 1 , U11_0(10, 9) -> 1 , U11_0(10, 10) -> 1 , U11_0(10, 11) -> 1 , U11_0(10, 12) -> 1 , U11_0(11, 2) -> 1 , U11_0(11, 9) -> 1 , U11_0(11, 10) -> 1 , U11_0(11, 11) -> 1 , U11_0(11, 12) -> 1 , U11_0(12, 2) -> 1 , U11_0(12, 9) -> 1 , U11_0(12, 10) -> 1 , U11_0(12, 11) -> 1 , U11_0(12, 12) -> 1 , tt_0() -> 1 , tt_0() -> 2 , tt_0() -> 3 , tt_0() -> 7 , tt_0() -> 19 , tt_0() -> 20 , tt_0() -> 23 , tt_0() -> 24 , tt_1() -> 1 , tt_1() -> 3 , tt_1() -> 7 , tt_1() -> 8 , tt_1() -> 15 , tt_1() -> 17 , tt_1() -> 20 , tt_1() -> 21 , tt_1() -> 24 , tt_2() -> 1 , tt_2() -> 3 , tt_2() -> 7 , tt_2() -> 8 , tt_2() -> 15 , tt_2() -> 17 , tt_2() -> 20 , tt_2() -> 21 , tt_2() -> 24 , tt_3() -> 1 , tt_3() -> 3 , tt_3() -> 7 , tt_3() -> 8 , tt_3() -> 15 , tt_3() -> 17 , tt_3() -> 20 , tt_3() -> 21 , tt_3() -> 24 , activate_0(2) -> 3 , activate_0(9) -> 3 , activate_0(10) -> 3 , activate_0(11) -> 3 , activate_0(12) -> 3 , activate_1(2) -> 1 , activate_1(2) -> 7 , activate_1(9) -> 1 , activate_1(9) -> 7 , activate_1(10) -> 1 , activate_1(10) -> 7 , activate_1(11) -> 1 , activate_1(11) -> 7 , activate_1(12) -> 1 , activate_1(12) -> 7 , activate_1(16) -> 21 , activate_1(16) -> 24 , activate_1(18) -> 21 , activate_1(18) -> 24 , activate_2(2) -> 19 , activate_2(2) -> 20 , activate_2(9) -> 20 , activate_2(10) -> 20 , activate_2(11) -> 20 , activate_2(12) -> 20 , activate_2(16) -> 1 , activate_2(16) -> 3 , activate_2(16) -> 7 , activate_2(16) -> 8 , activate_2(16) -> 15 , activate_2(16) -> 17 , activate_2(16) -> 20 , activate_2(16) -> 21 , activate_2(16) -> 24 , activate_2(18) -> 1 , activate_2(18) -> 3 , activate_2(18) -> 7 , activate_2(18) -> 8 , activate_2(18) -> 15 , activate_2(18) -> 17 , activate_2(18) -> 20 , activate_2(18) -> 21 , activate_2(18) -> 24 , activate_2(22) -> 1 , activate_2(22) -> 3 , activate_2(22) -> 7 , activate_2(22) -> 8 , activate_2(22) -> 15 , activate_2(22) -> 17 , activate_2(22) -> 20 , activate_2(22) -> 21 , activate_2(22) -> 24 , activate_3(2) -> 23 , activate_3(2) -> 24 , activate_3(9) -> 24 , activate_3(10) -> 24 , activate_3(11) -> 24 , activate_3(12) -> 24 , activate_3(18) -> 1 , activate_3(18) -> 3 , activate_3(18) -> 7 , activate_3(18) -> 8 , activate_3(18) -> 15 , activate_3(18) -> 17 , activate_3(18) -> 20 , activate_3(18) -> 21 , activate_3(18) -> 24 , activate_3(22) -> 1 , activate_3(22) -> 3 , activate_3(22) -> 7 , activate_3(22) -> 8 , activate_3(22) -> 15 , activate_3(22) -> 17 , activate_3(22) -> 20 , activate_3(22) -> 21 , activate_3(22) -> 24 , activate_4(22) -> 1 , activate_4(22) -> 3 , activate_4(22) -> 7 , activate_4(22) -> 8 , activate_4(22) -> 15 , activate_4(22) -> 17 , activate_4(22) -> 20 , activate_4(22) -> 21 , activate_4(22) -> 24 , U21_0(2, 2, 2) -> 4 , U21_0(2, 2, 9) -> 4 , U21_0(2, 2, 10) -> 4 , U21_0(2, 2, 11) -> 4 , U21_0(2, 2, 12) -> 4 , U21_0(2, 9, 2) -> 4 , U21_0(2, 9, 9) -> 4 , U21_0(2, 9, 10) -> 4 , U21_0(2, 9, 11) -> 4 , U21_0(2, 9, 12) -> 4 , U21_0(2, 10, 2) -> 4 , U21_0(2, 10, 9) -> 4 , U21_0(2, 10, 10) -> 4 , U21_0(2, 10, 11) -> 4 , U21_0(2, 10, 12) -> 4 , U21_0(2, 11, 2) -> 4 , U21_0(2, 11, 9) -> 4 , U21_0(2, 11, 10) -> 4 , U21_0(2, 11, 11) -> 4 , U21_0(2, 11, 12) -> 4 , U21_0(2, 12, 2) -> 4 , U21_0(2, 12, 9) -> 4 , U21_0(2, 12, 10) -> 4 , U21_0(2, 12, 11) -> 4 , U21_0(2, 12, 12) -> 4 , U21_0(9, 2, 2) -> 4 , U21_0(9, 2, 9) -> 4 , U21_0(9, 2, 10) -> 4 , U21_0(9, 2, 11) -> 4 , U21_0(9, 2, 12) -> 4 , U21_0(9, 9, 2) -> 4 , U21_0(9, 9, 9) -> 4 , U21_0(9, 9, 10) -> 4 , U21_0(9, 9, 11) -> 4 , U21_0(9, 9, 12) -> 4 , U21_0(9, 10, 2) -> 4 , U21_0(9, 10, 9) -> 4 , U21_0(9, 10, 10) -> 4 , U21_0(9, 10, 11) -> 4 , U21_0(9, 10, 12) -> 4 , U21_0(9, 11, 2) -> 4 , U21_0(9, 11, 9) -> 4 , U21_0(9, 11, 10) -> 4 , U21_0(9, 11, 11) -> 4 , U21_0(9, 11, 12) -> 4 , U21_0(9, 12, 2) -> 4 , U21_0(9, 12, 9) -> 4 , U21_0(9, 12, 10) -> 4 , U21_0(9, 12, 11) -> 4 , U21_0(9, 12, 12) -> 4 , U21_0(10, 2, 2) -> 4 , U21_0(10, 2, 9) -> 4 , U21_0(10, 2, 10) -> 4 , U21_0(10, 2, 11) -> 4 , U21_0(10, 2, 12) -> 4 , U21_0(10, 9, 2) -> 4 , U21_0(10, 9, 9) -> 4 , U21_0(10, 9, 10) -> 4 , U21_0(10, 9, 11) -> 4 , U21_0(10, 9, 12) -> 4 , U21_0(10, 10, 2) -> 4 , U21_0(10, 10, 9) -> 4 , U21_0(10, 10, 10) -> 4 , U21_0(10, 10, 11) -> 4 , U21_0(10, 10, 12) -> 4 , U21_0(10, 11, 2) -> 4 , U21_0(10, 11, 9) -> 4 , U21_0(10, 11, 10) -> 4 , U21_0(10, 11, 11) -> 4 , U21_0(10, 11, 12) -> 4 , U21_0(10, 12, 2) -> 4 , U21_0(10, 12, 9) -> 4 , U21_0(10, 12, 10) -> 4 , U21_0(10, 12, 11) -> 4 , U21_0(10, 12, 12) -> 4 , U21_0(11, 2, 2) -> 4 , U21_0(11, 2, 9) -> 4 , U21_0(11, 2, 10) -> 4 , U21_0(11, 2, 11) -> 4 , U21_0(11, 2, 12) -> 4 , U21_0(11, 9, 2) -> 4 , U21_0(11, 9, 9) -> 4 , U21_0(11, 9, 10) -> 4 , U21_0(11, 9, 11) -> 4 , U21_0(11, 9, 12) -> 4 , U21_0(11, 10, 2) -> 4 , U21_0(11, 10, 9) -> 4 , U21_0(11, 10, 10) -> 4 , U21_0(11, 10, 11) -> 4 , U21_0(11, 10, 12) -> 4 , U21_0(11, 11, 2) -> 4 , U21_0(11, 11, 9) -> 4 , U21_0(11, 11, 10) -> 4 , U21_0(11, 11, 11) -> 4 , U21_0(11, 11, 12) -> 4 , U21_0(11, 12, 2) -> 4 , U21_0(11, 12, 9) -> 4 , U21_0(11, 12, 10) -> 4 , U21_0(11, 12, 11) -> 4 , U21_0(11, 12, 12) -> 4 , U21_0(12, 2, 2) -> 4 , U21_0(12, 2, 9) -> 4 , U21_0(12, 2, 10) -> 4 , U21_0(12, 2, 11) -> 4 , U21_0(12, 2, 12) -> 4 , U21_0(12, 9, 2) -> 4 , U21_0(12, 9, 9) -> 4 , U21_0(12, 9, 10) -> 4 , U21_0(12, 9, 11) -> 4 , U21_0(12, 9, 12) -> 4 , U21_0(12, 10, 2) -> 4 , U21_0(12, 10, 9) -> 4 , U21_0(12, 10, 10) -> 4 , U21_0(12, 10, 11) -> 4 , U21_0(12, 10, 12) -> 4 , U21_0(12, 11, 2) -> 4 , U21_0(12, 11, 9) -> 4 , U21_0(12, 11, 10) -> 4 , U21_0(12, 11, 11) -> 4 , U21_0(12, 11, 12) -> 4 , U21_0(12, 12, 2) -> 4 , U21_0(12, 12, 9) -> 4 , U21_0(12, 12, 10) -> 4 , U21_0(12, 12, 11) -> 4 , U21_0(12, 12, 12) -> 4 , s_0(2) -> 5 , s_0(9) -> 5 , s_0(10) -> 5 , s_0(11) -> 5 , s_0(12) -> 5 , s_1(2) -> 1 , s_1(2) -> 3 , s_1(2) -> 7 , s_1(2) -> 20 , s_1(2) -> 24 , s_1(9) -> 1 , s_1(9) -> 3 , s_1(9) -> 7 , s_1(9) -> 20 , s_1(9) -> 24 , s_1(10) -> 1 , s_1(10) -> 3 , s_1(10) -> 7 , s_1(10) -> 20 , s_1(10) -> 24 , s_1(11) -> 1 , s_1(11) -> 3 , s_1(11) -> 7 , s_1(11) -> 20 , s_1(11) -> 24 , s_1(12) -> 1 , s_1(12) -> 3 , s_1(12) -> 7 , s_1(12) -> 20 , s_1(12) -> 24 , s_1(14) -> 4 , plus_0(2, 2) -> 6 , plus_0(2, 9) -> 6 , plus_0(2, 10) -> 6 , plus_0(2, 11) -> 6 , plus_0(2, 12) -> 6 , plus_0(9, 2) -> 6 , plus_0(9, 9) -> 6 , plus_0(9, 10) -> 6 , plus_0(9, 11) -> 6 , plus_0(9, 12) -> 6 , plus_0(10, 2) -> 6 , plus_0(10, 9) -> 6 , plus_0(10, 10) -> 6 , plus_0(10, 11) -> 6 , plus_0(10, 12) -> 6 , plus_0(11, 2) -> 6 , plus_0(11, 9) -> 6 , plus_0(11, 10) -> 6 , plus_0(11, 11) -> 6 , plus_0(11, 12) -> 6 , plus_0(12, 2) -> 6 , plus_0(12, 9) -> 6 , plus_0(12, 10) -> 6 , plus_0(12, 11) -> 6 , plus_0(12, 12) -> 6 , plus_1(1, 1) -> 14 , plus_1(2, 2) -> 1 , plus_1(2, 2) -> 3 , plus_1(2, 2) -> 7 , plus_1(2, 2) -> 20 , plus_1(2, 2) -> 24 , plus_1(2, 9) -> 1 , plus_1(2, 9) -> 3 , plus_1(2, 9) -> 7 , plus_1(2, 9) -> 20 , plus_1(2, 9) -> 24 , plus_1(2, 10) -> 1 , plus_1(2, 10) -> 3 , plus_1(2, 10) -> 7 , plus_1(2, 10) -> 20 , plus_1(2, 10) -> 24 , plus_1(2, 11) -> 1 , plus_1(2, 11) -> 3 , plus_1(2, 11) -> 7 , plus_1(2, 11) -> 20 , plus_1(2, 11) -> 24 , plus_1(2, 12) -> 1 , plus_1(2, 12) -> 3 , plus_1(2, 12) -> 7 , plus_1(2, 12) -> 20 , plus_1(2, 12) -> 24 , plus_1(9, 2) -> 1 , plus_1(9, 2) -> 3 , plus_1(9, 2) -> 7 , plus_1(9, 2) -> 20 , plus_1(9, 2) -> 24 , plus_1(9, 9) -> 1 , plus_1(9, 9) -> 3 , plus_1(9, 9) -> 7 , plus_1(9, 9) -> 20 , plus_1(9, 9) -> 24 , plus_1(9, 10) -> 1 , plus_1(9, 10) -> 3 , plus_1(9, 10) -> 7 , plus_1(9, 10) -> 20 , plus_1(9, 10) -> 24 , plus_1(9, 11) -> 1 , plus_1(9, 11) -> 3 , plus_1(9, 11) -> 7 , plus_1(9, 11) -> 20 , plus_1(9, 11) -> 24 , plus_1(9, 12) -> 1 , plus_1(9, 12) -> 3 , plus_1(9, 12) -> 7 , plus_1(9, 12) -> 20 , plus_1(9, 12) -> 24 , plus_1(10, 2) -> 1 , plus_1(10, 2) -> 3 , plus_1(10, 2) -> 7 , plus_1(10, 2) -> 20 , plus_1(10, 2) -> 24 , plus_1(10, 9) -> 1 , plus_1(10, 9) -> 3 , plus_1(10, 9) -> 7 , plus_1(10, 9) -> 20 , plus_1(10, 9) -> 24 , plus_1(10, 10) -> 1 , plus_1(10, 10) -> 3 , plus_1(10, 10) -> 7 , plus_1(10, 10) -> 20 , plus_1(10, 10) -> 24 , plus_1(10, 11) -> 1 , plus_1(10, 11) -> 3 , plus_1(10, 11) -> 7 , plus_1(10, 11) -> 20 , plus_1(10, 11) -> 24 , plus_1(10, 12) -> 1 , plus_1(10, 12) -> 3 , plus_1(10, 12) -> 7 , plus_1(10, 12) -> 20 , plus_1(10, 12) -> 24 , plus_1(11, 2) -> 1 , plus_1(11, 2) -> 3 , plus_1(11, 2) -> 7 , plus_1(11, 2) -> 20 , plus_1(11, 2) -> 24 , plus_1(11, 9) -> 1 , plus_1(11, 9) -> 3 , plus_1(11, 9) -> 7 , plus_1(11, 9) -> 20 , plus_1(11, 9) -> 24 , plus_1(11, 10) -> 1 , plus_1(11, 10) -> 3 , plus_1(11, 10) -> 7 , plus_1(11, 10) -> 20 , plus_1(11, 10) -> 24 , plus_1(11, 11) -> 1 , plus_1(11, 11) -> 3 , plus_1(11, 11) -> 7 , plus_1(11, 11) -> 20 , plus_1(11, 11) -> 24 , plus_1(11, 12) -> 1 , plus_1(11, 12) -> 3 , plus_1(11, 12) -> 7 , plus_1(11, 12) -> 20 , plus_1(11, 12) -> 24 , plus_1(12, 2) -> 1 , plus_1(12, 2) -> 3 , plus_1(12, 2) -> 7 , plus_1(12, 2) -> 20 , plus_1(12, 2) -> 24 , plus_1(12, 9) -> 1 , plus_1(12, 9) -> 3 , plus_1(12, 9) -> 7 , plus_1(12, 9) -> 20 , plus_1(12, 9) -> 24 , plus_1(12, 10) -> 1 , plus_1(12, 10) -> 3 , plus_1(12, 10) -> 7 , plus_1(12, 10) -> 20 , plus_1(12, 10) -> 24 , plus_1(12, 11) -> 1 , plus_1(12, 11) -> 3 , plus_1(12, 11) -> 7 , plus_1(12, 11) -> 20 , plus_1(12, 11) -> 24 , plus_1(12, 12) -> 1 , plus_1(12, 12) -> 3 , plus_1(12, 12) -> 7 , plus_1(12, 12) -> 20 , plus_1(12, 12) -> 24 , and_0(2, 2) -> 7 , and_0(2, 9) -> 7 , and_0(2, 10) -> 7 , and_0(2, 11) -> 7 , and_0(2, 12) -> 7 , and_0(9, 2) -> 7 , and_0(9, 9) -> 7 , and_0(9, 10) -> 7 , and_0(9, 11) -> 7 , and_0(9, 12) -> 7 , and_0(10, 2) -> 7 , and_0(10, 9) -> 7 , and_0(10, 10) -> 7 , and_0(10, 11) -> 7 , and_0(10, 12) -> 7 , and_0(11, 2) -> 7 , and_0(11, 9) -> 7 , and_0(11, 10) -> 7 , and_0(11, 11) -> 7 , and_0(11, 12) -> 7 , and_0(12, 2) -> 7 , and_0(12, 9) -> 7 , and_0(12, 10) -> 7 , and_0(12, 11) -> 7 , and_0(12, 12) -> 7 , and_1(15, 16) -> 1 , and_1(15, 16) -> 3 , and_1(15, 16) -> 7 , and_1(15, 16) -> 8 , and_1(15, 16) -> 15 , and_1(15, 16) -> 17 , and_1(15, 16) -> 20 , and_1(20, 16) -> 21 , and_1(20, 16) -> 24 , and_2(17, 18) -> 1 , and_2(17, 18) -> 3 , and_2(17, 18) -> 7 , and_2(17, 18) -> 8 , and_2(17, 18) -> 15 , and_2(17, 18) -> 17 , and_2(17, 18) -> 20 , and_2(20, 18) -> 21 , and_2(20, 18) -> 24 , and_3(21, 22) -> 1 , and_3(21, 22) -> 3 , and_3(21, 22) -> 7 , and_3(21, 22) -> 8 , and_3(21, 22) -> 15 , and_3(21, 22) -> 17 , and_3(21, 22) -> 20 , and_3(21, 22) -> 21 , and_3(21, 22) -> 24 , isNat_0(2) -> 8 , isNat_0(9) -> 8 , isNat_0(10) -> 8 , isNat_0(11) -> 8 , isNat_0(12) -> 8 , isNat_1(2) -> 1 , isNat_1(2) -> 3 , isNat_1(2) -> 7 , isNat_1(2) -> 20 , isNat_1(2) -> 24 , isNat_1(7) -> 1 , isNat_1(7) -> 3 , isNat_1(7) -> 7 , isNat_1(7) -> 8 , isNat_1(7) -> 15 , isNat_1(7) -> 17 , isNat_1(7) -> 20 , isNat_1(7) -> 21 , isNat_1(7) -> 24 , isNat_1(9) -> 1 , isNat_1(9) -> 3 , isNat_1(9) -> 7 , isNat_1(9) -> 20 , isNat_1(9) -> 24 , isNat_1(10) -> 1 , isNat_1(10) -> 3 , isNat_1(10) -> 7 , isNat_1(10) -> 20 , isNat_1(10) -> 24 , isNat_1(11) -> 1 , isNat_1(11) -> 3 , isNat_1(11) -> 7 , isNat_1(11) -> 20 , isNat_1(11) -> 24 , isNat_1(12) -> 1 , isNat_1(12) -> 3 , isNat_1(12) -> 7 , isNat_1(12) -> 20 , isNat_1(12) -> 24 , isNat_2(7) -> 1 , isNat_2(7) -> 3 , isNat_2(7) -> 7 , isNat_2(7) -> 8 , isNat_2(7) -> 15 , isNat_2(7) -> 17 , isNat_2(7) -> 20 , isNat_2(7) -> 21 , isNat_2(7) -> 24 , isNat_2(19) -> 17 , isNat_2(20) -> 1 , isNat_2(20) -> 3 , isNat_2(20) -> 7 , isNat_2(20) -> 8 , isNat_2(20) -> 15 , isNat_2(20) -> 17 , isNat_2(20) -> 20 , isNat_2(20) -> 21 , isNat_2(20) -> 24 , isNat_3(20) -> 1 , isNat_3(20) -> 3 , isNat_3(20) -> 7 , isNat_3(20) -> 8 , isNat_3(20) -> 15 , isNat_3(20) -> 17 , isNat_3(20) -> 20 , isNat_3(20) -> 21 , isNat_3(20) -> 24 , isNat_3(23) -> 21 , isNat_3(24) -> 1 , isNat_3(24) -> 3 , isNat_3(24) -> 7 , isNat_3(24) -> 8 , isNat_3(24) -> 15 , isNat_3(24) -> 17 , isNat_3(24) -> 20 , isNat_3(24) -> 21 , isNat_3(24) -> 24 , isNat_4(24) -> 1 , isNat_4(24) -> 3 , isNat_4(24) -> 7 , isNat_4(24) -> 8 , isNat_4(24) -> 15 , isNat_4(24) -> 17 , isNat_4(24) -> 20 , isNat_4(24) -> 21 , isNat_4(24) -> 24 , n__0_0() -> 1 , n__0_0() -> 3 , n__0_0() -> 7 , n__0_0() -> 9 , n__0_0() -> 20 , n__0_0() -> 24 , n__0_1() -> 13 , n__0_2() -> 1 , n__0_2() -> 3 , n__0_2() -> 7 , n__0_2() -> 20 , n__0_2() -> 24 , n__plus_0(2, 2) -> 1 , n__plus_0(2, 2) -> 3 , n__plus_0(2, 2) -> 7 , n__plus_0(2, 2) -> 10 , n__plus_0(2, 2) -> 20 , n__plus_0(2, 2) -> 24 , n__plus_0(2, 9) -> 1 , n__plus_0(2, 9) -> 3 , n__plus_0(2, 9) -> 7 , n__plus_0(2, 9) -> 10 , n__plus_0(2, 9) -> 20 , n__plus_0(2, 9) -> 24 , n__plus_0(2, 10) -> 1 , n__plus_0(2, 10) -> 3 , n__plus_0(2, 10) -> 7 , n__plus_0(2, 10) -> 10 , n__plus_0(2, 10) -> 20 , n__plus_0(2, 10) -> 24 , n__plus_0(2, 11) -> 1 , n__plus_0(2, 11) -> 3 , n__plus_0(2, 11) -> 7 , n__plus_0(2, 11) -> 10 , n__plus_0(2, 11) -> 20 , n__plus_0(2, 11) -> 24 , n__plus_0(2, 12) -> 1 , n__plus_0(2, 12) -> 3 , n__plus_0(2, 12) -> 7 , n__plus_0(2, 12) -> 10 , n__plus_0(2, 12) -> 20 , n__plus_0(2, 12) -> 24 , n__plus_0(9, 2) -> 1 , n__plus_0(9, 2) -> 3 , n__plus_0(9, 2) -> 7 , n__plus_0(9, 2) -> 10 , n__plus_0(9, 2) -> 20 , n__plus_0(9, 2) -> 24 , n__plus_0(9, 9) -> 1 , n__plus_0(9, 9) -> 3 , n__plus_0(9, 9) -> 7 , n__plus_0(9, 9) -> 10 , n__plus_0(9, 9) -> 20 , n__plus_0(9, 9) -> 24 , n__plus_0(9, 10) -> 1 , n__plus_0(9, 10) -> 3 , n__plus_0(9, 10) -> 7 , n__plus_0(9, 10) -> 10 , n__plus_0(9, 10) -> 20 , n__plus_0(9, 10) -> 24 , n__plus_0(9, 11) -> 1 , n__plus_0(9, 11) -> 3 , n__plus_0(9, 11) -> 7 , n__plus_0(9, 11) -> 10 , n__plus_0(9, 11) -> 20 , n__plus_0(9, 11) -> 24 , n__plus_0(9, 12) -> 1 , n__plus_0(9, 12) -> 3 , n__plus_0(9, 12) -> 7 , n__plus_0(9, 12) -> 10 , n__plus_0(9, 12) -> 20 , n__plus_0(9, 12) -> 24 , n__plus_0(10, 2) -> 1 , n__plus_0(10, 2) -> 3 , n__plus_0(10, 2) -> 7 , n__plus_0(10, 2) -> 10 , n__plus_0(10, 2) -> 20 , n__plus_0(10, 2) -> 24 , n__plus_0(10, 9) -> 1 , n__plus_0(10, 9) -> 3 , n__plus_0(10, 9) -> 7 , n__plus_0(10, 9) -> 10 , n__plus_0(10, 9) -> 20 , n__plus_0(10, 9) -> 24 , n__plus_0(10, 10) -> 1 , n__plus_0(10, 10) -> 3 , n__plus_0(10, 10) -> 7 , n__plus_0(10, 10) -> 10 , n__plus_0(10, 10) -> 20 , n__plus_0(10, 10) -> 24 , n__plus_0(10, 11) -> 1 , n__plus_0(10, 11) -> 3 , n__plus_0(10, 11) -> 7 , n__plus_0(10, 11) -> 10 , n__plus_0(10, 11) -> 20 , n__plus_0(10, 11) -> 24 , n__plus_0(10, 12) -> 1 , n__plus_0(10, 12) -> 3 , n__plus_0(10, 12) -> 7 , n__plus_0(10, 12) -> 10 , n__plus_0(10, 12) -> 20 , n__plus_0(10, 12) -> 24 , n__plus_0(11, 2) -> 1 , n__plus_0(11, 2) -> 3 , n__plus_0(11, 2) -> 7 , n__plus_0(11, 2) -> 10 , n__plus_0(11, 2) -> 20 , n__plus_0(11, 2) -> 24 , n__plus_0(11, 9) -> 1 , n__plus_0(11, 9) -> 3 , n__plus_0(11, 9) -> 7 , n__plus_0(11, 9) -> 10 , n__plus_0(11, 9) -> 20 , n__plus_0(11, 9) -> 24 , n__plus_0(11, 10) -> 1 , n__plus_0(11, 10) -> 3 , n__plus_0(11, 10) -> 7 , n__plus_0(11, 10) -> 10 , n__plus_0(11, 10) -> 20 , n__plus_0(11, 10) -> 24 , n__plus_0(11, 11) -> 1 , n__plus_0(11, 11) -> 3 , n__plus_0(11, 11) -> 7 , n__plus_0(11, 11) -> 10 , n__plus_0(11, 11) -> 20 , n__plus_0(11, 11) -> 24 , n__plus_0(11, 12) -> 1 , n__plus_0(11, 12) -> 3 , n__plus_0(11, 12) -> 7 , n__plus_0(11, 12) -> 10 , n__plus_0(11, 12) -> 20 , n__plus_0(11, 12) -> 24 , n__plus_0(12, 2) -> 1 , n__plus_0(12, 2) -> 3 , n__plus_0(12, 2) -> 7 , n__plus_0(12, 2) -> 10 , n__plus_0(12, 2) -> 20 , n__plus_0(12, 2) -> 24 , n__plus_0(12, 9) -> 1 , n__plus_0(12, 9) -> 3 , n__plus_0(12, 9) -> 7 , n__plus_0(12, 9) -> 10 , n__plus_0(12, 9) -> 20 , n__plus_0(12, 9) -> 24 , n__plus_0(12, 10) -> 1 , n__plus_0(12, 10) -> 3 , n__plus_0(12, 10) -> 7 , n__plus_0(12, 10) -> 10 , n__plus_0(12, 10) -> 20 , n__plus_0(12, 10) -> 24 , n__plus_0(12, 11) -> 1 , n__plus_0(12, 11) -> 3 , n__plus_0(12, 11) -> 7 , n__plus_0(12, 11) -> 10 , n__plus_0(12, 11) -> 20 , n__plus_0(12, 11) -> 24 , n__plus_0(12, 12) -> 1 , n__plus_0(12, 12) -> 3 , n__plus_0(12, 12) -> 7 , n__plus_0(12, 12) -> 10 , n__plus_0(12, 12) -> 20 , n__plus_0(12, 12) -> 24 , n__plus_1(2, 2) -> 6 , n__plus_1(2, 9) -> 6 , n__plus_1(2, 10) -> 6 , n__plus_1(2, 11) -> 6 , n__plus_1(2, 12) -> 6 , n__plus_1(9, 2) -> 6 , n__plus_1(9, 9) -> 6 , n__plus_1(9, 10) -> 6 , n__plus_1(9, 11) -> 6 , n__plus_1(9, 12) -> 6 , n__plus_1(10, 2) -> 6 , n__plus_1(10, 9) -> 6 , n__plus_1(10, 10) -> 6 , n__plus_1(10, 11) -> 6 , n__plus_1(10, 12) -> 6 , n__plus_1(11, 2) -> 6 , n__plus_1(11, 9) -> 6 , n__plus_1(11, 10) -> 6 , n__plus_1(11, 11) -> 6 , n__plus_1(11, 12) -> 6 , n__plus_1(12, 2) -> 6 , n__plus_1(12, 9) -> 6 , n__plus_1(12, 10) -> 6 , n__plus_1(12, 11) -> 6 , n__plus_1(12, 12) -> 6 , n__plus_2(1, 1) -> 14 , n__plus_2(2, 2) -> 1 , n__plus_2(2, 2) -> 3 , n__plus_2(2, 2) -> 7 , n__plus_2(2, 2) -> 20 , n__plus_2(2, 2) -> 24 , n__plus_2(2, 9) -> 1 , n__plus_2(2, 9) -> 3 , n__plus_2(2, 9) -> 7 , n__plus_2(2, 9) -> 20 , n__plus_2(2, 9) -> 24 , n__plus_2(2, 10) -> 1 , n__plus_2(2, 10) -> 3 , n__plus_2(2, 10) -> 7 , n__plus_2(2, 10) -> 20 , n__plus_2(2, 10) -> 24 , n__plus_2(2, 11) -> 1 , n__plus_2(2, 11) -> 3 , n__plus_2(2, 11) -> 7 , n__plus_2(2, 11) -> 20 , n__plus_2(2, 11) -> 24 , n__plus_2(2, 12) -> 1 , n__plus_2(2, 12) -> 3 , n__plus_2(2, 12) -> 7 , n__plus_2(2, 12) -> 20 , n__plus_2(2, 12) -> 24 , n__plus_2(9, 2) -> 1 , n__plus_2(9, 2) -> 3 , n__plus_2(9, 2) -> 7 , n__plus_2(9, 2) -> 20 , n__plus_2(9, 2) -> 24 , n__plus_2(9, 9) -> 1 , n__plus_2(9, 9) -> 3 , n__plus_2(9, 9) -> 7 , n__plus_2(9, 9) -> 20 , n__plus_2(9, 9) -> 24 , n__plus_2(9, 10) -> 1 , n__plus_2(9, 10) -> 3 , n__plus_2(9, 10) -> 7 , n__plus_2(9, 10) -> 20 , n__plus_2(9, 10) -> 24 , n__plus_2(9, 11) -> 1 , n__plus_2(9, 11) -> 3 , n__plus_2(9, 11) -> 7 , n__plus_2(9, 11) -> 20 , n__plus_2(9, 11) -> 24 , n__plus_2(9, 12) -> 1 , n__plus_2(9, 12) -> 3 , n__plus_2(9, 12) -> 7 , n__plus_2(9, 12) -> 20 , n__plus_2(9, 12) -> 24 , n__plus_2(10, 2) -> 1 , n__plus_2(10, 2) -> 3 , n__plus_2(10, 2) -> 7 , n__plus_2(10, 2) -> 20 , n__plus_2(10, 2) -> 24 , n__plus_2(10, 9) -> 1 , n__plus_2(10, 9) -> 3 , n__plus_2(10, 9) -> 7 , n__plus_2(10, 9) -> 20 , n__plus_2(10, 9) -> 24 , n__plus_2(10, 10) -> 1 , n__plus_2(10, 10) -> 3 , n__plus_2(10, 10) -> 7 , n__plus_2(10, 10) -> 20 , n__plus_2(10, 10) -> 24 , n__plus_2(10, 11) -> 1 , n__plus_2(10, 11) -> 3 , n__plus_2(10, 11) -> 7 , n__plus_2(10, 11) -> 20 , n__plus_2(10, 11) -> 24 , n__plus_2(10, 12) -> 1 , n__plus_2(10, 12) -> 3 , n__plus_2(10, 12) -> 7 , n__plus_2(10, 12) -> 20 , n__plus_2(10, 12) -> 24 , n__plus_2(11, 2) -> 1 , n__plus_2(11, 2) -> 3 , n__plus_2(11, 2) -> 7 , n__plus_2(11, 2) -> 20 , n__plus_2(11, 2) -> 24 , n__plus_2(11, 9) -> 1 , n__plus_2(11, 9) -> 3 , n__plus_2(11, 9) -> 7 , n__plus_2(11, 9) -> 20 , n__plus_2(11, 9) -> 24 , n__plus_2(11, 10) -> 1 , n__plus_2(11, 10) -> 3 , n__plus_2(11, 10) -> 7 , n__plus_2(11, 10) -> 20 , n__plus_2(11, 10) -> 24 , n__plus_2(11, 11) -> 1 , n__plus_2(11, 11) -> 3 , n__plus_2(11, 11) -> 7 , n__plus_2(11, 11) -> 20 , n__plus_2(11, 11) -> 24 , n__plus_2(11, 12) -> 1 , n__plus_2(11, 12) -> 3 , n__plus_2(11, 12) -> 7 , n__plus_2(11, 12) -> 20 , n__plus_2(11, 12) -> 24 , n__plus_2(12, 2) -> 1 , n__plus_2(12, 2) -> 3 , n__plus_2(12, 2) -> 7 , n__plus_2(12, 2) -> 20 , n__plus_2(12, 2) -> 24 , n__plus_2(12, 9) -> 1 , n__plus_2(12, 9) -> 3 , n__plus_2(12, 9) -> 7 , n__plus_2(12, 9) -> 20 , n__plus_2(12, 9) -> 24 , n__plus_2(12, 10) -> 1 , n__plus_2(12, 10) -> 3 , n__plus_2(12, 10) -> 7 , n__plus_2(12, 10) -> 20 , n__plus_2(12, 10) -> 24 , n__plus_2(12, 11) -> 1 , n__plus_2(12, 11) -> 3 , n__plus_2(12, 11) -> 7 , n__plus_2(12, 11) -> 20 , n__plus_2(12, 11) -> 24 , n__plus_2(12, 12) -> 1 , n__plus_2(12, 12) -> 3 , n__plus_2(12, 12) -> 7 , n__plus_2(12, 12) -> 20 , n__plus_2(12, 12) -> 24 , n__isNat_0(2) -> 1 , n__isNat_0(2) -> 3 , n__isNat_0(2) -> 7 , n__isNat_0(2) -> 11 , n__isNat_0(2) -> 20 , n__isNat_0(2) -> 24 , n__isNat_0(9) -> 1 , n__isNat_0(9) -> 3 , n__isNat_0(9) -> 7 , n__isNat_0(9) -> 11 , n__isNat_0(9) -> 20 , n__isNat_0(9) -> 24 , n__isNat_0(10) -> 1 , n__isNat_0(10) -> 3 , n__isNat_0(10) -> 7 , n__isNat_0(10) -> 11 , n__isNat_0(10) -> 20 , n__isNat_0(10) -> 24 , n__isNat_0(11) -> 1 , n__isNat_0(11) -> 3 , n__isNat_0(11) -> 7 , n__isNat_0(11) -> 11 , n__isNat_0(11) -> 20 , n__isNat_0(11) -> 24 , n__isNat_0(12) -> 1 , n__isNat_0(12) -> 3 , n__isNat_0(12) -> 7 , n__isNat_0(12) -> 11 , n__isNat_0(12) -> 20 , n__isNat_0(12) -> 24 , n__isNat_1(2) -> 8 , n__isNat_1(7) -> 1 , n__isNat_1(7) -> 3 , n__isNat_1(7) -> 7 , n__isNat_1(7) -> 8 , n__isNat_1(7) -> 15 , n__isNat_1(7) -> 16 , n__isNat_1(7) -> 17 , n__isNat_1(7) -> 20 , n__isNat_1(7) -> 21 , n__isNat_1(7) -> 24 , n__isNat_1(9) -> 8 , n__isNat_1(10) -> 8 , n__isNat_1(11) -> 8 , n__isNat_1(12) -> 8 , n__isNat_2(2) -> 1 , n__isNat_2(2) -> 3 , n__isNat_2(2) -> 7 , n__isNat_2(2) -> 20 , n__isNat_2(2) -> 24 , n__isNat_2(7) -> 1 , n__isNat_2(7) -> 3 , n__isNat_2(7) -> 7 , n__isNat_2(7) -> 8 , n__isNat_2(7) -> 15 , n__isNat_2(7) -> 17 , n__isNat_2(7) -> 20 , n__isNat_2(7) -> 21 , n__isNat_2(7) -> 24 , n__isNat_2(9) -> 1 , n__isNat_2(9) -> 3 , n__isNat_2(9) -> 7 , n__isNat_2(9) -> 20 , n__isNat_2(9) -> 24 , n__isNat_2(10) -> 1 , n__isNat_2(10) -> 3 , n__isNat_2(10) -> 7 , n__isNat_2(10) -> 20 , n__isNat_2(10) -> 24 , n__isNat_2(11) -> 1 , n__isNat_2(11) -> 3 , n__isNat_2(11) -> 7 , n__isNat_2(11) -> 20 , n__isNat_2(11) -> 24 , n__isNat_2(12) -> 1 , n__isNat_2(12) -> 3 , n__isNat_2(12) -> 7 , n__isNat_2(12) -> 20 , n__isNat_2(12) -> 24 , n__isNat_2(20) -> 1 , n__isNat_2(20) -> 3 , n__isNat_2(20) -> 7 , n__isNat_2(20) -> 8 , n__isNat_2(20) -> 15 , n__isNat_2(20) -> 17 , n__isNat_2(20) -> 18 , n__isNat_2(20) -> 20 , n__isNat_2(20) -> 21 , n__isNat_2(20) -> 24 , n__isNat_3(7) -> 1 , n__isNat_3(7) -> 3 , n__isNat_3(7) -> 7 , n__isNat_3(7) -> 8 , n__isNat_3(7) -> 15 , n__isNat_3(7) -> 17 , n__isNat_3(7) -> 20 , n__isNat_3(7) -> 21 , n__isNat_3(7) -> 24 , n__isNat_3(19) -> 17 , n__isNat_3(20) -> 1 , n__isNat_3(20) -> 3 , n__isNat_3(20) -> 7 , n__isNat_3(20) -> 8 , n__isNat_3(20) -> 15 , n__isNat_3(20) -> 17 , n__isNat_3(20) -> 20 , n__isNat_3(20) -> 21 , n__isNat_3(20) -> 24 , n__isNat_3(24) -> 1 , n__isNat_3(24) -> 3 , n__isNat_3(24) -> 7 , n__isNat_3(24) -> 8 , n__isNat_3(24) -> 15 , n__isNat_3(24) -> 17 , n__isNat_3(24) -> 20 , n__isNat_3(24) -> 21 , n__isNat_3(24) -> 22 , n__isNat_3(24) -> 24 , n__isNat_4(20) -> 1 , n__isNat_4(20) -> 3 , n__isNat_4(20) -> 7 , n__isNat_4(20) -> 8 , n__isNat_4(20) -> 15 , n__isNat_4(20) -> 17 , n__isNat_4(20) -> 20 , n__isNat_4(20) -> 21 , n__isNat_4(20) -> 24 , n__isNat_4(23) -> 21 , n__isNat_4(24) -> 1 , n__isNat_4(24) -> 3 , n__isNat_4(24) -> 7 , n__isNat_4(24) -> 8 , n__isNat_4(24) -> 15 , n__isNat_4(24) -> 17 , n__isNat_4(24) -> 20 , n__isNat_4(24) -> 21 , n__isNat_4(24) -> 24 , n__isNat_5(24) -> 1 , n__isNat_5(24) -> 3 , n__isNat_5(24) -> 7 , n__isNat_5(24) -> 8 , n__isNat_5(24) -> 15 , n__isNat_5(24) -> 17 , n__isNat_5(24) -> 20 , n__isNat_5(24) -> 21 , n__isNat_5(24) -> 24 , n__s_0(2) -> 1 , n__s_0(2) -> 3 , n__s_0(2) -> 7 , n__s_0(2) -> 12 , n__s_0(2) -> 20 , n__s_0(2) -> 24 , n__s_0(9) -> 1 , n__s_0(9) -> 3 , n__s_0(9) -> 7 , n__s_0(9) -> 12 , n__s_0(9) -> 20 , n__s_0(9) -> 24 , n__s_0(10) -> 1 , n__s_0(10) -> 3 , n__s_0(10) -> 7 , n__s_0(10) -> 12 , n__s_0(10) -> 20 , n__s_0(10) -> 24 , n__s_0(11) -> 1 , n__s_0(11) -> 3 , n__s_0(11) -> 7 , n__s_0(11) -> 12 , n__s_0(11) -> 20 , n__s_0(11) -> 24 , n__s_0(12) -> 1 , n__s_0(12) -> 3 , n__s_0(12) -> 7 , n__s_0(12) -> 12 , n__s_0(12) -> 20 , n__s_0(12) -> 24 , n__s_1(2) -> 5 , n__s_1(9) -> 5 , n__s_1(10) -> 5 , n__s_1(11) -> 5 , n__s_1(12) -> 5 , n__s_2(2) -> 1 , n__s_2(2) -> 3 , n__s_2(2) -> 7 , n__s_2(2) -> 20 , n__s_2(2) -> 24 , n__s_2(9) -> 1 , n__s_2(9) -> 3 , n__s_2(9) -> 7 , n__s_2(9) -> 20 , n__s_2(9) -> 24 , n__s_2(10) -> 1 , n__s_2(10) -> 3 , n__s_2(10) -> 7 , n__s_2(10) -> 20 , n__s_2(10) -> 24 , n__s_2(11) -> 1 , n__s_2(11) -> 3 , n__s_2(11) -> 7 , n__s_2(11) -> 20 , n__s_2(11) -> 24 , n__s_2(12) -> 1 , n__s_2(12) -> 3 , n__s_2(12) -> 7 , n__s_2(12) -> 20 , n__s_2(12) -> 24 , n__s_2(14) -> 4 , 0_0() -> 13 , 0_1() -> 1 , 0_1() -> 3 , 0_1() -> 7 , 0_1() -> 20 , 0_1() -> 24 , 2 -> 1 , 2 -> 3 , 2 -> 7 , 2 -> 19 , 2 -> 20 , 2 -> 23 , 2 -> 24 , 9 -> 1 , 9 -> 3 , 9 -> 7 , 9 -> 20 , 9 -> 24 , 10 -> 1 , 10 -> 3 , 10 -> 7 , 10 -> 20 , 10 -> 24 , 11 -> 1 , 11 -> 3 , 11 -> 7 , 11 -> 20 , 11 -> 24 , 12 -> 1 , 12 -> 3 , 12 -> 7 , 12 -> 20 , 12 -> 24 , 16 -> 1 , 16 -> 3 , 16 -> 7 , 16 -> 8 , 16 -> 15 , 16 -> 17 , 16 -> 20 , 16 -> 21 , 16 -> 24 , 18 -> 1 , 18 -> 3 , 18 -> 7 , 18 -> 8 , 18 -> 15 , 18 -> 17 , 18 -> 20 , 18 -> 21 , 18 -> 24 , 22 -> 1 , 22 -> 3 , 22 -> 7 , 22 -> 8 , 22 -> 15 , 22 -> 17 , 22 -> 20 , 22 -> 21 , 22 -> 24 } Hurray, we answered YES(?,O(n^1))