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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [q4](x0) = x0,
     
     [b](x0) = x0,
     
     [q3](x0) = x0 + 1,
     
     [q2](x0) = x0,
     
     [1](x0) = x0,
     
     [1'](x0) = x0,
     
     [0'](x0) = x0,
     
     [q1](x0) = x0,
     
     [q0](x0) = x0,
     
     [0](x0) = x0
    orientation:
     q0(0(x1)) = x1 >= x1 = 0'(q1(x1))
     
     q1(0(x1)) = x1 >= x1 = 0(q1(x1))
     
     q1(1'(x1)) = x1 >= x1 = 1'(q1(x1))
     
     0(q1(1(x1))) = x1 >= x1 = q2(0(1'(x1)))
     
     0'(q1(1(x1))) = x1 >= x1 = q2(0'(1'(x1)))
     
     1'(q1(1(x1))) = x1 >= x1 = q2(1'(1'(x1)))
     
     0(q2(0(x1))) = x1 >= x1 = q2(0(0(x1)))
     
     0'(q2(0(x1))) = x1 >= x1 = q2(0'(0(x1)))
     
     1'(q2(0(x1))) = x1 >= x1 = q2(1'(0(x1)))
     
     0(q2(1'(x1))) = x1 >= x1 = q2(0(1'(x1)))
     
     0'(q2(1'(x1))) = x1 >= x1 = q2(0'(1'(x1)))
     
     1'(q2(1'(x1))) = x1 >= x1 = q2(1'(1'(x1)))
     
     q2(0'(x1)) = x1 >= x1 = 0'(q0(x1))
     
     q0(1'(x1)) = x1 >= x1 + 1 = 1'(q3(x1))
     
     q3(1'(x1)) = x1 + 1 >= x1 + 1 = 1'(q3(x1))
     
     q3(b(x1)) = x1 + 1 >= x1 = b(q4(x1))
    problem:
     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))
     weak:
      q3(b(x1)) -> b(q4(x1))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [q4](x0) = x0,
       
       [b](x0) = x0,
       
       [q3](x0) = x0,
       
       [q2](x0) = x0 + 1,
       
       [1](x0) = x0,
       
       [1'](x0) = x0,
       
       [0'](x0) = x0 + 1,
       
       [q1](x0) = x0 + 1,
       
       [q0](x0) = x0 + 1,
       
       [0](x0) = x0
      orientation:
       q0(0(x1)) = x1 + 1 >= x1 + 2 = 0'(q1(x1))
       
       q1(0(x1)) = x1 + 1 >= x1 + 1 = 0(q1(x1))
       
       q1(1'(x1)) = x1 + 1 >= x1 + 1 = 1'(q1(x1))
       
       0(q1(1(x1))) = x1 + 1 >= x1 + 1 = q2(0(1'(x1)))
       
       0'(q1(1(x1))) = x1 + 2 >= x1 + 2 = q2(0'(1'(x1)))
       
       1'(q1(1(x1))) = x1 + 1 >= x1 + 1 = q2(1'(1'(x1)))
       
       0(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(0(0(x1)))
       
       0'(q2(0(x1))) = x1 + 2 >= x1 + 2 = q2(0'(0(x1)))
       
       1'(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(1'(0(x1)))
       
       0(q2(1'(x1))) = x1 + 1 >= x1 + 1 = q2(0(1'(x1)))
       
       0'(q2(1'(x1))) = x1 + 2 >= x1 + 2 = q2(0'(1'(x1)))
       
       1'(q2(1'(x1))) = x1 + 1 >= x1 + 1 = q2(1'(1'(x1)))
       
       q2(0'(x1)) = x1 + 2 >= x1 + 2 = 0'(q0(x1))
       
       q0(1'(x1)) = x1 + 1 >= x1 = 1'(q3(x1))
       
       q3(1'(x1)) = x1 >= x1 = 1'(q3(x1))
       
       q3(b(x1)) = x1 >= x1 = b(q4(x1))
      problem:
       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))
        q3(1'(x1)) -> 1'(q3(x1))
       weak:
        q0(1'(x1)) -> 1'(q3(x1))
        q3(b(x1)) -> b(q4(x1))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [q4](x0) = x0,
         
         [b](x0) = x0,
         
         [q3](x0) = x0,
         
         [q2](x0) = x0 + 1,
         
         [1](x0) = x0,
         
         [1'](x0) = x0,
         
         [0'](x0) = x0,
         
         [q1](x0) = x0,
         
         [q0](x0) = x0,
         
         [0](x0) = x0
        orientation:
         q0(0(x1)) = x1 >= x1 = 0'(q1(x1))
         
         q1(0(x1)) = x1 >= x1 = 0(q1(x1))
         
         q1(1'(x1)) = x1 >= x1 = 1'(q1(x1))
         
         0(q1(1(x1))) = x1 >= x1 + 1 = q2(0(1'(x1)))
         
         0'(q1(1(x1))) = x1 >= x1 + 1 = q2(0'(1'(x1)))
         
         1'(q1(1(x1))) = x1 >= x1 + 1 = q2(1'(1'(x1)))
         
         0(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(0(0(x1)))
         
         0'(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(0'(0(x1)))
         
         1'(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(1'(0(x1)))
         
         0(q2(1'(x1))) = x1 + 1 >= x1 + 1 = q2(0(1'(x1)))
         
         0'(q2(1'(x1))) = x1 + 1 >= x1 + 1 = q2(0'(1'(x1)))
         
         1'(q2(1'(x1))) = x1 + 1 >= x1 + 1 = q2(1'(1'(x1)))
         
         q2(0'(x1)) = x1 + 1 >= x1 = 0'(q0(x1))
         
         q3(1'(x1)) = x1 >= x1 = 1'(q3(x1))
         
         q0(1'(x1)) = x1 >= x1 = 1'(q3(x1))
         
         q3(b(x1)) = x1 >= x1 = b(q4(x1))
        problem:
         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)))
          q3(1'(x1)) -> 1'(q3(x1))
         weak:
          q2(0'(x1)) -> 0'(q0(x1))
          q0(1'(x1)) -> 1'(q3(x1))
          q3(b(x1)) -> b(q4(x1))
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [q4](x0) = x0,
           
           [b](x0) = x0 + 1,
           
           [q3](x0) = x0,
           
           [q2](x0) = x0,
           
           [1](x0) = x0 + 1,
           
           [1'](x0) = x0,
           
           [0'](x0) = x0,
           
           [q1](x0) = x0,
           
           [q0](x0) = x0,
           
           [0](x0) = x0
          orientation:
           q0(0(x1)) = x1 >= x1 = 0'(q1(x1))
           
           q1(0(x1)) = x1 >= x1 = 0(q1(x1))
           
           q1(1'(x1)) = x1 >= x1 = 1'(q1(x1))
           
           0(q1(1(x1))) = x1 + 1 >= x1 = q2(0(1'(x1)))
           
           0'(q1(1(x1))) = x1 + 1 >= x1 = q2(0'(1'(x1)))
           
           1'(q1(1(x1))) = x1 + 1 >= x1 = q2(1'(1'(x1)))
           
           0(q2(0(x1))) = x1 >= x1 = q2(0(0(x1)))
           
           0'(q2(0(x1))) = x1 >= x1 = q2(0'(0(x1)))
           
           1'(q2(0(x1))) = x1 >= x1 = q2(1'(0(x1)))
           
           0(q2(1'(x1))) = x1 >= x1 = q2(0(1'(x1)))
           
           0'(q2(1'(x1))) = x1 >= x1 = q2(0'(1'(x1)))
           
           1'(q2(1'(x1))) = x1 >= x1 = q2(1'(1'(x1)))
           
           q3(1'(x1)) = x1 >= x1 = 1'(q3(x1))
           
           q2(0'(x1)) = x1 >= x1 = 0'(q0(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:
            0(q1(1(x1))) -> q2(0(1'(x1)))
            0'(q1(1(x1))) -> q2(0'(1'(x1)))
            1'(q1(1(x1))) -> q2(1'(1'(x1)))
            q2(0'(x1)) -> 0'(q0(x1))
            q0(1'(x1)) -> 1'(q3(x1))
            q3(b(x1)) -> b(q4(x1))
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [q4](x0) = x0,
             
             [b](x0) = x0,
             
             [q3](x0) = x0,
             
             [q2](x0) = x0,
             
             [1](x0) = x0,
             
             [1'](x0) = x0,
             
             [0'](x0) = x0,
             
             [q1](x0) = x0,
             
             [q0](x0) = x0,
             
             [0](x0) = x0 + 1
            orientation:
             q0(0(x1)) = x1 + 1 >= x1 = 0'(q1(x1))
             
             q1(0(x1)) = x1 + 1 >= x1 + 1 = 0(q1(x1))
             
             q1(1'(x1)) = x1 >= x1 = 1'(q1(x1))
             
             0(q2(0(x1))) = x1 + 2 >= x1 + 2 = q2(0(0(x1)))
             
             0'(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(0'(0(x1)))
             
             1'(q2(0(x1))) = x1 + 1 >= x1 + 1 = q2(1'(0(x1)))
             
             0(q2(1'(x1))) = x1 + 1 >= x1 + 1 = q2(0(1'(x1)))
             
             0'(q2(1'(x1))) = x1 >= x1 = q2(0'(1'(x1)))
             
             1'(q2(1'(x1))) = x1 >= x1 = q2(1'(1'(x1)))
             
             q3(1'(x1)) = x1 >= x1 = 1'(q3(x1))
             
             0(q1(1(x1))) = x1 + 1 >= x1 + 1 = q2(0(1'(x1)))
             
             0'(q1(1(x1))) = x1 >= x1 = q2(0'(1'(x1)))
             
             1'(q1(1(x1))) = x1 >= x1 = q2(1'(1'(x1)))
             
             q2(0'(x1)) = x1 >= x1 = 0'(q0(x1))
             
             q0(1'(x1)) = x1 >= x1 = 1'(q3(x1))
             
             q3(b(x1)) = x1 >= x1 = 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))
              0(q1(1(x1))) -> q2(0(1'(x1)))
              0'(q1(1(x1))) -> q2(0'(1'(x1)))
              1'(q1(1(x1))) -> q2(1'(1'(x1)))
              q2(0'(x1)) -> 0'(q0(x1))
              q0(1'(x1)) -> 1'(q3(x1))
              q3(b(x1)) -> b(q4(x1))
            Matrix Interpretation Processor:
             dimension: 2
             max_matrix:
              [1 1]
              [0 1]
              interpretation:
                          [1 1]  
               [q4](x0) = [0 0]x0,
               
                         [1 1]  
               [b](x0) = [0 0]x0,
               
                          [1 0]  
               [q3](x0) = [0 0]x0,
               
                               [0]
               [q2](x0) = x0 + [1],
               
                         [1 1]     [1]
               [1](x0) = [0 1]x0 + [1],
               
                          [1 1]  
               [1'](x0) = [0 1]x0,
               
                               [0]
               [0'](x0) = x0 + [1],
               
                            
               [q1](x0) = x0,
               
                               [0]
               [q0](x0) = x0 + [1],
               
                           
               [0](x0) = x0
              orientation:
                                               
               q1(0(x1)) = x1 >= x1 = 0(q1(x1))
               
                            [1 1]      [1 1]               
               q1(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q1(x1))
               
                                   [0]         [0]               
               0(q2(0(x1))) = x1 + [1] >= x1 + [1] = q2(0(0(x1)))
               
                                    [0]         [0]                
               0'(q2(0(x1))) = x1 + [2] >= x1 + [2] = q2(0'(0(x1)))
               
                               [1 1]     [1]    [1 1]     [0]                
               1'(q2(0(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(0(x1)))
               
                               [1 1]     [0]    [1 1]     [0]                
               0(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0(1'(x1)))
               
                                [1 1]     [0]    [1 1]     [0]                 
               0'(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
               
                                [1 2]     [1]    [1 2]     [0]                 
               1'(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(1'(x1)))
               
                            [1 1]      [1 0]               
               q3(1'(x1)) = [0 0]x1 >= [0 0]x1 = 1'(q3(x1))
               
                                [0]         [0]             
               q0(0(x1)) = x1 + [1] >= x1 + [1] = 0'(q1(x1))
               
                              [1 1]     [1]    [1 1]     [0]                
               0(q1(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0(1'(x1)))
               
                               [1 1]     [1]    [1 1]     [0]                 
               0'(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
               
                               [1 2]     [2]    [1 2]     [0]                 
               1'(q1(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(1'(x1)))
               
                                 [0]         [0]             
               q2(0'(x1)) = x1 + [2] >= x1 + [2] = 0'(q0(x1))
               
                            [1 1]     [0]    [1 0]               
               q0(1'(x1)) = [0 1]x1 + [1] >= [0 0]x1 = 1'(q3(x1))
               
                           [1 1]      [1 1]              
               q3(b(x1)) = [0 0]x1 >= [0 0]x1 = 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)))
                0(q2(1'(x1))) -> q2(0(1'(x1)))
                0'(q2(1'(x1))) -> q2(0'(1'(x1)))
                q3(1'(x1)) -> 1'(q3(x1))
               weak:
                1'(q2(0(x1))) -> q2(1'(0(x1)))
                1'(q2(1'(x1))) -> q2(1'(1'(x1)))
                q0(0(x1)) -> 0'(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)))
                q2(0'(x1)) -> 0'(q0(x1))
                q0(1'(x1)) -> 1'(q3(x1))
                q3(b(x1)) -> b(q4(x1))
              Matrix Interpretation Processor:
               dimension: 2
               max_matrix:
                [1 1]
                [0 1]
                interpretation:
                            [1 0]  
                 [q4](x0) = [0 0]x0,
                 
                           [1 1]     [0]
                 [b](x0) = [0 0]x0 + [1],
                 
                            [1 1]  
                 [q3](x0) = [0 1]x0,
                 
                            [1 1]     [0]
                 [q2](x0) = [0 1]x0 + [1],
                 
                           [1 1]     [0]
                 [1](x0) = [0 1]x0 + [1],
                 
                            [1 1]     [0]
                 [1'](x0) = [0 1]x0 + [1],
                 
                              
                 [0'](x0) = x0,
                 
                            [1 1]     [0]
                 [q1](x0) = [0 1]x0 + [1],
                 
                            [1 1]     [0]
                 [q0](x0) = [0 1]x0 + [1],
                 
                             
                 [0](x0) = x0
                orientation:
                             [1 1]     [0]    [1 1]     [0]            
                 q1(0(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(q1(x1))
                 
                              [1 2]     [1]    [1 2]     [1]             
                 q1(1'(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1'(q1(x1))
                 
                                [1 1]     [0]    [1 1]     [0]               
                 0(q2(0(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0(0(x1)))
                 
                                 [1 1]     [0]    [1 1]     [0]                
                 0'(q2(0(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0'(0(x1)))
                 
                                 [1 2]     [1]    [1 2]     [1]                
                 0(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0(1'(x1)))
                 
                                  [1 2]     [1]    [1 2]     [1]                 
                 0'(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
                 
                              [1 2]     [1]    [1 2]     [0]             
                 q3(1'(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 1'(q3(x1))
                 
                                 [1 2]     [1]    [1 2]     [1]                
                 1'(q2(0(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(1'(0(x1)))
                 
                                  [1 3]     [3]    [1 3]     [3]                 
                 1'(q2(1'(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(1'(1'(x1)))
                 
                             [1 1]     [0]    [1 1]     [0]             
                 q0(0(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0'(q1(x1))
                 
                                [1 2]     [1]    [1 2]     [1]                
                 0(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0(1'(x1)))
                 
                                 [1 2]     [1]    [1 2]     [1]                 
                 0'(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
                 
                                 [1 3]     [3]    [1 3]     [3]                 
                 1'(q1(1(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(1'(1'(x1)))
                 
                              [1 1]     [0]    [1 1]     [0]             
                 q2(0'(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0'(q0(x1))
                 
                              [1 2]     [1]    [1 2]     [0]             
                 q0(1'(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [1] = 1'(q3(x1))
                 
                             [1 1]     [1]    [1 0]     [0]            
                 q3(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 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)))
                  0(q2(1'(x1))) -> q2(0(1'(x1)))
                  0'(q2(1'(x1))) -> q2(0'(1'(x1)))
                 weak:
                  q3(1'(x1)) -> 1'(q3(x1))
                  1'(q2(0(x1))) -> q2(1'(0(x1)))
                  1'(q2(1'(x1))) -> q2(1'(1'(x1)))
                  q0(0(x1)) -> 0'(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)))
                  q2(0'(x1)) -> 0'(q0(x1))
                  q0(1'(x1)) -> 1'(q3(x1))
                  q3(b(x1)) -> b(q4(x1))
                Matrix Interpretation Processor:
                 dimension: 2
                 max_matrix:
                  [1 1]
                  [0 1]
                  interpretation:
                                
                   [q4](x0) = x0,
                   
                             [1 1]  
                   [b](x0) = [0 0]x0,
                   
                              [1 1]  
                   [q3](x0) = [0 0]x0,
                   
                                   [0]
                   [q2](x0) = x0 + [1],
                   
                             [1 1]     [1]
                   [1](x0) = [0 1]x0 + [1],
                   
                              [1 1]     [1]
                   [1'](x0) = [0 1]x0 + [0],
                   
                                   [0]
                   [0'](x0) = x0 + [1],
                   
                                
                   [q1](x0) = x0,
                   
                                
                   [q0](x0) = x0,
                   
                             [1 1]     [0]
                   [0](x0) = [0 1]x0 + [1]
                  orientation:
                               [1 1]     [0]    [1 1]     [0]            
                   q1(0(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(q1(x1))
                   
                                [1 1]     [1]    [1 1]     [1]             
                   q1(1'(x1)) = [0 1]x1 + [0] >= [0 1]x1 + [0] = 1'(q1(x1))
                   
                                  [1 2]     [2]    [1 2]     [1]               
                   0(q2(0(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(0(0(x1)))
                   
                                   [1 1]     [0]    [1 1]     [0]                
                   0'(q2(0(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(0'(0(x1)))
                   
                                   [1 2]     [2]    [1 2]     [1]                
                   0(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0(1'(x1)))
                   
                                    [1 1]     [1]    [1 1]     [1]                 
                   0'(q2(1'(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
                   
                                [1 2]     [1]    [1 1]     [1]             
                   q3(1'(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1'(q3(x1))
                   
                                   [1 2]     [3]    [1 2]     [2]                
                   1'(q2(0(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(1'(0(x1)))
                   
                                    [1 2]     [3]    [1 2]     [2]                 
                   1'(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(1'(x1)))
                   
                               [1 1]     [0]         [0]             
                   q0(0(x1)) = [0 1]x1 + [1] >= x1 + [1] = 0'(q1(x1))
                   
                                  [1 2]     [2]    [1 2]     [1]                
                   0(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0(1'(x1)))
                   
                                   [1 1]     [1]    [1 1]     [1]                 
                   0'(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(1'(x1)))
                   
                                   [1 2]     [3]    [1 2]     [2]                 
                   1'(q1(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(1'(x1)))
                   
                                     [0]         [0]             
                   q2(0'(x1)) = x1 + [2] >= x1 + [1] = 0'(q0(x1))
                   
                                [1 1]     [1]    [1 1]     [1]             
                   q0(1'(x1)) = [0 1]x1 + [0] >= [0 0]x1 + [0] = 1'(q3(x1))
                   
                               [1 1]      [1 1]              
                   q3(b(x1)) = [0 0]x1 >= [0 0]x1 = 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(1'(x1))) -> q2(0'(1'(x1)))
                   weak:
                    0(q2(0(x1))) -> q2(0(0(x1)))
                    0(q2(1'(x1))) -> q2(0(1'(x1)))
                    q3(1'(x1)) -> 1'(q3(x1))
                    1'(q2(0(x1))) -> q2(1'(0(x1)))
                    1'(q2(1'(x1))) -> q2(1'(1'(x1)))
                    q0(0(x1)) -> 0'(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)))
                    q2(0'(x1)) -> 0'(q0(x1))
                    q0(1'(x1)) -> 1'(q3(x1))
                    q3(b(x1)) -> b(q4(x1))
                  Matrix Interpretation Processor:
                   dimension: 2
                   max_matrix:
                    [1 1]
                    [0 1]
                    interpretation:
                                [1 0]  
                     [q4](x0) = [0 0]x0,
                     
                               [1 0]  
                     [b](x0) = [0 0]x0,
                     
                                [1 0]  
                     [q3](x0) = [0 0]x0,
                     
                                     [1]
                     [q2](x0) = x0 + [0],
                     
                               [1 1]     [1]
                     [1](x0) = [0 1]x0 + [0],
                     
                                  
                     [1'](x0) = x0,
                     
                                [1 0]  
                     [0'](x0) = [0 0]x0,
                     
                                [1 1]  
                     [q1](x0) = [0 1]x0,
                     
                                [1 0]  
                     [q0](x0) = [0 0]x0,
                     
                               [1 1]     [0]
                     [0](x0) = [0 1]x0 + [1]
                    orientation:
                                 [1 2]     [1]    [1 2]     [0]            
                     q1(0(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 0(q1(x1))
                     
                                  [1 1]      [1 1]               
                     q1(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q1(x1))
                     
                                     [1 1]     [1]    [1 1]     [1]                
                     0'(q2(0(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(0(x1)))
                     
                                      [1 0]     [1]    [1 0]     [1]                 
                     0'(q2(1'(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(1'(x1)))
                     
                                    [1 2]     [2]    [1 2]     [2]               
                     0(q2(0(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0(0(x1)))
                     
                                     [1 1]     [1]    [1 1]     [1]                
                     0(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0(1'(x1)))
                     
                                  [1 0]      [1 0]               
                     q3(1'(x1)) = [0 0]x1 >= [0 0]x1 = 1'(q3(x1))
                     
                                     [1 1]     [1]    [1 1]     [1]                
                     1'(q2(0(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(0(x1)))
                     
                                           [1]         [1]                 
                     1'(q2(1'(x1))) = x1 + [0] >= x1 + [0] = q2(1'(1'(x1)))
                     
                                 [1 1]      [1 1]               
                     q0(0(x1)) = [0 0]x1 >= [0 0]x1 = 0'(q1(x1))
                     
                                    [1 3]     [1]    [1 1]     [1]                
                     0(q1(1(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0(1'(x1)))
                     
                                     [1 2]     [1]    [1 0]     [1]                 
                     0'(q1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(1'(x1)))
                     
                                     [1 2]     [1]         [1]                 
                     1'(q1(1(x1))) = [0 1]x1 + [0] >= x1 + [0] = q2(1'(1'(x1)))
                     
                                  [1 0]     [1]    [1 0]               
                     q2(0'(x1)) = [0 0]x1 + [0] >= [0 0]x1 = 0'(q0(x1))
                     
                                  [1 0]      [1 0]               
                     q0(1'(x1)) = [0 0]x1 >= [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(1'(x1)) -> 1'(q1(x1))
                      0'(q2(0(x1))) -> q2(0'(0(x1)))
                      0'(q2(1'(x1))) -> q2(0'(1'(x1)))
                     weak:
                      q1(0(x1)) -> 0(q1(x1))
                      0(q2(0(x1))) -> q2(0(0(x1)))
                      0(q2(1'(x1))) -> q2(0(1'(x1)))
                      q3(1'(x1)) -> 1'(q3(x1))
                      1'(q2(0(x1))) -> q2(1'(0(x1)))
                      1'(q2(1'(x1))) -> q2(1'(1'(x1)))
                      q0(0(x1)) -> 0'(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)))
                      q2(0'(x1)) -> 0'(q0(x1))
                      q0(1'(x1)) -> 1'(q3(x1))
                      q3(b(x1)) -> b(q4(x1))
                    Matrix Interpretation Processor:
                     dimension: 2
                     max_matrix:
                      [1 1]
                      [0 1]
                      interpretation:
                                  [1 0]  
                       [q4](x0) = [0 0]x0,
                       
                                      [1]
                       [b](x0) = x0 + [0],
                       
                                    
                       [q3](x0) = x0,
                       
                                       [0]
                       [q2](x0) = x0 + [1],
                       
                                 [1 1]     [0]
                       [1](x0) = [0 1]x0 + [1],
                       
                                       [0]
                       [1'](x0) = x0 + [1],
                       
                                    
                       [0'](x0) = x0,
                       
                                  [1 1]     [0]
                       [q1](x0) = [0 1]x0 + [1],
                       
                                       [0]
                       [q0](x0) = x0 + [1],
                       
                                 [1 1]     [0]
                       [0](x0) = [0 1]x0 + [1]
                      orientation:
                                    [1 1]     [1]    [1 1]     [0]             
                       q1(1'(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 1'(q1(x1))
                       
                                       [1 1]     [0]    [1 1]     [0]                
                       0'(q2(0(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(0'(0(x1)))
                       
                                             [0]         [0]                 
                       0'(q2(1'(x1))) = x1 + [2] >= x1 + [2] = q2(0'(1'(x1)))
                       
                                   [1 2]     [1]    [1 2]     [1]            
                       q1(0(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = 0(q1(x1))
                       
                                      [1 2]     [2]    [1 2]     [1]               
                       0(q2(0(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(0(0(x1)))
                       
                                       [1 1]     [2]    [1 1]     [1]                
                       0(q2(1'(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(0(1'(x1)))
                       
                                         [0]         [0]             
                       q3(1'(x1)) = x1 + [1] >= x1 + [1] = 1'(q3(x1))
                       
                                       [1 1]     [0]    [1 1]     [0]                
                       1'(q2(0(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(1'(0(x1)))
                       
                                             [0]         [0]                 
                       1'(q2(1'(x1))) = x1 + [3] >= x1 + [3] = q2(1'(1'(x1)))
                       
                                   [1 1]     [0]    [1 1]     [0]             
                       q0(0(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [1] = 0'(q1(x1))
                       
                                      [1 3]     [3]    [1 1]     [1]                
                       0(q1(1(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(0(1'(x1)))
                       
                                       [1 2]     [1]         [0]                 
                       0'(q1(1(x1))) = [0 1]x1 + [2] >= x1 + [2] = q2(0'(1'(x1)))
                       
                                       [1 2]     [1]         [0]                 
                       1'(q1(1(x1))) = [0 1]x1 + [3] >= x1 + [3] = q2(1'(1'(x1)))
                       
                                         [0]         [0]             
                       q2(0'(x1)) = x1 + [1] >= x1 + [1] = 0'(q0(x1))
                       
                                         [0]         [0]             
                       q0(1'(x1)) = x1 + [2] >= x1 + [1] = 1'(q3(x1))
                       
                                        [1]    [1 0]     [1]            
                       q3(b(x1)) = x1 + [0] >= [0 0]x1 + [0] = b(q4(x1))
                      problem:
                       strict:
                        0'(q2(0(x1))) -> q2(0'(0(x1)))
                        0'(q2(1'(x1))) -> q2(0'(1'(x1)))
                       weak:
                        q1(1'(x1)) -> 1'(q1(x1))
                        q1(0(x1)) -> 0(q1(x1))
                        0(q2(0(x1))) -> q2(0(0(x1)))
                        0(q2(1'(x1))) -> q2(0(1'(x1)))
                        q3(1'(x1)) -> 1'(q3(x1))
                        1'(q2(0(x1))) -> q2(1'(0(x1)))
                        1'(q2(1'(x1))) -> q2(1'(1'(x1)))
                        q0(0(x1)) -> 0'(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)))
                        q2(0'(x1)) -> 0'(q0(x1))
                        q0(1'(x1)) -> 1'(q3(x1))
                        q3(b(x1)) -> b(q4(x1))
                      Matrix Interpretation Processor:
                       dimension: 2
                       max_matrix:
                        [1 1]
                        [0 1]
                        interpretation:
                                    [1 1]  
                         [q4](x0) = [0 0]x0,
                         
                                   [1 1]  
                         [b](x0) = [0 0]x0,
                         
                                    [1 0]     [0]
                         [q3](x0) = [0 0]x0 + [1],
                         
                                    [1 1]  
                         [q2](x0) = [0 0]x0,
                         
                                   [1 1]     [1]
                         [1](x0) = [0 0]x0 + [0],
                         
                                    [1 0]     [0]
                         [1'](x0) = [0 0]x0 + [1],
                         
                                    [1 0]     [1]
                         [0'](x0) = [0 0]x0 + [0],
                         
                                      
                         [q1](x0) = x0,
                         
                                    [1 0]     [0]
                         [q0](x0) = [0 0]x0 + [1],
                         
                                   [1 0]     [1]
                         [0](x0) = [0 0]x0 + [1]
                        orientation:
                                         [1 0]     [3]    [1 0]     [2]                
                         0'(q2(0(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(0(x1)))
                         
                                          [1 0]     [2]    [1 0]     [1]                 
                         0'(q2(1'(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(1'(x1)))
                         
                                      [1 0]     [0]    [1 0]     [0]             
                         q1(1'(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1'(q1(x1))
                         
                                     [1 0]     [1]    [1 0]     [1]            
                         q1(0(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 0(q1(x1))
                         
                                        [1 0]     [3]    [1 0]     [3]               
                         0(q2(0(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = q2(0(0(x1)))
                         
                                         [1 0]     [2]    [1 0]     [2]                
                         0(q2(1'(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = q2(0(1'(x1)))
                         
                                      [1 0]     [0]    [1 0]     [0]             
                         q3(1'(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1'(q3(x1))
                         
                                         [1 0]     [2]    [1 0]     [2]                
                         1'(q2(0(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = q2(1'(0(x1)))
                         
                                          [1 0]     [1]    [1 0]     [1]                 
                         1'(q2(1'(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = q2(1'(1'(x1)))
                         
                                     [1 0]     [1]    [1 0]     [1]             
                         q0(0(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [0] = 0'(q1(x1))
                         
                                        [1 1]     [2]    [1 0]     [2]                
                         0(q1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = q2(0(1'(x1)))
                         
                                         [1 1]     [2]    [1 0]     [1]                 
                         0'(q1(1(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = q2(0'(1'(x1)))
                         
                                         [1 1]     [1]    [1 0]     [1]                 
                         1'(q1(1(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = q2(1'(1'(x1)))
                         
                                      [1 0]     [1]    [1 0]     [1]             
                         q2(0'(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 0'(q0(x1))
                         
                                      [1 0]     [0]    [1 0]     [0]             
                         q0(1'(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 1'(q3(x1))
                         
                                     [1 1]     [0]    [1 1]              
                         q3(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 = b(q4(x1))
                        problem:
                         strict:
                          
                         weak:
                          0'(q2(0(x1))) -> q2(0'(0(x1)))
                          0'(q2(1'(x1))) -> q2(0'(1'(x1)))
                          q1(1'(x1)) -> 1'(q1(x1))
                          q1(0(x1)) -> 0(q1(x1))
                          0(q2(0(x1))) -> q2(0(0(x1)))
                          0(q2(1'(x1))) -> q2(0(1'(x1)))
                          q3(1'(x1)) -> 1'(q3(x1))
                          1'(q2(0(x1))) -> q2(1'(0(x1)))
                          1'(q2(1'(x1))) -> q2(1'(1'(x1)))
                          q0(0(x1)) -> 0'(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)))
                          q2(0'(x1)) -> 0'(q0(x1))
                          q0(1'(x1)) -> 1'(q3(x1))
                          q3(b(x1)) -> b(q4(x1))
                        Qed