YES(?,O(n^1))
9.94/5.41	YES(?,O(n^1))
9.94/5.41	
9.94/5.41	We are left with following problem, upon which TcT provides the
9.94/5.41	certificate YES(?,O(n^1)).
9.94/5.41	
9.94/5.41	Strict Trs:
9.94/5.41	  { f(x, f(f(a(), a()), a())) -> f(f(a(), f(a(), a())), x) }
9.94/5.41	Obligation:
9.94/5.41	  derivational complexity
9.94/5.41	Answer:
9.94/5.41	  YES(?,O(n^1))
9.94/5.41	
9.94/5.41	TcT has computed the following matrix interpretation satisfying
9.94/5.41	not(EDA) and not(IDA(1)).
9.94/5.41	
9.94/5.41	                [1 0 0 1]      [1 0 0 0]      [0]
9.94/5.41	  [f](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
9.94/5.41	                [0 0 0 0]      [0 0 0 0]      [0]
9.94/5.41	                [0 1 0 0]      [0 1 0 0]      [0]
9.94/5.41	                                                 
9.94/5.41	                [0]                              
9.94/5.41	          [a] = [1]                              
9.94/5.41	                [0]                              
9.94/5.41	                [0]                              
9.94/5.41	
9.94/5.41	The order satisfies the following ordering constraints:
9.94/5.41	
9.94/5.41	  [f(x, f(f(a(), a()), a()))] = [1 0 0 1]     [2]          
9.94/5.41	                                [0 0 0 0] x + [0]          
9.94/5.41	                                [0 0 0 0]     [0]          
9.94/5.41	                                [0 1 0 0]     [0]          
9.94/5.41	                              > [1 0 0 0]     [1]          
9.94/5.41	                                [0 0 0 0] x + [0]          
9.94/5.41	                                [0 0 0 0]     [0]          
9.94/5.41	                                [0 1 0 0]     [0]          
9.94/5.41	                              = [f(f(a(), f(a(), a())), x)]
9.94/5.41	                                                           
9.94/5.41	
9.94/5.41	Hurray, we answered YES(?,O(n^1))
9.94/5.42	EOF