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