MAYBE

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:
 Complexity Transformation Processor:
  strict:
   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)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [ql](x0) = x0 + 1,
     
     [qr](x0) = x0,
     
     [b](x0) = x0,
     
     [r1](x0) = x0,
     
     [m](x0) = x0,
     
     [1](x0) = x0,
     
     [r0](x0) = x0 + 1,
     
     [0](x0) = x0 + 1
    orientation:
     r0(0(x1)) = x1 + 2 >= x1 + 2 = 0(r0(x1))
     
     r0(1(x1)) = x1 + 1 >= x1 + 1 = 1(r0(x1))
     
     r0(m(x1)) = x1 + 1 >= x1 + 1 = m(r0(x1))
     
     r1(0(x1)) = x1 + 1 >= x1 + 1 = 0(r1(x1))
     
     r1(1(x1)) = x1 >= x1 = 1(r1(x1))
     
     r1(m(x1)) = x1 >= x1 = m(r1(x1))
     
     r0(b(x1)) = x1 + 1 >= x1 + 1 = qr(0(b(x1)))
     
     r1(b(x1)) = x1 >= x1 = qr(1(b(x1)))
     
     0(qr(x1)) = x1 + 1 >= x1 + 1 = qr(0(x1))
     
     1(qr(x1)) = x1 >= x1 = qr(1(x1))
     
     m(qr(x1)) = x1 >= x1 + 1 = ql(m(x1))
     
     0(ql(x1)) = x1 + 2 >= x1 + 2 = ql(0(x1))
     
     1(ql(x1)) = x1 + 1 >= x1 + 1 = ql(1(x1))
     
     b(ql(0(x1))) = x1 + 2 >= x1 + 2 = 0(b(r0(x1)))
     
     b(ql(1(x1))) = x1 + 1 >= x1 = 1(b(r1(x1)))
    problem:
     strict:
      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)))
     weak:
      b(ql(1(x1))) -> 1(b(r1(x1)))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [ql](x0) = x0 + 1,
       
       [qr](x0) = x0 + 1,
       
       [b](x0) = x0,
       
       [r1](x0) = x0 + 1,
       
       [m](x0) = x0,
       
       [1](x0) = x0 + 1,
       
       [r0](x0) = x0,
       
       [0](x0) = x0 + 1
      orientation:
       r0(0(x1)) = x1 + 1 >= x1 + 1 = 0(r0(x1))
       
       r0(1(x1)) = x1 + 1 >= x1 + 1 = 1(r0(x1))
       
       r0(m(x1)) = x1 >= x1 = m(r0(x1))
       
       r1(0(x1)) = x1 + 2 >= x1 + 2 = 0(r1(x1))
       
       r1(1(x1)) = x1 + 2 >= x1 + 2 = 1(r1(x1))
       
       r1(m(x1)) = x1 + 1 >= x1 + 1 = m(r1(x1))
       
       r0(b(x1)) = x1 >= x1 + 2 = qr(0(b(x1)))
       
       r1(b(x1)) = x1 + 1 >= x1 + 2 = qr(1(b(x1)))
       
       0(qr(x1)) = x1 + 2 >= x1 + 2 = qr(0(x1))
       
       1(qr(x1)) = x1 + 2 >= x1 + 2 = qr(1(x1))
       
       m(qr(x1)) = x1 + 1 >= x1 + 1 = ql(m(x1))
       
       0(ql(x1)) = x1 + 2 >= x1 + 2 = ql(0(x1))
       
       1(ql(x1)) = x1 + 2 >= x1 + 2 = ql(1(x1))
       
       b(ql(0(x1))) = x1 + 2 >= x1 + 1 = 0(b(r0(x1)))
       
       b(ql(1(x1))) = x1 + 2 >= x1 + 2 = 1(b(r1(x1)))
      problem:
       strict:
        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))
       weak:
        b(ql(0(x1))) -> 0(b(r0(x1)))
        b(ql(1(x1))) -> 1(b(r1(x1)))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [ql](x0) = x0,
         
         [qr](x0) = x0 + 1,
         
         [b](x0) = x0,
         
         [r1](x0) = x0,
         
         [m](x0) = x0,
         
         [1](x0) = x0,
         
         [r0](x0) = x0,
         
         [0](x0) = x0
        orientation:
         r0(0(x1)) = x1 >= x1 = 0(r0(x1))
         
         r0(1(x1)) = x1 >= x1 = 1(r0(x1))
         
         r0(m(x1)) = x1 >= x1 = m(r0(x1))
         
         r1(0(x1)) = x1 >= x1 = 0(r1(x1))
         
         r1(1(x1)) = x1 >= x1 = 1(r1(x1))
         
         r1(m(x1)) = x1 >= x1 = m(r1(x1))
         
         r0(b(x1)) = x1 >= x1 + 1 = qr(0(b(x1)))
         
         r1(b(x1)) = x1 >= x1 + 1 = qr(1(b(x1)))
         
         0(qr(x1)) = x1 + 1 >= x1 + 1 = qr(0(x1))
         
         1(qr(x1)) = x1 + 1 >= x1 + 1 = qr(1(x1))
         
         m(qr(x1)) = x1 + 1 >= x1 = ql(m(x1))
         
         0(ql(x1)) = x1 >= x1 = ql(0(x1))
         
         1(ql(x1)) = x1 >= x1 = ql(1(x1))
         
         b(ql(0(x1))) = x1 >= x1 = 0(b(r0(x1)))
         
         b(ql(1(x1))) = x1 >= x1 = 1(b(r1(x1)))
        problem:
         strict:
          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))
          0(ql(x1)) -> ql(0(x1))
          1(ql(x1)) -> ql(1(x1))
         weak:
          m(qr(x1)) -> ql(m(x1))
          b(ql(0(x1))) -> 0(b(r0(x1)))
          b(ql(1(x1))) -> 1(b(r1(x1)))
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                        
           [ql](x0) = x0,
           
                        
           [qr](x0) = x0,
           
                     [1 0]  
           [b](x0) = [0 0]x0,
           
                      [1 1]  
           [r1](x0) = [0 1]x0,
           
                          [0]
           [m](x0) = x0 + [1],
           
                     [1 1]  
           [1](x0) = [0 1]x0,
           
                        
           [r0](x0) = x0,
           
                       
           [0](x0) = x0
          orientation:
                                           
           r0(0(x1)) = x1 >= x1 = 0(r0(x1))
           
                       [1 1]      [1 1]              
           r0(1(x1)) = [0 1]x1 >= [0 1]x1 = 1(r0(x1))
           
                            [0]         [0]            
           r0(m(x1)) = x1 + [1] >= x1 + [1] = m(r0(x1))
           
                       [1 1]      [1 1]              
           r1(0(x1)) = [0 1]x1 >= [0 1]x1 = 0(r1(x1))
           
                       [1 2]      [1 2]              
           r1(1(x1)) = [0 1]x1 >= [0 1]x1 = 1(r1(x1))
           
                       [1 1]     [1]    [1 1]     [0]            
           r1(m(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = m(r1(x1))
           
                       [1 0]      [1 0]                 
           r0(b(x1)) = [0 0]x1 >= [0 0]x1 = qr(0(b(x1)))
           
                       [1 0]      [1 0]                 
           r1(b(x1)) = [0 0]x1 >= [0 0]x1 = qr(1(b(x1)))
           
                                           
           0(qr(x1)) = x1 >= x1 = qr(0(x1))
           
                       [1 1]      [1 1]              
           1(qr(x1)) = [0 1]x1 >= [0 1]x1 = qr(1(x1))
           
                                           
           0(ql(x1)) = x1 >= x1 = ql(0(x1))
           
                       [1 1]      [1 1]              
           1(ql(x1)) = [0 1]x1 >= [0 1]x1 = ql(1(x1))
           
                            [0]         [0]            
           m(qr(x1)) = x1 + [1] >= x1 + [1] = ql(m(x1))
           
                          [1 0]      [1 0]                 
           b(ql(0(x1))) = [0 0]x1 >= [0 0]x1 = 0(b(r0(x1)))
           
                          [1 1]      [1 1]                 
           b(ql(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(b(r1(x1)))
          problem:
           strict:
            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))
            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))
            0(ql(x1)) -> ql(0(x1))
            1(ql(x1)) -> ql(1(x1))
           weak:
            r1(m(x1)) -> m(r1(x1))
            m(qr(x1)) -> ql(m(x1))
            b(ql(0(x1))) -> 0(b(r0(x1)))
            b(ql(1(x1))) -> 1(b(r1(x1)))
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                          
             [ql](x0) = x0,
             
                        [1 0]  
             [qr](x0) = [0 0]x0,
             
                       [1 1]  
             [b](x0) = [0 1]x0,
             
                          
             [r1](x0) = x0,
             
                       [1 0]  
             [m](x0) = [0 0]x0,
             
                         
             [1](x0) = x0,
             
                             [1]
             [r0](x0) = x0 + [0],
             
                            [0]
             [0](x0) = x0 + [1]
            orientation:
                              [1]         [1]            
             r0(0(x1)) = x1 + [1] >= x1 + [1] = 0(r0(x1))
             
                              [1]         [1]            
             r0(1(x1)) = x1 + [0] >= x1 + [0] = 1(r0(x1))
             
                         [1 0]     [1]    [1 0]     [1]            
             r0(m(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = m(r0(x1))
             
                              [0]         [0]            
             r1(0(x1)) = x1 + [1] >= x1 + [1] = 0(r1(x1))
             
                                             
             r1(1(x1)) = x1 >= x1 = 1(r1(x1))
             
                         [1 1]     [1]    [1 1]                 
             r0(b(x1)) = [0 1]x1 + [0] >= [0 0]x1 = qr(0(b(x1)))
             
                         [1 1]      [1 1]                 
             r1(b(x1)) = [0 1]x1 >= [0 0]x1 = qr(1(b(x1)))
             
                         [1 0]     [0]    [1 0]              
             0(qr(x1)) = [0 0]x1 + [1] >= [0 0]x1 = qr(0(x1))
             
                         [1 0]      [1 0]              
             1(qr(x1)) = [0 0]x1 >= [0 0]x1 = qr(1(x1))
             
                              [0]         [0]            
             0(ql(x1)) = x1 + [1] >= x1 + [1] = ql(0(x1))
             
                                             
             1(ql(x1)) = x1 >= x1 = ql(1(x1))
             
                         [1 0]      [1 0]              
             r1(m(x1)) = [0 0]x1 >= [0 0]x1 = m(r1(x1))
             
                         [1 0]      [1 0]              
             m(qr(x1)) = [0 0]x1 >= [0 0]x1 = ql(m(x1))
             
                            [1 1]     [1]    [1 1]     [1]               
             b(ql(0(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(b(r0(x1)))
             
                            [1 1]      [1 1]                 
             b(ql(1(x1))) = [0 1]x1 >= [0 1]x1 = 1(b(r1(x1)))
            problem:
             strict:
              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(b(x1)) -> qr(1(b(x1)))
              0(qr(x1)) -> qr(0(x1))
              1(qr(x1)) -> qr(1(x1))
              0(ql(x1)) -> ql(0(x1))
              1(ql(x1)) -> ql(1(x1))
             weak:
              r0(b(x1)) -> qr(0(b(x1)))
              r1(m(x1)) -> m(r1(x1))
              m(qr(x1)) -> ql(m(x1))
              b(ql(0(x1))) -> 0(b(r0(x1)))
              b(ql(1(x1))) -> 1(b(r1(x1)))
            Matrix Interpretation Processor:
             dimension: 2
             max_matrix:
              [1 1]
              [0 1]
              interpretation:
                            
               [ql](x0) = x0,
               
                          [1 0]  
               [qr](x0) = [0 0]x0,
               
                         [1 1]  
               [b](x0) = [0 1]x0,
               
                               [1]
               [r1](x0) = x0 + [0],
               
                         [1 0]  
               [m](x0) = [0 0]x0,
               
                              [0]
               [1](x0) = x0 + [1],
               
                            
               [r0](x0) = x0,
               
                           
               [0](x0) = x0
              orientation:
                                               
               r0(0(x1)) = x1 >= x1 = 0(r0(x1))
               
                                [0]         [0]            
               r0(1(x1)) = x1 + [1] >= x1 + [1] = 1(r0(x1))
               
                           [1 0]      [1 0]              
               r0(m(x1)) = [0 0]x1 >= [0 0]x1 = m(r0(x1))
               
                                [1]         [1]            
               r1(0(x1)) = x1 + [0] >= x1 + [0] = 0(r1(x1))
               
                                [1]         [1]            
               r1(1(x1)) = x1 + [1] >= x1 + [1] = 1(r1(x1))
               
                           [1 1]     [1]    [1 1]                 
               r1(b(x1)) = [0 1]x1 + [0] >= [0 0]x1 = qr(1(b(x1)))
               
                           [1 0]      [1 0]              
               0(qr(x1)) = [0 0]x1 >= [0 0]x1 = qr(0(x1))
               
                           [1 0]     [0]    [1 0]              
               1(qr(x1)) = [0 0]x1 + [1] >= [0 0]x1 = qr(1(x1))
               
                                               
               0(ql(x1)) = x1 >= x1 = ql(0(x1))
               
                                [0]         [0]            
               1(ql(x1)) = x1 + [1] >= x1 + [1] = ql(1(x1))
               
                           [1 1]      [1 1]                 
               r0(b(x1)) = [0 1]x1 >= [0 0]x1 = qr(0(b(x1)))
               
                           [1 0]     [1]    [1 0]     [1]            
               r1(m(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = m(r1(x1))
               
                           [1 0]      [1 0]              
               m(qr(x1)) = [0 0]x1 >= [0 0]x1 = ql(m(x1))
               
                              [1 1]      [1 1]                 
               b(ql(0(x1))) = [0 1]x1 >= [0 1]x1 = 0(b(r0(x1)))
               
                              [1 1]     [1]    [1 1]     [1]               
               b(ql(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1(b(r1(x1)))
              problem:
               strict:
                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))
                0(qr(x1)) -> qr(0(x1))
                1(qr(x1)) -> qr(1(x1))
                0(ql(x1)) -> ql(0(x1))
                1(ql(x1)) -> ql(1(x1))
               weak:
                r1(b(x1)) -> qr(1(b(x1)))
                r0(b(x1)) -> qr(0(b(x1)))
                r1(m(x1)) -> m(r1(x1))
                m(qr(x1)) -> ql(m(x1))
                b(ql(0(x1))) -> 0(b(r0(x1)))
                b(ql(1(x1))) -> 1(b(r1(x1)))
              Matrix Interpretation Processor:
               dimension: 2
               max_matrix:
                [1 1]
                [0 1]
                interpretation:
                              
                 [ql](x0) = x0,
                 
                              
                 [qr](x0) = x0,
                 
                           [1 1]  
                 [b](x0) = [0 0]x0,
                 
                              
                 [r1](x0) = x0,
                 
                           [1 1]     [0]
                 [m](x0) = [0 1]x0 + [1],
                 
                             
                 [1](x0) = x0,
                 
                            [1 1]  
                 [r0](x0) = [0 1]x0,
                 
                           [1 1]  
                 [0](x0) = [0 1]x0
                orientation:
                             [1 2]      [1 2]              
                 r0(0(x1)) = [0 1]x1 >= [0 1]x1 = 0(r0(x1))
                 
                             [1 1]      [1 1]              
                 r0(1(x1)) = [0 1]x1 >= [0 1]x1 = 1(r0(x1))
                 
                             [1 2]     [1]    [1 2]     [0]            
                 r0(m(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = m(r0(x1))
                 
                             [1 1]      [1 1]              
                 r1(0(x1)) = [0 1]x1 >= [0 1]x1 = 0(r1(x1))
                 
                                                 
                 r1(1(x1)) = x1 >= x1 = 1(r1(x1))
                 
                             [1 1]      [1 1]              
                 0(qr(x1)) = [0 1]x1 >= [0 1]x1 = qr(0(x1))
                 
                                                 
                 1(qr(x1)) = x1 >= x1 = qr(1(x1))
                 
                             [1 1]      [1 1]              
                 0(ql(x1)) = [0 1]x1 >= [0 1]x1 = ql(0(x1))
                 
                                                 
                 1(ql(x1)) = x1 >= x1 = ql(1(x1))
                 
                             [1 1]      [1 1]                 
                 r1(b(x1)) = [0 0]x1 >= [0 0]x1 = qr(1(b(x1)))
                 
                             [1 1]      [1 1]                 
                 r0(b(x1)) = [0 0]x1 >= [0 0]x1 = qr(0(b(x1)))
                 
                             [1 1]     [0]    [1 1]     [0]            
                 r1(m(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = m(r1(x1))
                 
                             [1 1]     [0]    [1 1]     [0]            
                 m(qr(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = ql(m(x1))
                 
                                [1 2]      [1 2]                 
                 b(ql(0(x1))) = [0 0]x1 >= [0 0]x1 = 0(b(r0(x1)))
                 
                                [1 1]      [1 1]                 
                 b(ql(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(b(r1(x1)))
                problem:
                 strict:
                  r0(0(x1)) -> 0(r0(x1))
                  r0(1(x1)) -> 1(r0(x1))
                  r1(0(x1)) -> 0(r1(x1))
                  r1(1(x1)) -> 1(r1(x1))
                  0(qr(x1)) -> qr(0(x1))
                  1(qr(x1)) -> qr(1(x1))
                  0(ql(x1)) -> ql(0(x1))
                  1(ql(x1)) -> ql(1(x1))
                 weak:
                  r0(m(x1)) -> m(r0(x1))
                  r1(b(x1)) -> qr(1(b(x1)))
                  r0(b(x1)) -> qr(0(b(x1)))
                  r1(m(x1)) -> m(r1(x1))
                  m(qr(x1)) -> ql(m(x1))
                  b(ql(0(x1))) -> 0(b(r0(x1)))
                  b(ql(1(x1))) -> 1(b(r1(x1)))
                Open