YES

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:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [q](x0) = 1x0,
   
   [Q](x0) = x0,
   
   [p](x0) = 1x0,
   
   [P](x0) = 1x0
  orientation:
   P(x1) = 1x1 >= 1x1 = Q(Q(p(x1)))
   
   p(p(x1)) = 2x1 >= 2x1 = q(q(x1))
   
   p(Q(Q(x1))) = 1x1 >= 1x1 = Q(Q(p(x1)))
   
   Q(p(q(x1))) = 2x1 >= 2x1 = q(p(Q(x1)))
   
   q(q(p(x1))) = 3x1 >= 3x1 = p(q(q(x1)))
   
   q(Q(x1)) = 1x1 >= x1 = x1
   
   Q(q(x1)) = 1x1 >= x1 = x1
   
   p(P(x1)) = 2x1 >= x1 = x1
   
   P(p(x1)) = 2x1 >= x1 = x1
  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)))
  Arctic Interpretation Processor:
   dimension: 2
   interpretation:
                
    [q](x0) = x0,
    
              [0  -&]  
    [Q](x0) = [1  0 ]x0,
    
                
    [p](x0) = x0,
    
              [1 0]  
    [P](x0) = [2 2]x0
   orientation:
            [1 0]      [0  -&]                
    P(x1) = [2 2]x1 >= [1  0 ]x1 = Q(Q(p(x1)))
    
                                  
    p(p(x1)) = x1 >= x1 = q(q(x1))
    
                  [0  -&]      [0  -&]                
    p(Q(Q(x1))) = [1  0 ]x1 >= [1  0 ]x1 = Q(Q(p(x1)))
    
                  [0  -&]      [0  -&]                
    Q(p(q(x1))) = [1  0 ]x1 >= [1  0 ]x1 = q(p(Q(x1)))
    
                                        
    q(q(p(x1))) = x1 >= x1 = p(q(q(x1)))
   problem:
    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)))
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [q](x0) = x0,
     
     [Q](x0) = x0,
     
     [p](x0) = 8x0
    orientation:
     p(p(x1)) = 16x1 >= x1 = q(q(x1))
     
     p(Q(Q(x1))) = 8x1 >= 8x1 = Q(Q(p(x1)))
     
     Q(p(q(x1))) = 8x1 >= 8x1 = q(p(Q(x1)))
     
     q(q(p(x1))) = 8x1 >= 8x1 = p(q(q(x1)))
    problem:
     p(Q(Q(x1))) -> Q(Q(p(x1)))
     Q(p(q(x1))) -> q(p(Q(x1)))
     q(q(p(x1))) -> p(q(q(x1)))
    String Reversal Processor:
     Q(Q(p(x1))) -> p(Q(Q(x1)))
     q(p(Q(x1))) -> Q(p(q(x1)))
     p(q(q(x1))) -> q(q(p(x1)))
     Bounds Processor:
      bound: 0
      enrichment: match
      automaton:
       final states: {8,5,1}
       transitions:
        f40() -> 2*
        p0(2) -> 9*
        p0(4) -> 1*
        p0(6) -> 7*
        Q0(7) -> 5*
        Q0(2) -> 3*
        Q0(3) -> 4*
        q0(10) -> 8*
        q0(2) -> 6*
        q0(9) -> 10*
        1 -> 3,4
        5 -> 6,10
        8 -> 9,7
      problem:
       
      Qed