YES(?,O(n^2))
25.41/8.82	YES(?,O(n^2))
25.41/8.82	
25.41/8.82	Problem:
25.41/8.82	 b(c(x1)) -> c(b(x1))
25.41/8.82	 c(b(x1)) -> a(a(a(x1)))
25.41/8.82	 a(a(a(a(x1)))) -> b(c(x1))
25.41/8.82	
25.41/8.82	Proof:
25.41/8.82	 Complexity Transformation Processor:
25.41/8.82	  strict:
25.41/8.82	   b(c(x1)) -> c(b(x1))
25.41/8.82	   c(b(x1)) -> a(a(a(x1)))
25.41/8.82	   a(a(a(a(x1)))) -> b(c(x1))
25.41/8.82	  weak:
25.41/8.82	   
25.41/8.82	  Matrix Interpretation Processor: dim=1
25.41/8.82	   
25.41/8.82	   max_matrix:
25.41/8.82	    1
25.41/8.82	   interpretation:
25.41/8.82	    [a](x0) = x0 + 54,
25.41/8.82	    
25.41/8.82	    [b](x0) = x0 + 8,
25.41/8.82	    
25.41/8.82	    [c](x0) = x0 + 1
25.41/8.82	   orientation:
25.41/8.82	    b(c(x1)) = x1 + 9 >= x1 + 9 = c(b(x1))
25.41/8.82	    
25.41/8.82	    c(b(x1)) = x1 + 9 >= x1 + 162 = a(a(a(x1)))
25.41/8.82	    
25.41/8.82	    a(a(a(a(x1)))) = x1 + 216 >= x1 + 9 = b(c(x1))
25.41/8.82	   problem:
25.41/8.82	    strict:
25.41/8.82	     b(c(x1)) -> c(b(x1))
25.41/8.82	     c(b(x1)) -> a(a(a(x1)))
25.41/8.82	    weak:
25.41/8.82	     a(a(a(a(x1)))) -> b(c(x1))
25.41/8.82	   Matrix Interpretation Processor: dim=1
25.41/8.82	    
25.41/8.82	    max_matrix:
25.41/8.82	     1
25.41/8.82	    interpretation:
25.41/8.82	     [a](x0) = x0 + 8,
25.41/8.82	     
25.41/8.82	     [b](x0) = x0,
25.41/8.82	     
25.41/8.82	     [c](x0) = x0 + 32
25.41/8.82	    orientation:
25.41/8.82	     b(c(x1)) = x1 + 32 >= x1 + 32 = c(b(x1))
25.41/8.82	     
25.41/8.82	     c(b(x1)) = x1 + 32 >= x1 + 24 = a(a(a(x1)))
25.41/8.82	     
25.41/8.82	     a(a(a(a(x1)))) = x1 + 32 >= x1 + 32 = b(c(x1))
25.41/8.82	    problem:
25.41/8.82	     strict:
25.41/8.82	      b(c(x1)) -> c(b(x1))
25.41/8.82	     weak:
25.41/8.82	      c(b(x1)) -> a(a(a(x1)))
25.41/8.82	      a(a(a(a(x1)))) -> b(c(x1))
25.41/8.82	    Matrix Interpretation Processor: dim=4
25.41/8.82	     
25.41/8.82	     max_matrix:
25.41/8.82	      [1 1 1 0]
25.41/8.82	      [0 0 1 1]
25.41/8.82	      [0 0 1 1]
25.41/8.82	      [0 0 0 0]
25.41/8.82	     interpretation:
25.41/8.82	                [1 1 0 0]     [0]
25.41/8.82	                [0 0 1 0]     [0]
25.41/8.82	      [a](x0) = [0 0 1 1]x0 + [0]
25.41/8.82	                [0 0 0 0]     [1],
25.41/8.82	      
25.41/8.82	                [1 1 1 0]     [0]
25.41/8.82	                [0 0 1 0]     [0]
25.41/8.82	      [b](x0) = [0 0 1 1]x0 + [0]
25.41/8.82	                [0 0 0 0]     [1],
25.41/8.82	      
25.41/8.82	                [1 1 1 0]     [0]
25.41/8.82	                [0 0 1 1]     [0]
25.41/8.82	      [c](x0) = [0 0 1 1]x0 + [1]
25.41/8.82	                [0 0 0 0]     [1]
25.41/8.82	     orientation:
25.41/8.82	                 [1 1 3 2]     [1]    [1 1 3 1]     [0]           
25.41/8.82	                 [0 0 1 1]     [1]    [0 0 1 1]     [1]           
25.41/8.82	      b(c(x1)) = [0 0 1 1]x1 + [2] >= [0 0 1 1]x1 + [2] = c(b(x1))
25.41/8.82	                 [0 0 0 0]     [1]    [0 0 0 0]     [1]           
25.41/8.82	      
25.41/8.82	                 [1 1 3 1]     [0]    [1 1 2 1]     [0]              
25.41/8.82	                 [0 0 1 1]     [1]    [0 0 1 1]     [1]              
25.41/8.82	      c(b(x1)) = [0 0 1 1]x1 + [2] >= [0 0 1 1]x1 + [2] = a(a(a(x1)))
25.41/8.82	                 [0 0 0 0]     [1]    [0 0 0 0]     [1]              
25.41/8.82	      
25.41/8.82	                       [1 1 3 2]     [1]    [1 1 3 2]     [1]           
25.41/8.82	                       [0 0 1 1]     [2]    [0 0 1 1]     [1]           
25.41/8.82	      a(a(a(a(x1)))) = [0 0 1 1]x1 + [3] >= [0 0 1 1]x1 + [2] = b(c(x1))
25.41/8.82	                       [0 0 0 0]     [1]    [0 0 0 0]     [1]           
25.41/8.82	     problem:
25.41/8.82	      strict:
25.41/8.82	       
25.41/8.82	      weak:
25.41/8.82	       b(c(x1)) -> c(b(x1))
25.41/8.82	       c(b(x1)) -> a(a(a(x1)))
25.41/8.82	       a(a(a(a(x1)))) -> b(c(x1))
25.41/8.82	     Qed
25.41/8.83	EOF