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