YES(?,O(n^1))
700.68/263.29	YES(?,O(n^1))
700.68/263.29	
700.68/263.29	We are left with following problem, upon which TcT provides the
700.68/263.29	certificate YES(?,O(n^1)).
700.68/263.29	
700.68/263.29	Strict Trs:
700.68/263.29	  { b(b(0(), y), x) -> y
700.68/263.29	  , c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0())))
700.68/263.29	  , a(y, 0()) -> b(y, 0()) }
700.68/263.29	Obligation:
700.68/263.29	  derivational complexity
700.68/263.29	Answer:
700.68/263.29	  YES(?,O(n^1))
700.68/263.29	
700.68/263.29	The problem is match-bounded by 2. The enriched problem is
700.68/263.29	compatible with the following automaton.
700.68/263.29	{ b_0(1, 1) -> 1
700.68/263.29	, b_1(1, 9) -> 1
700.68/263.29	, b_1(9, 1) -> 8
700.68/263.29	, b_1(9, 2) -> 8
700.68/263.29	, b_1(9, 3) -> 8
700.68/263.29	, b_2(4, 10) -> 3
700.68/263.29	, b_2(6, 10) -> 4
700.68/263.29	, 0_0() -> 1
700.68/263.29	, 0_1() -> 1
700.68/263.29	, 0_1() -> 5
700.68/263.29	, 0_1() -> 7
700.68/263.29	, 0_1() -> 9
700.68/263.29	, 0_2() -> 10
700.68/263.29	, c_0(1) -> 1
700.68/263.29	, c_1(2) -> 1
700.68/263.29	, c_1(3) -> 2
700.68/263.29	, c_1(8) -> 6
700.68/263.29	, a_0(1, 1) -> 1
700.68/263.29	, a_1(4, 5) -> 3
700.68/263.29	, a_1(6, 7) -> 4 }
700.68/263.29	
700.68/263.29	Hurray, we answered YES(?,O(n^1))
701.05/263.32	EOF