YES(?,O(n^1))
1128.53/297.05	YES(?,O(n^1))
1128.53/297.05	
1128.53/297.05	We are left with following problem, upon which TcT provides the
1128.53/297.05	certificate YES(?,O(n^1)).
1128.53/297.05	
1128.53/297.05	Strict Trs:
1128.53/297.05	  { a(b(a(a(x1)))) -> c(b(a(b(a(x1)))))
1128.53/297.05	  , a(c(b(x1))) -> a(a(b(c(b(a(x1)))))) }
1128.53/297.05	Obligation:
1128.53/297.05	  derivational complexity
1128.53/297.05	Answer:
1128.53/297.05	  YES(?,O(n^1))
1128.53/297.05	
1128.53/297.05	The problem is match-bounded by 3. The enriched problem is
1128.53/297.05	compatible with the following automaton.
1128.53/297.05	{ a_0(1) -> 1
1128.53/297.05	, a_1(1) -> 5
1128.53/297.05	, a_1(3) -> 5
1128.53/297.05	, a_1(4) -> 3
1128.53/297.05	, a_1(6) -> 1
1128.53/297.05	, a_1(6) -> 5
1128.53/297.05	, a_1(7) -> 6
1128.53/297.05	, a_2(3) -> 13
1128.53/297.05	, a_2(4) -> 17
1128.53/297.05	, a_2(6) -> 17
1128.53/297.05	, a_2(7) -> 17
1128.53/297.05	, a_2(9) -> 5
1128.53/297.05	, a_2(9) -> 13
1128.53/297.05	, a_2(10) -> 9
1128.53/297.05	, a_2(15) -> 13
1128.53/297.05	, a_2(16) -> 15
1128.53/297.05	, a_3(15) -> 22
1128.53/297.05	, a_3(18) -> 13
1128.53/297.05	, a_3(18) -> 22
1128.53/297.05	, a_3(19) -> 18
1128.53/297.05	, b_0(1) -> 1
1128.53/297.05	, b_1(3) -> 2
1128.53/297.05	, b_1(5) -> 4
1128.53/297.05	, b_1(6) -> 4
1128.53/297.05	, b_1(8) -> 7
1128.53/297.05	, b_2(9) -> 16
1128.53/297.05	, b_2(11) -> 10
1128.53/297.05	, b_2(13) -> 12
1128.53/297.05	, b_2(15) -> 14
1128.53/297.05	, b_2(17) -> 16
1128.53/297.05	, b_3(20) -> 19
1128.53/297.05	, b_3(22) -> 21
1128.53/297.05	, c_0(1) -> 1
1128.53/297.05	, c_1(2) -> 1
1128.53/297.05	, c_1(2) -> 3
1128.53/297.05	, c_1(2) -> 5
1128.53/297.05	, c_1(2) -> 17
1128.53/297.05	, c_1(4) -> 8
1128.53/297.05	, c_2(12) -> 11
1128.53/297.05	, c_2(14) -> 3
1128.53/297.05	, c_2(14) -> 15
1128.53/297.05	, c_2(14) -> 17
1128.53/297.05	, c_3(21) -> 20 }
1128.53/297.05	
1128.53/297.05	Hurray, we answered YES(?,O(n^1))
1128.89/297.35	EOF