YES(?,O(n^1))
1109.66/297.03	YES(?,O(n^1))
1109.66/297.03	
1109.66/297.03	We are left with following problem, upon which TcT provides the
1109.66/297.03	certificate YES(?,O(n^1)).
1109.66/297.03	
1109.66/297.03	Strict Trs:
1109.66/297.03	  { b(b(a(b(b(a(b(b(b(b(b(b(a(b(x1)))))))))))))) ->
1109.66/297.03	    b(b(b(b(b(a(b(b(a(b(b(a(b(b(b(b(b(b(x1)))))))))))))))))) }
1109.66/297.03	Obligation:
1109.66/297.03	  derivational complexity
1109.66/297.03	Answer:
1109.66/297.03	  YES(?,O(n^1))
1109.66/297.03	
1109.66/297.03	The problem is match-bounded by 1. The enriched problem is
1109.66/297.03	compatible with the following automaton.
1109.66/297.03	{ b_0(1) -> 1
1109.66/297.03	, b_1(1) -> 18
1109.66/297.03	, b_1(2) -> 1
1109.66/297.03	, b_1(2) -> 7
1109.66/297.03	, b_1(2) -> 17
1109.66/297.03	, b_1(2) -> 18
1109.66/297.03	, b_1(3) -> 2
1109.66/297.03	, b_1(4) -> 3
1109.66/297.03	, b_1(5) -> 4
1109.66/297.03	, b_1(6) -> 5
1109.66/297.03	, b_1(7) -> 17
1109.66/297.03	, b_1(8) -> 7
1109.66/297.03	, b_1(9) -> 8
1109.66/297.03	, b_1(11) -> 10
1109.66/297.03	, b_1(12) -> 11
1109.66/297.03	, b_1(14) -> 13
1109.66/297.03	, b_1(15) -> 14
1109.66/297.03	, b_1(16) -> 15
1109.66/297.03	, b_1(17) -> 16
1109.66/297.03	, b_1(18) -> 17
1109.66/297.03	, a_0(1) -> 1
1109.66/297.03	, a_1(7) -> 6
1109.66/297.03	, a_1(10) -> 9
1109.66/297.03	, a_1(13) -> 12 }
1109.66/297.03	
1109.66/297.03	Hurray, we answered YES(?,O(n^1))
1110.21/297.59	EOF