YES(?,O(n^1))
0.16/0.33	YES(?,O(n^1))
0.16/0.33	
0.16/0.33	Problem:
0.16/0.33	 a(a(x1)) -> b(c(x1))
0.16/0.33	 b(b(x1)) -> c(d(x1))
0.16/0.33	 c(c(x1)) -> d(d(d(x1)))
0.16/0.33	 d(d(d(x1))) -> a(c(x1))
0.16/0.33	
0.16/0.33	Proof:
0.16/0.33	 Complexity Transformation Processor:
0.16/0.33	  strict:
0.16/0.33	   a(a(x1)) -> b(c(x1))
0.16/0.33	   b(b(x1)) -> c(d(x1))
0.16/0.33	   c(c(x1)) -> d(d(d(x1)))
0.16/0.33	   d(d(d(x1))) -> a(c(x1))
0.16/0.33	  weak:
0.16/0.33	   
0.16/0.33	  Matrix Interpretation Processor: dim=1
0.16/0.33	   
0.16/0.33	   max_matrix:
0.16/0.33	    1
0.16/0.33	   interpretation:
0.16/0.33	    [d](x0) = x0 + 8,
0.16/0.33	    
0.16/0.33	    [b](x0) = x0,
0.16/0.33	    
0.16/0.33	    [c](x0) = x0 + 72,
0.16/0.33	    
0.16/0.33	    [a](x0) = x0 + 132
0.16/0.33	   orientation:
0.16/0.33	    a(a(x1)) = x1 + 264 >= x1 + 72 = b(c(x1))
0.16/0.33	    
0.16/0.33	    b(b(x1)) = x1 >= x1 + 80 = c(d(x1))
0.16/0.33	    
0.16/0.33	    c(c(x1)) = x1 + 144 >= x1 + 24 = d(d(d(x1)))
0.16/0.33	    
0.16/0.33	    d(d(d(x1))) = x1 + 24 >= x1 + 204 = a(c(x1))
0.16/0.33	   problem:
0.16/0.33	    strict:
0.16/0.33	     b(b(x1)) -> c(d(x1))
0.16/0.33	     d(d(d(x1))) -> a(c(x1))
0.16/0.33	    weak:
0.16/0.33	     a(a(x1)) -> b(c(x1))
0.16/0.33	     c(c(x1)) -> d(d(d(x1)))
0.16/0.33	   Matrix Interpretation Processor: dim=1
0.16/0.33	    
0.16/0.33	    max_matrix:
0.16/0.33	     1
0.16/0.33	    interpretation:
0.16/0.33	     [d](x0) = x0 + 2,
0.16/0.33	     
0.16/0.33	     [b](x0) = x0 + 132,
0.16/0.33	     
0.16/0.33	     [c](x0) = x0 + 36,
0.16/0.33	     
0.16/0.33	     [a](x0) = x0 + 144
0.16/0.33	    orientation:
0.16/0.33	     b(b(x1)) = x1 + 264 >= x1 + 38 = c(d(x1))
0.16/0.33	     
0.16/0.33	     d(d(d(x1))) = x1 + 6 >= x1 + 180 = a(c(x1))
0.16/0.33	     
0.16/0.33	     a(a(x1)) = x1 + 288 >= x1 + 168 = b(c(x1))
0.16/0.33	     
0.16/0.33	     c(c(x1)) = x1 + 72 >= x1 + 6 = d(d(d(x1)))
0.16/0.33	    problem:
0.16/0.33	     strict:
0.16/0.33	      d(d(d(x1))) -> a(c(x1))
0.16/0.33	     weak:
0.16/0.33	      b(b(x1)) -> c(d(x1))
0.16/0.33	      a(a(x1)) -> b(c(x1))
0.16/0.33	      c(c(x1)) -> d(d(d(x1)))
0.16/0.33	    Matrix Interpretation Processor: dim=1
0.16/0.33	     
0.16/0.33	     max_matrix:
0.16/0.33	      1
0.16/0.33	     interpretation:
0.16/0.33	      [d](x0) = x0 + 8,
0.16/0.33	      
0.16/0.33	      [b](x0) = x0 + 10,
0.16/0.33	      
0.16/0.33	      [c](x0) = x0 + 12,
0.16/0.33	      
0.16/0.33	      [a](x0) = x0 + 11
0.16/0.33	     orientation:
0.16/0.33	      d(d(d(x1))) = x1 + 24 >= x1 + 23 = a(c(x1))
0.16/0.33	      
0.16/0.33	      b(b(x1)) = x1 + 20 >= x1 + 20 = c(d(x1))
0.16/0.33	      
0.16/0.33	      a(a(x1)) = x1 + 22 >= x1 + 22 = b(c(x1))
0.16/0.33	      
0.16/0.33	      c(c(x1)) = x1 + 24 >= x1 + 24 = d(d(d(x1)))
0.16/0.33	     problem:
0.16/0.33	      strict:
0.16/0.33	       
0.16/0.33	      weak:
0.16/0.33	       d(d(d(x1))) -> a(c(x1))
0.16/0.33	       b(b(x1)) -> c(d(x1))
0.16/0.33	       a(a(x1)) -> b(c(x1))
0.16/0.33	       c(c(x1)) -> d(d(d(x1)))
0.16/0.33	     Qed
0.16/0.33	EOF