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