YES(?,O(n^2))

Problem:
 q0(0(x1)) -> 0'(q1(x1))
 q1(0(x1)) -> 0(q1(x1))
 q1(1'(x1)) -> 1'(q1(x1))
 0(q1(1(x1))) -> q2(0(1'(x1)))
 0'(q1(1(x1))) -> q2(0'(1'(x1)))
 1'(q1(1(x1))) -> q2(1'(1'(x1)))
 0(q2(0(x1))) -> q2(0(0(x1)))
 0'(q2(0(x1))) -> q2(0'(0(x1)))
 1'(q2(0(x1))) -> q2(1'(0(x1)))
 0(q2(1'(x1))) -> q2(0(1'(x1)))
 0'(q2(1'(x1))) -> q2(0'(1'(x1)))
 1'(q2(1'(x1))) -> q2(1'(1'(x1)))
 q2(0'(x1)) -> 0'(q0(x1))
 q0(1'(x1)) -> 1'(q3(x1))
 q3(1'(x1)) -> 1'(q3(x1))
 q3(b(x1)) -> b(q4(x1))

Proof:
 RT Transformation Processor:
  strict:
   q0(0(x1)) -> 0'(q1(x1))
   q1(0(x1)) -> 0(q1(x1))
   q1(1'(x1)) -> 1'(q1(x1))
   0(q1(1(x1))) -> q2(0(1'(x1)))
   0'(q1(1(x1))) -> q2(0'(1'(x1)))
   1'(q1(1(x1))) -> q2(1'(1'(x1)))
   0(q2(0(x1))) -> q2(0(0(x1)))
   0'(q2(0(x1))) -> q2(0'(0(x1)))
   1'(q2(0(x1))) -> q2(1'(0(x1)))
   0(q2(1'(x1))) -> q2(0(1'(x1)))
   0'(q2(1'(x1))) -> q2(0'(1'(x1)))
   1'(q2(1'(x1))) -> q2(1'(1'(x1)))
   q2(0'(x1)) -> 0'(q0(x1))
   q0(1'(x1)) -> 1'(q3(x1))
   q3(1'(x1)) -> 1'(q3(x1))
   q3(b(x1)) -> b(q4(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [q4](x0) = x0 + 1,
    
    [b](x0) = x0 + 3,
    
    [q3](x0) = x0 + 18,
    
    [q2](x0) = x0 + 13,
    
    [1](x0) = x0 + 10,
    
    [1'](x0) = x0,
    
    [0'](x0) = x0 + 19,
    
    [q1](x0) = x0 + 6,
    
    [q0](x0) = x0 + 22,
    
    [0](x0) = x0 + 3
   orientation:
    q0(0(x1)) = x1 + 25 >= x1 + 25 = 0'(q1(x1))
    
    q1(0(x1)) = x1 + 9 >= x1 + 9 = 0(q1(x1))
    
    q1(1'(x1)) = x1 + 6 >= x1 + 6 = 1'(q1(x1))
    
    0(q1(1(x1))) = x1 + 19 >= x1 + 16 = q2(0(1'(x1)))
    
    0'(q1(1(x1))) = x1 + 35 >= x1 + 32 = q2(0'(1'(x1)))
    
    1'(q1(1(x1))) = x1 + 16 >= x1 + 13 = q2(1'(1'(x1)))
    
    0(q2(0(x1))) = x1 + 19 >= x1 + 19 = q2(0(0(x1)))
    
    0'(q2(0(x1))) = x1 + 35 >= x1 + 35 = q2(0'(0(x1)))
    
    1'(q2(0(x1))) = x1 + 16 >= x1 + 16 = q2(1'(0(x1)))
    
    0(q2(1'(x1))) = x1 + 16 >= x1 + 16 = q2(0(1'(x1)))
    
    0'(q2(1'(x1))) = x1 + 32 >= x1 + 32 = q2(0'(1'(x1)))
    
    1'(q2(1'(x1))) = x1 + 13 >= x1 + 13 = q2(1'(1'(x1)))
    
    q2(0'(x1)) = x1 + 32 >= x1 + 41 = 0'(q0(x1))
    
    q0(1'(x1)) = x1 + 22 >= x1 + 18 = 1'(q3(x1))
    
    q3(1'(x1)) = x1 + 18 >= x1 + 18 = 1'(q3(x1))
    
    q3(b(x1)) = x1 + 21 >= x1 + 4 = b(q4(x1))
   problem:
    strict:
     q0(0(x1)) -> 0'(q1(x1))
     q1(0(x1)) -> 0(q1(x1))
     q1(1'(x1)) -> 1'(q1(x1))
     0(q2(0(x1))) -> q2(0(0(x1)))
     0'(q2(0(x1))) -> q2(0'(0(x1)))
     1'(q2(0(x1))) -> q2(1'(0(x1)))
     0(q2(1'(x1))) -> q2(0(1'(x1)))
     0'(q2(1'(x1))) -> q2(0'(1'(x1)))
     1'(q2(1'(x1))) -> q2(1'(1'(x1)))
     q2(0'(x1)) -> 0'(q0(x1))
     q3(1'(x1)) -> 1'(q3(x1))
    weak:
     0(q1(1(x1))) -> q2(0(1'(x1)))
     0'(q1(1(x1))) -> q2(0'(1'(x1)))
     1'(q1(1(x1))) -> q2(1'(1'(x1)))
     q0(1'(x1)) -> 1'(q3(x1))
     q3(b(x1)) -> b(q4(x1))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [q4](x0) = x0,
     
     [b](x0) = x0 + 1,
     
     [q3](x0) = x0,
     
     [q2](x0) = x0 + 4,
     
     [1](x0) = x0 + 7,
     
     [1'](x0) = x0,
     
     [0'](x0) = x0 + 14,
     
     [q1](x0) = x0,
     
     [q0](x0) = x0,
     
     [0](x0) = x0
    orientation:
     q0(0(x1)) = x1 >= x1 + 14 = 0'(q1(x1))
     
     q1(0(x1)) = x1 >= x1 = 0(q1(x1))
     
     q1(1'(x1)) = x1 >= x1 = 1'(q1(x1))
     
     0(q2(0(x1))) = x1 + 4 >= x1 + 4 = q2(0(0(x1)))
     
     0'(q2(0(x1))) = x1 + 18 >= x1 + 18 = q2(0'(0(x1)))
     
     1'(q2(0(x1))) = x1 + 4 >= x1 + 4 = q2(1'(0(x1)))
     
     0(q2(1'(x1))) = x1 + 4 >= x1 + 4 = q2(0(1'(x1)))
     
     0'(q2(1'(x1))) = x1 + 18 >= x1 + 18 = q2(0'(1'(x1)))
     
     1'(q2(1'(x1))) = x1 + 4 >= x1 + 4 = q2(1'(1'(x1)))
     
     q2(0'(x1)) = x1 + 18 >= x1 + 14 = 0'(q0(x1))
     
     q3(1'(x1)) = x1 >= x1 = 1'(q3(x1))
     
     0(q1(1(x1))) = x1 + 7 >= x1 + 4 = q2(0(1'(x1)))
     
     0'(q1(1(x1))) = x1 + 21 >= x1 + 18 = q2(0'(1'(x1)))
     
     1'(q1(1(x1))) = x1 + 7 >= x1 + 4 = q2(1'(1'(x1)))
     
     q0(1'(x1)) = x1 >= x1 = 1'(q3(x1))
     
     q3(b(x1)) = x1 + 1 >= x1 + 1 = b(q4(x1))
    problem:
     strict:
      q0(0(x1)) -> 0'(q1(x1))
      q1(0(x1)) -> 0(q1(x1))
      q1(1'(x1)) -> 1'(q1(x1))
      0(q2(0(x1))) -> q2(0(0(x1)))
      0'(q2(0(x1))) -> q2(0'(0(x1)))
      1'(q2(0(x1))) -> q2(1'(0(x1)))
      0(q2(1'(x1))) -> q2(0(1'(x1)))
      0'(q2(1'(x1))) -> q2(0'(1'(x1)))
      1'(q2(1'(x1))) -> q2(1'(1'(x1)))
      q3(1'(x1)) -> 1'(q3(x1))
     weak:
      q2(0'(x1)) -> 0'(q0(x1))
      0(q1(1(x1))) -> q2(0(1'(x1)))
      0'(q1(1(x1))) -> q2(0'(1'(x1)))
      1'(q1(1(x1))) -> q2(1'(1'(x1)))
      q0(1'(x1)) -> 1'(q3(x1))
      q3(b(x1)) -> b(q4(x1))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [q4](x0) = x0,
      
      [b](x0) = x0 + 8,
      
      [q3](x0) = x0 + 7,
      
      [q2](x0) = x0 + 20,
      
      [1](x0) = x0 + 16,
      
      [1'](x0) = x0 + 4,
      
      [0'](x0) = x0 + 2,
      
      [q1](x0) = x0 + 8,
      
      [q0](x0) = x0 + 8,
      
      [0](x0) = x0 + 12
     orientation:
      q0(0(x1)) = x1 + 20 >= x1 + 10 = 0'(q1(x1))
      
      q1(0(x1)) = x1 + 20 >= x1 + 20 = 0(q1(x1))
      
      q1(1'(x1)) = x1 + 12 >= x1 + 12 = 1'(q1(x1))
      
      0(q2(0(x1))) = x1 + 44 >= x1 + 44 = q2(0(0(x1)))
      
      0'(q2(0(x1))) = x1 + 34 >= x1 + 34 = q2(0'(0(x1)))
      
      1'(q2(0(x1))) = x1 + 36 >= x1 + 36 = q2(1'(0(x1)))
      
      0(q2(1'(x1))) = x1 + 36 >= x1 + 36 = q2(0(1'(x1)))
      
      0'(q2(1'(x1))) = x1 + 26 >= x1 + 26 = q2(0'(1'(x1)))
      
      1'(q2(1'(x1))) = x1 + 28 >= x1 + 28 = q2(1'(1'(x1)))
      
      q3(1'(x1)) = x1 + 11 >= x1 + 11 = 1'(q3(x1))
      
      q2(0'(x1)) = x1 + 22 >= x1 + 10 = 0'(q0(x1))
      
      0(q1(1(x1))) = x1 + 36 >= x1 + 36 = q2(0(1'(x1)))
      
      0'(q1(1(x1))) = x1 + 26 >= x1 + 26 = q2(0'(1'(x1)))
      
      1'(q1(1(x1))) = x1 + 28 >= x1 + 28 = q2(1'(1'(x1)))
      
      q0(1'(x1)) = x1 + 12 >= x1 + 11 = 1'(q3(x1))
      
      q3(b(x1)) = x1 + 15 >= x1 + 8 = b(q4(x1))
     problem:
      strict:
       q1(0(x1)) -> 0(q1(x1))
       q1(1'(x1)) -> 1'(q1(x1))
       0(q2(0(x1))) -> q2(0(0(x1)))
       0'(q2(0(x1))) -> q2(0'(0(x1)))
       1'(q2(0(x1))) -> q2(1'(0(x1)))
       0(q2(1'(x1))) -> q2(0(1'(x1)))
       0'(q2(1'(x1))) -> q2(0'(1'(x1)))
       1'(q2(1'(x1))) -> q2(1'(1'(x1)))
       q3(1'(x1)) -> 1'(q3(x1))
      weak:
       q0(0(x1)) -> 0'(q1(x1))
       q2(0'(x1)) -> 0'(q0(x1))
       0(q1(1(x1))) -> q2(0(1'(x1)))
       0'(q1(1(x1))) -> q2(0'(1'(x1)))
       1'(q1(1(x1))) -> q2(1'(1'(x1)))
       q0(1'(x1)) -> 1'(q3(x1))
       q3(b(x1)) -> b(q4(x1))
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
                  [1 0]  
       [q4](x0) = [0 0]x0,
       
                 [1 0]     [4 ]
       [b](x0) = [0 0]x0 + [10],
       
                    
       [q3](x0) = x0,
       
                    
       [q2](x0) = x0,
       
                 [1 8]     [6]
       [1](x0) = [0 1]x0 + [2],
       
                       [0]
       [1'](x0) = x0 + [8],
       
                  [1 0]  
       [0'](x0) = [0 0]x0,
       
                  [1 1]     [0]
       [q1](x0) = [0 1]x0 + [6],
       
                       [0]
       [q0](x0) = x0 + [1],
       
                 [1 2]     [3 ]
       [0](x0) = [0 1]x0 + [12]
      orientation:
                   [1 3]     [15]    [1 3]     [15]            
       q1(0(x1)) = [0 1]x1 + [18] >= [0 1]x1 + [18] = 0(q1(x1))
       
                    [1 1]     [8 ]    [1 1]     [0 ]             
       q1(1'(x1)) = [0 1]x1 + [14] >= [0 1]x1 + [14] = 1'(q1(x1))
       
                      [1 4]     [30]    [1 4]     [30]               
       0(q2(0(x1))) = [0 1]x1 + [24] >= [0 1]x1 + [24] = q2(0(0(x1)))
       
                       [1 2]     [3]    [1 2]     [3]                
       0'(q2(0(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(0(x1)))
       
                       [1 2]     [3 ]    [1 2]     [3 ]                
       1'(q2(0(x1))) = [0 1]x1 + [20] >= [0 1]x1 + [20] = q2(1'(0(x1)))
       
                       [1 2]     [19]    [1 2]     [19]                
       0(q2(1'(x1))) = [0 1]x1 + [20] >= [0 1]x1 + [20] = q2(0(1'(x1)))
       
                        [1 0]      [1 0]                   
       0'(q2(1'(x1))) = [0 0]x1 >= [0 0]x1 = q2(0'(1'(x1)))
       
                             [0 ]         [0 ]                 
       1'(q2(1'(x1))) = x1 + [16] >= x1 + [16] = q2(1'(1'(x1)))
       
                         [0]         [0]             
       q3(1'(x1)) = x1 + [8] >= x1 + [8] = 1'(q3(x1))
       
                   [1 2]     [3 ]    [1 1]               
       q0(0(x1)) = [0 1]x1 + [13] >= [0 0]x1 = 0'(q1(x1))
       
                    [1 0]      [1 0]               
       q2(0'(x1)) = [0 0]x1 >= [0 0]x1 = 0'(q0(x1))
       
                      [1  11]     [27]    [1 2]     [19]                
       0(q1(1(x1))) = [0  1 ]x1 + [20] >= [0 1]x1 + [20] = q2(0(1'(x1)))
       
                       [1 9]     [8]    [1 0]                   
       0'(q1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 = q2(0'(1'(x1)))
       
                       [1 9]     [8 ]         [0 ]                 
       1'(q1(1(x1))) = [0 1]x1 + [16] >= x1 + [16] = q2(1'(1'(x1)))
       
                         [0]         [0]             
       q0(1'(x1)) = x1 + [9] >= x1 + [8] = 1'(q3(x1))
       
                   [1 0]     [4 ]    [1 0]     [4 ]            
       q3(b(x1)) = [0 0]x1 + [10] >= [0 0]x1 + [10] = b(q4(x1))
      problem:
       strict:
        q1(0(x1)) -> 0(q1(x1))
        0(q2(0(x1))) -> q2(0(0(x1)))
        0'(q2(0(x1))) -> q2(0'(0(x1)))
        1'(q2(0(x1))) -> q2(1'(0(x1)))
        0(q2(1'(x1))) -> q2(0(1'(x1)))
        0'(q2(1'(x1))) -> q2(0'(1'(x1)))
        1'(q2(1'(x1))) -> q2(1'(1'(x1)))
        q3(1'(x1)) -> 1'(q3(x1))
       weak:
        q1(1'(x1)) -> 1'(q1(x1))
        q0(0(x1)) -> 0'(q1(x1))
        q2(0'(x1)) -> 0'(q0(x1))
        0(q1(1(x1))) -> q2(0(1'(x1)))
        0'(q1(1(x1))) -> q2(0'(1'(x1)))
        1'(q1(1(x1))) -> q2(1'(1'(x1)))
        q0(1'(x1)) -> 1'(q3(x1))
        q3(b(x1)) -> b(q4(x1))
      Matrix Interpretation Processor:
       dimension: 2
       interpretation:
                   [1 9]  
        [q4](x0) = [0 0]x0,
        
                  [1  12]     [4]
        [b](x0) = [0  1 ]x0 + [0],
        
                   [1 7]  
        [q3](x0) = [0 0]x0,
        
                   [1 8]     [0]
        [q2](x0) = [0 1]x0 + [2],
        
                  [1 9]     [7]
        [1](x0) = [0 1]x0 + [2],
        
                     
        [1'](x0) = x0,
        
                   [1 1]  
        [0'](x0) = [0 1]x0,
        
                   [1 8]  
        [q1](x0) = [0 1]x0,
        
                   [1 7]  
        [q0](x0) = [0 1]x0,
        
                  [1 4]  
        [0](x0) = [0 1]x0
       orientation:
                    [1  12]      [1  12]              
        q1(0(x1)) = [0  1 ]x1 >= [0  1 ]x1 = 0(q1(x1))
        
                       [1  16]     [8]    [1  16]     [0]               
        0(q2(0(x1))) = [0  1 ]x1 + [2] >= [0  1 ]x1 + [2] = q2(0(0(x1)))
        
                        [1  13]     [2]    [1  13]     [0]                
        0'(q2(0(x1))) = [0  1 ]x1 + [2] >= [0  1 ]x1 + [2] = q2(0'(0(x1)))
        
                        [1  12]     [0]    [1  12]     [0]                
        1'(q2(0(x1))) = [0  1 ]x1 + [2] >= [0  1 ]x1 + [2] = q2(1'(0(x1)))
        
                        [1  12]     [8]    [1  12]     [0]                
        0(q2(1'(x1))) = [0  1 ]x1 + [2] >= [0  1 ]x1 + [2] = q2(0(1'(x1)))
        
                         [1 9]     [2]    [1 9]     [0]                 
        0'(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
        
                         [1 8]     [0]    [1 8]     [0]                 
        1'(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(1'(1'(x1)))
        
                     [1 7]      [1 7]               
        q3(1'(x1)) = [0 0]x1 >= [0 0]x1 = 1'(q3(x1))
        
                     [1 8]      [1 8]               
        q1(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q1(x1))
        
                    [1  11]      [1 9]               
        q0(0(x1)) = [0  1 ]x1 >= [0 1]x1 = 0'(q1(x1))
        
                     [1 9]     [0]    [1 8]               
        q2(0'(x1)) = [0 1]x1 + [2] >= [0 1]x1 = 0'(q0(x1))
        
                       [1  21]     [31]    [1  12]     [0]                
        0(q1(1(x1))) = [0  1 ]x1 + [2 ] >= [0  1 ]x1 + [2] = q2(0(1'(x1)))
        
                        [1  18]     [25]    [1 9]     [0]                 
        0'(q1(1(x1))) = [0  1 ]x1 + [2 ] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
        
                        [1  17]     [23]    [1 8]     [0]                 
        1'(q1(1(x1))) = [0  1 ]x1 + [2 ] >= [0 1]x1 + [2] = q2(1'(1'(x1)))
        
                     [1 7]      [1 7]               
        q0(1'(x1)) = [0 1]x1 >= [0 0]x1 = 1'(q3(x1))
        
                    [1  19]     [4]    [1 9]     [4]            
        q3(b(x1)) = [0  0 ]x1 + [0] >= [0 0]x1 + [0] = b(q4(x1))
       problem:
        strict:
         q1(0(x1)) -> 0(q1(x1))
         1'(q2(0(x1))) -> q2(1'(0(x1)))
         1'(q2(1'(x1))) -> q2(1'(1'(x1)))
         q3(1'(x1)) -> 1'(q3(x1))
        weak:
         0(q2(0(x1))) -> q2(0(0(x1)))
         0'(q2(0(x1))) -> q2(0'(0(x1)))
         0(q2(1'(x1))) -> q2(0(1'(x1)))
         0'(q2(1'(x1))) -> q2(0'(1'(x1)))
         q1(1'(x1)) -> 1'(q1(x1))
         q0(0(x1)) -> 0'(q1(x1))
         q2(0'(x1)) -> 0'(q0(x1))
         0(q1(1(x1))) -> q2(0(1'(x1)))
         0'(q1(1(x1))) -> q2(0'(1'(x1)))
         1'(q1(1(x1))) -> q2(1'(1'(x1)))
         q0(1'(x1)) -> 1'(q3(x1))
         q3(b(x1)) -> b(q4(x1))
       Matrix Interpretation Processor:
        dimension: 2
        interpretation:
                    [1 0]  
         [q4](x0) = [0 0]x0,
         
                   [1 0]  
         [b](x0) = [0 0]x0,
         
                    [1 8]  
         [q3](x0) = [0 0]x0,
         
                         [0]
         [q2](x0) = x0 + [2],
         
                   [1  15]     [0]
         [1](x0) = [0  1 ]x0 + [3],
         
                    [1 8]  
         [1'](x0) = [0 1]x0,
         
                         [0]
         [0'](x0) = x0 + [2],
         
                      
         [q1](x0) = x0,
         
                         [0]
         [q0](x0) = x0 + [2],
         
                        [9]
         [0](x0) = x0 + [0]
        orientation:
                          [9]         [9]            
         q1(0(x1)) = x1 + [0] >= x1 + [0] = 0(q1(x1))
         
                         [1 8]     [25]    [1 8]     [9]                
         1'(q2(0(x1))) = [0 1]x1 + [2 ] >= [0 1]x1 + [2] = q2(1'(0(x1)))
         
                          [1  16]     [16]    [1  16]     [0]                 
         1'(q2(1'(x1))) = [0  1 ]x1 + [2 ] >= [0  1 ]x1 + [2] = q2(1'(1'(x1)))
         
                      [1  16]      [1 8]               
         q3(1'(x1)) = [0  0 ]x1 >= [0 0]x1 = 1'(q3(x1))
         
                             [18]         [18]               
         0(q2(0(x1))) = x1 + [2 ] >= x1 + [2 ] = q2(0(0(x1)))
         
                              [9]         [9]                
         0'(q2(0(x1))) = x1 + [4] >= x1 + [4] = q2(0'(0(x1)))
         
                         [1 8]     [9]    [1 8]     [9]                
         0(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0(1'(x1)))
         
                          [1 8]     [0]    [1 8]     [0]                 
         0'(q2(1'(x1))) = [0 1]x1 + [4] >= [0 1]x1 + [4] = q2(0'(1'(x1)))
         
                      [1 8]      [1 8]               
         q1(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q1(x1))
         
                          [9]         [0]             
         q0(0(x1)) = x1 + [2] >= x1 + [2] = 0'(q1(x1))
         
                           [0]         [0]             
         q2(0'(x1)) = x1 + [4] >= x1 + [4] = 0'(q0(x1))
         
                        [1  15]     [9]    [1 8]     [9]                
         0(q1(1(x1))) = [0  1 ]x1 + [3] >= [0 1]x1 + [2] = q2(0(1'(x1)))
         
                         [1  15]     [0]    [1 8]     [0]                 
         0'(q1(1(x1))) = [0  1 ]x1 + [5] >= [0 1]x1 + [4] = q2(0'(1'(x1)))
         
                         [1  23]     [24]    [1  16]     [0]                 
         1'(q1(1(x1))) = [0  1 ]x1 + [3 ] >= [0  1 ]x1 + [2] = q2(1'(1'(x1)))
         
                      [1 8]     [0]    [1 8]               
         q0(1'(x1)) = [0 1]x1 + [2] >= [0 0]x1 = 1'(q3(x1))
         
                     [1 0]      [1 0]              
         q3(b(x1)) = [0 0]x1 >= [0 0]x1 = b(q4(x1))
        problem:
         strict:
          q1(0(x1)) -> 0(q1(x1))
          q3(1'(x1)) -> 1'(q3(x1))
         weak:
          1'(q2(0(x1))) -> q2(1'(0(x1)))
          1'(q2(1'(x1))) -> q2(1'(1'(x1)))
          0(q2(0(x1))) -> q2(0(0(x1)))
          0'(q2(0(x1))) -> q2(0'(0(x1)))
          0(q2(1'(x1))) -> q2(0(1'(x1)))
          0'(q2(1'(x1))) -> q2(0'(1'(x1)))
          q1(1'(x1)) -> 1'(q1(x1))
          q0(0(x1)) -> 0'(q1(x1))
          q2(0'(x1)) -> 0'(q0(x1))
          0(q1(1(x1))) -> q2(0(1'(x1)))
          0'(q1(1(x1))) -> q2(0'(1'(x1)))
          1'(q1(1(x1))) -> q2(1'(1'(x1)))
          q0(1'(x1)) -> 1'(q3(x1))
          q3(b(x1)) -> b(q4(x1))
        Matrix Interpretation Processor:
         dimension: 2
         interpretation:
                     [1 0]     [8]
          [q4](x0) = [0 0]x0 + [8],
          
                    [1 1]     [0]
          [b](x0) = [0 0]x0 + [3],
          
                     [1 4]     [4]
          [q3](x0) = [0 1]x0 + [0],
          
                     [1 8]     [0]
          [q2](x0) = [0 1]x0 + [2],
          
                    [1 9]     [1]
          [1](x0) = [0 1]x0 + [3],
          
                     [1 4]     [3]
          [1'](x0) = [0 1]x0 + [1],
          
                     [1 6]     [0]
          [0'](x0) = [0 1]x0 + [1],
          
                     [1 4]  
          [q1](x0) = [0 1]x0,
          
                     [1 8]     [8]
          [q0](x0) = [0 1]x0 + [0],
          
                    [1 4]     [0]
          [0](x0) = [0 1]x0 + [1]
         orientation:
                      [1 8]     [4]    [1 8]     [0]            
          q1(0(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(q1(x1))
          
                       [1 8]     [11]    [1 8]     [7]             
          q3(1'(x1)) = [0 1]x1 + [1 ] >= [0 1]x1 + [1] = 1'(q3(x1))
          
                          [1  16]     [23]    [1  16]     [23]                
          1'(q2(0(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(1'(0(x1)))
          
                           [1  16]     [26]    [1  16]     [26]                 
          1'(q2(1'(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(1'(1'(x1)))
          
                         [1  16]     [20]    [1  16]     [20]               
          0(q2(0(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(0(0(x1)))
          
                          [1  18]     [26]    [1  18]     [22]                
          0'(q2(0(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(0'(0(x1)))
          
                          [1  16]     [23]    [1  16]     [23]                
          0(q2(1'(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(0(1'(x1)))
          
                           [1  18]     [29]    [1  18]     [25]                 
          0'(q2(1'(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(0'(1'(x1)))
          
                       [1 8]     [7]    [1 8]     [3]             
          q1(1'(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1'(q1(x1))
          
                      [1  12]     [16]    [1  10]     [0]             
          q0(0(x1)) = [0  1 ]x1 + [1 ] >= [0  1 ]x1 + [1] = 0'(q1(x1))
          
                       [1  14]     [8]    [1  14]     [8]             
          q2(0'(x1)) = [0  1 ]x1 + [3] >= [0  1 ]x1 + [1] = 0'(q0(x1))
          
                         [1  17]     [25]    [1  16]     [23]                
          0(q1(1(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(0(1'(x1)))
          
                          [1  19]     [31]    [1  18]     [25]                 
          0'(q1(1(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(0'(1'(x1)))
          
                          [1  17]     [28]    [1  16]     [26]                 
          1'(q1(1(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = q2(1'(1'(x1)))
          
                       [1  12]     [19]    [1 8]     [7]             
          q0(1'(x1)) = [0  1 ]x1 + [1 ] >= [0 1]x1 + [1] = 1'(q3(x1))
          
                      [1 1]     [16]    [1 0]     [16]            
          q3(b(x1)) = [0 0]x1 + [3 ] >= [0 0]x1 + [3 ] = b(q4(x1))
         problem:
          strict:
           
          weak:
           q1(0(x1)) -> 0(q1(x1))
           q3(1'(x1)) -> 1'(q3(x1))
           1'(q2(0(x1))) -> q2(1'(0(x1)))
           1'(q2(1'(x1))) -> q2(1'(1'(x1)))
           0(q2(0(x1))) -> q2(0(0(x1)))
           0'(q2(0(x1))) -> q2(0'(0(x1)))
           0(q2(1'(x1))) -> q2(0(1'(x1)))
           0'(q2(1'(x1))) -> q2(0'(1'(x1)))
           q1(1'(x1)) -> 1'(q1(x1))
           q0(0(x1)) -> 0'(q1(x1))
           q2(0'(x1)) -> 0'(q0(x1))
           0(q1(1(x1))) -> q2(0(1'(x1)))
           0'(q1(1(x1))) -> q2(0'(1'(x1)))
           1'(q1(1(x1))) -> q2(1'(1'(x1)))
           q0(1'(x1)) -> 1'(q3(x1))
           q3(b(x1)) -> b(q4(x1))
         Qed