YES(?,O(n^1))
0.16/0.51	YES(?,O(n^1))
0.16/0.52	
0.16/0.52	Problem:
0.16/0.52	 f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	 c(X) -> d(activate(X))
0.16/0.52	 h(X) -> c(n__d(X))
0.16/0.52	 f(X) -> n__f(X)
0.16/0.52	 d(X) -> n__d(X)
0.16/0.52	 activate(n__f(X)) -> f(X)
0.16/0.52	 activate(n__d(X)) -> d(X)
0.16/0.52	 activate(X) -> X
0.16/0.52	
0.16/0.52	Proof:
0.16/0.52	 Complexity Transformation Processor:
0.16/0.52	  strict:
0.16/0.52	   f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	   c(X) -> d(activate(X))
0.16/0.52	   h(X) -> c(n__d(X))
0.16/0.52	   f(X) -> n__f(X)
0.16/0.52	   d(X) -> n__d(X)
0.16/0.52	   activate(n__f(X)) -> f(X)
0.16/0.52	   activate(n__d(X)) -> d(X)
0.16/0.52	   activate(X) -> X
0.16/0.52	  weak:
0.16/0.52	   
0.16/0.52	  Matrix Interpretation Processor: dim=1
0.16/0.52	   
0.16/0.52	   max_matrix:
0.16/0.52	    1
0.16/0.52	   interpretation:
0.16/0.52	    [n__d](x0) = x0 + 160,
0.16/0.52	    
0.16/0.52	    [h](x0) = x0,
0.16/0.52	    
0.16/0.52	    [d](x0) = x0 + 142,
0.16/0.52	    
0.16/0.52	    [activate](x0) = x0 + 115,
0.16/0.52	    
0.16/0.52	    [c](x0) = x0 + 59,
0.16/0.52	    
0.16/0.52	    [g](x0) = x0 + 195,
0.16/0.52	    
0.16/0.52	    [n__f](x0) = x0 + 97,
0.16/0.52	    
0.16/0.52	    [f](x0) = x0
0.16/0.52	   orientation:
0.16/0.52	    f(f(X)) = X >= X + 448 = c(n__f(g(n__f(X))))
0.16/0.52	    
0.16/0.52	    c(X) = X + 59 >= X + 257 = d(activate(X))
0.16/0.52	    
0.16/0.52	    h(X) = X >= X + 219 = c(n__d(X))
0.16/0.52	    
0.16/0.52	    f(X) = X >= X + 97 = n__f(X)
0.16/0.52	    
0.16/0.52	    d(X) = X + 142 >= X + 160 = n__d(X)
0.16/0.52	    
0.16/0.52	    activate(n__f(X)) = X + 212 >= X = f(X)
0.16/0.52	    
0.16/0.52	    activate(n__d(X)) = X + 275 >= X + 142 = d(X)
0.16/0.52	    
0.16/0.52	    activate(X) = X + 115 >= X = X
0.16/0.52	   problem:
0.16/0.52	    strict:
0.16/0.52	     f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	     c(X) -> d(activate(X))
0.16/0.52	     h(X) -> c(n__d(X))
0.16/0.52	     f(X) -> n__f(X)
0.16/0.52	     d(X) -> n__d(X)
0.16/0.52	    weak:
0.16/0.52	     activate(n__f(X)) -> f(X)
0.16/0.52	     activate(n__d(X)) -> d(X)
0.16/0.52	     activate(X) -> X
0.16/0.52	   Matrix Interpretation Processor: dim=1
0.16/0.52	    
0.16/0.52	    max_matrix:
0.16/0.52	     1
0.16/0.52	    interpretation:
0.16/0.52	     [n__d](x0) = x0,
0.16/0.52	     
0.16/0.52	     [h](x0) = x0,
0.16/0.52	     
0.16/0.52	     [d](x0) = x0 + 4,
0.16/0.52	     
0.16/0.52	     [activate](x0) = x0 + 8,
0.16/0.52	     
0.16/0.52	     [c](x0) = x0,
0.16/0.52	     
0.16/0.52	     [g](x0) = x0 + 6,
0.16/0.52	     
0.16/0.52	     [n__f](x0) = x0 + 7,
0.16/0.52	     
0.16/0.52	     [f](x0) = x0
0.16/0.52	    orientation:
0.16/0.52	     f(f(X)) = X >= X + 20 = c(n__f(g(n__f(X))))
0.16/0.52	     
0.16/0.52	     c(X) = X >= X + 12 = d(activate(X))
0.16/0.52	     
0.16/0.52	     h(X) = X >= X = c(n__d(X))
0.16/0.52	     
0.16/0.52	     f(X) = X >= X + 7 = n__f(X)
0.16/0.52	     
0.16/0.52	     d(X) = X + 4 >= X = n__d(X)
0.16/0.52	     
0.16/0.52	     activate(n__f(X)) = X + 15 >= X = f(X)
0.16/0.52	     
0.16/0.52	     activate(n__d(X)) = X + 8 >= X + 4 = d(X)
0.16/0.52	     
0.16/0.52	     activate(X) = X + 8 >= X = X
0.16/0.52	    problem:
0.16/0.52	     strict:
0.16/0.52	      f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	      c(X) -> d(activate(X))
0.16/0.52	      h(X) -> c(n__d(X))
0.16/0.52	      f(X) -> n__f(X)
0.16/0.52	     weak:
0.16/0.52	      d(X) -> n__d(X)
0.16/0.52	      activate(n__f(X)) -> f(X)
0.16/0.52	      activate(n__d(X)) -> d(X)
0.16/0.52	      activate(X) -> X
0.16/0.52	    Matrix Interpretation Processor: dim=1
0.16/0.52	     
0.16/0.52	     max_matrix:
0.16/0.52	      1
0.16/0.52	     interpretation:
0.16/0.52	      [n__d](x0) = x0 + 27,
0.16/0.52	      
0.16/0.52	      [h](x0) = x0,
0.16/0.52	      
0.16/0.52	      [d](x0) = x0 + 28,
0.16/0.52	      
0.16/0.52	      [activate](x0) = x0 + 4,
0.16/0.52	      
0.16/0.52	      [c](x0) = x0 + 101,
0.16/0.52	      
0.16/0.52	      [g](x0) = x0 + 10,
0.16/0.52	      
0.16/0.52	      [n__f](x0) = x0 + 4,
0.16/0.52	      
0.16/0.52	      [f](x0) = x0 + 4
0.16/0.52	     orientation:
0.16/0.52	      f(f(X)) = X + 8 >= X + 119 = c(n__f(g(n__f(X))))
0.16/0.52	      
0.16/0.52	      c(X) = X + 101 >= X + 32 = d(activate(X))
0.16/0.52	      
0.16/0.52	      h(X) = X >= X + 128 = c(n__d(X))
0.16/0.52	      
0.16/0.52	      f(X) = X + 4 >= X + 4 = n__f(X)
0.16/0.52	      
0.16/0.52	      d(X) = X + 28 >= X + 27 = n__d(X)
0.16/0.52	      
0.16/0.52	      activate(n__f(X)) = X + 8 >= X + 4 = f(X)
0.16/0.52	      
0.16/0.52	      activate(n__d(X)) = X + 31 >= X + 28 = d(X)
0.16/0.52	      
0.16/0.52	      activate(X) = X + 4 >= X = X
0.16/0.52	     problem:
0.16/0.52	      strict:
0.16/0.52	       f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	       h(X) -> c(n__d(X))
0.16/0.52	       f(X) -> n__f(X)
0.16/0.52	      weak:
0.16/0.52	       c(X) -> d(activate(X))
0.16/0.52	       d(X) -> n__d(X)
0.16/0.52	       activate(n__f(X)) -> f(X)
0.16/0.52	       activate(n__d(X)) -> d(X)
0.16/0.52	       activate(X) -> X
0.16/0.52	     Matrix Interpretation Processor: dim=1
0.16/0.52	      
0.16/0.52	      max_matrix:
0.16/0.52	       1
0.16/0.52	      interpretation:
0.16/0.52	       [n__d](x0) = x0,
0.16/0.52	       
0.16/0.52	       [h](x0) = x0 + 38,
0.16/0.52	       
0.16/0.52	       [d](x0) = x0 + 1,
0.16/0.52	       
0.16/0.52	       [activate](x0) = x0 + 3,
0.16/0.52	       
0.16/0.52	       [c](x0) = x0 + 37,
0.16/0.52	       
0.16/0.52	       [g](x0) = x0 + 72,
0.16/0.52	       
0.16/0.52	       [n__f](x0) = x0 + 9,
0.16/0.52	       
0.16/0.52	       [f](x0) = x0 + 4
0.16/0.52	      orientation:
0.16/0.52	       f(f(X)) = X + 8 >= X + 127 = c(n__f(g(n__f(X))))
0.16/0.52	       
0.16/0.52	       h(X) = X + 38 >= X + 37 = c(n__d(X))
0.16/0.52	       
0.16/0.52	       f(X) = X + 4 >= X + 9 = n__f(X)
0.16/0.52	       
0.16/0.52	       c(X) = X + 37 >= X + 4 = d(activate(X))
0.16/0.52	       
0.16/0.52	       d(X) = X + 1 >= X = n__d(X)
0.16/0.52	       
0.16/0.52	       activate(n__f(X)) = X + 12 >= X + 4 = f(X)
0.16/0.52	       
0.16/0.52	       activate(n__d(X)) = X + 3 >= X + 1 = d(X)
0.16/0.52	       
0.16/0.52	       activate(X) = X + 3 >= X = X
0.16/0.52	      problem:
0.16/0.52	       strict:
0.16/0.52	        f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	        f(X) -> n__f(X)
0.16/0.52	       weak:
0.16/0.52	        h(X) -> c(n__d(X))
0.16/0.52	        c(X) -> d(activate(X))
0.16/0.52	        d(X) -> n__d(X)
0.16/0.52	        activate(n__f(X)) -> f(X)
0.16/0.52	        activate(n__d(X)) -> d(X)
0.16/0.52	        activate(X) -> X
0.16/0.52	      Matrix Interpretation Processor: dim=1
0.16/0.52	       
0.16/0.52	       max_matrix:
0.16/0.52	        1
0.16/0.52	       interpretation:
0.16/0.52	        [n__d](x0) = x0 + 8,
0.16/0.52	        
0.16/0.52	        [h](x0) = x0 + 128,
0.16/0.52	        
0.16/0.52	        [d](x0) = x0 + 8,
0.16/0.52	        
0.16/0.52	        [activate](x0) = x0 + 21,
0.16/0.52	        
0.16/0.52	        [c](x0) = x0 + 120,
0.16/0.52	        
0.16/0.52	        [g](x0) = x0 + 141,
0.16/0.52	        
0.16/0.52	        [n__f](x0) = x0 + 11,
0.16/0.52	        
0.16/0.52	        [f](x0) = x0 + 16
0.16/0.52	       orientation:
0.16/0.52	        f(f(X)) = X + 32 >= X + 283 = c(n__f(g(n__f(X))))
0.16/0.52	        
0.16/0.52	        f(X) = X + 16 >= X + 11 = n__f(X)
0.16/0.52	        
0.16/0.52	        h(X) = X + 128 >= X + 128 = c(n__d(X))
0.16/0.52	        
0.16/0.52	        c(X) = X + 120 >= X + 29 = d(activate(X))
0.16/0.52	        
0.16/0.52	        d(X) = X + 8 >= X + 8 = n__d(X)
0.16/0.52	        
0.16/0.52	        activate(n__f(X)) = X + 32 >= X + 16 = f(X)
0.16/0.52	        
0.16/0.52	        activate(n__d(X)) = X + 29 >= X + 8 = d(X)
0.16/0.52	        
0.16/0.52	        activate(X) = X + 21 >= X = X
0.16/0.52	       problem:
0.16/0.52	        strict:
0.16/0.52	         f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	        weak:
0.16/0.52	         f(X) -> n__f(X)
0.16/0.52	         h(X) -> c(n__d(X))
0.16/0.52	         c(X) -> d(activate(X))
0.16/0.52	         d(X) -> n__d(X)
0.16/0.52	         activate(n__f(X)) -> f(X)
0.16/0.52	         activate(n__d(X)) -> d(X)
0.16/0.52	         activate(X) -> X
0.16/0.52	       Matrix Interpretation Processor: dim=1
0.16/0.52	        
0.16/0.52	        max_matrix:
0.16/0.52	         1
0.16/0.52	        interpretation:
0.16/0.52	         [n__d](x0) = x0,
0.16/0.52	         
0.16/0.52	         [h](x0) = x0 + 2,
0.16/0.52	         
0.16/0.52	         [d](x0) = x0,
0.16/0.52	         
0.16/0.52	         [activate](x0) = x0 + 1,
0.16/0.52	         
0.16/0.52	         [c](x0) = x0 + 1,
0.16/0.52	         
0.16/0.52	         [g](x0) = x0,
0.16/0.52	         
0.16/0.52	         [n__f](x0) = x0 + 4,
0.16/0.52	         
0.16/0.52	         [f](x0) = x0 + 5
0.16/0.52	        orientation:
0.16/0.52	         f(f(X)) = X + 10 >= X + 9 = c(n__f(g(n__f(X))))
0.16/0.52	         
0.16/0.52	         f(X) = X + 5 >= X + 4 = n__f(X)
0.16/0.52	         
0.16/0.52	         h(X) = X + 2 >= X + 1 = c(n__d(X))
0.16/0.52	         
0.16/0.52	         c(X) = X + 1 >= X + 1 = d(activate(X))
0.16/0.52	         
0.16/0.52	         d(X) = X >= X = n__d(X)
0.16/0.52	         
0.16/0.52	         activate(n__f(X)) = X + 5 >= X + 5 = f(X)
0.16/0.52	         
0.16/0.52	         activate(n__d(X)) = X + 1 >= X = d(X)
0.16/0.52	         
0.16/0.52	         activate(X) = X + 1 >= X = X
0.16/0.52	        problem:
0.16/0.52	         strict:
0.16/0.52	          
0.16/0.52	         weak:
0.16/0.52	          f(f(X)) -> c(n__f(g(n__f(X))))
0.16/0.52	          f(X) -> n__f(X)
0.16/0.52	          h(X) -> c(n__d(X))
0.16/0.52	          c(X) -> d(activate(X))
0.16/0.52	          d(X) -> n__d(X)
0.16/0.52	          activate(n__f(X)) -> f(X)
0.16/0.52	          activate(n__d(X)) -> d(X)
0.16/0.52	          activate(X) -> X
0.16/0.52	        Qed
0.16/0.53	EOF