YES(?,O(n^1))
3.65/1.17	YES(?,O(n^1))
3.65/1.17	
3.65/1.17	We are left with following problem, upon which TcT provides the
3.65/1.17	certificate YES(?,O(n^1)).
3.65/1.17	
3.65/1.17	Strict Trs:
3.65/1.17	  { revconsapp(C(x1, x2), r) -> revconsapp(x2, C(x1, r))
3.65/1.17	  , revconsapp(V(n), r) -> r
3.65/1.17	  , revconsapp(N(), r) -> r
3.65/1.17	  , deeprevapp(C(x1, x2), rest) -> deeprevapp(x2, C(x1, rest))
3.65/1.17	  , deeprevapp(V(n), rest) -> revconsapp(rest, V(n))
3.65/1.17	  , deeprevapp(N(), rest) -> rest
3.65/1.17	  , deeprev(C(x1, x2)) -> deeprevapp(C(x1, x2), N())
3.65/1.17	  , deeprev(V(n)) -> V(n)
3.65/1.17	  , deeprev(N()) -> N()
3.65/1.17	  , second(C(x1, x2)) -> x2
3.65/1.17	  , second(V(n)) -> N()
3.65/1.17	  , isVal(C(x1, x2)) -> False()
3.65/1.17	  , isVal(V(n)) -> True()
3.65/1.17	  , isVal(N()) -> False()
3.65/1.17	  , isNotEmptyT(C(x1, x2)) -> True()
3.65/1.17	  , isNotEmptyT(V(n)) -> False()
3.65/1.17	  , isNotEmptyT(N()) -> False()
3.65/1.17	  , isEmptyT(C(x1, x2)) -> False()
3.65/1.17	  , isEmptyT(V(n)) -> False()
3.65/1.17	  , isEmptyT(N()) -> True()
3.65/1.17	  , first(C(x1, x2)) -> x1
3.65/1.17	  , first(V(n)) -> N()
3.65/1.17	  , goal(x) -> deeprev(x) }
3.65/1.17	Obligation:
3.65/1.17	  innermost runtime complexity
3.65/1.17	Answer:
3.65/1.17	  YES(?,O(n^1))
3.65/1.17	
3.65/1.17	The problem is match-bounded by 3. The enriched problem is
3.65/1.17	compatible with the following automaton.
3.65/1.17	{ revconsapp_0(2, 2) -> 1
3.65/1.17	, revconsapp_0(2, 4) -> 1
3.65/1.17	, revconsapp_0(2, 5) -> 1
3.65/1.17	, revconsapp_0(2, 9) -> 1
3.65/1.17	, revconsapp_0(2, 10) -> 1
3.65/1.17	, revconsapp_0(4, 2) -> 1
3.65/1.17	, revconsapp_0(4, 4) -> 1
3.65/1.17	, revconsapp_0(4, 5) -> 1
3.65/1.17	, revconsapp_0(4, 9) -> 1
3.65/1.17	, revconsapp_0(4, 10) -> 1
3.65/1.17	, revconsapp_0(5, 2) -> 1
3.65/1.17	, revconsapp_0(5, 4) -> 1
3.65/1.17	, revconsapp_0(5, 5) -> 1
3.65/1.17	, revconsapp_0(5, 9) -> 1
3.65/1.17	, revconsapp_0(5, 10) -> 1
3.65/1.17	, revconsapp_0(9, 2) -> 1
3.65/1.17	, revconsapp_0(9, 4) -> 1
3.65/1.17	, revconsapp_0(9, 5) -> 1
3.65/1.17	, revconsapp_0(9, 9) -> 1
3.65/1.17	, revconsapp_0(9, 10) -> 1
3.65/1.17	, revconsapp_0(10, 2) -> 1
3.65/1.17	, revconsapp_0(10, 4) -> 1
3.65/1.17	, revconsapp_0(10, 5) -> 1
3.65/1.17	, revconsapp_0(10, 9) -> 1
3.65/1.17	, revconsapp_0(10, 10) -> 1
3.65/1.17	, revconsapp_1(2, 15) -> 1
3.65/1.17	, revconsapp_1(2, 16) -> 3
3.65/1.17	, revconsapp_1(4, 15) -> 1
3.65/1.17	, revconsapp_1(4, 16) -> 3
3.65/1.17	, revconsapp_1(5, 15) -> 1
3.65/1.17	, revconsapp_1(5, 16) -> 3
3.65/1.17	, revconsapp_1(9, 15) -> 1
3.65/1.17	, revconsapp_1(9, 16) -> 3
3.65/1.17	, revconsapp_1(10, 15) -> 1
3.65/1.17	, revconsapp_1(10, 16) -> 3
3.65/1.17	, revconsapp_1(15, 16) -> 3
3.65/1.17	, revconsapp_1(19, 16) -> 6
3.65/1.17	, revconsapp_1(19, 16) -> 14
3.65/1.17	, revconsapp_1(20, 16) -> 6
3.65/1.17	, revconsapp_1(20, 16) -> 14
3.65/1.17	, revconsapp_2(2, 18) -> 3
3.65/1.17	, revconsapp_2(4, 18) -> 3
3.65/1.17	, revconsapp_2(5, 18) -> 3
3.65/1.17	, revconsapp_2(9, 18) -> 3
3.65/1.17	, revconsapp_2(10, 18) -> 3
3.65/1.17	, revconsapp_2(15, 18) -> 3
3.65/1.17	, revconsapp_2(17, 18) -> 6
3.65/1.17	, revconsapp_2(17, 18) -> 14
3.65/1.17	, revconsapp_2(19, 18) -> 6
3.65/1.17	, revconsapp_2(19, 18) -> 14
3.65/1.17	, revconsapp_2(20, 18) -> 6
3.65/1.17	, revconsapp_2(20, 18) -> 14
3.65/1.17	, revconsapp_3(17, 21) -> 6
3.65/1.17	, revconsapp_3(17, 21) -> 14
3.65/1.17	, revconsapp_3(19, 21) -> 6
3.65/1.17	, revconsapp_3(19, 21) -> 14
3.65/1.17	, C_0(2, 2) -> 1
3.65/1.17	, C_0(2, 2) -> 2
3.65/1.17	, C_0(2, 2) -> 3
3.65/1.17	, C_0(2, 2) -> 7
3.65/1.17	, C_0(2, 2) -> 13
3.65/1.17	, C_0(2, 4) -> 1
3.65/1.17	, C_0(2, 4) -> 2
3.65/1.17	, C_0(2, 4) -> 3
3.65/1.17	, C_0(2, 4) -> 7
3.65/1.17	, C_0(2, 4) -> 13
3.65/1.17	, C_0(2, 5) -> 1
3.65/1.17	, C_0(2, 5) -> 2
3.65/1.17	, C_0(2, 5) -> 3
3.65/1.17	, C_0(2, 5) -> 7
3.65/1.17	, C_0(2, 5) -> 13
3.65/1.17	, C_0(2, 9) -> 1
3.65/1.17	, C_0(2, 9) -> 2
3.65/1.17	, C_0(2, 9) -> 3
3.65/1.17	, C_0(2, 9) -> 7
3.65/1.17	, C_0(2, 9) -> 13
3.65/1.17	, C_0(2, 10) -> 1
3.65/1.17	, C_0(2, 10) -> 2
3.65/1.17	, C_0(2, 10) -> 3
3.65/1.17	, C_0(2, 10) -> 7
3.65/1.17	, C_0(2, 10) -> 13
3.65/1.17	, C_0(4, 2) -> 1
3.65/1.17	, C_0(4, 2) -> 2
3.65/1.17	, C_0(4, 2) -> 3
3.65/1.17	, C_0(4, 2) -> 7
3.65/1.17	, C_0(4, 2) -> 13
3.65/1.17	, C_0(4, 4) -> 1
3.65/1.17	, C_0(4, 4) -> 2
3.65/1.17	, C_0(4, 4) -> 3
3.65/1.17	, C_0(4, 4) -> 7
3.65/1.17	, C_0(4, 4) -> 13
3.65/1.17	, C_0(4, 5) -> 1
3.65/1.17	, C_0(4, 5) -> 2
3.65/1.17	, C_0(4, 5) -> 3
3.65/1.17	, C_0(4, 5) -> 7
3.65/1.17	, C_0(4, 5) -> 13
3.65/1.17	, C_0(4, 9) -> 1
3.65/1.17	, C_0(4, 9) -> 2
3.65/1.17	, C_0(4, 9) -> 3
3.65/1.17	, C_0(4, 9) -> 7
3.65/1.17	, C_0(4, 9) -> 13
3.65/1.17	, C_0(4, 10) -> 1
3.65/1.17	, C_0(4, 10) -> 2
3.65/1.17	, C_0(4, 10) -> 3
3.65/1.17	, C_0(4, 10) -> 7
3.65/1.17	, C_0(4, 10) -> 13
3.65/1.17	, C_0(5, 2) -> 1
3.65/1.17	, C_0(5, 2) -> 2
3.65/1.17	, C_0(5, 2) -> 3
3.65/1.17	, C_0(5, 2) -> 7
3.65/1.17	, C_0(5, 2) -> 13
3.65/1.17	, C_0(5, 4) -> 1
3.65/1.17	, C_0(5, 4) -> 2
3.65/1.17	, C_0(5, 4) -> 3
3.65/1.17	, C_0(5, 4) -> 7
3.65/1.17	, C_0(5, 4) -> 13
3.65/1.17	, C_0(5, 5) -> 1
3.65/1.17	, C_0(5, 5) -> 2
3.65/1.17	, C_0(5, 5) -> 3
3.65/1.17	, C_0(5, 5) -> 7
3.65/1.17	, C_0(5, 5) -> 13
3.65/1.17	, C_0(5, 9) -> 1
3.65/1.17	, C_0(5, 9) -> 2
3.65/1.17	, C_0(5, 9) -> 3
3.65/1.17	, C_0(5, 9) -> 7
3.65/1.17	, C_0(5, 9) -> 13
3.65/1.17	, C_0(5, 10) -> 1
3.65/1.17	, C_0(5, 10) -> 2
3.65/1.17	, C_0(5, 10) -> 3
3.65/1.17	, C_0(5, 10) -> 7
3.65/1.17	, C_0(5, 10) -> 13
3.65/1.17	, C_0(9, 2) -> 1
3.65/1.17	, C_0(9, 2) -> 2
3.65/1.17	, C_0(9, 2) -> 3
3.65/1.17	, C_0(9, 2) -> 7
3.65/1.17	, C_0(9, 2) -> 13
3.65/1.17	, C_0(9, 4) -> 1
3.65/1.17	, C_0(9, 4) -> 2
3.65/1.17	, C_0(9, 4) -> 3
3.65/1.17	, C_0(9, 4) -> 7
3.65/1.17	, C_0(9, 4) -> 13
3.65/1.17	, C_0(9, 5) -> 1
3.65/1.17	, C_0(9, 5) -> 2
3.65/1.17	, C_0(9, 5) -> 3
3.65/1.17	, C_0(9, 5) -> 7
3.65/1.17	, C_0(9, 5) -> 13
3.65/1.17	, C_0(9, 9) -> 1
3.65/1.17	, C_0(9, 9) -> 2
3.65/1.17	, C_0(9, 9) -> 3
3.65/1.17	, C_0(9, 9) -> 7
3.65/1.17	, C_0(9, 9) -> 13
3.65/1.17	, C_0(9, 10) -> 1
3.65/1.17	, C_0(9, 10) -> 2
3.65/1.17	, C_0(9, 10) -> 3
3.65/1.17	, C_0(9, 10) -> 7
3.65/1.17	, C_0(9, 10) -> 13
3.65/1.17	, C_0(10, 2) -> 1
3.65/1.17	, C_0(10, 2) -> 2
3.65/1.17	, C_0(10, 2) -> 3
3.65/1.17	, C_0(10, 2) -> 7
3.65/1.17	, C_0(10, 2) -> 13
3.65/1.17	, C_0(10, 4) -> 1
3.65/1.17	, C_0(10, 4) -> 2
3.65/1.17	, C_0(10, 4) -> 3
3.65/1.17	, C_0(10, 4) -> 7
3.65/1.17	, C_0(10, 4) -> 13
3.65/1.17	, C_0(10, 5) -> 1
3.65/1.17	, C_0(10, 5) -> 2
3.65/1.17	, C_0(10, 5) -> 3
3.65/1.17	, C_0(10, 5) -> 7
3.65/1.17	, C_0(10, 5) -> 13
3.65/1.17	, C_0(10, 9) -> 1
3.65/1.17	, C_0(10, 9) -> 2
3.65/1.17	, C_0(10, 9) -> 3
3.65/1.17	, C_0(10, 9) -> 7
3.65/1.17	, C_0(10, 9) -> 13
3.65/1.17	, C_0(10, 10) -> 1
3.65/1.17	, C_0(10, 10) -> 2
3.65/1.17	, C_0(10, 10) -> 3
3.65/1.17	, C_0(10, 10) -> 7
3.65/1.17	, C_0(10, 10) -> 13
3.65/1.17	, C_1(2, 2) -> 1
3.65/1.17	, C_1(2, 2) -> 3
3.65/1.17	, C_1(2, 2) -> 15
3.65/1.17	, C_1(2, 4) -> 1
3.65/1.17	, C_1(2, 4) -> 3
3.65/1.17	, C_1(2, 4) -> 15
3.65/1.17	, C_1(2, 5) -> 1
3.65/1.17	, C_1(2, 5) -> 3
3.65/1.17	, C_1(2, 5) -> 15
3.65/1.17	, C_1(2, 9) -> 1
3.65/1.17	, C_1(2, 9) -> 3
3.65/1.17	, C_1(2, 9) -> 15
3.65/1.17	, C_1(2, 10) -> 1
3.65/1.17	, C_1(2, 10) -> 3
3.65/1.17	, C_1(2, 10) -> 15
3.65/1.17	, C_1(2, 15) -> 1
3.65/1.17	, C_1(2, 15) -> 3
3.65/1.17	, C_1(2, 15) -> 15
3.65/1.17	, C_1(2, 16) -> 3
3.65/1.17	, C_1(2, 16) -> 16
3.65/1.17	, C_1(2, 18) -> 3
3.65/1.17	, C_1(2, 18) -> 16
3.65/1.17	, C_1(2, 19) -> 6
3.65/1.17	, C_1(2, 19) -> 14
3.65/1.17	, C_1(2, 19) -> 20
3.65/1.17	, C_1(2, 20) -> 6
3.65/1.17	, C_1(2, 20) -> 14
3.65/1.17	, C_1(2, 20) -> 20
3.65/1.17	, C_1(4, 2) -> 1
3.65/1.17	, C_1(4, 2) -> 3
3.65/1.17	, C_1(4, 2) -> 15
3.65/1.17	, C_1(4, 4) -> 1
3.65/1.17	, C_1(4, 4) -> 3
3.65/1.17	, C_1(4, 4) -> 15
3.65/1.17	, C_1(4, 5) -> 1
3.65/1.17	, C_1(4, 5) -> 3
3.65/1.17	, C_1(4, 5) -> 15
3.65/1.17	, C_1(4, 9) -> 1
3.65/1.17	, C_1(4, 9) -> 3
3.65/1.17	, C_1(4, 9) -> 15
3.65/1.17	, C_1(4, 10) -> 1
3.65/1.17	, C_1(4, 10) -> 3
3.65/1.17	, C_1(4, 10) -> 15
3.65/1.17	, C_1(4, 15) -> 1
3.65/1.17	, C_1(4, 15) -> 3
3.65/1.17	, C_1(4, 15) -> 15
3.65/1.17	, C_1(4, 16) -> 3
3.65/1.17	, C_1(4, 16) -> 16
3.65/1.17	, C_1(4, 18) -> 3
3.65/1.17	, C_1(4, 18) -> 16
3.65/1.17	, C_1(4, 19) -> 6
3.65/1.17	, C_1(4, 19) -> 14
3.65/1.17	, C_1(4, 19) -> 20
3.65/1.17	, C_1(4, 20) -> 6
3.65/1.17	, C_1(4, 20) -> 14
3.65/1.17	, C_1(4, 20) -> 20
3.65/1.17	, C_1(5, 2) -> 1
3.65/1.17	, C_1(5, 2) -> 3
3.65/1.17	, C_1(5, 2) -> 15
3.65/1.17	, C_1(5, 4) -> 1
3.65/1.17	, C_1(5, 4) -> 3
3.65/1.17	, C_1(5, 4) -> 15
3.65/1.17	, C_1(5, 5) -> 1
3.65/1.17	, C_1(5, 5) -> 3
3.65/1.17	, C_1(5, 5) -> 15
3.65/1.17	, C_1(5, 9) -> 1
3.65/1.17	, C_1(5, 9) -> 3
3.65/1.17	, C_1(5, 9) -> 15
3.65/1.17	, C_1(5, 10) -> 1
3.65/1.17	, C_1(5, 10) -> 3
3.65/1.17	, C_1(5, 10) -> 15
3.65/1.17	, C_1(5, 15) -> 1
3.65/1.17	, C_1(5, 15) -> 3
3.65/1.17	, C_1(5, 15) -> 15
3.65/1.17	, C_1(5, 16) -> 3
3.65/1.17	, C_1(5, 16) -> 16
3.65/1.17	, C_1(5, 18) -> 3
3.65/1.17	, C_1(5, 18) -> 16
3.65/1.17	, C_1(5, 19) -> 6
3.65/1.17	, C_1(5, 19) -> 14
3.65/1.17	, C_1(5, 19) -> 20
3.65/1.17	, C_1(5, 20) -> 6
3.65/1.17	, C_1(5, 20) -> 14
3.65/1.17	, C_1(5, 20) -> 20
3.65/1.17	, C_1(9, 2) -> 1
3.65/1.17	, C_1(9, 2) -> 3
3.65/1.17	, C_1(9, 2) -> 15
3.65/1.17	, C_1(9, 4) -> 1
3.65/1.17	, C_1(9, 4) -> 3
3.65/1.17	, C_1(9, 4) -> 15
3.65/1.17	, C_1(9, 5) -> 1
3.65/1.17	, C_1(9, 5) -> 3
3.65/1.17	, C_1(9, 5) -> 15
3.65/1.17	, C_1(9, 9) -> 1
3.65/1.17	, C_1(9, 9) -> 3
3.65/1.17	, C_1(9, 9) -> 15
3.65/1.17	, C_1(9, 10) -> 1
3.65/1.17	, C_1(9, 10) -> 3
3.65/1.17	, C_1(9, 10) -> 15
3.65/1.17	, C_1(9, 15) -> 1
3.65/1.17	, C_1(9, 15) -> 3
3.65/1.17	, C_1(9, 15) -> 15
3.65/1.17	, C_1(9, 16) -> 3
3.65/1.17	, C_1(9, 16) -> 16
3.65/1.17	, C_1(9, 18) -> 3
3.65/1.17	, C_1(9, 18) -> 16
3.65/1.17	, C_1(9, 19) -> 6
3.65/1.17	, C_1(9, 19) -> 14
3.65/1.17	, C_1(9, 19) -> 20
3.65/1.17	, C_1(9, 20) -> 6
3.65/1.17	, C_1(9, 20) -> 14
3.65/1.17	, C_1(9, 20) -> 20
3.65/1.17	, C_1(10, 2) -> 1
3.65/1.17	, C_1(10, 2) -> 3
3.65/1.17	, C_1(10, 2) -> 15
3.65/1.17	, C_1(10, 4) -> 1
3.65/1.17	, C_1(10, 4) -> 3
3.65/1.17	, C_1(10, 4) -> 15
3.65/1.17	, C_1(10, 5) -> 1
3.65/1.17	, C_1(10, 5) -> 3
3.65/1.17	, C_1(10, 5) -> 15
3.65/1.17	, C_1(10, 9) -> 1
3.65/1.17	, C_1(10, 9) -> 3
3.65/1.17	, C_1(10, 9) -> 15
3.65/1.17	, C_1(10, 10) -> 1
3.65/1.17	, C_1(10, 10) -> 3
3.65/1.17	, C_1(10, 10) -> 15
3.65/1.17	, C_1(10, 15) -> 1
3.65/1.17	, C_1(10, 15) -> 3
3.65/1.17	, C_1(10, 15) -> 15
3.65/1.17	, C_1(10, 16) -> 3
3.65/1.17	, C_1(10, 16) -> 16
3.65/1.17	, C_1(10, 18) -> 3
3.65/1.17	, C_1(10, 18) -> 16
3.65/1.17	, C_1(10, 19) -> 6
3.65/1.17	, C_1(10, 19) -> 14
3.65/1.17	, C_1(10, 19) -> 20
3.65/1.17	, C_1(10, 20) -> 6
3.65/1.17	, C_1(10, 20) -> 14
3.65/1.17	, C_1(10, 20) -> 20
3.65/1.17	, C_2(2, 16) -> 3
3.65/1.17	, C_2(2, 16) -> 6
3.65/1.17	, C_2(2, 16) -> 14
3.65/1.17	, C_2(2, 16) -> 18
3.65/1.17	, C_2(2, 17) -> 6
3.65/1.17	, C_2(2, 17) -> 14
3.65/1.17	, C_2(2, 17) -> 19
3.65/1.17	, C_2(2, 18) -> 3
3.65/1.17	, C_2(2, 18) -> 6
3.65/1.17	, C_2(2, 18) -> 14
3.65/1.17	, C_2(2, 18) -> 18
3.65/1.17	, C_2(2, 19) -> 6
3.65/1.17	, C_2(2, 19) -> 14
3.65/1.17	, C_2(2, 19) -> 19
3.65/1.17	, C_2(4, 16) -> 3
3.65/1.17	, C_2(4, 16) -> 6
3.65/1.17	, C_2(4, 16) -> 14
3.65/1.17	, C_2(4, 16) -> 18
3.65/1.17	, C_2(4, 17) -> 6
3.65/1.17	, C_2(4, 17) -> 14
3.65/1.17	, C_2(4, 17) -> 19
3.65/1.17	, C_2(4, 18) -> 3
3.65/1.17	, C_2(4, 18) -> 6
3.65/1.17	, C_2(4, 18) -> 14
3.65/1.17	, C_2(4, 18) -> 18
3.65/1.17	, C_2(4, 19) -> 6
3.65/1.17	, C_2(4, 19) -> 14
3.65/1.17	, C_2(4, 19) -> 19
3.65/1.17	, C_2(5, 16) -> 3
3.65/1.17	, C_2(5, 16) -> 6
3.65/1.17	, C_2(5, 16) -> 14
3.65/1.17	, C_2(5, 16) -> 18
3.65/1.17	, C_2(5, 17) -> 6
3.65/1.17	, C_2(5, 17) -> 14
3.65/1.17	, C_2(5, 17) -> 19
3.65/1.17	, C_2(5, 18) -> 3
3.65/1.17	, C_2(5, 18) -> 6
3.65/1.17	, C_2(5, 18) -> 14
3.65/1.17	, C_2(5, 18) -> 18
3.65/1.17	, C_2(5, 19) -> 6
3.65/1.17	, C_2(5, 19) -> 14
3.65/1.17	, C_2(5, 19) -> 19
3.65/1.17	, C_2(9, 16) -> 3
3.65/1.17	, C_2(9, 16) -> 6
3.65/1.17	, C_2(9, 16) -> 14
3.65/1.17	, C_2(9, 16) -> 18
3.65/1.17	, C_2(9, 17) -> 6
3.65/1.17	, C_2(9, 17) -> 14
3.65/1.17	, C_2(9, 17) -> 19
3.65/1.17	, C_2(9, 18) -> 3
3.65/1.17	, C_2(9, 18) -> 6
3.65/1.17	, C_2(9, 18) -> 14
3.65/1.17	, C_2(9, 18) -> 18
3.65/1.17	, C_2(9, 19) -> 6
3.65/1.17	, C_2(9, 19) -> 14
3.65/1.17	, C_2(9, 19) -> 19
3.65/1.17	, C_2(10, 16) -> 3
3.65/1.17	, C_2(10, 16) -> 6
3.65/1.17	, C_2(10, 16) -> 14
3.65/1.17	, C_2(10, 16) -> 18
3.65/1.17	, C_2(10, 17) -> 6
3.65/1.17	, C_2(10, 17) -> 14
3.65/1.17	, C_2(10, 17) -> 19
3.65/1.17	, C_2(10, 18) -> 3
3.65/1.17	, C_2(10, 18) -> 6
3.65/1.17	, C_2(10, 18) -> 14
3.65/1.17	, C_2(10, 18) -> 18
3.65/1.17	, C_2(10, 19) -> 6
3.65/1.17	, C_2(10, 19) -> 14
3.65/1.17	, C_2(10, 19) -> 19
3.65/1.17	, C_3(2, 18) -> 6
3.65/1.17	, C_3(2, 18) -> 14
3.65/1.17	, C_3(2, 18) -> 21
3.65/1.17	, C_3(2, 21) -> 6
3.65/1.17	, C_3(2, 21) -> 14
3.65/1.17	, C_3(2, 21) -> 21
3.65/1.17	, C_3(4, 18) -> 6
3.65/1.17	, C_3(4, 18) -> 14
3.65/1.17	, C_3(4, 18) -> 21
3.65/1.17	, C_3(4, 21) -> 6
3.65/1.17	, C_3(4, 21) -> 14
3.65/1.17	, C_3(4, 21) -> 21
3.65/1.17	, C_3(5, 18) -> 6
3.65/1.17	, C_3(5, 18) -> 14
3.65/1.17	, C_3(5, 18) -> 21
3.65/1.17	, C_3(5, 21) -> 6
3.65/1.17	, C_3(5, 21) -> 14
3.65/1.17	, C_3(5, 21) -> 21
3.65/1.17	, C_3(9, 18) -> 6
3.65/1.17	, C_3(9, 18) -> 14
3.65/1.17	, C_3(9, 18) -> 21
3.65/1.17	, C_3(9, 21) -> 6
3.65/1.17	, C_3(9, 21) -> 14
3.65/1.17	, C_3(9, 21) -> 21
3.65/1.17	, C_3(10, 18) -> 6
3.65/1.17	, C_3(10, 18) -> 14
3.65/1.17	, C_3(10, 18) -> 21
3.65/1.17	, C_3(10, 21) -> 6
3.65/1.17	, C_3(10, 21) -> 14
3.65/1.17	, C_3(10, 21) -> 21
3.65/1.17	, deeprevapp_0(2, 2) -> 3
3.65/1.17	, deeprevapp_0(2, 4) -> 3
3.65/1.17	, deeprevapp_0(2, 5) -> 3
3.65/1.17	, deeprevapp_0(2, 9) -> 3
3.65/1.17	, deeprevapp_0(2, 10) -> 3
3.65/1.17	, deeprevapp_0(4, 2) -> 3
3.65/1.17	, deeprevapp_0(4, 4) -> 3
3.65/1.17	, deeprevapp_0(4, 5) -> 3
3.65/1.17	, deeprevapp_0(4, 9) -> 3
3.65/1.17	, deeprevapp_0(4, 10) -> 3
3.65/1.17	, deeprevapp_0(5, 2) -> 3
3.65/1.17	, deeprevapp_0(5, 4) -> 3
3.65/1.17	, deeprevapp_0(5, 5) -> 3
3.65/1.17	, deeprevapp_0(5, 9) -> 3
3.65/1.17	, deeprevapp_0(5, 10) -> 3
3.65/1.17	, deeprevapp_0(9, 2) -> 3
3.65/1.17	, deeprevapp_0(9, 4) -> 3
3.65/1.17	, deeprevapp_0(9, 5) -> 3
3.65/1.17	, deeprevapp_0(9, 9) -> 3
3.65/1.17	, deeprevapp_0(9, 10) -> 3
3.65/1.17	, deeprevapp_0(10, 2) -> 3
3.65/1.17	, deeprevapp_0(10, 4) -> 3
3.65/1.17	, deeprevapp_0(10, 5) -> 3
3.65/1.17	, deeprevapp_0(10, 9) -> 3
3.65/1.17	, deeprevapp_0(10, 10) -> 3
3.65/1.17	, deeprevapp_1(2, 15) -> 3
3.65/1.17	, deeprevapp_1(2, 20) -> 6
3.65/1.17	, deeprevapp_1(2, 20) -> 14
3.65/1.17	, deeprevapp_1(4, 15) -> 3
3.65/1.17	, deeprevapp_1(4, 20) -> 6
3.65/1.17	, deeprevapp_1(4, 20) -> 14
3.65/1.17	, deeprevapp_1(5, 15) -> 3
3.65/1.17	, deeprevapp_1(5, 20) -> 6
3.65/1.17	, deeprevapp_1(5, 20) -> 14
3.65/1.17	, deeprevapp_1(9, 15) -> 3
3.65/1.17	, deeprevapp_1(9, 20) -> 6
3.65/1.17	, deeprevapp_1(9, 20) -> 14
3.65/1.17	, deeprevapp_1(10, 15) -> 3
3.65/1.17	, deeprevapp_1(10, 20) -> 6
3.65/1.17	, deeprevapp_1(10, 20) -> 14
3.65/1.17	, deeprevapp_1(15, 17) -> 6
3.65/1.17	, deeprevapp_1(15, 17) -> 14
3.65/1.17	, deeprevapp_2(2, 19) -> 6
3.65/1.17	, deeprevapp_2(2, 19) -> 14
3.65/1.17	, deeprevapp_2(4, 19) -> 6
3.65/1.17	, deeprevapp_2(4, 19) -> 14
3.65/1.17	, deeprevapp_2(5, 19) -> 6
3.65/1.17	, deeprevapp_2(5, 19) -> 14
3.65/1.17	, deeprevapp_2(9, 19) -> 6
3.65/1.17	, deeprevapp_2(9, 19) -> 14
3.65/1.17	, deeprevapp_2(10, 19) -> 6
3.65/1.17	, deeprevapp_2(10, 19) -> 14
3.65/1.17	, deeprevapp_2(15, 19) -> 6
3.65/1.17	, deeprevapp_2(15, 19) -> 14
3.65/1.17	, V_0(2) -> 1
3.65/1.17	, V_0(2) -> 3
3.65/1.17	, V_0(2) -> 4
3.65/1.17	, V_0(2) -> 7
3.65/1.17	, V_0(2) -> 13
3.65/1.17	, V_0(4) -> 1
3.65/1.17	, V_0(4) -> 3
3.65/1.17	, V_0(4) -> 4
3.65/1.17	, V_0(4) -> 7
3.65/1.17	, V_0(4) -> 13
3.65/1.17	, V_0(5) -> 1
3.65/1.17	, V_0(5) -> 3
3.65/1.17	, V_0(5) -> 4
3.65/1.17	, V_0(5) -> 7
3.65/1.17	, V_0(5) -> 13
3.65/1.17	, V_0(9) -> 1
3.65/1.17	, V_0(9) -> 3
3.65/1.17	, V_0(9) -> 4
3.65/1.17	, V_0(9) -> 7
3.65/1.17	, V_0(9) -> 13
3.65/1.17	, V_0(10) -> 1
3.65/1.17	, V_0(10) -> 3
3.65/1.17	, V_0(10) -> 4
3.65/1.17	, V_0(10) -> 7
3.65/1.17	, V_0(10) -> 13
3.65/1.17	, V_1(2) -> 3
3.65/1.17	, V_1(2) -> 6
3.65/1.17	, V_1(2) -> 14
3.65/1.17	, V_1(2) -> 16
3.65/1.17	, V_1(4) -> 3
3.65/1.17	, V_1(4) -> 6
3.65/1.17	, V_1(4) -> 14
3.65/1.17	, V_1(4) -> 16
3.65/1.17	, V_1(5) -> 3
3.65/1.17	, V_1(5) -> 6
3.65/1.17	, V_1(5) -> 14
3.65/1.17	, V_1(5) -> 16
3.65/1.17	, V_1(9) -> 3
3.65/1.17	, V_1(9) -> 6
3.65/1.17	, V_1(9) -> 14
3.65/1.17	, V_1(9) -> 16
3.65/1.18	, V_1(10) -> 3
3.65/1.18	, V_1(10) -> 6
3.65/1.18	, V_1(10) -> 14
3.65/1.18	, V_1(10) -> 16
3.65/1.18	, N_0() -> 1
3.65/1.18	, N_0() -> 3
3.65/1.18	, N_0() -> 5
3.65/1.18	, N_0() -> 7
3.65/1.18	, N_0() -> 13
3.65/1.18	, N_1() -> 6
3.65/1.18	, N_1() -> 7
3.65/1.18	, N_1() -> 13
3.65/1.18	, N_1() -> 14
3.65/1.18	, N_1() -> 17
3.65/1.18	, deeprev_0(2) -> 6
3.65/1.18	, deeprev_0(4) -> 6
3.65/1.18	, deeprev_0(5) -> 6
3.65/1.18	, deeprev_0(9) -> 6
3.65/1.18	, deeprev_0(10) -> 6
3.65/1.18	, deeprev_1(2) -> 14
3.65/1.18	, deeprev_1(4) -> 14
3.65/1.18	, deeprev_1(5) -> 14
3.65/1.18	, deeprev_1(9) -> 14
3.65/1.18	, deeprev_1(10) -> 14
3.65/1.18	, second_0(2) -> 7
3.65/1.18	, second_0(4) -> 7
3.65/1.18	, second_0(5) -> 7
3.65/1.18	, second_0(9) -> 7
3.65/1.18	, second_0(10) -> 7
3.65/1.18	, isVal_0(2) -> 8
3.65/1.18	, isVal_0(4) -> 8
3.65/1.18	, isVal_0(5) -> 8
3.65/1.18	, isVal_0(9) -> 8
3.65/1.18	, isVal_0(10) -> 8
3.65/1.18	, False_0() -> 1
3.65/1.18	, False_0() -> 3
3.65/1.18	, False_0() -> 7
3.65/1.18	, False_0() -> 9
3.65/1.18	, False_0() -> 13
3.65/1.18	, False_1() -> 8
3.65/1.18	, False_1() -> 11
3.65/1.18	, False_1() -> 12
3.65/1.18	, True_0() -> 1
3.65/1.18	, True_0() -> 3
3.65/1.18	, True_0() -> 7
3.65/1.18	, True_0() -> 10
3.65/1.18	, True_0() -> 13
3.65/1.18	, True_1() -> 8
3.65/1.18	, True_1() -> 11
3.65/1.18	, True_1() -> 12
3.65/1.18	, isNotEmptyT_0(2) -> 11
3.65/1.18	, isNotEmptyT_0(4) -> 11
3.65/1.18	, isNotEmptyT_0(5) -> 11
3.65/1.18	, isNotEmptyT_0(9) -> 11
3.65/1.18	, isNotEmptyT_0(10) -> 11
3.65/1.18	, isEmptyT_0(2) -> 12
3.65/1.18	, isEmptyT_0(4) -> 12
3.65/1.18	, isEmptyT_0(5) -> 12
3.65/1.18	, isEmptyT_0(9) -> 12
3.65/1.18	, isEmptyT_0(10) -> 12
3.65/1.18	, first_0(2) -> 13
3.65/1.18	, first_0(4) -> 13
3.65/1.18	, first_0(5) -> 13
3.65/1.18	, first_0(9) -> 13
3.65/1.18	, first_0(10) -> 13
3.65/1.18	, goal_0(2) -> 14
3.65/1.18	, goal_0(4) -> 14
3.65/1.18	, goal_0(5) -> 14
3.65/1.18	, goal_0(9) -> 14
3.65/1.18	, goal_0(10) -> 14 }
3.65/1.18	
3.65/1.18	Hurray, we answered YES(?,O(n^1))
3.65/1.18	EOF