NO

Problem:
 a(b(x)) -> b(c(x))
 a(c(x)) -> c(a(x))
 b(b(x)) -> a(c(x))
 c(b(x)) -> b(c(x))
 c(b(x)) -> c(c(x))
 c(c(x)) -> c(b(x))
 P(x) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 p(Q(Q(x))) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 q(q(p(x))) -> p(q(q(x)))
 q(Q(x)) -> x
 Q(q(x)) -> x
 p(P(x)) -> x
 P(p(x)) -> x

Proof:
 sorted: (order-sorted)
 0:P(x) -> Q(Q(p(x)))
   p(p(x)) -> q(q(x))
   p(Q(Q(x))) -> Q(Q(p(x)))
   Q(p(q(x))) -> q(p(Q(x)))
   q(q(p(x))) -> p(q(q(x)))
   q(Q(x)) -> x
   Q(q(x)) -> x
   p(P(x)) -> x
   P(p(x)) -> x
 1:a(b(x)) -> b(c(x))
   a(c(x)) -> c(a(x))
   b(b(x)) -> a(c(x))
   c(b(x)) -> b(c(x))
   c(b(x)) -> c(c(x))
   c(c(x)) -> c(b(x))
 -----
 sorts
   []
 sort attachment (non-strict)
   a : 1 -> 1
   b : 1 -> 1
   c : 1 -> 1
   P : 0 -> 0
   Q : 0 -> 0
   p : 0 -> 0
   q : 0 -> 0
 -----
 0:P(x) -> Q(Q(p(x)))
   p(p(x)) -> q(q(x))
   p(Q(Q(x))) -> Q(Q(p(x)))
   Q(p(q(x))) -> q(p(Q(x)))
   q(q(p(x))) -> p(q(q(x)))
   q(Q(x)) -> x
   Q(q(x)) -> x
   p(P(x)) -> x
   P(p(x)) -> x
   AT confluence processor
    Complete TRS T' of input TRS:
    P(x) -> Q(Q(p(x)))
    p(p(x)) -> q(q(x))
    p(Q(Q(x))) -> Q(Q(p(x)))
    Q(p(q(x))) -> q(p(Q(x)))
    q(q(p(x))) -> p(q(q(x)))
    q(Q(x)) -> x
    Q(q(x)) -> x
    p(P(x)) -> x
    P(p(x)) -> x
    
     T' = (P union S) with
    
     TRS P:
    
     TRS S:P(x) -> Q(Q(p(x)))
           p(p(x)) -> q(q(x))
           p(Q(Q(x))) -> Q(Q(p(x)))
           Q(p(q(x))) -> q(p(Q(x)))
           q(q(p(x))) -> p(q(q(x)))
           q(Q(x)) -> x
           Q(q(x)) -> x
           p(P(x)) -> x
           P(p(x)) -> x
    
    S is left-linear and P is reversible.
    
     CP(S,S) = 
    p(Q(Q(p(x)))) = x, Q(Q(p(p(x)))) = x, p(q(q(x1838))) = q(q(p(x1838))), 
    q(q(q(q(x1839)))) = p(q(q(p(x1839)))), P(q(q(x1840))) = p(x1840), 
    p(Q(Q(p(x1841)))) = q(q(Q(Q(x1841)))), q(q(Q(Q(p(x1842))))) = p(q(q(Q(Q(x1842))))), 
    P(Q(Q(p(x1843)))) = Q(Q(x1843)), p(Q(q(p(Q(x1844))))) = Q(Q(p(p(q(x1844))))), 
    q(q(p(Q(x1845)))) = p(q(x1845)), Q(p(p(q(q(x1846))))) = q(p(Q(q(p(x1846))))), 
    Q(p(q(q(x1847)))) = q(p(x1847)), Q(p(x1848)) = q(p(Q(Q(x1848)))), 
    Q(x1849) = Q(x1849), p(Q(x1850)) = Q(Q(p(q(x1850)))), q(x1851) = 
    q(x1851), p(x1852) = q(q(P(x1852))), q(q(x1853)) = p(q(q(P(x1853)))), 
    P(x1854) = P(x1854), x1855 = Q(Q(p(p(x1855)))), p(x1856) = p(x1856)
    
     CP(S,P union P^-1) = 
    
    
     PCP_in(P union P^-1,S) = 
    
    
    We have to check termination of S:
    
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [p](x0) = 4x0 + 3,
      
      [P](x0) = 5x0 + 4,
      
      [Q](x0) = x0,
      
      [q](x0) = 2x0 + 1
     orientation:
      P(x) = 5x + 4 >= 4x + 3 = Q(Q(p(x)))
      
      p(p(x)) = 16x + 15 >= 4x + 3 = q(q(x))
      
      p(Q(Q(x))) = 4x + 3 >= 4x + 3 = Q(Q(p(x)))
      
      Q(p(q(x))) = 8x + 7 >= 8x + 7 = q(p(Q(x)))
      
      q(q(p(x))) = 16x + 15 >= 16x + 15 = p(q(q(x)))
      
      q(Q(x)) = 2x + 1 >= x = x
      
      Q(q(x)) = 2x + 1 >= x = x
      
      p(P(x)) = 20x + 19 >= x = x
      
      P(p(x)) = 20x + 19 >= x = x
     problem:
      p(Q(Q(x))) -> Q(Q(p(x)))
      Q(p(q(x))) -> q(p(Q(x)))
      q(q(p(x))) -> p(q(q(x)))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [p](x0) = x0,
       
       [Q](x0) = 4x0,
       
       [q](x0) = 2x0 + 1
      orientation:
       p(Q(Q(x))) = 16x >= 16x = Q(Q(p(x)))
       
       Q(p(q(x))) = 8x + 4 >= 8x + 1 = q(p(Q(x)))
       
       q(q(p(x))) = 4x + 3 >= 4x + 3 = p(q(q(x)))
      problem:
       p(Q(Q(x))) -> Q(Q(p(x)))
       q(q(p(x))) -> p(q(q(x)))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [p](x0) = 2x0 + 2,
        
        [Q](x0) = x0,
        
        [q](x0) = 2x0 + 1
       orientation:
        p(Q(Q(x))) = 2x + 2 >= 2x + 2 = Q(Q(p(x)))
        
        q(q(p(x))) = 8x + 11 >= 8x + 8 = p(q(q(x)))
       problem:
        p(Q(Q(x))) -> Q(Q(p(x)))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [p](x0) = 2x0 + 1,
         
         [Q](x0) = 2x0 + 4
        orientation:
         p(Q(Q(x))) = 8x + 25 >= 8x + 16 = Q(Q(p(x)))
        problem:
         
        Qed


1:a(b(x)) -> b(c(x))
  a(c(x)) -> c(a(x))
  b(b(x)) -> a(c(x))
  c(b(x)) -> b(c(x))
  c(b(x)) -> c(c(x))
  c(c(x)) -> c(b(x))
  Nonconfluence Processor:
   terms: c(a(a(x1644))) *<- a(b(b(x1644))) ->* b(c(a(x1644)))
   Qed