MAYBE

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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [q](x0) = x0 + 1,
     
     [Q](x0) = x0 + 1,
     
     [p](x0) = x0 + 1,
     
     [P](x0) = x0
    orientation:
     P(x1) = x1 >= x1 + 3 = Q(Q(p(x1)))
     
     p(p(x1)) = x1 + 2 >= x1 + 2 = q(q(x1))
     
     p(Q(Q(x1))) = x1 + 3 >= x1 + 3 = Q(Q(p(x1)))
     
     Q(p(q(x1))) = x1 + 3 >= x1 + 3 = q(p(Q(x1)))
     
     q(q(p(x1))) = x1 + 3 >= x1 + 3 = p(q(q(x1)))
     
     q(Q(x1)) = x1 + 2 >= x1 = x1
     
     Q(q(x1)) = x1 + 2 >= x1 = x1
     
     p(P(x1)) = x1 + 1 >= x1 = x1
     
     P(p(x1)) = x1 + 1 >= x1 = x1
    problem:
     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)))
     weak:
      q(Q(x1)) -> x1
      Q(q(x1)) -> x1
      p(P(x1)) -> x1
      P(p(x1)) -> x1
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [q](x0) = x0,
       
       [Q](x0) = x0,
       
       [p](x0) = x0,
       
       [P](x0) = x0 + 1
      orientation:
       P(x1) = x1 + 1 >= x1 = Q(Q(p(x1)))
       
       p(p(x1)) = x1 >= x1 = q(q(x1))
       
       p(Q(Q(x1))) = x1 >= x1 = Q(Q(p(x1)))
       
       Q(p(q(x1))) = x1 >= x1 = q(p(Q(x1)))
       
       q(q(p(x1))) = x1 >= x1 = p(q(q(x1)))
       
       q(Q(x1)) = x1 >= x1 = x1
       
       Q(q(x1)) = x1 >= x1 = x1
       
       p(P(x1)) = x1 + 1 >= x1 = x1
       
       P(p(x1)) = x1 + 1 >= x1 = x1
      problem:
       strict:
        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)))
       weak:
        P(x1) -> Q(Q(p(x1)))
        q(Q(x1)) -> x1
        Q(q(x1)) -> x1
        p(P(x1)) -> x1
        P(p(x1)) -> x1
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [q](x0) = x0,
         
         [Q](x0) = x0,
         
         [p](x0) = x0 + 1,
         
         [P](x0) = x0 + 1
        orientation:
         p(p(x1)) = x1 + 2 >= x1 = q(q(x1))
         
         p(Q(Q(x1))) = x1 + 1 >= x1 + 1 = Q(Q(p(x1)))
         
         Q(p(q(x1))) = x1 + 1 >= x1 + 1 = q(p(Q(x1)))
         
         q(q(p(x1))) = x1 + 1 >= x1 + 1 = p(q(q(x1)))
         
         P(x1) = x1 + 1 >= x1 + 1 = Q(Q(p(x1)))
         
         q(Q(x1)) = x1 >= x1 = x1
         
         Q(q(x1)) = x1 >= x1 = x1
         
         p(P(x1)) = x1 + 2 >= x1 = x1
         
         P(p(x1)) = x1 + 2 >= 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(p(x1)) -> q(q(x1))
          P(x1) -> Q(Q(p(x1)))
          q(Q(x1)) -> x1
          Q(q(x1)) -> x1
          p(P(x1)) -> x1
          P(p(x1)) -> x1
        Open