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