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