YES(?,O(n^1))
734.74/297.10	YES(?,O(n^1))
734.74/297.10	
734.74/297.10	We are left with following problem, upon which TcT provides the
734.74/297.10	certificate YES(?,O(n^1)).
734.74/297.10	
734.74/297.10	Strict Trs:
734.74/297.10	  { f(x, f(a(), a())) -> f(f(f(f(a(), a()), a()), x), a()) }
734.74/297.10	Obligation:
734.74/297.10	  derivational complexity
734.74/297.10	Answer:
734.74/297.10	  YES(?,O(n^1))
734.74/297.10	
734.74/297.10	The problem is match-bounded by 1. The enriched problem is
734.74/297.10	compatible with the following automaton.
734.74/297.10	{ f_0(1, 1) -> 1
734.74/297.10	, f_1(2, 3) -> 1
734.74/297.10	, f_1(4, 1) -> 2
734.74/297.10	, f_1(4, 4) -> 9
734.74/297.10	, f_1(5, 6) -> 4
734.74/297.10	, f_1(7, 8) -> 5
734.74/297.10	, f_1(9, 8) -> 2
734.74/297.10	, a_0() -> 1
734.74/297.10	, a_1() -> 3
734.74/297.10	, a_1() -> 6
734.74/297.10	, a_1() -> 7
734.74/297.10	, a_1() -> 8 }
734.74/297.10	
734.74/297.10	Hurray, we answered YES(?,O(n^1))
734.74/297.18	EOF