YES(?,O(n^3))

Problem:
 P(x1) -> Q(Q(p(x1)))
 p(p(x1)) -> q(q(x1))
 p(Q(Q(x1))) -> Q(Q(p(x1)))
 Q(p(q(x1))) -> q(p(Q(x1)))
 q(q(p(x1))) -> p(q(q(x1)))
 q(Q(x1)) -> x1
 Q(q(x1)) -> x1
 p(P(x1)) -> x1
 P(p(x1)) -> x1

Proof:
 RT Transformation Processor:
  strict:
   P(x1) -> Q(Q(p(x1)))
   p(p(x1)) -> q(q(x1))
   p(Q(Q(x1))) -> Q(Q(p(x1)))
   Q(p(q(x1))) -> q(p(Q(x1)))
   q(q(p(x1))) -> p(q(q(x1)))
   q(Q(x1)) -> x1
   Q(q(x1)) -> x1
   p(P(x1)) -> x1
   P(p(x1)) -> x1
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [q](x0) = x0,
    
    [Q](x0) = x0 + 8,
    
    [p](x0) = x0 + 20,
    
    [P](x0) = x0 + 15
   orientation:
    P(x1) = x1 + 15 >= x1 + 36 = Q(Q(p(x1)))
    
    p(p(x1)) = x1 + 40 >= x1 = q(q(x1))
    
    p(Q(Q(x1))) = x1 + 36 >= x1 + 36 = Q(Q(p(x1)))
    
    Q(p(q(x1))) = x1 + 28 >= x1 + 28 = q(p(Q(x1)))
    
    q(q(p(x1))) = x1 + 20 >= x1 + 20 = p(q(q(x1)))
    
    q(Q(x1)) = x1 + 8 >= x1 = x1
    
    Q(q(x1)) = x1 + 8 >= x1 = x1
    
    p(P(x1)) = x1 + 35 >= x1 = x1
    
    P(p(x1)) = x1 + 35 >= x1 = x1
   problem:
    strict:
     P(x1) -> Q(Q(p(x1)))
     p(Q(Q(x1))) -> Q(Q(p(x1)))
     Q(p(q(x1))) -> q(p(Q(x1)))
     q(q(p(x1))) -> p(q(q(x1)))
    weak:
     p(p(x1)) -> q(q(x1))
     q(Q(x1)) -> x1
     Q(q(x1)) -> x1
     p(P(x1)) -> x1
     P(p(x1)) -> x1
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [q](x0) = x0 + 4,
     
     [Q](x0) = x0 + 2,
     
     [p](x0) = x0 + 24,
     
     [P](x0) = x0 + 29
    orientation:
     P(x1) = x1 + 29 >= x1 + 28 = Q(Q(p(x1)))
     
     p(Q(Q(x1))) = x1 + 28 >= x1 + 28 = Q(Q(p(x1)))
     
     Q(p(q(x1))) = x1 + 30 >= x1 + 30 = q(p(Q(x1)))
     
     q(q(p(x1))) = x1 + 32 >= x1 + 32 = p(q(q(x1)))
     
     p(p(x1)) = x1 + 48 >= x1 + 8 = q(q(x1))
     
     q(Q(x1)) = x1 + 6 >= x1 = x1
     
     Q(q(x1)) = x1 + 6 >= x1 = x1
     
     p(P(x1)) = x1 + 53 >= x1 = x1
     
     P(p(x1)) = x1 + 53 >= x1 = x1
    problem:
     strict:
      p(Q(Q(x1))) -> Q(Q(p(x1)))
      Q(p(q(x1))) -> q(p(Q(x1)))
      q(q(p(x1))) -> p(q(q(x1)))
     weak:
      P(x1) -> Q(Q(p(x1)))
      p(p(x1)) -> q(q(x1))
      q(Q(x1)) -> x1
      Q(q(x1)) -> x1
      p(P(x1)) -> x1
      P(p(x1)) -> x1
    Matrix Interpretation Processor:
     dimension: 3
     interpretation:
                     [0]
      [q](x0) = x0 + [1]
                     [0],
      
                [1 1 0]     [0]
      [Q](x0) = [0 1 3]x0 + [1]
                [0 0 1]     [1],
      
                [1 0 1]     [0]
      [p](x0) = [0 1 0]x0 + [1]
                [0 0 1]     [0],
      
                [1 2 4]     [3]
      [P](x0) = [0 1 6]x0 + [6]
                [0 0 1]     [2]
     orientation:
                    [1 2 4]     [3]    [1 2 4]     [3]              
      p(Q(Q(x1))) = [0 1 6]x1 + [6] >= [0 1 6]x1 + [6] = Q(Q(p(x1)))
                    [0 0 1]     [2]    [0 0 1]     [2]              
      
                    [1 1 1]     [2]    [1 1 1]     [1]              
      Q(p(q(x1))) = [0 1 3]x1 + [3] >= [0 1 3]x1 + [3] = q(p(Q(x1)))
                    [0 0 1]     [1]    [0 0 1]     [1]              
      
                    [1 0 1]     [0]    [1 0 1]     [0]              
      q(q(p(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = p(q(q(x1)))
                    [0 0 1]     [0]    [0 0 1]     [0]              
      
              [1 2 4]     [3]    [1 2 4]     [3]              
      P(x1) = [0 1 6]x1 + [6] >= [0 1 6]x1 + [6] = Q(Q(p(x1)))
              [0 0 1]     [2]    [0 0 1]     [2]              
      
                 [1 0 2]     [0]         [0]           
      p(p(x1)) = [0 1 0]x1 + [2] >= x1 + [2] = q(q(x1))
                 [0 0 1]     [0]         [0]           
      
                 [1 1 0]     [0]           
      q(Q(x1)) = [0 1 3]x1 + [2] >= x1 = x1
                 [0 0 1]     [1]           
      
                 [1 1 0]     [1]           
      Q(q(x1)) = [0 1 3]x1 + [2] >= x1 = x1
                 [0 0 1]     [1]           
      
                 [1 2 5]     [5]           
      p(P(x1)) = [0 1 6]x1 + [7] >= x1 = x1
                 [0 0 1]     [2]           
      
                 [1 2 5]     [5]           
      P(p(x1)) = [0 1 6]x1 + [7] >= x1 = x1
                 [0 0 1]     [2]           
     problem:
      strict:
       p(Q(Q(x1))) -> Q(Q(p(x1)))
       q(q(p(x1))) -> p(q(q(x1)))
      weak:
       Q(p(q(x1))) -> q(p(Q(x1)))
       P(x1) -> Q(Q(p(x1)))
       p(p(x1)) -> q(q(x1))
       q(Q(x1)) -> x1
       Q(q(x1)) -> x1
       p(P(x1)) -> x1
       P(p(x1)) -> x1
     Matrix Interpretation Processor:
      dimension: 3
      interpretation:
                      [0]
       [q](x0) = x0 + [1]
                      [0],
       
                 [1 2 0]     [0]
       [Q](x0) = [0 1 0]x0 + [0]
                 [0 0 1]     [2],
       
                 [1 0 2]     [0]
       [p](x0) = [0 1 0]x0 + [1]
                 [0 0 1]     [0],
       
                 [1 4 2]     [4]
       [P](x0) = [0 1 0]x0 + [1]
                 [0 0 1]     [4]
      orientation:
                     [1 4 2]     [8]    [1 4 2]     [4]              
       p(Q(Q(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = Q(Q(p(x1)))
                     [0 0 1]     [4]    [0 0 1]     [4]              
       
                     [1 0 2]     [0]    [1 0 2]     [0]              
       q(q(p(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = p(q(q(x1)))
                     [0 0 1]     [0]    [0 0 1]     [0]              
       
                     [1 2 2]     [4]    [1 2 2]     [4]              
       Q(p(q(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q(p(Q(x1)))
                     [0 0 1]     [2]    [0 0 1]     [2]              
       
               [1 4 2]     [4]    [1 4 2]     [4]              
       P(x1) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = Q(Q(p(x1)))
               [0 0 1]     [4]    [0 0 1]     [4]              
       
                  [1 0 4]     [0]         [0]           
       p(p(x1)) = [0 1 0]x1 + [2] >= x1 + [2] = q(q(x1))
                  [0 0 1]     [0]         [0]           
       
                  [1 2 0]     [0]           
       q(Q(x1)) = [0 1 0]x1 + [1] >= x1 = x1
                  [0 0 1]     [2]           
       
                  [1 2 0]     [2]           
       Q(q(x1)) = [0 1 0]x1 + [1] >= x1 = x1
                  [0 0 1]     [2]           
       
                  [1 4 4]     [12]           
       p(P(x1)) = [0 1 0]x1 + [2 ] >= x1 = x1
                  [0 0 1]     [4 ]           
       
                  [1 4 4]     [8]           
       P(p(x1)) = [0 1 0]x1 + [2] >= x1 = x1
                  [0 0 1]     [4]           
      problem:
       strict:
        q(q(p(x1))) -> p(q(q(x1)))
       weak:
        p(Q(Q(x1))) -> Q(Q(p(x1)))
        Q(p(q(x1))) -> q(p(Q(x1)))
        P(x1) -> Q(Q(p(x1)))
        p(p(x1)) -> q(q(x1))
        q(Q(x1)) -> x1
        Q(q(x1)) -> x1
        p(P(x1)) -> x1
        P(p(x1)) -> x1
      Matrix Interpretation Processor:
       dimension: 3
       interpretation:
                  [1 2 0]     [0]
        [q](x0) = [0 1 0]x0 + [1]
                  [0 0 1]     [0],
        
                  [1 1 0]     [1]
        [Q](x0) = [0 1 0]x0 + [0]
                  [0 0 1]     [2],
        
                  [1 3 1]     [1]
        [p](x0) = [0 1 0]x0 + [2]
                  [0 0 1]     [0],
        
                  [1 6 3]     [7]
        [P](x0) = [0 1 0]x0 + [2]
                  [0 0 1]     [4]
       orientation:
                      [1 7 1]     [11]    [1 7 1]     [9]              
        q(q(p(x1))) = [0 1 0]x1 + [4 ] >= [0 1 0]x1 + [4] = p(q(q(x1)))
                      [0 0 1]     [0 ]    [0 0 1]     [0]              
        
                      [1 5 1]     [7]    [1 5 1]     [7]              
        p(Q(Q(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = Q(Q(p(x1)))
                      [0 0 1]     [4]    [0 0 1]     [4]              
        
                      [1 6 1]     [8]    [1 6 1]     [8]              
        Q(p(q(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q(p(Q(x1)))
                      [0 0 1]     [2]    [0 0 1]     [2]              
        
                [1 6 3]     [7]    [1 5 1]     [7]              
        P(x1) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = Q(Q(p(x1)))
                [0 0 1]     [4]    [0 0 1]     [4]              
        
                   [1 6 2]     [8]    [1 4 0]     [2]           
        p(p(x1)) = [0 1 0]x1 + [4] >= [0 1 0]x1 + [2] = q(q(x1))
                   [0 0 1]     [0]    [0 0 1]     [0]           
        
                   [1 3 0]     [1]           
        q(Q(x1)) = [0 1 0]x1 + [1] >= x1 = x1
                   [0 0 1]     [2]           
        
                   [1 3 0]     [2]           
        Q(q(x1)) = [0 1 0]x1 + [1] >= x1 = x1
                   [0 0 1]     [2]           
        
                   [1 9 4]     [18]           
        p(P(x1)) = [0 1 0]x1 + [4 ] >= x1 = x1
                   [0 0 1]     [4 ]           
        
                   [1 9 4]     [20]           
        P(p(x1)) = [0 1 0]x1 + [4 ] >= x1 = x1
                   [0 0 1]     [4 ]           
       problem:
        strict:
         
        weak:
         q(q(p(x1))) -> p(q(q(x1)))
         p(Q(Q(x1))) -> Q(Q(p(x1)))
         Q(p(q(x1))) -> q(p(Q(x1)))
         P(x1) -> Q(Q(p(x1)))
         p(p(x1)) -> q(q(x1))
         q(Q(x1)) -> x1
         Q(q(x1)) -> x1
         p(P(x1)) -> x1
         P(p(x1)) -> x1
       Qed