YES(?,O(n^2))

Problem:
 q0(a(x1)) -> x(q1(x1))
 q1(a(x1)) -> a(q1(x1))
 q1(y(x1)) -> y(q1(x1))
 a(q1(b(x1))) -> q2(a(y(x1)))
 a(q2(a(x1))) -> q2(a(a(x1)))
 a(q2(y(x1))) -> q2(a(y(x1)))
 y(q1(b(x1))) -> q2(y(y(x1)))
 y(q2(a(x1))) -> q2(y(a(x1)))
 y(q2(y(x1))) -> q2(y(y(x1)))
 q2(x(x1)) -> x(q0(x1))
 q0(y(x1)) -> y(q3(x1))
 q3(y(x1)) -> y(q3(x1))
 q3(bl(x1)) -> bl(q4(x1))

Proof:
 Complexity Transformation Processor:
  strict:
   q0(a(x1)) -> x(q1(x1))
   q1(a(x1)) -> a(q1(x1))
   q1(y(x1)) -> y(q1(x1))
   a(q1(b(x1))) -> q2(a(y(x1)))
   a(q2(a(x1))) -> q2(a(a(x1)))
   a(q2(y(x1))) -> q2(a(y(x1)))
   y(q1(b(x1))) -> q2(y(y(x1)))
   y(q2(a(x1))) -> q2(y(a(x1)))
   y(q2(y(x1))) -> q2(y(y(x1)))
   q2(x(x1)) -> x(q0(x1))
   q0(y(x1)) -> y(q3(x1))
   q3(y(x1)) -> y(q3(x1))
   q3(bl(x1)) -> bl(q4(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [q4](x0) = x0,
     
     [bl](x0) = x0,
     
     [q3](x0) = x0 + 1,
     
     [q2](x0) = x0,
     
     [b](x0) = x0,
     
     [y](x0) = x0 + 1,
     
     [x](x0) = x0 + 1,
     
     [q1](x0) = x0 + 1,
     
     [q0](x0) = x0,
     
     [a](x0) = x0 + 1
    orientation:
     q0(a(x1)) = x1 + 1 >= x1 + 2 = x(q1(x1))
     
     q1(a(x1)) = x1 + 2 >= x1 + 2 = a(q1(x1))
     
     q1(y(x1)) = x1 + 2 >= x1 + 2 = y(q1(x1))
     
     a(q1(b(x1))) = x1 + 2 >= x1 + 2 = q2(a(y(x1)))
     
     a(q2(a(x1))) = x1 + 2 >= x1 + 2 = q2(a(a(x1)))
     
     a(q2(y(x1))) = x1 + 2 >= x1 + 2 = q2(a(y(x1)))
     
     y(q1(b(x1))) = x1 + 2 >= x1 + 2 = q2(y(y(x1)))
     
     y(q2(a(x1))) = x1 + 2 >= x1 + 2 = q2(y(a(x1)))
     
     y(q2(y(x1))) = x1 + 2 >= x1 + 2 = q2(y(y(x1)))
     
     q2(x(x1)) = x1 + 1 >= x1 + 1 = x(q0(x1))
     
     q0(y(x1)) = x1 + 1 >= x1 + 2 = y(q3(x1))
     
     q3(y(x1)) = x1 + 2 >= x1 + 2 = y(q3(x1))
     
     q3(bl(x1)) = x1 + 1 >= x1 = bl(q4(x1))
    problem:
     strict:
      q0(a(x1)) -> x(q1(x1))
      q1(a(x1)) -> a(q1(x1))
      q1(y(x1)) -> y(q1(x1))
      a(q1(b(x1))) -> q2(a(y(x1)))
      a(q2(a(x1))) -> q2(a(a(x1)))
      a(q2(y(x1))) -> q2(a(y(x1)))
      y(q1(b(x1))) -> q2(y(y(x1)))
      y(q2(a(x1))) -> q2(y(a(x1)))
      y(q2(y(x1))) -> q2(y(y(x1)))
      q2(x(x1)) -> x(q0(x1))
      q0(y(x1)) -> y(q3(x1))
      q3(y(x1)) -> y(q3(x1))
     weak:
      q3(bl(x1)) -> bl(q4(x1))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [q4](x0) = x0,
       
       [bl](x0) = x0,
       
       [q3](x0) = x0,
       
       [q2](x0) = x0 + 1,
       
       [b](x0) = x0,
       
       [y](x0) = x0,
       
       [x](x0) = x0,
       
       [q1](x0) = x0,
       
       [q0](x0) = x0 + 1,
       
       [a](x0) = x0
      orientation:
       q0(a(x1)) = x1 + 1 >= x1 = x(q1(x1))
       
       q1(a(x1)) = x1 >= x1 = a(q1(x1))
       
       q1(y(x1)) = x1 >= x1 = y(q1(x1))
       
       a(q1(b(x1))) = x1 >= x1 + 1 = q2(a(y(x1)))
       
       a(q2(a(x1))) = x1 + 1 >= x1 + 1 = q2(a(a(x1)))
       
       a(q2(y(x1))) = x1 + 1 >= x1 + 1 = q2(a(y(x1)))
       
       y(q1(b(x1))) = x1 >= x1 + 1 = q2(y(y(x1)))
       
       y(q2(a(x1))) = x1 + 1 >= x1 + 1 = q2(y(a(x1)))
       
       y(q2(y(x1))) = x1 + 1 >= x1 + 1 = q2(y(y(x1)))
       
       q2(x(x1)) = x1 + 1 >= x1 + 1 = x(q0(x1))
       
       q0(y(x1)) = x1 + 1 >= x1 = y(q3(x1))
       
       q3(y(x1)) = x1 >= x1 = y(q3(x1))
       
       q3(bl(x1)) = x1 >= x1 = bl(q4(x1))
      problem:
       strict:
        q1(a(x1)) -> a(q1(x1))
        q1(y(x1)) -> y(q1(x1))
        a(q1(b(x1))) -> q2(a(y(x1)))
        a(q2(a(x1))) -> q2(a(a(x1)))
        a(q2(y(x1))) -> q2(a(y(x1)))
        y(q1(b(x1))) -> q2(y(y(x1)))
        y(q2(a(x1))) -> q2(y(a(x1)))
        y(q2(y(x1))) -> q2(y(y(x1)))
        q2(x(x1)) -> x(q0(x1))
        q3(y(x1)) -> y(q3(x1))
       weak:
        q0(a(x1)) -> x(q1(x1))
        q0(y(x1)) -> y(q3(x1))
        q3(bl(x1)) -> bl(q4(x1))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [q4](x0) = x0,
         
         [bl](x0) = x0,
         
         [q3](x0) = x0,
         
         [q2](x0) = x0,
         
         [b](x0) = x0 + 1,
         
         [y](x0) = x0,
         
         [x](x0) = x0,
         
         [q1](x0) = x0,
         
         [q0](x0) = x0,
         
         [a](x0) = x0
        orientation:
         q1(a(x1)) = x1 >= x1 = a(q1(x1))
         
         q1(y(x1)) = x1 >= x1 = y(q1(x1))
         
         a(q1(b(x1))) = x1 + 1 >= x1 = q2(a(y(x1)))
         
         a(q2(a(x1))) = x1 >= x1 = q2(a(a(x1)))
         
         a(q2(y(x1))) = x1 >= x1 = q2(a(y(x1)))
         
         y(q1(b(x1))) = x1 + 1 >= x1 = q2(y(y(x1)))
         
         y(q2(a(x1))) = x1 >= x1 = q2(y(a(x1)))
         
         y(q2(y(x1))) = x1 >= x1 = q2(y(y(x1)))
         
         q2(x(x1)) = x1 >= x1 = x(q0(x1))
         
         q3(y(x1)) = x1 >= x1 = y(q3(x1))
         
         q0(a(x1)) = x1 >= x1 = x(q1(x1))
         
         q0(y(x1)) = x1 >= x1 = y(q3(x1))
         
         q3(bl(x1)) = x1 >= x1 = bl(q4(x1))
        problem:
         strict:
          q1(a(x1)) -> a(q1(x1))
          q1(y(x1)) -> y(q1(x1))
          a(q2(a(x1))) -> q2(a(a(x1)))
          a(q2(y(x1))) -> q2(a(y(x1)))
          y(q2(a(x1))) -> q2(y(a(x1)))
          y(q2(y(x1))) -> q2(y(y(x1)))
          q2(x(x1)) -> x(q0(x1))
          q3(y(x1)) -> y(q3(x1))
         weak:
          a(q1(b(x1))) -> q2(a(y(x1)))
          y(q1(b(x1))) -> q2(y(y(x1)))
          q0(a(x1)) -> x(q1(x1))
          q0(y(x1)) -> y(q3(x1))
          q3(bl(x1)) -> bl(q4(x1))
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [q4](x0) = x0,
           
           [bl](x0) = x0,
           
           [q3](x0) = x0,
           
           [q2](x0) = x0 + 1,
           
           [b](x0) = x0 + 1,
           
           [y](x0) = x0,
           
           [x](x0) = x0,
           
           [q1](x0) = x0,
           
           [q0](x0) = x0,
           
           [a](x0) = x0
          orientation:
           q1(a(x1)) = x1 >= x1 = a(q1(x1))
           
           q1(y(x1)) = x1 >= x1 = y(q1(x1))
           
           a(q2(a(x1))) = x1 + 1 >= x1 + 1 = q2(a(a(x1)))
           
           a(q2(y(x1))) = x1 + 1 >= x1 + 1 = q2(a(y(x1)))
           
           y(q2(a(x1))) = x1 + 1 >= x1 + 1 = q2(y(a(x1)))
           
           y(q2(y(x1))) = x1 + 1 >= x1 + 1 = q2(y(y(x1)))
           
           q2(x(x1)) = x1 + 1 >= x1 = x(q0(x1))
           
           q3(y(x1)) = x1 >= x1 = y(q3(x1))
           
           a(q1(b(x1))) = x1 + 1 >= x1 + 1 = q2(a(y(x1)))
           
           y(q1(b(x1))) = x1 + 1 >= x1 + 1 = q2(y(y(x1)))
           
           q0(a(x1)) = x1 >= x1 = x(q1(x1))
           
           q0(y(x1)) = x1 >= x1 = y(q3(x1))
           
           q3(bl(x1)) = x1 >= x1 = bl(q4(x1))
          problem:
           strict:
            q1(a(x1)) -> a(q1(x1))
            q1(y(x1)) -> y(q1(x1))
            a(q2(a(x1))) -> q2(a(a(x1)))
            a(q2(y(x1))) -> q2(a(y(x1)))
            y(q2(a(x1))) -> q2(y(a(x1)))
            y(q2(y(x1))) -> q2(y(y(x1)))
            q3(y(x1)) -> y(q3(x1))
           weak:
            q2(x(x1)) -> x(q0(x1))
            a(q1(b(x1))) -> q2(a(y(x1)))
            y(q1(b(x1))) -> q2(y(y(x1)))
            q0(a(x1)) -> x(q1(x1))
            q0(y(x1)) -> y(q3(x1))
            q3(bl(x1)) -> bl(q4(x1))
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                        [1 0]  
             [q4](x0) = [0 0]x0,
             
                        [1 1]     [1]
             [bl](x0) = [0 0]x0 + [0],
             
                        [1 0]  
             [q3](x0) = [0 0]x0,
             
                             [0]
             [q2](x0) = x0 + [1],
             
                       [1 1]     [0]
             [b](x0) = [0 1]x0 + [1],
             
                       [1 1]  
             [y](x0) = [0 1]x0,
             
                       [1 0]  
             [x](x0) = [0 0]x0,
             
                          
             [q1](x0) = x0,
             
                        [1 0]  
             [q0](x0) = [0 0]x0,
             
                         
             [a](x0) = x0
            orientation:
                                             
             q1(a(x1)) = x1 >= x1 = a(q1(x1))
             
                         [1 1]      [1 1]              
             q1(y(x1)) = [0 1]x1 >= [0 1]x1 = y(q1(x1))
             
                                 [0]         [0]               
             a(q2(a(x1))) = x1 + [1] >= x1 + [1] = q2(a(a(x1)))
             
                            [1 1]     [0]    [1 1]     [0]               
             a(q2(y(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
             
                            [1 1]     [1]    [1 1]     [0]               
             y(q2(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(a(x1)))
             
                            [1 2]     [1]    [1 2]     [0]               
             y(q2(y(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(y(x1)))
             
                         [1 1]      [1 0]              
             q3(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
             
                         [1 0]     [0]    [1 0]              
             q2(x(x1)) = [0 0]x1 + [1] >= [0 0]x1 = x(q0(x1))
             
                            [1 1]     [0]    [1 1]     [0]               
             a(q1(b(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
             
                            [1 2]     [1]    [1 2]     [0]               
             y(q1(b(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(y(x1)))
             
                         [1 0]      [1 0]              
             q0(a(x1)) = [0 0]x1 >= [0 0]x1 = x(q1(x1))
             
                         [1 1]      [1 0]              
             q0(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
             
                          [1 1]     [1]    [1 0]     [1]             
             q3(bl(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = bl(q4(x1))
            problem:
             strict:
              q1(a(x1)) -> a(q1(x1))
              q1(y(x1)) -> y(q1(x1))
              a(q2(a(x1))) -> q2(a(a(x1)))
              a(q2(y(x1))) -> q2(a(y(x1)))
              q3(y(x1)) -> y(q3(x1))
             weak:
              y(q2(a(x1))) -> q2(y(a(x1)))
              y(q2(y(x1))) -> q2(y(y(x1)))
              q2(x(x1)) -> x(q0(x1))
              a(q1(b(x1))) -> q2(a(y(x1)))
              y(q1(b(x1))) -> q2(y(y(x1)))
              q0(a(x1)) -> x(q1(x1))
              q0(y(x1)) -> y(q3(x1))
              q3(bl(x1)) -> bl(q4(x1))
            Matrix Interpretation Processor:
             dimension: 2
             max_matrix:
              [1 1]
              [0 1]
              interpretation:
                          [1 0]  
               [q4](x0) = [0 0]x0,
               
                          [1 0]     [1]
               [bl](x0) = [0 0]x0 + [0],
               
                          [1 0]  
               [q3](x0) = [0 0]x0,
               
                            
               [q2](x0) = x0,
               
                              [1]
               [b](x0) = x0 + [1],
               
                           
               [y](x0) = x0,
               
                         [1 0]  
               [x](x0) = [0 0]x0,
               
                          [1 1]  
               [q1](x0) = [0 1]x0,
               
                            
               [q0](x0) = x0,
               
                         [1 1]     [0]
               [a](x0) = [0 1]x0 + [1]
              orientation:
                           [1 2]     [1]    [1 2]     [0]            
               q1(a(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(q1(x1))
               
                           [1 1]      [1 1]              
               q1(y(x1)) = [0 1]x1 >= [0 1]x1 = y(q1(x1))
               
                              [1 2]     [1]    [1 2]     [1]               
               a(q2(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(a(x1)))
               
                              [1 1]     [0]    [1 1]     [0]               
               a(q2(y(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
               
                           [1 0]      [1 0]              
               q3(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
               
                              [1 1]     [0]    [1 1]     [0]               
               y(q2(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(a(x1)))
               
                                                     
               y(q2(y(x1))) = x1 >= x1 = q2(y(y(x1)))
               
                           [1 0]      [1 0]              
               q2(x(x1)) = [0 0]x1 >= [0 0]x1 = x(q0(x1))
               
                              [1 2]     [3]    [1 1]     [0]               
               a(q1(b(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [1] = q2(a(y(x1)))
               
                              [1 1]     [2]                     
               y(q1(b(x1))) = [0 1]x1 + [1] >= x1 = q2(y(y(x1)))
               
                           [1 1]     [0]    [1 1]              
               q0(a(x1)) = [0 1]x1 + [1] >= [0 0]x1 = x(q1(x1))
               
                                 [1 0]              
               q0(y(x1)) = x1 >= [0 0]x1 = y(q3(x1))
               
                            [1 0]     [1]    [1 0]     [1]             
               q3(bl(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = bl(q4(x1))
              problem:
               strict:
                q1(y(x1)) -> y(q1(x1))
                a(q2(a(x1))) -> q2(a(a(x1)))
                a(q2(y(x1))) -> q2(a(y(x1)))
                q3(y(x1)) -> y(q3(x1))
               weak:
                q1(a(x1)) -> a(q1(x1))
                y(q2(a(x1))) -> q2(y(a(x1)))
                y(q2(y(x1))) -> q2(y(y(x1)))
                q2(x(x1)) -> x(q0(x1))
                a(q1(b(x1))) -> q2(a(y(x1)))
                y(q1(b(x1))) -> q2(y(y(x1)))
                q0(a(x1)) -> x(q1(x1))
                q0(y(x1)) -> y(q3(x1))
                q3(bl(x1)) -> bl(q4(x1))
              Matrix Interpretation Processor:
               dimension: 2
               max_matrix:
                [1 1]
                [0 1]
                interpretation:
                            [1 1]  
                 [q4](x0) = [0 0]x0,
                 
                            [1 1]     [1]
                 [bl](x0) = [0 1]x0 + [0],
                 
                              
                 [q3](x0) = x0,
                 
                              
                 [q2](x0) = x0,
                 
                           [1 1]     [0]
                 [b](x0) = [0 1]x0 + [1],
                 
                                [0]
                 [y](x0) = x0 + [1],
                 
                           [1 0]  
                 [x](x0) = [0 0]x0,
                 
                            [1 1]  
                 [q1](x0) = [0 1]x0,
                 
                              
                 [q0](x0) = x0,
                 
                           [1 1]  
                 [a](x0) = [0 1]x0
                orientation:
                             [1 1]     [1]    [1 1]     [0]            
                 q1(y(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = y(q1(x1))
                 
                                [1 2]      [1 2]                 
                 a(q2(a(x1))) = [0 1]x1 >= [0 1]x1 = q2(a(a(x1)))
                 
                                [1 1]     [1]    [1 1]     [1]               
                 a(q2(y(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
                 
                                  [0]         [0]            
                 q3(y(x1)) = x1 + [1] >= x1 + [1] = y(q3(x1))
                 
                             [1 2]      [1 2]              
                 q1(a(x1)) = [0 1]x1 >= [0 1]x1 = a(q1(x1))
                 
                                [1 1]     [0]    [1 1]     [0]               
                 y(q2(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(a(x1)))
                 
                                     [0]         [0]               
                 y(q2(y(x1))) = x1 + [2] >= x1 + [2] = q2(y(y(x1)))
                 
                             [1 0]      [1 0]              
                 q2(x(x1)) = [0 0]x1 >= [0 0]x1 = x(q0(x1))
                 
                                [1 3]     [2]    [1 1]     [1]               
                 a(q1(b(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
                 
                                [1 2]     [1]         [0]               
                 y(q1(b(x1))) = [0 1]x1 + [2] >= x1 + [2] = q2(y(y(x1)))
                 
                             [1 1]      [1 1]              
                 q0(a(x1)) = [0 1]x1 >= [0 0]x1 = x(q1(x1))
                 
                                  [0]         [0]            
                 q0(y(x1)) = x1 + [1] >= x1 + [1] = y(q3(x1))
                 
                              [1 1]     [1]    [1 1]     [1]             
                 q3(bl(x1)) = [0 1]x1 + [0] >= [0 0]x1 + [0] = bl(q4(x1))
                problem:
                 strict:
                  a(q2(a(x1))) -> q2(a(a(x1)))
                  a(q2(y(x1))) -> q2(a(y(x1)))
                  q3(y(x1)) -> y(q3(x1))
                 weak:
                  q1(y(x1)) -> y(q1(x1))
                  q1(a(x1)) -> a(q1(x1))
                  y(q2(a(x1))) -> q2(y(a(x1)))
                  y(q2(y(x1))) -> q2(y(y(x1)))
                  q2(x(x1)) -> x(q0(x1))
                  a(q1(b(x1))) -> q2(a(y(x1)))
                  y(q1(b(x1))) -> q2(y(y(x1)))
                  q0(a(x1)) -> x(q1(x1))
                  q0(y(x1)) -> y(q3(x1))
                  q3(bl(x1)) -> bl(q4(x1))
                Matrix Interpretation Processor:
                 dimension: 2
                 max_matrix:
                  [1 1]
                  [0 1]
                  interpretation:
                              [1 0]  
                   [q4](x0) = [0 0]x0,
                   
                              [1 0]     [1]
                   [bl](x0) = [0 0]x0 + [0],
                   
                              [1 0]  
                   [q3](x0) = [0 0]x0,
                   
                                   [0]
                   [q2](x0) = x0 + [1],
                   
                             [1 1]     [0]
                   [b](x0) = [0 1]x0 + [1],
                   
                             [1 1]  
                   [y](x0) = [0 1]x0,
                   
                             [1 0]     [0]
                   [x](x0) = [0 0]x0 + [1],
                   
                              [1 1]  
                   [q1](x0) = [0 1]x0,
                   
                              [1 0]     [0]
                   [q0](x0) = [0 0]x0 + [1],
                   
                             [1 1]  
                   [a](x0) = [0 1]x0
                  orientation:
                                  [1 2]     [1]    [1 2]     [0]               
                   a(q2(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(a(x1)))
                   
                                  [1 2]     [1]    [1 2]     [0]               
                   a(q2(y(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
                   
                               [1 1]      [1 0]              
                   q3(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
                   
                               [1 2]      [1 2]              
                   q1(y(x1)) = [0 1]x1 >= [0 1]x1 = y(q1(x1))
                   
                               [1 2]      [1 2]              
                   q1(a(x1)) = [0 1]x1 >= [0 1]x1 = a(q1(x1))
                   
                                  [1 2]     [1]    [1 2]     [0]               
                   y(q2(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(a(x1)))
                   
                                  [1 2]     [1]    [1 2]     [0]               
                   y(q2(y(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(y(x1)))
                   
                               [1 0]     [0]    [1 0]     [0]            
                   q2(x(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [1] = x(q0(x1))
                   
                                  [1 3]     [2]    [1 2]     [0]               
                   a(q1(b(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(y(x1)))
                   
                                  [1 3]     [2]    [1 2]     [0]               
                   y(q1(b(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(y(y(x1)))
                   
                               [1 1]     [0]    [1 1]     [0]            
                   q0(a(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = x(q1(x1))
                   
                               [1 1]     [0]    [1 0]              
                   q0(y(x1)) = [0 0]x1 + [1] >= [0 0]x1 = y(q3(x1))
                   
                                [1 0]     [1]    [1 0]     [1]             
                   q3(bl(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = bl(q4(x1))
                  problem:
                   strict:
                    q3(y(x1)) -> y(q3(x1))
                   weak:
                    a(q2(a(x1))) -> q2(a(a(x1)))
                    a(q2(y(x1))) -> q2(a(y(x1)))
                    q1(y(x1)) -> y(q1(x1))
                    q1(a(x1)) -> a(q1(x1))
                    y(q2(a(x1))) -> q2(y(a(x1)))
                    y(q2(y(x1))) -> q2(y(y(x1)))
                    q2(x(x1)) -> x(q0(x1))
                    a(q1(b(x1))) -> q2(a(y(x1)))
                    y(q1(b(x1))) -> q2(y(y(x1)))
                    q0(a(x1)) -> x(q1(x1))
                    q0(y(x1)) -> y(q3(x1))
                    q3(bl(x1)) -> bl(q4(x1))
                  Matrix Interpretation Processor:
                   dimension: 2
                   max_matrix:
                    [1 1]
                    [0 1]
                    interpretation:
                                [1 0]  
                     [q4](x0) = [0 0]x0,
                     
                                [1 0]  
                     [bl](x0) = [0 0]x0,
                     
                                [1 1]  
                     [q3](x0) = [0 1]x0,
                     
                                [1 1]     [0]
                     [q2](x0) = [0 1]x0 + [1],
                     
                               [1 1]     [0]
                     [b](x0) = [0 1]x0 + [1],
                     
                               [1 1]     [0]
                     [y](x0) = [0 1]x0 + [1],
                     
                                 
                     [x](x0) = x0,
                     
                                [1 1]     [0]
                     [q1](x0) = [0 1]x0 + [1],
                     
                                [1 1]     [0]
                     [q0](x0) = [0 1]x0 + [1],
                     
                                 
                     [a](x0) = x0
                    orientation:
                                 [1 2]     [1]    [1 2]     [0]            
                     q3(y(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = y(q3(x1))
                     
                                    [1 1]     [0]    [1 1]     [0]               
                     a(q2(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(a(a(x1)))
                     
                                    [1 2]     [1]    [1 2]     [1]               
                     a(q2(y(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(y(x1)))
                     
                                 [1 2]     [1]    [1 2]     [1]            
                     q1(y(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = y(q1(x1))
                     
                                 [1 1]     [0]    [1 1]     [0]            
                     q1(a(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(q1(x1))
                     
                                    [1 2]     [1]    [1 2]     [1]               
                     y(q2(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(y(a(x1)))
                     
                                    [1 3]     [3]    [1 3]     [3]               
                     y(q2(y(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(y(y(x1)))
                     
                                 [1 1]     [0]    [1 1]     [0]            
                     q2(x(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = x(q0(x1))
                     
                                    [1 2]     [1]    [1 2]     [1]               
                     a(q1(b(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(y(x1)))
                     
                                    [1 3]     [3]    [1 3]     [3]               
                     y(q1(b(x1))) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(y(y(x1)))
                     
                                 [1 1]     [0]    [1 1]     [0]            
                     q0(a(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = x(q1(x1))
                     
                                 [1 2]     [1]    [1 2]     [0]            
                     q0(y(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [1] = y(q3(x1))
                     
                                  [1 0]      [1 0]               
                     q3(bl(x1)) = [0 0]x1 >= [0 0]x1 = bl(q4(x1))
                    problem:
                     strict:
                      
                     weak:
                      q3(y(x1)) -> y(q3(x1))
                      a(q2(a(x1))) -> q2(a(a(x1)))
                      a(q2(y(x1))) -> q2(a(y(x1)))
                      q1(y(x1)) -> y(q1(x1))
                      q1(a(x1)) -> a(q1(x1))
                      y(q2(a(x1))) -> q2(y(a(x1)))
                      y(q2(y(x1))) -> q2(y(y(x1)))
                      q2(x(x1)) -> x(q0(x1))
                      a(q1(b(x1))) -> q2(a(y(x1)))
                      y(q1(b(x1))) -> q2(y(y(x1)))
                      q0(a(x1)) -> x(q1(x1))
                      q0(y(x1)) -> y(q3(x1))
                      q3(bl(x1)) -> bl(q4(x1))
                    Qed