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