YES(?,O(n^1))
14.20/4.00	YES(?,O(n^1))
14.20/4.00	
14.20/4.00	Problem:
14.20/4.00	 b(b(x1)) -> c(d(x1))
14.20/4.00	 c(c(x1)) -> d(d(d(x1)))
14.20/4.00	 c(x1) -> g(x1)
14.20/4.00	 d(d(x1)) -> c(f(x1))
14.20/4.00	 d(d(d(x1))) -> g(c(x1))
14.20/4.00	 f(x1) -> a(g(x1))
14.20/4.00	 g(x1) -> d(a(b(x1)))
14.20/4.00	 g(g(x1)) -> b(c(x1))
14.20/4.00	
14.20/4.00	Proof:
14.20/4.00	 Complexity Transformation Processor:
14.20/4.00	  strict:
14.20/4.00	   b(b(x1)) -> c(d(x1))
14.20/4.00	   c(c(x1)) -> d(d(d(x1)))
14.20/4.00	   c(x1) -> g(x1)
14.20/4.00	   d(d(x1)) -> c(f(x1))
14.20/4.00	   d(d(d(x1))) -> g(c(x1))
14.20/4.00	   f(x1) -> a(g(x1))
14.20/4.00	   g(x1) -> d(a(b(x1)))
14.20/4.00	   g(g(x1)) -> b(c(x1))
14.20/4.00	  weak:
14.20/4.00	   
14.20/4.00	  Matrix Interpretation Processor: dim=1
14.20/4.00	   
14.20/4.00	   max_matrix:
14.20/4.00	    1
14.20/4.00	   interpretation:
14.20/4.00	    [a](x0) = x0 + 242,
14.20/4.00	    
14.20/4.00	    [f](x0) = x0 + 32,
14.20/4.00	    
14.20/4.00	    [g](x0) = x0 + 44,
14.20/4.00	    
14.20/4.00	    [c](x0) = x0 + 66,
14.20/4.00	    
14.20/4.00	    [d](x0) = x0 + 8,
14.20/4.00	    
14.20/4.00	    [b](x0) = x0 + 84
14.20/4.00	   orientation:
14.20/4.00	    b(b(x1)) = x1 + 168 >= x1 + 74 = c(d(x1))
14.20/4.00	    
14.20/4.00	    c(c(x1)) = x1 + 132 >= x1 + 24 = d(d(d(x1)))
14.20/4.00	    
14.20/4.00	    c(x1) = x1 + 66 >= x1 + 44 = g(x1)
14.20/4.00	    
14.20/4.00	    d(d(x1)) = x1 + 16 >= x1 + 98 = c(f(x1))
14.20/4.00	    
14.20/4.00	    d(d(d(x1))) = x1 + 24 >= x1 + 110 = g(c(x1))
14.20/4.00	    
14.20/4.00	    f(x1) = x1 + 32 >= x1 + 286 = a(g(x1))
14.20/4.00	    
14.20/4.00	    g(x1) = x1 + 44 >= x1 + 334 = d(a(b(x1)))
14.20/4.00	    
14.20/4.00	    g(g(x1)) = x1 + 88 >= x1 + 150 = b(c(x1))
14.20/4.00	   problem:
14.20/4.00	    strict:
14.20/4.00	     d(d(x1)) -> c(f(x1))
14.20/4.00	     d(d(d(x1))) -> g(c(x1))
14.20/4.00	     f(x1) -> a(g(x1))
14.20/4.00	     g(x1) -> d(a(b(x1)))
14.20/4.00	     g(g(x1)) -> b(c(x1))
14.20/4.00	    weak:
14.20/4.00	     b(b(x1)) -> c(d(x1))
14.20/4.00	     c(c(x1)) -> d(d(d(x1)))
14.20/4.00	     c(x1) -> g(x1)
14.20/4.00	   Matrix Interpretation Processor: dim=1
14.20/4.00	    
14.20/4.00	    max_matrix:
14.20/4.00	     1
14.20/4.00	    interpretation:
14.20/4.00	     [a](x0) = x0 + 2,
14.20/4.00	     
14.20/4.00	     [f](x0) = x0 + 4,
14.20/4.00	     
14.20/4.00	     [g](x0) = x0,
14.20/4.00	     
14.20/4.00	     [c](x0) = x0 + 12,
14.20/4.00	     
14.20/4.00	     [d](x0) = x0 + 8,
14.20/4.00	     
14.20/4.00	     [b](x0) = x0 + 14
14.20/4.00	    orientation:
14.20/4.00	     d(d(x1)) = x1 + 16 >= x1 + 16 = c(f(x1))
14.20/4.00	     
14.20/4.00	     d(d(d(x1))) = x1 + 24 >= x1 + 12 = g(c(x1))
14.20/4.00	     
14.20/4.00	     f(x1) = x1 + 4 >= x1 + 2 = a(g(x1))
14.20/4.00	     
14.20/4.00	     g(x1) = x1 >= x1 + 24 = d(a(b(x1)))
14.20/4.00	     
14.20/4.00	     g(g(x1)) = x1 >= x1 + 26 = b(c(x1))
14.20/4.00	     
14.20/4.00	     b(b(x1)) = x1 + 28 >= x1 + 20 = c(d(x1))
14.20/4.00	     
14.20/4.00	     c(c(x1)) = x1 + 24 >= x1 + 24 = d(d(d(x1)))
14.20/4.00	     
14.20/4.00	     c(x1) = x1 + 12 >= x1 = g(x1)
14.20/4.00	    problem:
14.20/4.00	     strict:
14.20/4.00	      d(d(x1)) -> c(f(x1))
14.20/4.00	      g(x1) -> d(a(b(x1)))
14.20/4.00	      g(g(x1)) -> b(c(x1))
14.20/4.00	     weak:
14.20/4.00	      d(d(d(x1))) -> g(c(x1))
14.20/4.00	      f(x1) -> a(g(x1))
14.20/4.00	      b(b(x1)) -> c(d(x1))
14.20/4.00	      c(c(x1)) -> d(d(d(x1)))
14.20/4.00	      c(x1) -> g(x1)
14.20/4.00	    Matrix Interpretation Processor: dim=1
14.20/4.00	     
14.20/4.00	     max_matrix:
14.20/4.00	      1
14.20/4.00	     interpretation:
14.20/4.00	      [a](x0) = x0 + 18,
14.20/4.00	      
14.20/4.00	      [f](x0) = x0 + 24,
14.20/4.00	      
14.20/4.00	      [g](x0) = x0 + 6,
14.20/4.00	      
14.20/4.00	      [c](x0) = x0 + 6,
14.20/4.00	      
14.20/4.00	      [d](x0) = x0 + 4,
14.20/4.00	      
14.20/4.00	      [b](x0) = x0 + 5
14.20/4.00	     orientation:
14.20/4.00	      d(d(x1)) = x1 + 8 >= x1 + 30 = c(f(x1))
14.20/4.00	      
14.20/4.00	      g(x1) = x1 + 6 >= x1 + 27 = d(a(b(x1)))
14.20/4.00	      
14.20/4.00	      g(g(x1)) = x1 + 12 >= x1 + 11 = b(c(x1))
14.20/4.00	      
14.20/4.00	      d(d(d(x1))) = x1 + 12 >= x1 + 12 = g(c(x1))
14.20/4.00	      
14.20/4.00	      f(x1) = x1 + 24 >= x1 + 24 = a(g(x1))
14.20/4.00	      
14.20/4.00	      b(b(x1)) = x1 + 10 >= x1 + 10 = c(d(x1))
14.20/4.00	      
14.20/4.00	      c(c(x1)) = x1 + 12 >= x1 + 12 = d(d(d(x1)))
14.20/4.00	      
14.20/4.00	      c(x1) = x1 + 6 >= x1 + 6 = g(x1)
14.20/4.00	     problem:
14.20/4.00	      strict:
14.20/4.00	       d(d(x1)) -> c(f(x1))
14.20/4.00	       g(x1) -> d(a(b(x1)))
14.20/4.00	      weak:
14.20/4.00	       g(g(x1)) -> b(c(x1))
14.20/4.00	       d(d(d(x1))) -> g(c(x1))
14.20/4.00	       f(x1) -> a(g(x1))
14.20/4.00	       b(b(x1)) -> c(d(x1))
14.20/4.00	       c(c(x1)) -> d(d(d(x1)))
14.20/4.00	       c(x1) -> g(x1)
14.20/4.00	     Matrix Interpretation Processor: dim=4
14.20/4.00	      
14.20/4.00	      max_matrix:
14.20/4.00	       [1 1 1 1]
14.20/4.00	       [0 0 1 1]
14.20/4.00	       [0 0 0 1]
14.20/4.00	       [0 0 0 0]
14.20/4.00	      interpretation:
14.20/4.00	                 [1 0 0 0]  
14.20/4.00	                 [0 0 0 0]  
14.20/4.00	       [a](x0) = [0 0 0 0]x0
14.20/4.00	                 [0 0 0 0]  ,
14.20/4.00	       
14.20/4.00	                 [1 1 1 1]  
14.20/4.00	                 [0 0 0 0]  
14.20/4.00	       [f](x0) = [0 0 0 0]x0
14.20/4.00	                 [0 0 0 0]  ,
14.20/4.00	       
14.20/4.00	                 [1 1 1 1]     [0]
14.20/4.00	                 [0 0 0 1]     [0]
14.20/4.00	       [g](x0) = [0 0 0 0]x0 + [1]
14.20/4.00	                 [0 0 0 0]     [1],
14.20/4.00	       
14.20/4.00	                 [1 1 1 1]     [0]
14.20/4.00	                 [0 0 0 1]     [0]
14.20/4.00	       [c](x0) = [0 0 0 0]x0 + [1]
14.20/4.00	                 [0 0 0 0]     [1],
14.20/4.00	       
14.20/4.00	                 [1 1 0 1]     [0]
14.20/4.00	                 [0 0 1 0]     [0]
14.20/4.00	       [d](x0) = [0 0 0 1]x0 + [0]
14.20/4.00	                 [0 0 0 0]     [1],
14.20/4.00	       
14.20/4.00	                 [1 1 1 1]     [0]
14.20/4.01	                 [0 0 0 0]     [1]
14.20/4.01	       [b](x0) = [0 0 0 1]x0 + [0]
14.20/4.01	                 [0 0 0 0]     [1]
14.20/4.01	      orientation:
14.20/4.01	                  [1 1 1 1]     [1]    [1 1 1 1]     [0]           
14.20/4.01	                  [0 0 0 1]     [0]    [0 0 0 0]     [0]           
14.20/4.01	       d(d(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = c(f(x1))
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       
14.20/4.01	               [1 1 1 1]     [0]    [1 1 1 1]     [0]              
14.20/4.01	               [0 0 0 1]     [0]    [0 0 0 0]     [0]              
14.20/4.01	       g(x1) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = d(a(b(x1)))
14.20/4.01	               [0 0 0 0]     [1]    [0 0 0 0]     [1]              
14.20/4.01	       
14.20/4.01	                  [1 1 1 2]     [2]    [1 1 1 2]     [2]           
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       g(g(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(c(x1))
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       
14.20/4.01	                     [1 1 1 2]     [2]    [1 1 1 2]     [2]           
14.20/4.01	                     [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       d(d(d(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = g(c(x1))
14.20/4.01	                     [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       
14.20/4.01	               [1 1 1 1]      [1 1 1 1]             
14.20/4.01	               [0 0 0 0]      [0 0 0 0]             
14.20/4.01	       f(x1) = [0 0 0 0]x1 >= [0 0 0 0]x1 = a(g(x1))
14.20/4.01	               [0 0 0 0]      [0 0 0 0]             
14.20/4.01	       
14.20/4.01	                  [1 1 1 2]     [2]    [1 1 1 2]     [1]           
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       b(b(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = c(d(x1))
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]           
14.20/4.01	       
14.20/4.01	                  [1 1 1 2]     [2]    [1 1 1 2]     [2]              
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]              
14.20/4.01	       c(c(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = d(d(d(x1)))
14.20/4.01	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]              
14.20/4.01	       
14.20/4.01	               [1 1 1 1]     [0]    [1 1 1 1]     [0]        
14.20/4.01	               [0 0 0 1]     [0]    [0 0 0 1]     [0]        
14.20/4.01	       c(x1) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = g(x1)
14.20/4.01	               [0 0 0 0]     [1]    [0 0 0 0]     [1]        
14.20/4.01	      problem:
14.20/4.01	       strict:
14.20/4.01	        g(x1) -> d(a(b(x1)))
14.20/4.01	       weak:
14.20/4.01	        d(d(x1)) -> c(f(x1))
14.20/4.01	        g(g(x1)) -> b(c(x1))
14.20/4.01	        d(d(d(x1))) -> g(c(x1))
14.20/4.01	        f(x1) -> a(g(x1))
14.20/4.01	        b(b(x1)) -> c(d(x1))
14.20/4.01	        c(c(x1)) -> d(d(d(x1)))
14.20/4.01	        c(x1) -> g(x1)
14.20/4.01	      Matrix Interpretation Processor: dim=2
14.20/4.01	       
14.20/4.01	       max_matrix:
14.20/4.01	        [1 2]
14.20/4.01	        [0 0]
14.20/4.01	       interpretation:
14.20/4.01	                  [1 0]  
14.20/4.01	        [a](x0) = [0 0]x0,
14.20/4.01	        
14.20/4.01	                  [1 2]     [2]
14.20/4.01	        [f](x0) = [0 0]x0 + [0],
14.20/4.01	        
14.20/4.01	                  [1 2]     [2]
14.20/4.01	        [g](x0) = [0 0]x0 + [2],
14.20/4.01	        
14.20/4.01	                  [1 2]     [2]
14.20/4.01	        [c](x0) = [0 0]x0 + [2],
14.20/4.01	        
14.20/4.01	                  [1 2]     [0]
14.20/4.01	        [d](x0) = [0 0]x0 + [2],
14.20/4.01	        
14.20/4.01	                  [1 2]     [1]
14.20/4.01	        [b](x0) = [0 0]x0 + [2]
14.20/4.01	       orientation:
14.20/4.01	                [1 2]     [2]    [1 2]     [1]              
14.20/4.01	        g(x1) = [0 0]x1 + [2] >= [0 0]x1 + [2] = d(a(b(x1)))
14.20/4.01	        
14.20/4.01	                   [1 2]     [4]    [1 2]     [4]           
14.20/4.01	        d(d(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = c(f(x1))
14.20/4.01	        
14.20/4.01	                   [1 2]     [8]    [1 2]     [7]           
14.20/4.01	        g(g(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = b(c(x1))
14.20/4.01	        
14.20/4.01	                      [1 2]     [8]    [1 2]     [8]           
14.20/4.01	        d(d(d(x1))) = [0 0]x1 + [2] >= [0 0]x1 + [2] = g(c(x1))
14.20/4.01	        
14.20/4.01	                [1 2]     [2]    [1 2]     [2]           
14.20/4.01	        f(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = a(g(x1))
14.20/4.01	        
14.20/4.01	                   [1 2]     [6]    [1 2]     [6]           
14.20/4.01	        b(b(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = c(d(x1))
14.20/4.01	        
14.20/4.01	                   [1 2]     [8]    [1 2]     [8]              
14.20/4.01	        c(c(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = d(d(d(x1)))
14.20/4.01	        
14.20/4.01	                [1 2]     [2]    [1 2]     [2]        
14.20/4.01	        c(x1) = [0 0]x1 + [2] >= [0 0]x1 + [2] = g(x1)
14.20/4.01	       problem:
14.20/4.01	        strict:
14.20/4.01	         
14.20/4.01	        weak:
14.20/4.01	         g(x1) -> d(a(b(x1)))
14.20/4.01	         d(d(x1)) -> c(f(x1))
14.20/4.01	         g(g(x1)) -> b(c(x1))
14.20/4.01	         d(d(d(x1))) -> g(c(x1))
14.20/4.01	         f(x1) -> a(g(x1))
14.20/4.01	         b(b(x1)) -> c(d(x1))
14.20/4.01	         c(c(x1)) -> d(d(d(x1)))
14.20/4.01	         c(x1) -> g(x1)
14.20/4.01	       Qed
14.20/4.02	EOF