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