YES(?,O(n^1))
11.73/4.94	YES(?,O(n^1))
11.73/4.94	
11.73/4.94	We are left with following problem, upon which TcT provides the
11.73/4.94	certificate YES(?,O(n^1)).
11.73/4.94	
11.73/4.94	Strict Trs:
11.73/4.94	  { a(x, y) -> b(x, b(0(), c(y)))
11.73/4.94	  , b(y, 0()) -> y
11.73/4.94	  , c(b(y, c(x))) -> c(c(b(a(0(), 0()), y))) }
11.73/4.94	Obligation:
11.73/4.94	  derivational complexity
11.73/4.94	Answer:
11.73/4.94	  YES(?,O(n^1))
11.73/4.94	
11.73/4.94	The problem is match-bounded by 3. The enriched problem is
11.73/4.94	compatible with the following automaton.
11.73/4.94	{ a_0(1, 1) -> 1
11.73/4.94	, a_1(3, 3) -> 6
11.73/4.94	, a_1(3, 3) -> 7
11.73/4.94	, a_2(9, 9) -> 14
11.73/4.94	, b_0(1, 1) -> 1
11.73/4.94	, b_1(1, 2) -> 1
11.73/4.94	, b_1(3, 4) -> 2
11.73/4.94	, b_1(7, 1) -> 6
11.73/4.94	, b_1(7, 7) -> 11
11.73/4.94	, b_2(3, 8) -> 6
11.73/4.94	, b_2(3, 8) -> 7
11.73/4.94	, b_2(9, 10) -> 8
11.73/4.94	, b_2(14, 7) -> 13
11.73/4.94	, b_3(9, 15) -> 14
11.73/4.94	, b_3(16, 17) -> 15
11.73/4.94	, 0_0() -> 1
11.73/4.94	, 0_1() -> 3
11.73/4.94	, 0_2() -> 9
11.73/4.94	, 0_3() -> 16
11.73/4.94	, c_0(1) -> 1
11.73/4.94	, c_1(1) -> 4
11.73/4.94	, c_1(5) -> 1
11.73/4.94	, c_1(5) -> 4
11.73/4.94	, c_1(6) -> 5
11.73/4.94	, c_1(11) -> 6
11.73/4.94	, c_2(3) -> 10
11.73/4.94	, c_2(12) -> 5
11.73/4.94	, c_2(13) -> 12
11.73/4.94	, c_3(9) -> 17 }
11.73/4.94	
11.73/4.94	Hurray, we answered YES(?,O(n^1))
11.73/4.95	EOF