YES(?,O(n^2))
51.76/15.45	YES(?,O(n^2))
51.76/15.46	
51.76/15.46	Problem:
51.76/15.46	 a(b(x1)) -> d(x1)
51.76/15.46	 b(a(x1)) -> a(b(x1))
51.76/15.46	 d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	 d(f(x1)) -> f(a(b(x1)))
51.76/15.46	 a(f(x1)) -> a(x1)
51.76/15.46	
51.76/15.46	Proof:
51.76/15.46	 Complexity Transformation Processor:
51.76/15.46	  strict:
51.76/15.46	   a(b(x1)) -> d(x1)
51.76/15.46	   b(a(x1)) -> a(b(x1))
51.76/15.46	   d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	   d(f(x1)) -> f(a(b(x1)))
51.76/15.46	   a(f(x1)) -> a(x1)
51.76/15.46	  weak:
51.76/15.46	   
51.76/15.46	  Matrix Interpretation Processor: dim=1
51.76/15.46	   
51.76/15.46	   max_matrix:
51.76/15.46	    1
51.76/15.46	   interpretation:
51.76/15.46	    [f](x0) = x0 + 11,
51.76/15.46	    
51.76/15.46	    [c](x0) = x0 + 45,
51.76/15.46	    
51.76/15.46	    [d](x0) = x0 + 65,
51.76/15.46	    
51.76/15.46	    [a](x0) = x0 + 51,
51.76/15.46	    
51.76/15.46	    [b](x0) = x0 + 48
51.76/15.46	   orientation:
51.76/15.46	    a(b(x1)) = x1 + 99 >= x1 + 65 = d(x1)
51.76/15.46	    
51.76/15.46	    b(a(x1)) = x1 + 99 >= x1 + 99 = a(b(x1))
51.76/15.46	    
51.76/15.46	    d(c(x1)) = x1 + 110 >= x1 + 203 = f(a(b(b(c(x1)))))
51.76/15.46	    
51.76/15.46	    d(f(x1)) = x1 + 76 >= x1 + 110 = f(a(b(x1)))
51.76/15.46	    
51.76/15.46	    a(f(x1)) = x1 + 62 >= x1 + 51 = a(x1)
51.76/15.46	   problem:
51.76/15.46	    strict:
51.76/15.46	     b(a(x1)) -> a(b(x1))
51.76/15.46	     d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	     d(f(x1)) -> f(a(b(x1)))
51.76/15.46	    weak:
51.76/15.46	     a(b(x1)) -> d(x1)
51.76/15.46	     a(f(x1)) -> a(x1)
51.76/15.46	   Splitting Processor:
51.76/15.46	    strict:
51.76/15.46	     d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	    weak:
51.76/15.46	     a(b(x1)) -> d(x1)
51.76/15.46	     a(f(x1)) -> a(x1)
51.76/15.46	     b(a(x1)) -> a(b(x1))
51.76/15.46	     d(f(x1)) -> f(a(b(x1)))
51.76/15.46	    Bounds Processor:
51.76/15.46	     bound: 1
51.76/15.46	     enrichment: match
51.76/15.46	     automaton:
51.76/15.46	      final states: {6}
51.76/15.46	      transitions:
51.76/15.46	       f1(17) -> 18*
51.76/15.46	       a1(25) -> 26*
51.76/15.46	       a1(44) -> 45*
51.76/15.46	       a1(51) -> 52*
51.76/15.46	       a1(16) -> 17*
51.76/15.46	       b1(65) -> 66*
51.76/15.46	       b1(50) -> 51*
51.76/15.46	       b1(15) -> 16*
51.76/15.46	       b1(27) -> 28*
51.76/15.46	       b1(74) -> 75*
51.76/15.46	       b1(14) -> 15*
51.76/15.46	       b1(43) -> 44*
51.76/15.46	       b1(33) -> 34*
51.76/15.46	       c1(13) -> 14*
51.76/15.46	       d1(35) -> 36*
51.76/15.46	       d1(57) -> 58*
51.76/15.46	       d1(59) -> 60*
51.76/15.46	       d1(39) -> 40*
51.76/15.46	       d1(19) -> 20*
51.76/15.46	       d1(76) -> 77*
51.76/15.46	       d1(83) -> 84*
51.76/15.46	       d0(6) -> 6*
51.76/15.46	       c0(6) -> 6*
51.76/15.46	       f0(6) -> 6*
51.76/15.46	       a0(6) -> 6*
51.76/15.46	       b0(6) -> 6*
51.76/15.46	       6 -> 33,13
51.76/15.46	       15 -> 19*
51.76/15.46	       16 -> 50*
51.76/15.46	       17 -> 45,66,75,51,6,34,27,25
51.76/15.46	       18 -> 77,84,60,58,36,40,6
51.76/15.46	       20 -> 17*
51.76/15.46	       25 -> 43*
51.76/15.46	       26 -> 6*
51.76/15.46	       27 -> 35*
51.76/15.46	       28 -> 16*
51.76/15.46	       33 -> 39*
51.76/15.46	       34 -> 16*
51.76/15.46	       36 -> 17*
51.76/15.46	       40 -> 17*
51.76/15.46	       43 -> 59*
51.76/15.46	       44 -> 65*
51.76/15.46	       45 -> 6,34
51.76/15.46	       50 -> 57*
51.76/15.46	       51 -> 74*
51.76/15.46	       52 -> 6,34,75,51,44,28
51.76/15.46	       58 -> 52*
51.76/15.46	       60 -> 45*
51.76/15.46	       65 -> 76*
51.76/15.46	       66 -> 16*
51.76/15.46	       74 -> 83*
51.76/15.46	       75 -> 16*
51.76/15.46	       77 -> 17*
51.76/15.46	       84 -> 17*
51.76/15.46	     problem:
51.76/15.46	      strict:
51.76/15.46	       
51.76/15.46	      weak:
51.76/15.46	       d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	       a(b(x1)) -> d(x1)
51.76/15.46	       a(f(x1)) -> a(x1)
51.76/15.46	       b(a(x1)) -> a(b(x1))
51.76/15.46	       d(f(x1)) -> f(a(b(x1)))
51.76/15.46	     Qed
51.76/15.46	    
51.76/15.46	    strict:
51.76/15.46	     b(a(x1)) -> a(b(x1))
51.76/15.46	     d(f(x1)) -> f(a(b(x1)))
51.76/15.46	    weak:
51.76/15.46	     d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	     a(b(x1)) -> d(x1)
51.76/15.46	     a(f(x1)) -> a(x1)
51.76/15.46	    Splitting Processor:
51.76/15.46	     strict:
51.76/15.46	      b(a(x1)) -> a(b(x1))
51.76/15.46	     weak:
51.76/15.46	      d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.46	      a(b(x1)) -> d(x1)
51.76/15.46	      a(f(x1)) -> a(x1)
51.76/15.46	      d(f(x1)) -> f(a(b(x1)))
51.76/15.46	     Matrix Interpretation Processor: dim=4
51.76/15.46	      
51.76/15.46	      max_matrix:
51.76/15.46	       [1 1 1 1]
51.76/15.46	       [0 1 1 1]
51.76/15.46	       [0 0 0 1]
51.76/15.46	       [0 0 0 0]
51.76/15.46	      interpretation:
51.76/15.46	                 [1 0 0 0]     [0]
51.76/15.46	                 [0 1 1 1]     [1]
51.76/15.46	       [f](x0) = [0 0 0 0]x0 + [0]
51.76/15.46	                 [0 0 0 0]     [0],
51.76/15.46	       
51.76/15.46	                 [1 0 1 0]     [0]
51.76/15.46	                 [0 0 1 0]     [0]
51.76/15.46	       [c](x0) = [0 0 0 0]x0 + [0]
51.76/15.46	                 [0 0 0 0]     [1],
51.76/15.46	       
51.76/15.46	                 [1 1 0 0]     [1]
51.76/15.46	                 [0 1 0 1]     [0]
51.76/15.46	       [d](x0) = [0 0 0 0]x0 + [0]
51.76/15.46	                 [0 0 0 0]     [0],
51.76/15.46	       
51.76/15.46	                 [1 1 0 1]     [1]
51.76/15.46	                 [0 1 1 1]     [0]
51.76/15.46	       [a](x0) = [0 0 0 0]x0 + [0]
51.76/15.46	                 [0 0 0 0]     [0],
51.76/15.46	       
51.76/15.46	                 [1 0 0 0]  
51.76/15.46	                 [0 1 0 0]  
51.76/15.46	       [b](x0) = [0 0 0 1]x0
51.76/15.46	                 [0 0 0 0]  
51.76/15.46	      orientation:
51.76/15.46	                  [1 1 1 1]     [2]    [1 1 0 0]     [1]              
51.76/15.46	                  [0 1 1 1]     [1]    [0 1 0 1]     [1]              
51.76/15.46	       d(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(a(b(x1)))
51.76/15.46	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]              
51.76/15.46	       
51.76/15.46	                  [1 1 0 1]     [1]    [1 1 0 0]     [1]           
51.76/15.47	                  [0 1 1 1]     [0]    [0 1 0 1]     [0]           
51.76/15.47	       b(a(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = a(b(x1))
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]           
51.76/15.47	       
51.76/15.47	                  [1 0 2 0]     [1]    [1 0 2 0]     [1]                    
51.76/15.47	                  [0 0 1 0]     [1]    [0 0 1 0]     [1]                    
51.76/15.47	       d(c(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(a(b(b(c(x1)))))
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]                    
51.76/15.47	       
51.76/15.47	                  [1 1 0 0]     [1]    [1 1 0 0]     [1]        
51.76/15.47	                  [0 1 0 1]     [0]    [0 1 0 1]     [0]        
51.76/15.47	       a(b(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = d(x1)
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]        
51.76/15.47	       
51.76/15.47	                  [1 1 1 1]     [2]    [1 1 0 1]     [1]        
51.76/15.47	                  [0 1 1 1]     [1]    [0 1 1 1]     [0]        
51.76/15.47	       a(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = a(x1)
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]        
51.76/15.47	      problem:
51.76/15.47	       strict:
51.76/15.47	        
51.76/15.47	       weak:
51.76/15.47	        d(f(x1)) -> f(a(b(x1)))
51.76/15.47	        b(a(x1)) -> a(b(x1))
51.76/15.47	        d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.47	        a(b(x1)) -> d(x1)
51.76/15.47	        a(f(x1)) -> a(x1)
51.76/15.47	      Qed
51.76/15.47	     
51.76/15.47	     strict:
51.76/15.47	      d(f(x1)) -> f(a(b(x1)))
51.76/15.47	     weak:
51.76/15.47	      b(a(x1)) -> a(b(x1))
51.76/15.47	      d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.47	      a(b(x1)) -> d(x1)
51.76/15.47	      a(f(x1)) -> a(x1)
51.76/15.47	     Matrix Interpretation Processor: dim=4
51.76/15.47	      
51.76/15.47	      max_matrix:
51.76/15.47	       [1 1 0 0]
51.76/15.47	       [0 1 1 1]
51.76/15.47	       [0 0 0 0]
51.76/15.47	       [0 0 0 0]
51.76/15.47	      interpretation:
51.76/15.47	                 [1 0 0 0]  
51.76/15.47	                 [0 1 1 1]  
51.76/15.47	       [f](x0) = [0 0 0 0]x0
51.76/15.47	                 [0 0 0 0]  ,
51.76/15.47	       
51.76/15.47	                 [1 1 0 0]     [1]
51.76/15.47	                 [0 0 0 0]     [0]
51.76/15.47	       [c](x0) = [0 0 0 0]x0 + [0]
51.76/15.47	                 [0 0 0 0]     [0],
51.76/15.47	       
51.76/15.47	                 [1 1 0 0]     [0]
51.76/15.47	                 [0 1 0 0]     [1]
51.76/15.47	       [d](x0) = [0 0 0 0]x0 + [0]
51.76/15.47	                 [0 0 0 0]     [0],
51.76/15.47	       
51.76/15.47	                 [1 0 0 0]     [0]
51.76/15.47	                 [0 1 1 1]     [1]
51.76/15.47	       [a](x0) = [0 0 0 0]x0 + [0]
51.76/15.47	                 [0 0 0 0]     [0],
51.76/15.47	       
51.76/15.47	                 [1 1 0 0]  
51.76/15.47	                 [0 1 0 0]  
51.76/15.47	       [b](x0) = [0 0 0 0]x0
51.76/15.47	                 [0 0 0 0]  
51.76/15.47	      orientation:
51.76/15.47	                  [1 1 1 1]     [1]    [1 1 0 0]     [0]           
51.76/15.47	                  [0 1 1 1]     [1]    [0 1 0 0]     [1]           
51.76/15.47	       b(a(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = a(b(x1))
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]           
51.76/15.47	       
51.76/15.47	                  [1 1 0 0]     [1]    [1 1 0 0]     [1]                    
51.76/15.47	                  [0 0 0 0]     [1]    [0 0 0 0]     [1]                    
51.76/15.47	       d(c(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(a(b(b(c(x1)))))
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]                    
51.76/15.47	       
51.76/15.47	                  [1 1 0 0]     [0]    [1 1 0 0]     [0]        
51.76/15.47	                  [0 1 0 0]     [1]    [0 1 0 0]     [1]        
51.76/15.47	       a(b(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = d(x1)
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]        
51.76/15.47	       
51.76/15.47	                  [1 0 0 0]     [0]    [1 0 0 0]     [0]        
51.76/15.47	                  [0 1 1 1]     [1]    [0 1 1 1]     [1]        
51.76/15.47	       a(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = a(x1)
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]        
51.76/15.47	       
51.76/15.47	                  [1 1 1 1]     [0]    [1 1 0 0]     [0]              
51.76/15.47	                  [0 1 1 1]     [1]    [0 1 0 0]     [1]              
51.76/15.47	       d(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(a(b(x1)))
51.76/15.47	                  [0 0 0 0]     [0]    [0 0 0 0]     [0]              
51.76/15.47	      problem:
51.76/15.47	       strict:
51.76/15.47	        
51.76/15.47	       weak:
51.76/15.47	        b(a(x1)) -> a(b(x1))
51.76/15.47	        d(c(x1)) -> f(a(b(b(c(x1)))))
51.76/15.47	        a(b(x1)) -> d(x1)
51.76/15.47	        a(f(x1)) -> a(x1)
51.76/15.47	        d(f(x1)) -> f(a(b(x1)))
51.76/15.47	      Qed
51.76/15.47	EOF