YES(?,O(n^1))
9.91/2.77	YES(?,O(n^1))
9.91/2.77	
9.91/2.77	Problem:
9.91/2.77	 a(x1) -> g(d(x1))
9.91/2.77	 b(b(b(x1))) -> c(d(c(x1)))
9.91/2.77	 b(b(x1)) -> a(g(g(x1)))
9.91/2.77	 c(d(x1)) -> g(g(x1))
9.91/2.77	 g(g(g(x1))) -> b(b(x1))
9.91/2.77	
9.91/2.77	Proof:
9.91/2.77	 Complexity Transformation Processor:
9.91/2.77	  strict:
9.91/2.77	   a(x1) -> g(d(x1))
9.91/2.77	   b(b(b(x1))) -> c(d(c(x1)))
9.91/2.77	   b(b(x1)) -> a(g(g(x1)))
9.91/2.77	   c(d(x1)) -> g(g(x1))
9.91/2.77	   g(g(g(x1))) -> b(b(x1))
9.91/2.77	  weak:
9.91/2.77	   
9.91/2.77	  Matrix Interpretation Processor: dim=1
9.91/2.77	   
9.91/2.77	   max_matrix:
9.91/2.77	    1
9.91/2.77	   interpretation:
9.91/2.77	    [c](x0) = x0 + 14,
9.91/2.77	    
9.91/2.77	    [b](x0) = x0 + 1,
9.91/2.77	    
9.91/2.77	    [g](x0) = x0 + 136,
9.91/2.77	    
9.91/2.77	    [d](x0) = x0 + 4,
9.91/2.77	    
9.91/2.77	    [a](x0) = x0 + 189
9.91/2.77	   orientation:
9.91/2.77	    a(x1) = x1 + 189 >= x1 + 140 = g(d(x1))
9.91/2.77	    
9.91/2.77	    b(b(b(x1))) = x1 + 3 >= x1 + 32 = c(d(c(x1)))
9.91/2.77	    
9.91/2.77	    b(b(x1)) = x1 + 2 >= x1 + 461 = a(g(g(x1)))
9.91/2.77	    
9.91/2.77	    c(d(x1)) = x1 + 18 >= x1 + 272 = g(g(x1))
9.91/2.77	    
9.91/2.77	    g(g(g(x1))) = x1 + 408 >= x1 + 2 = b(b(x1))
9.91/2.77	   problem:
9.91/2.77	    strict:
9.91/2.77	     b(b(b(x1))) -> c(d(c(x1)))
9.91/2.77	     b(b(x1)) -> a(g(g(x1)))
9.91/2.77	     c(d(x1)) -> g(g(x1))
9.91/2.77	    weak:
9.91/2.77	     a(x1) -> g(d(x1))
9.91/2.77	     g(g(g(x1))) -> b(b(x1))
9.91/2.77	   Matrix Interpretation Processor: dim=1
9.91/2.77	    
9.91/2.77	    max_matrix:
9.91/2.77	     1
9.91/2.77	    interpretation:
9.91/2.77	     [c](x0) = x0 + 64,
9.91/2.77	     
9.91/2.77	     [b](x0) = x0,
9.91/2.77	     
9.91/2.77	     [g](x0) = x0 + 10,
9.91/2.77	     
9.91/2.77	     [d](x0) = x0 + 48,
9.91/2.77	     
9.91/2.77	     [a](x0) = x0 + 68
9.91/2.77	    orientation:
9.91/2.77	     b(b(b(x1))) = x1 >= x1 + 176 = c(d(c(x1)))
9.91/2.77	     
9.91/2.77	     b(b(x1)) = x1 >= x1 + 88 = a(g(g(x1)))
9.91/2.77	     
9.91/2.77	     c(d(x1)) = x1 + 112 >= x1 + 20 = g(g(x1))
9.91/2.77	     
9.91/2.77	     a(x1) = x1 + 68 >= x1 + 58 = g(d(x1))
9.91/2.77	     
9.91/2.77	     g(g(g(x1))) = x1 + 30 >= x1 = b(b(x1))
9.91/2.77	    problem:
9.91/2.77	     strict:
9.91/2.77	      b(b(b(x1))) -> c(d(c(x1)))
9.91/2.77	      b(b(x1)) -> a(g(g(x1)))
9.91/2.77	     weak:
9.91/2.77	      c(d(x1)) -> g(g(x1))
9.91/2.77	      a(x1) -> g(d(x1))
9.91/2.77	      g(g(g(x1))) -> b(b(x1))
9.91/2.77	    Matrix Interpretation Processor: dim=1
9.91/2.77	     
9.91/2.77	     max_matrix:
9.91/2.77	      1
9.91/2.77	     interpretation:
9.91/2.77	      [c](x0) = x0,
9.91/2.77	      
9.91/2.77	      [b](x0) = x0 + 1,
9.91/2.77	      
9.91/2.77	      [g](x0) = x0 + 1,
9.91/2.77	      
9.91/2.77	      [d](x0) = x0 + 2,
9.91/2.77	      
9.91/2.77	      [a](x0) = x0 + 9
9.91/2.77	     orientation:
9.91/2.77	      b(b(b(x1))) = x1 + 3 >= x1 + 2 = c(d(c(x1)))
9.91/2.77	      
9.91/2.77	      b(b(x1)) = x1 + 2 >= x1 + 11 = a(g(g(x1)))
9.91/2.77	      
9.91/2.77	      c(d(x1)) = x1 + 2 >= x1 + 2 = g(g(x1))
9.91/2.77	      
9.91/2.77	      a(x1) = x1 + 9 >= x1 + 3 = g(d(x1))
9.91/2.77	      
9.91/2.77	      g(g(g(x1))) = x1 + 3 >= x1 + 2 = b(b(x1))
9.91/2.77	     problem:
9.91/2.77	      strict:
9.91/2.77	       b(b(x1)) -> a(g(g(x1)))
9.91/2.77	      weak:
9.91/2.77	       b(b(b(x1))) -> c(d(c(x1)))
9.91/2.77	       c(d(x1)) -> g(g(x1))
9.91/2.77	       a(x1) -> g(d(x1))
9.91/2.77	       g(g(g(x1))) -> b(b(x1))
9.91/2.77	     Arctic Interpretation Processor:
9.91/2.77	      dimension: 2
9.91/2.77	      interpretation:
9.91/2.77	                 [3 4]  
9.91/2.77	       [c](x0) = [4 5]x0,
9.91/2.77	       
9.91/2.77	                 [0 2]  
9.91/2.77	       [b](x0) = [2 3]x0,
9.91/2.77	       
9.91/2.77	                 [0 1]  
9.91/2.77	       [g](x0) = [1 2]x0,
9.91/2.77	       
9.91/2.77	                 [0  0 ]  
9.91/2.77	       [d](x0) = [0  -&]x0,
9.91/2.77	       
9.91/2.77	                 [1 0]  
9.91/2.77	       [a](x0) = [2 1]x0
9.91/2.77	      orientation:
9.91/2.77	                  [4 5]      [3 4]                
9.91/2.77	       b(b(x1)) = [5 6]x1 >= [4 5]x1 = a(g(g(x1)))
9.91/2.77	       
9.91/2.77	                     [7 8]      [7 8]                
9.91/2.77	       b(b(b(x1))) = [8 9]x1 >= [8 9]x1 = c(d(c(x1)))
9.91/2.77	       
9.91/2.77	                  [4 3]      [2 3]             
9.91/2.77	       c(d(x1)) = [5 4]x1 >= [3 4]x1 = g(g(x1))
9.91/2.77	       
9.91/2.77	               [1 0]      [1 0]             
9.91/2.77	       a(x1) = [2 1]x1 >= [2 1]x1 = g(d(x1))
9.91/2.77	       
9.91/2.77	                     [4 5]      [4 5]             
9.91/2.77	       g(g(g(x1))) = [5 6]x1 >= [5 6]x1 = b(b(x1))
9.91/2.77	      problem:
9.91/2.77	       strict:
9.91/2.77	        
9.91/2.77	       weak:
9.91/2.77	        b(b(x1)) -> a(g(g(x1)))
9.91/2.77	        b(b(b(x1))) -> c(d(c(x1)))
9.91/2.77	        c(d(x1)) -> g(g(x1))
9.91/2.77	        a(x1) -> g(d(x1))
9.91/2.77	        g(g(g(x1))) -> b(b(x1))
9.91/2.77	      Qed
9.91/2.78	EOF