YES

Problem:
 r0(0(x1)) -> 0(r0(x1))
 r0(1(x1)) -> 1(r0(x1))
 r0(m(x1)) -> m(r0(x1))
 r1(0(x1)) -> 0(r1(x1))
 r1(1(x1)) -> 1(r1(x1))
 r1(m(x1)) -> m(r1(x1))
 r0(b(x1)) -> qr(0(b(x1)))
 r1(b(x1)) -> qr(1(b(x1)))
 0(qr(x1)) -> qr(0(x1))
 1(qr(x1)) -> qr(1(x1))
 m(qr(x1)) -> ql(m(x1))
 0(ql(x1)) -> ql(0(x1))
 1(ql(x1)) -> ql(1(x1))
 b(ql(0(x1))) -> 0(b(r0(x1)))
 b(ql(1(x1))) -> 1(b(r1(x1)))

Proof:
 String Reversal Processor:
  0(r0(x1)) -> r0(0(x1))
  1(r0(x1)) -> r0(1(x1))
  m(r0(x1)) -> r0(m(x1))
  0(r1(x1)) -> r1(0(x1))
  1(r1(x1)) -> r1(1(x1))
  m(r1(x1)) -> r1(m(x1))
  b(r0(x1)) -> b(0(qr(x1)))
  b(r1(x1)) -> b(1(qr(x1)))
  qr(0(x1)) -> 0(qr(x1))
  qr(1(x1)) -> 1(qr(x1))
  qr(m(x1)) -> m(ql(x1))
  ql(0(x1)) -> 0(ql(x1))
  ql(1(x1)) -> 1(ql(x1))
  0(ql(b(x1))) -> r0(b(0(x1)))
  1(ql(b(x1))) -> r1(b(1(x1)))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
               [1 0 0]  
    [ql](x0) = [0 0 0]x0
               [0 0 1]  ,
    
                 
    [qr](x0) = x0
                 ,
    
              [1 0 0]  
    [b](x0) = [0 0 0]x0
              [1 0 0]  ,
    
               [1 0 0]  
    [r1](x0) = [0 0 0]x0
               [0 0 1]  ,
    
              [1 0 1]  
    [m](x0) = [0 1 0]x0
              [0 0 1]  ,
    
              [1 0 0]  
    [1](x0) = [0 0 0]x0
              [0 0 1]  ,
    
               [1 0 0]     [0]
    [r0](x0) = [0 0 0]x0 + [0]
               [0 0 1]     [1],
    
              [1 0 0]     [0]
    [0](x0) = [0 0 0]x0 + [0]
              [0 0 1]     [1]
   orientation:
                [1 0 0]     [0]    [1 0 0]     [0]            
    0(r0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = r0(0(x1))
                [0 0 1]     [2]    [0 0 1]     [2]            
    
                [1 0 0]     [0]    [1 0 0]     [0]            
    1(r0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = r0(1(x1))
                [0 0 1]     [1]    [0 0 1]     [1]            
    
                [1 0 1]     [1]    [1 0 1]     [0]            
    m(r0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = r0(m(x1))
                [0 0 1]     [1]    [0 0 1]     [1]            
    
                [1 0 0]     [0]    [1 0 0]     [0]            
    0(r1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = r1(0(x1))
                [0 0 1]     [1]    [0 0 1]     [1]            
    
                [1 0 0]      [1 0 0]              
    1(r1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = r1(1(x1))
                [0 0 1]      [0 0 1]              
    
                [1 0 1]      [1 0 1]              
    m(r1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = r1(m(x1))
                [0 0 1]      [0 0 1]              
    
                [1 0 0]      [1 0 0]                 
    b(r0(x1)) = [0 0 0]x1 >= [0 0 0]x1 = b(0(qr(x1)))
                [1 0 0]      [1 0 0]                 
    
                [1 0 0]      [1 0 0]                 
    b(r1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = b(1(qr(x1)))
                [1 0 0]      [1 0 0]                 
    
                [1 0 0]     [0]    [1 0 0]     [0]            
    qr(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(qr(x1))
                [0 0 1]     [1]    [0 0 1]     [1]            
    
                [1 0 0]      [1 0 0]              
    qr(1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 1(qr(x1))
                [0 0 1]      [0 0 1]              
    
                [1 0 1]      [1 0 1]              
    qr(m(x1)) = [0 1 0]x1 >= [0 0 0]x1 = m(ql(x1))
                [0 0 1]      [0 0 1]              
    
                [1 0 0]     [0]    [1 0 0]     [0]            
    ql(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(ql(x1))
                [0 0 1]     [1]    [0 0 1]     [1]            
    
                [1 0 0]      [1 0 0]              
    ql(1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 1(ql(x1))
                [0 0 1]      [0 0 1]              
    
                   [1 0 0]     [0]    [1 0 0]     [0]               
    0(ql(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = r0(b(0(x1)))
                   [1 0 0]     [1]    [1 0 0]     [1]               
    
                   [1 0 0]      [1 0 0]                 
    1(ql(b(x1))) = [0 0 0]x1 >= [0 0 0]x1 = r1(b(1(x1)))
                   [1 0 0]      [1 0 0]                 
   problem:
    0(r0(x1)) -> r0(0(x1))
    1(r0(x1)) -> r0(1(x1))
    0(r1(x1)) -> r1(0(x1))
    1(r1(x1)) -> r1(1(x1))
    m(r1(x1)) -> r1(m(x1))
    b(r0(x1)) -> b(0(qr(x1)))
    b(r1(x1)) -> b(1(qr(x1)))
    qr(0(x1)) -> 0(qr(x1))
    qr(1(x1)) -> 1(qr(x1))
    qr(m(x1)) -> m(ql(x1))
    ql(0(x1)) -> 0(ql(x1))
    ql(1(x1)) -> 1(ql(x1))
    0(ql(b(x1))) -> r0(b(0(x1)))
    1(ql(b(x1))) -> r1(b(1(x1)))
   String Reversal Processor:
    r0(0(x1)) -> 0(r0(x1))
    r0(1(x1)) -> 1(r0(x1))
    r1(0(x1)) -> 0(r1(x1))
    r1(1(x1)) -> 1(r1(x1))
    r1(m(x1)) -> m(r1(x1))
    r0(b(x1)) -> qr(0(b(x1)))
    r1(b(x1)) -> qr(1(b(x1)))
    0(qr(x1)) -> qr(0(x1))
    1(qr(x1)) -> qr(1(x1))
    m(qr(x1)) -> ql(m(x1))
    0(ql(x1)) -> ql(0(x1))
    1(ql(x1)) -> ql(1(x1))
    b(ql(0(x1))) -> 0(b(r0(x1)))
    b(ql(1(x1))) -> 1(b(r1(x1)))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                   
      [ql](x0) = x0
                   ,
      
                 [1 0 0]  
      [qr](x0) = [0 0 0]x0
                 [0 0 0]  ,
      
                [1 1 1]     [0]
      [b](x0) = [0 0 0]x0 + [1]
                [0 0 0]     [1],
      
                 [1 0 0]  
      [r1](x0) = [0 0 0]x0
                 [0 0 0]  ,
      
                [1 0 0]  
      [m](x0) = [0 0 0]x0
                [0 0 0]  ,
      
                [1 0 0]  
      [1](x0) = [0 0 1]x0
                [0 1 0]  ,
      
                 [1 1 1]  
      [r0](x0) = [0 0 0]x0
                 [0 0 0]  ,
      
                [1 0 0]  
      [0](x0) = [0 0 1]x0
                [0 1 0]  
     orientation:
                  [1 1 1]      [1 1 1]              
      r0(0(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 0(r0(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 1 1]      [1 1 1]              
      r0(1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 1(r0(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 0 0]      [1 0 0]              
      r1(0(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 0(r1(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 0 0]      [1 0 0]              
      r1(1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 1(r1(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 0 0]      [1 0 0]              
      r1(m(x1)) = [0 0 0]x1 >= [0 0 0]x1 = m(r1(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 1 1]     [2]    [1 1 1]                 
      r0(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = qr(0(b(x1)))
                  [0 0 0]     [0]    [0 0 0]                 
      
                  [1 1 1]      [1 1 1]                 
      r1(b(x1)) = [0 0 0]x1 >= [0 0 0]x1 = qr(1(b(x1)))
                  [0 0 0]      [0 0 0]                 
      
                  [1 0 0]      [1 0 0]              
      0(qr(x1)) = [0 0 0]x1 >= [0 0 0]x1 = qr(0(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 0 0]      [1 0 0]              
      1(qr(x1)) = [0 0 0]x1 >= [0 0 0]x1 = qr(1(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 0 0]      [1 0 0]              
      m(qr(x1)) = [0 0 0]x1 >= [0 0 0]x1 = ql(m(x1))
                  [0 0 0]      [0 0 0]              
      
                  [1 0 0]      [1 0 0]              
      0(ql(x1)) = [0 0 1]x1 >= [0 0 1]x1 = ql(0(x1))
                  [0 1 0]      [0 1 0]              
      
                  [1 0 0]      [1 0 0]              
      1(ql(x1)) = [0 0 1]x1 >= [0 0 1]x1 = ql(1(x1))
                  [0 1 0]      [0 1 0]              
      
                     [1 1 1]     [0]    [1 1 1]     [0]               
      b(ql(0(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(b(r0(x1)))
                     [0 0 0]     [1]    [0 0 0]     [1]               
      
                     [1 1 1]     [0]    [1 0 0]     [0]               
      b(ql(1(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 1(b(r1(x1)))
                     [0 0 0]     [1]    [0 0 0]     [1]               
     problem:
      r0(0(x1)) -> 0(r0(x1))
      r0(1(x1)) -> 1(r0(x1))
      r1(0(x1)) -> 0(r1(x1))
      r1(1(x1)) -> 1(r1(x1))
      r1(m(x1)) -> m(r1(x1))
      r1(b(x1)) -> qr(1(b(x1)))
      0(qr(x1)) -> qr(0(x1))
      1(qr(x1)) -> qr(1(x1))
      m(qr(x1)) -> ql(m(x1))
      0(ql(x1)) -> ql(0(x1))
      1(ql(x1)) -> ql(1(x1))
      b(ql(0(x1))) -> 0(b(r0(x1)))
      b(ql(1(x1))) -> 1(b(r1(x1)))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [ql](x0) = 1x0,
       
       [qr](x0) = 1x0,
       
       [b](x0) = x0,
       
       [r1](x0) = 1x0,
       
       [m](x0) = 4x0,
       
       [1](x0) = x0,
       
       [r0](x0) = x0,
       
       [0](x0) = 9x0
      orientation:
       r0(0(x1)) = 9x1 >= 9x1 = 0(r0(x1))
       
       r0(1(x1)) = x1 >= x1 = 1(r0(x1))
       
       r1(0(x1)) = 10x1 >= 10x1 = 0(r1(x1))
       
       r1(1(x1)) = 1x1 >= 1x1 = 1(r1(x1))
       
       r1(m(x1)) = 5x1 >= 5x1 = m(r1(x1))
       
       r1(b(x1)) = 1x1 >= 1x1 = qr(1(b(x1)))
       
       0(qr(x1)) = 10x1 >= 10x1 = qr(0(x1))
       
       1(qr(x1)) = 1x1 >= 1x1 = qr(1(x1))
       
       m(qr(x1)) = 5x1 >= 5x1 = ql(m(x1))
       
       0(ql(x1)) = 10x1 >= 10x1 = ql(0(x1))
       
       1(ql(x1)) = 1x1 >= 1x1 = ql(1(x1))
       
       b(ql(0(x1))) = 10x1 >= 9x1 = 0(b(r0(x1)))
       
       b(ql(1(x1))) = 1x1 >= 1x1 = 1(b(r1(x1)))
      problem:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(1(x1))) -> 1(b(r1(x1)))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [ql](x0) = x0 + 14,
        
        [qr](x0) = x0 + 14,
        
        [b](x0) = 2x0,
        
        [r1](x0) = x0 + 14,
        
        [m](x0) = x0,
        
        [1](x0) = x0,
        
        [r0](x0) = 8x0 + 3,
        
        [0](x0) = x0 + 1
       orientation:
        r0(0(x1)) = 8x1 + 11 >= 8x1 + 4 = 0(r0(x1))
        
        r0(1(x1)) = 8x1 + 3 >= 8x1 + 3 = 1(r0(x1))
        
        r1(0(x1)) = x1 + 15 >= x1 + 15 = 0(r1(x1))
        
        r1(1(x1)) = x1 + 14 >= x1 + 14 = 1(r1(x1))
        
        r1(m(x1)) = x1 + 14 >= x1 + 14 = m(r1(x1))
        
        r1(b(x1)) = 2x1 + 14 >= 2x1 + 14 = qr(1(b(x1)))
        
        0(qr(x1)) = x1 + 15 >= x1 + 15 = qr(0(x1))
        
        1(qr(x1)) = x1 + 14 >= x1 + 14 = qr(1(x1))
        
        m(qr(x1)) = x1 + 14 >= x1 + 14 = ql(m(x1))
        
        0(ql(x1)) = x1 + 15 >= x1 + 15 = ql(0(x1))
        
        1(ql(x1)) = x1 + 14 >= x1 + 14 = ql(1(x1))
        
        b(ql(1(x1))) = 2x1 + 28 >= 2x1 + 28 = 1(b(r1(x1)))
       problem:
        r0(1(x1)) -> 1(r0(x1))
        r1(0(x1)) -> 0(r1(x1))
        r1(1(x1)) -> 1(r1(x1))
        r1(m(x1)) -> m(r1(x1))
        r1(b(x1)) -> qr(1(b(x1)))
        0(qr(x1)) -> qr(0(x1))
        1(qr(x1)) -> qr(1(x1))
        m(qr(x1)) -> ql(m(x1))
        0(ql(x1)) -> ql(0(x1))
        1(ql(x1)) -> ql(1(x1))
        b(ql(1(x1))) -> 1(b(r1(x1)))
       String Reversal Processor:
        1(r0(x1)) -> r0(1(x1))
        0(r1(x1)) -> r1(0(x1))
        1(r1(x1)) -> r1(1(x1))
        m(r1(x1)) -> r1(m(x1))
        b(r1(x1)) -> b(1(qr(x1)))
        qr(0(x1)) -> 0(qr(x1))
        qr(1(x1)) -> 1(qr(x1))
        qr(m(x1)) -> m(ql(x1))
        ql(0(x1)) -> 0(ql(x1))
        ql(1(x1)) -> 1(ql(x1))
        1(ql(b(x1))) -> r1(b(1(x1)))
        Matrix Interpretation Processor: dim=3
         
         interpretation:
                       
          [ql](x0) = x0
                       ,
          
                       
          [qr](x0) = x0
                       ,
          
                    [1 0 0]  
          [b](x0) = [0 0 0]x0
                    [0 0 0]  ,
          
                     [1 0 0]     [0]
          [r1](x0) = [0 0 1]x0 + [1]
                     [0 1 0]     [0],
          
                    [1 1 1]  
          [m](x0) = [0 1 0]x0
                    [0 0 1]  ,
          
                    [1 0 0]     [0]
          [1](x0) = [0 0 1]x0 + [1]
                    [0 1 0]     [0],
          
                     [1 0 0]  
          [r0](x0) = [0 0 0]x0
                     [0 0 0]  ,
          
                    [1 0 0]     [0]
          [0](x0) = [0 0 1]x0 + [1]
                    [0 1 0]     [0]
         orientation:
                      [1 0 0]     [0]    [1 0 0]              
          1(r0(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = r0(1(x1))
                      [0 0 0]     [0]    [0 0 0]              
          
                           [0]         [0]            
          0(r1(x1)) = x1 + [1] >= x1 + [1] = r1(0(x1))
                           [1]         [1]            
          
                           [0]         [0]            
          1(r1(x1)) = x1 + [1] >= x1 + [1] = r1(1(x1))
                           [1]         [1]            
          
                      [1 1 1]     [1]    [1 1 1]     [0]            
          m(r1(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = r1(m(x1))
                      [0 1 0]     [0]    [0 1 0]     [0]            
          
                      [1 0 0]      [1 0 0]                 
          b(r1(x1)) = [0 0 0]x1 >= [0 0 0]x1 = b(1(qr(x1)))
                      [0 0 0]      [0 0 0]                 
          
                      [1 0 0]     [0]    [1 0 0]     [0]            
          qr(0(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = 0(qr(x1))
                      [0 1 0]     [0]    [0 1 0]     [0]            
          
                      [1 0 0]     [0]    [1 0 0]     [0]            
          qr(1(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = 1(qr(x1))
                      [0 1 0]     [0]    [0 1 0]     [0]            
          
                      [1 1 1]      [1 1 1]              
          qr(m(x1)) = [0 1 0]x1 >= [0 1 0]x1 = m(ql(x1))
                      [0 0 1]      [0 0 1]              
          
                      [1 0 0]     [0]    [1 0 0]     [0]            
          ql(0(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = 0(ql(x1))
                      [0 1 0]     [0]    [0 1 0]     [0]            
          
                      [1 0 0]     [0]    [1 0 0]     [0]            
          ql(1(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = 1(ql(x1))
                      [0 1 0]     [0]    [0 1 0]     [0]            
          
                         [1 0 0]     [0]    [1 0 0]     [0]               
          1(ql(b(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r1(b(1(x1)))
                         [0 0 0]     [0]    [0 0 0]     [0]               
         problem:
          1(r0(x1)) -> r0(1(x1))
          0(r1(x1)) -> r1(0(x1))
          1(r1(x1)) -> r1(1(x1))
          b(r1(x1)) -> b(1(qr(x1)))
          qr(0(x1)) -> 0(qr(x1))
          qr(1(x1)) -> 1(qr(x1))
          qr(m(x1)) -> m(ql(x1))
          ql(0(x1)) -> 0(ql(x1))
          ql(1(x1)) -> 1(ql(x1))
          1(ql(b(x1))) -> r1(b(1(x1)))
         String Reversal Processor:
          r0(1(x1)) -> 1(r0(x1))
          r1(0(x1)) -> 0(r1(x1))
          r1(1(x1)) -> 1(r1(x1))
          r1(b(x1)) -> qr(1(b(x1)))
          0(qr(x1)) -> qr(0(x1))
          1(qr(x1)) -> qr(1(x1))
          m(qr(x1)) -> ql(m(x1))
          0(ql(x1)) -> ql(0(x1))
          1(ql(x1)) -> ql(1(x1))
          b(ql(1(x1))) -> 1(b(r1(x1)))
          Matrix Interpretation Processor: dim=3
           
           interpretation:
                       [1 0 0]  
            [ql](x0) = [0 0 0]x0
                       [0 0 1]  ,
            
                       [1 0 0]  
            [qr](x0) = [0 0 0]x0
                       [0 0 0]  ,
            
                      [1 0 0]  
            [b](x0) = [1 0 0]x0
                      [0 0 1]  ,
            
                       [1 0 0]  
            [r1](x0) = [0 0 0]x0
                       [0 0 1]  ,
            
                      [1 0 0]  
            [m](x0) = [1 0 0]x0
                      [0 0 0]  ,
            
                      [1 0 0]     [0]
            [1](x0) = [0 0 0]x0 + [0]
                      [0 0 1]     [1],
            
                       [1 0 1]     [0]
            [r0](x0) = [0 0 0]x0 + [0]
                       [0 0 1]     [1],
            
                      [1 0 0]  
            [0](x0) = [0 0 0]x0
                      [1 0 0]  
           orientation:
                        [1 0 1]     [1]    [1 0 1]     [0]            
            r0(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(r0(x1))
                        [0 0 1]     [2]    [0 0 1]     [2]            
            
                        [1 0 0]      [1 0 0]              
            r1(0(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 0(r1(x1))
                        [1 0 0]      [1 0 0]              
            
                        [1 0 0]     [0]    [1 0 0]     [0]            
            r1(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(r1(x1))
                        [0 0 1]     [1]    [0 0 1]     [1]            
            
                        [1 0 0]      [1 0 0]                 
            r1(b(x1)) = [0 0 0]x1 >= [0 0 0]x1 = qr(1(b(x1)))
                        [0 0 1]      [0 0 0]                 
            
                        [1 0 0]      [1 0 0]              
            0(qr(x1)) = [0 0 0]x1 >= [0 0 0]x1 = qr(0(x1))
                        [1 0 0]      [0 0 0]              
            
                        [1 0 0]     [0]    [1 0 0]              
            1(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = qr(1(x1))
                        [0 0 0]     [1]    [0 0 0]              
            
                        [1 0 0]      [1 0 0]              
            m(qr(x1)) = [1 0 0]x1 >= [0 0 0]x1 = ql(m(x1))
                        [0 0 0]      [0 0 0]              
            
                        [1 0 0]      [1 0 0]              
            0(ql(x1)) = [0 0 0]x1 >= [0 0 0]x1 = ql(0(x1))
                        [1 0 0]      [1 0 0]              
            
                        [1 0 0]     [0]    [1 0 0]     [0]            
            1(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(1(x1))
                        [0 0 1]     [1]    [0 0 1]     [1]            
            
                           [1 0 0]     [0]    [1 0 0]     [0]               
            b(ql(1(x1))) = [1 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(b(r1(x1)))
                           [0 0 1]     [1]    [0 0 1]     [1]               
           problem:
            r1(0(x1)) -> 0(r1(x1))
            r1(1(x1)) -> 1(r1(x1))
            r1(b(x1)) -> qr(1(b(x1)))
            0(qr(x1)) -> qr(0(x1))
            1(qr(x1)) -> qr(1(x1))
            m(qr(x1)) -> ql(m(x1))
            0(ql(x1)) -> ql(0(x1))
            1(ql(x1)) -> ql(1(x1))
            b(ql(1(x1))) -> 1(b(r1(x1)))
           String Reversal Processor:
            0(r1(x1)) -> r1(0(x1))
            1(r1(x1)) -> r1(1(x1))
            b(r1(x1)) -> b(1(qr(x1)))
            qr(0(x1)) -> 0(qr(x1))
            qr(1(x1)) -> 1(qr(x1))
            qr(m(x1)) -> m(ql(x1))
            ql(0(x1)) -> 0(ql(x1))
            ql(1(x1)) -> 1(ql(x1))
            1(ql(b(x1))) -> r1(b(1(x1)))
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [ql](x0) = 2x0 + 1,
              
              [qr](x0) = 2x0,
              
              [b](x0) = x0,
              
              [r1](x0) = 2x0,
              
              [m](x0) = 2x0 + 2,
              
              [1](x0) = x0,
              
              [0](x0) = x0
             orientation:
              0(r1(x1)) = 2x1 >= 2x1 = r1(0(x1))
              
              1(r1(x1)) = 2x1 >= 2x1 = r1(1(x1))
              
              b(r1(x1)) = 2x1 >= 2x1 = b(1(qr(x1)))
              
              qr(0(x1)) = 2x1 >= 2x1 = 0(qr(x1))
              
              qr(1(x1)) = 2x1 >= 2x1 = 1(qr(x1))
              
              qr(m(x1)) = 4x1 + 4 >= 4x1 + 4 = m(ql(x1))
              
              ql(0(x1)) = 2x1 + 1 >= 2x1 + 1 = 0(ql(x1))
              
              ql(1(x1)) = 2x1 + 1 >= 2x1 + 1 = 1(ql(x1))
              
              1(ql(b(x1))) = 2x1 + 1 >= 2x1 = r1(b(1(x1)))
             problem:
              0(r1(x1)) -> r1(0(x1))
              1(r1(x1)) -> r1(1(x1))
              b(r1(x1)) -> b(1(qr(x1)))
              qr(0(x1)) -> 0(qr(x1))
              qr(1(x1)) -> 1(qr(x1))
              qr(m(x1)) -> m(ql(x1))
              ql(0(x1)) -> 0(ql(x1))
              ql(1(x1)) -> 1(ql(x1))
             Arctic Interpretation Processor:
              dimension: 1
              interpretation:
               [ql](x0) = x0,
               
               [qr](x0) = 3x0,
               
               [b](x0) = 2x0,
               
               [r1](x0) = 8x0,
               
               [m](x0) = 12x0,
               
               [1](x0) = 1x0,
               
               [0](x0) = x0
              orientation:
               0(r1(x1)) = 8x1 >= 8x1 = r1(0(x1))
               
               1(r1(x1)) = 9x1 >= 9x1 = r1(1(x1))
               
               b(r1(x1)) = 10x1 >= 6x1 = b(1(qr(x1)))
               
               qr(0(x1)) = 3x1 >= 3x1 = 0(qr(x1))
               
               qr(1(x1)) = 4x1 >= 4x1 = 1(qr(x1))
               
               qr(m(x1)) = 15x1 >= 12x1 = m(ql(x1))
               
               ql(0(x1)) = x1 >= x1 = 0(ql(x1))
               
               ql(1(x1)) = 1x1 >= 1x1 = 1(ql(x1))
              problem:
               0(r1(x1)) -> r1(0(x1))
               1(r1(x1)) -> r1(1(x1))
               qr(0(x1)) -> 0(qr(x1))
               qr(1(x1)) -> 1(qr(x1))
               ql(0(x1)) -> 0(ql(x1))
               ql(1(x1)) -> 1(ql(x1))
              KBO Processor:
               weight function:
                w0 = 1
                w(ql) = w(qr) = w(r1) = w(1) = w(0) = 1
               precedence:
                qr > ql > 1 ~ 0 > r1
               problem:
                
               Qed