YES(?,O(n^1))
0.16/0.30	YES(?,O(n^1))
0.16/0.30	
0.16/0.30	Problem:
0.16/0.30	 a(a(a(x1))) -> b(b(x1))
0.16/0.30	 b(b(b(x1))) -> c(d(x1))
0.16/0.30	 c(x1) -> a(a(x1))
0.16/0.30	 d(x1) -> c(x1)
0.16/0.30	
0.16/0.30	Proof:
0.16/0.30	 Complexity Transformation Processor:
0.16/0.30	  strict:
0.16/0.30	   a(a(a(x1))) -> b(b(x1))
0.16/0.30	   b(b(b(x1))) -> c(d(x1))
0.16/0.30	   c(x1) -> a(a(x1))
0.16/0.30	   d(x1) -> c(x1)
0.16/0.30	  weak:
0.16/0.30	   
0.16/0.30	  Matrix Interpretation Processor: dim=1
0.16/0.30	   
0.16/0.30	   max_matrix:
0.16/0.30	    1
0.16/0.30	   interpretation:
0.16/0.30	    [c](x0) = x0 + 18,
0.16/0.30	    
0.16/0.30	    [d](x0) = x0 + 55,
0.16/0.30	    
0.16/0.30	    [b](x0) = x0,
0.16/0.30	    
0.16/0.30	    [a](x0) = x0
0.16/0.30	   orientation:
0.16/0.30	    a(a(a(x1))) = x1 >= x1 = b(b(x1))
0.16/0.30	    
0.16/0.30	    b(b(b(x1))) = x1 >= x1 + 73 = c(d(x1))
0.16/0.30	    
0.16/0.30	    c(x1) = x1 + 18 >= x1 = a(a(x1))
0.16/0.30	    
0.16/0.30	    d(x1) = x1 + 55 >= x1 + 18 = c(x1)
0.16/0.30	   problem:
0.16/0.30	    strict:
0.16/0.30	     a(a(a(x1))) -> b(b(x1))
0.16/0.30	     b(b(b(x1))) -> c(d(x1))
0.16/0.30	    weak:
0.16/0.30	     c(x1) -> a(a(x1))
0.16/0.30	     d(x1) -> c(x1)
0.16/0.30	   Matrix Interpretation Processor: dim=1
0.16/0.30	    
0.16/0.30	    max_matrix:
0.16/0.30	     1
0.16/0.30	    interpretation:
0.16/0.30	     [c](x0) = x0 + 34,
0.16/0.30	     
0.16/0.30	     [d](x0) = x0 + 34,
0.16/0.30	     
0.16/0.30	     [b](x0) = x0 + 8,
0.16/0.30	     
0.16/0.30	     [a](x0) = x0 + 17
0.16/0.30	    orientation:
0.16/0.30	     a(a(a(x1))) = x1 + 51 >= x1 + 16 = b(b(x1))
0.16/0.30	     
0.16/0.30	     b(b(b(x1))) = x1 + 24 >= x1 + 68 = c(d(x1))
0.16/0.30	     
0.16/0.30	     c(x1) = x1 + 34 >= x1 + 34 = a(a(x1))
0.16/0.30	     
0.16/0.30	     d(x1) = x1 + 34 >= x1 + 34 = c(x1)
0.16/0.30	    problem:
0.16/0.30	     strict:
0.16/0.30	      b(b(b(x1))) -> c(d(x1))
0.16/0.30	     weak:
0.16/0.30	      a(a(a(x1))) -> b(b(x1))
0.16/0.30	      c(x1) -> a(a(x1))
0.16/0.30	      d(x1) -> c(x1)
0.16/0.30	    Matrix Interpretation Processor: dim=1
0.16/0.30	     
0.16/0.30	     max_matrix:
0.16/0.30	      1
0.16/0.30	     interpretation:
0.16/0.30	      [c](x0) = x0 + 96,
0.16/0.30	      
0.16/0.30	      [d](x0) = x0 + 96,
0.16/0.30	      
0.16/0.30	      [b](x0) = x0 + 66,
0.16/0.30	      
0.16/0.30	      [a](x0) = x0 + 48
0.16/0.30	     orientation:
0.16/0.30	      b(b(b(x1))) = x1 + 198 >= x1 + 192 = c(d(x1))
0.16/0.30	      
0.16/0.30	      a(a(a(x1))) = x1 + 144 >= x1 + 132 = b(b(x1))
0.16/0.30	      
0.16/0.30	      c(x1) = x1 + 96 >= x1 + 96 = a(a(x1))
0.16/0.30	      
0.16/0.30	      d(x1) = x1 + 96 >= x1 + 96 = c(x1)
0.16/0.30	     problem:
0.16/0.30	      strict:
0.16/0.30	       
0.16/0.30	      weak:
0.16/0.30	       b(b(b(x1))) -> c(d(x1))
0.16/0.30	       a(a(a(x1))) -> b(b(x1))
0.16/0.30	       c(x1) -> a(a(x1))
0.16/0.30	       d(x1) -> c(x1)
0.16/0.30	     Qed
0.16/0.31	EOF