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 }

Hurray, we answered YES(?,O(n^1))