YES(?,O(n^1))
133.62/75.86	YES(?,O(n^1))
133.62/75.86	
133.62/75.86	We are left with following problem, upon which TcT provides the
133.62/75.86	certificate YES(?,O(n^1)).
133.62/75.86	
133.62/75.86	Strict Trs:
133.62/75.86	  { c(X) -> e()
133.62/75.86	  , c(b(a(X))) -> a(a(b(b(c(c(X))))))
133.62/75.86	  , b(X) -> e()
133.62/75.86	  , a(X) -> e() }
133.62/75.86	Obligation:
133.62/75.86	  derivational complexity
133.62/75.86	Answer:
133.62/75.86	  YES(?,O(n^1))
133.62/75.86	
133.62/75.86	The problem is match-bounded by 2. The enriched problem is
133.62/75.86	compatible with the following automaton.
133.62/75.86	{ c_0(1) -> 1
133.62/75.86	, c_0(2) -> 1
133.62/75.86	, c_0(3) -> 1
133.62/75.86	, c_0(4) -> 1
133.62/75.86	, c_1(1) -> 9
133.62/75.86	, c_1(2) -> 9
133.62/75.86	, c_1(3) -> 9
133.62/75.86	, c_1(4) -> 9
133.62/75.86	, c_1(5) -> 9
133.62/75.86	, c_1(9) -> 8
133.62/75.86	, b_0(1) -> 2
133.62/75.86	, b_0(2) -> 2
133.62/75.86	, b_0(3) -> 2
133.62/75.86	, b_0(4) -> 2
133.62/75.86	, b_1(7) -> 6
133.62/75.86	, b_1(8) -> 7
133.62/75.86	, a_0(1) -> 3
133.62/75.86	, a_0(2) -> 3
133.62/75.86	, a_0(3) -> 3
133.62/75.86	, a_0(4) -> 3
133.62/75.86	, a_1(5) -> 1
133.62/75.86	, a_1(5) -> 9
133.62/75.86	, a_1(6) -> 5
133.62/75.86	, e_0() -> 4
133.62/75.86	, e_1() -> 1
133.62/75.86	, e_1() -> 2
133.62/75.86	, e_1() -> 3
133.62/75.86	, e_2() -> 1
133.62/75.86	, e_2() -> 5
133.62/75.86	, e_2() -> 6
133.62/75.86	, e_2() -> 7
133.62/75.86	, e_2() -> 8
133.62/75.86	, e_2() -> 9 }
133.62/75.86	
133.62/75.86	Hurray, we answered YES(?,O(n^1))
133.95/75.94	EOF