YES(?,O(n^2))

Problem:
 1(q0(1(x1))) -> 0(1(q1(x1)))
 1(q0(0(x1))) -> 0(0(q1(x1)))
 1(q1(1(x1))) -> 1(1(q1(x1)))
 1(q1(0(x1))) -> 1(0(q1(x1)))
 0(q1(x1)) -> q2(1(x1))
 1(q2(x1)) -> q2(1(x1))
 0(q2(x1)) -> 0(q0(x1))

Proof:
 RT Transformation Processor:
  strict:
   1(q0(1(x1))) -> 0(1(q1(x1)))
   1(q0(0(x1))) -> 0(0(q1(x1)))
   1(q1(1(x1))) -> 1(1(q1(x1)))
   1(q1(0(x1))) -> 1(0(q1(x1)))
   0(q1(x1)) -> q2(1(x1))
   1(q2(x1)) -> q2(1(x1))
   0(q2(x1)) -> 0(q0(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [q2](x0) = x0 + 20,
    
    [0](x0) = x0 + 3,
    
    [q1](x0) = x0 + 13,
    
    [q0](x0) = x0 + 1,
    
    [1](x0) = x0 + 20
   orientation:
    1(q0(1(x1))) = x1 + 41 >= x1 + 36 = 0(1(q1(x1)))
    
    1(q0(0(x1))) = x1 + 24 >= x1 + 19 = 0(0(q1(x1)))
    
    1(q1(1(x1))) = x1 + 53 >= x1 + 53 = 1(1(q1(x1)))
    
    1(q1(0(x1))) = x1 + 36 >= x1 + 36 = 1(0(q1(x1)))
    
    0(q1(x1)) = x1 + 16 >= x1 + 40 = q2(1(x1))
    
    1(q2(x1)) = x1 + 40 >= x1 + 40 = q2(1(x1))
    
    0(q2(x1)) = x1 + 23 >= x1 + 4 = 0(q0(x1))
   problem:
    strict:
     1(q1(1(x1))) -> 1(1(q1(x1)))
     1(q1(0(x1))) -> 1(0(q1(x1)))
     0(q1(x1)) -> q2(1(x1))
     1(q2(x1)) -> q2(1(x1))
    weak:
     1(q0(1(x1))) -> 0(1(q1(x1)))
     1(q0(0(x1))) -> 0(0(q1(x1)))
     0(q2(x1)) -> 0(q0(x1))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                     [9]
     [q2](x0) = x0 + [0],
     
               [1 1]     [5]
     [0](x0) = [0 1]x0 + [1],
     
                [1 7]     [5]
     [q1](x0) = [0 1]x0 + [0],
     
                     [4]
     [q0](x0) = x0 + [0],
     
               [1 8]     [1]
     [1](x0) = [0 1]x0 + [1]
    orientation:
                    [1  23]     [22]    [1  23]     [15]               
     1(q1(1(x1))) = [0  1 ]x1 + [2 ] >= [0  1 ]x1 + [2 ] = 1(1(q1(x1)))
     
                    [1  16]     [26]    [1  16]     [19]               
     1(q1(0(x1))) = [0  1 ]x1 + [2 ] >= [0  1 ]x1 + [2 ] = 1(0(q1(x1)))
     
                 [1 8]     [10]    [1 8]     [10]            
     0(q1(x1)) = [0 1]x1 + [1 ] >= [0 1]x1 + [1 ] = q2(1(x1))
     
                 [1 8]     [10]    [1 8]     [10]            
     1(q2(x1)) = [0 1]x1 + [1 ] >= [0 1]x1 + [1 ] = q2(1(x1))
     
                    [1  16]     [14]    [1  16]     [12]               
     1(q0(1(x1))) = [0  1 ]x1 + [2 ] >= [0  1 ]x1 + [2 ] = 0(1(q1(x1)))
     
                    [1 9]     [18]    [1 9]     [16]               
     1(q0(0(x1))) = [0 1]x1 + [2 ] >= [0 1]x1 + [2 ] = 0(0(q1(x1)))
     
                 [1 1]     [14]    [1 1]     [9]            
     0(q2(x1)) = [0 1]x1 + [1 ] >= [0 1]x1 + [1] = 0(q0(x1))
    problem:
     strict:
      0(q1(x1)) -> q2(1(x1))
      1(q2(x1)) -> q2(1(x1))
     weak:
      1(q1(1(x1))) -> 1(1(q1(x1)))
      1(q1(0(x1))) -> 1(0(q1(x1)))
      1(q0(1(x1))) -> 0(1(q1(x1)))
      1(q0(0(x1))) -> 0(0(q1(x1)))
      0(q2(x1)) -> 0(q0(x1))
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                 [1 1]     [2]
      [q2](x0) = [0 1]x0 + [3],
      
                [1 1]     [0]
      [0](x0) = [0 1]x0 + [3],
      
                 [1 3]     [4]
      [q1](x0) = [0 1]x0 + [0],
      
                 [1 1]     [2]
      [q0](x0) = [0 1]x0 + [3],
      
                [1 3]     [2]
      [1](x0) = [0 1]x0 + [0]
     orientation:
                  [1 4]     [4]    [1 4]     [4]            
      0(q1(x1)) = [0 1]x1 + [3] >= [0 1]x1 + [3] = q2(1(x1))
      
                  [1 4]     [13]    [1 4]     [4]            
      1(q2(x1)) = [0 1]x1 + [3 ] >= [0 1]x1 + [3] = q2(1(x1))
      
                     [1 9]     [8]    [1 9]     [8]               
      1(q1(1(x1))) = [0 1]x1 + [0] >= [0 1]x1 + [0] = 1(1(q1(x1)))
      
                     [1 7]     [24]    [1 7]     [15]               
      1(q1(0(x1))) = [0 1]x1 + [3 ] >= [0 1]x1 + [3 ] = 1(0(q1(x1)))
      
                     [1 7]     [15]    [1 7]     [6]               
      1(q0(1(x1))) = [0 1]x1 + [3 ] >= [0 1]x1 + [3] = 0(1(q1(x1)))
      
                     [1 5]     [25]    [1 5]     [7]               
      1(q0(0(x1))) = [0 1]x1 + [6 ] >= [0 1]x1 + [6] = 0(0(q1(x1)))
      
                  [1 2]     [5]    [1 2]     [5]            
      0(q2(x1)) = [0 1]x1 + [6] >= [0 1]x1 + [6] = 0(q0(x1))
     problem:
      strict:
       0(q1(x1)) -> q2(1(x1))
      weak:
       1(q2(x1)) -> q2(1(x1))
       1(q1(1(x1))) -> 1(1(q1(x1)))
       1(q1(0(x1))) -> 1(0(q1(x1)))
       1(q0(1(x1))) -> 0(1(q1(x1)))
       1(q0(0(x1))) -> 0(0(q1(x1)))
       0(q2(x1)) -> 0(q0(x1))
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
                       [2]
       [q2](x0) = x0 + [0],
       
                      [0]
       [0](x0) = x0 + [4],
       
                  [1 1]     [7]
       [q1](x0) = [0 1]x0 + [0],
       
                       [2]
       [q0](x0) = x0 + [0],
       
                 [1 1]     [1]
       [1](x0) = [0 1]x0 + [4]
      orientation:
                   [1 1]     [7]    [1 1]     [3]            
       0(q1(x1)) = [0 1]x1 + [4] >= [0 1]x1 + [4] = q2(1(x1))
       
                   [1 1]     [3]    [1 1]     [3]            
       1(q2(x1)) = [0 1]x1 + [4] >= [0 1]x1 + [4] = q2(1(x1))
       
                      [1 3]     [17]    [1 3]     [13]               
       1(q1(1(x1))) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = 1(1(q1(x1)))
       
                      [1 2]     [16]    [1 2]     [12]               
       1(q1(0(x1))) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = 1(0(q1(x1)))
       
                      [1 2]     [8]    [1 2]     [8]               
       1(q0(1(x1))) = [0 1]x1 + [8] >= [0 1]x1 + [8] = 0(1(q1(x1)))
       
                      [1 1]     [7]    [1 1]     [7]               
       1(q0(0(x1))) = [0 1]x1 + [8] >= [0 1]x1 + [8] = 0(0(q1(x1)))
       
                        [2]         [2]            
       0(q2(x1)) = x1 + [4] >= x1 + [4] = 0(q0(x1))
      problem:
       strict:
        
       weak:
        0(q1(x1)) -> q2(1(x1))
        1(q2(x1)) -> q2(1(x1))
        1(q1(1(x1))) -> 1(1(q1(x1)))
        1(q1(0(x1))) -> 1(0(q1(x1)))
        1(q0(1(x1))) -> 0(1(q1(x1)))
        1(q0(0(x1))) -> 0(0(q1(x1)))
        0(q2(x1)) -> 0(q0(x1))
      Qed