YES(?,O(n^3))
43.62/14.06	YES(?,O(n^3))
43.62/14.07	
43.62/14.07	Problem:
43.62/14.07	 a(a(x1)) -> b(b(b(x1)))
43.62/14.07	 b(x1) -> c(c(d(x1)))
43.62/14.07	 c(x1) -> d(d(d(x1)))
43.62/14.07	 b(c(x1)) -> c(b(x1))
43.62/14.07	 b(c(d(x1))) -> a(x1)
43.62/14.07	
43.62/14.07	Proof:
43.62/14.07	 Complexity Transformation Processor:
43.62/14.07	  strict:
43.62/14.07	   a(a(x1)) -> b(b(b(x1)))
43.62/14.07	   b(x1) -> c(c(d(x1)))
43.62/14.07	   c(x1) -> d(d(d(x1)))
43.62/14.07	   b(c(x1)) -> c(b(x1))
43.62/14.07	   b(c(d(x1))) -> a(x1)
43.62/14.07	  weak:
43.62/14.07	   
43.62/14.07	  Matrix Interpretation Processor: dim=1
43.62/14.07	   
43.62/14.07	   max_matrix:
43.62/14.07	    1
43.62/14.07	   interpretation:
43.62/14.07	    [c](x0) = x0 + 139,
43.62/14.07	    
43.62/14.07	    [d](x0) = x0 + 37,
43.62/14.07	    
43.62/14.07	    [b](x0) = x0 + 72,
43.62/14.07	    
43.62/14.07	    [a](x0) = x0
43.62/14.07	   orientation:
43.62/14.07	    a(a(x1)) = x1 >= x1 + 216 = b(b(b(x1)))
43.62/14.07	    
43.62/14.07	    b(x1) = x1 + 72 >= x1 + 315 = c(c(d(x1)))
43.62/14.07	    
43.62/14.07	    c(x1) = x1 + 139 >= x1 + 111 = d(d(d(x1)))
43.62/14.07	    
43.62/14.07	    b(c(x1)) = x1 + 211 >= x1 + 211 = c(b(x1))
43.62/14.07	    
43.62/14.07	    b(c(d(x1))) = x1 + 248 >= x1 = a(x1)
43.62/14.07	   problem:
43.62/14.07	    strict:
43.62/14.07	     a(a(x1)) -> b(b(b(x1)))
43.62/14.07	     b(x1) -> c(c(d(x1)))
43.62/14.07	     b(c(x1)) -> c(b(x1))
43.62/14.07	    weak:
43.62/14.07	     c(x1) -> d(d(d(x1)))
43.62/14.07	     b(c(d(x1))) -> a(x1)
43.62/14.07	   Matrix Interpretation Processor: dim=1
43.62/14.07	    
43.62/14.07	    max_matrix:
43.62/14.07	     1
43.62/14.07	    interpretation:
43.62/14.07	     [c](x0) = x0,
43.62/14.07	     
43.62/14.07	     [d](x0) = x0,
43.62/14.07	     
43.62/14.07	     [b](x0) = x0 + 4,
43.62/14.07	     
43.62/14.07	     [a](x0) = x0
43.62/14.07	    orientation:
43.62/14.07	     a(a(x1)) = x1 >= x1 + 12 = b(b(b(x1)))
43.62/14.07	     
43.62/14.07	     b(x1) = x1 + 4 >= x1 = c(c(d(x1)))
43.62/14.07	     
43.62/14.07	     b(c(x1)) = x1 + 4 >= x1 + 4 = c(b(x1))
43.62/14.07	     
43.62/14.07	     c(x1) = x1 >= x1 = d(d(d(x1)))
43.62/14.07	     
43.62/14.07	     b(c(d(x1))) = x1 + 4 >= x1 = a(x1)
43.62/14.07	    problem:
43.62/14.07	     strict:
43.62/14.07	      a(a(x1)) -> b(b(b(x1)))
43.62/14.07	      b(c(x1)) -> c(b(x1))
43.62/14.07	     weak:
43.62/14.07	      b(x1) -> c(c(d(x1)))
43.62/14.07	      c(x1) -> d(d(d(x1)))
43.62/14.07	      b(c(d(x1))) -> a(x1)
43.62/14.07	    Matrix Interpretation Processor: dim=1
43.62/14.07	     
43.62/14.07	     max_matrix:
43.62/14.07	      1
43.62/14.07	     interpretation:
43.62/14.07	      [c](x0) = x0 + 32,
43.62/14.07	      
43.62/14.07	      [d](x0) = x0 + 8,
43.62/14.07	      
43.62/14.07	      [b](x0) = x0 + 73,
43.62/14.07	      
43.62/14.07	      [a](x0) = x0 + 112
43.62/14.07	     orientation:
43.62/14.07	      a(a(x1)) = x1 + 224 >= x1 + 219 = b(b(b(x1)))
43.62/14.07	      
43.62/14.07	      b(c(x1)) = x1 + 105 >= x1 + 105 = c(b(x1))
43.62/14.07	      
43.62/14.07	      b(x1) = x1 + 73 >= x1 + 72 = c(c(d(x1)))
43.62/14.07	      
43.62/14.07	      c(x1) = x1 + 32 >= x1 + 24 = d(d(d(x1)))
43.62/14.07	      
43.62/14.07	      b(c(d(x1))) = x1 + 113 >= x1 + 112 = a(x1)
43.62/14.07	     problem:
43.62/14.07	      strict:
43.62/14.07	       b(c(x1)) -> c(b(x1))
43.62/14.07	      weak:
43.62/14.07	       a(a(x1)) -> b(b(b(x1)))
43.62/14.07	       b(x1) -> c(c(d(x1)))
43.62/14.07	       c(x1) -> d(d(d(x1)))
43.62/14.07	       b(c(d(x1))) -> a(x1)
43.62/14.07	     Matrix Interpretation Processor: dim=3
43.62/14.07	      
43.62/14.07	      max_matrix:
43.62/14.07	       [1 1 2]
43.62/14.07	       [0 0 1]
43.62/14.07	       [0 1 1]
43.62/14.07	      interpretation:
43.62/14.07	                 [1 1 0]     [0]
43.62/14.07	       [c](x0) = [0 0 0]x0 + [0]
43.62/14.07	                 [0 1 1]     [1],
43.62/14.07	       
43.62/14.07	                 [1 0 0]  
43.62/14.07	       [d](x0) = [0 0 1]x0
43.62/14.07	                 [0 0 0]  ,
43.62/14.07	       
43.62/14.07	                 [1 0 1]     [0]
43.62/14.07	       [b](x0) = [0 0 0]x0 + [0]
43.62/14.07	                 [0 0 1]     [2],
43.62/14.07	       
43.62/14.07	                 [1 0 2]     [0]
43.62/14.07	       [a](x0) = [0 0 0]x0 + [0]
43.62/14.07	                 [0 0 1]     [3]
43.62/14.07	      orientation:
43.62/14.07	                  [1 2 1]     [1]    [1 0 1]     [0]           
43.62/14.07	       b(c(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c(b(x1))
43.62/14.07	                  [0 1 1]     [3]    [0 0 1]     [3]           
43.62/14.07	       
43.62/14.07	                  [1 0 4]     [6]    [1 0 3]     [6]              
43.62/14.07	       a(a(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(b(b(x1)))
43.62/14.07	                  [0 0 1]     [6]    [0 0 1]     [6]              
43.62/14.07	       
43.62/14.07	               [1 0 1]     [0]    [1 0 1]     [0]              
43.62/14.07	       b(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c(c(d(x1)))
43.62/14.07	               [0 0 1]     [2]    [0 0 1]     [2]              
43.62/14.07	       
43.62/14.07	               [1 1 0]     [0]    [1 0 0]                
43.62/14.07	       c(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 = d(d(d(x1)))
43.62/14.07	               [0 1 1]     [1]    [0 0 0]                
43.62/14.07	       
43.62/14.07	                     [1 0 2]     [1]    [1 0 2]     [0]        
43.62/14.07	       b(c(d(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(x1)
43.62/14.07	                     [0 0 1]     [3]    [0 0 1]     [3]        
43.62/14.07	      problem:
43.62/14.07	       strict:
43.62/14.07	        
43.62/14.07	       weak:
43.62/14.07	        b(c(x1)) -> c(b(x1))
43.62/14.07	        a(a(x1)) -> b(b(b(x1)))
43.62/14.07	        b(x1) -> c(c(d(x1)))
43.62/14.07	        c(x1) -> d(d(d(x1)))
43.62/14.07	        b(c(d(x1))) -> a(x1)
43.62/14.07	      Qed
43.62/14.07	EOF