YES

Problem:
 a(b(x)) -> b(a(a(x)))
 b(c(x)) -> c(b(b(x)))
 c(a(x)) -> a(c(c(x)))
 u(a(x)) -> x
 v(b(x)) -> x
 w(c(x)) -> x
 a(u(x)) -> x
 b(v(x)) -> x
 c(w(x)) -> x

Proof:
 DP Processor:
  DPs:
   a#(b(x)) -> a#(x)
   a#(b(x)) -> a#(a(x))
   a#(b(x)) -> b#(a(a(x)))
   b#(c(x)) -> b#(x)
   b#(c(x)) -> b#(b(x))
   b#(c(x)) -> c#(b(b(x)))
   c#(a(x)) -> c#(x)
   c#(a(x)) -> c#(c(x))
   c#(a(x)) -> a#(c(c(x)))
  TRS:
   a(b(x)) -> b(a(a(x)))
   b(c(x)) -> c(b(b(x)))
   c(a(x)) -> a(c(c(x)))
   u(a(x)) -> x
   v(b(x)) -> x
   w(c(x)) -> x
   a(u(x)) -> x
   b(v(x)) -> x
   c(w(x)) -> x
  Usable Rule Processor:
   DPs:
    a#(b(x)) -> a#(x)
    a#(b(x)) -> a#(a(x))
    a#(b(x)) -> b#(a(a(x)))
    b#(c(x)) -> b#(x)
    b#(c(x)) -> b#(b(x))
    b#(c(x)) -> c#(b(b(x)))
    c#(a(x)) -> c#(x)
    c#(a(x)) -> c#(c(x))
    c#(a(x)) -> a#(c(c(x)))
   TRS:
    a(b(x)) -> b(a(a(x)))
    a(u(x)) -> x
    b(c(x)) -> c(b(b(x)))
    b(v(x)) -> x
    c(a(x)) -> a(c(c(x)))
    c(w(x)) -> x
   Matrix Interpretation Processor: dim=5
    
    interpretation:
     [c#](x0) = [1 0 1 0 0]x0,
     
     [b#](x0) = [0 1 0 0 1]x0,
     
     [a#](x0) = [0 0 0 1 0]x0,
     
               [1 0 1 1 0]  
               [0 0 0 0 0]  
     [w](x0) = [0 1 1 1 1]x0
               [0 0 0 0 0]  
               [0 0 0 1 0]  ,
     
               [0 0 0 0 0]     [0]
               [0 1 1 1 1]     [0]
     [v](x0) = [0 0 0 0 1]x0 + [0]
               [0 0 0 0 1]     [1]
               [1 1 1 1 0]     [0],
     
               [1 1 0 1 1]     [1]
               [0 0 0 0 0]     [0]
     [u](x0) = [0 1 1 0 1]x0 + [0]
               [1 1 0 1 1]     [1]
               [1 1 1 0 1]     [0],
     
               [1 0 0 0 0]     [0]
               [0 1 1 0 1]     [1]
     [c](x0) = [0 0 1 0 0]x0 + [0]
               [0 0 1 0 0]     [0]
               [0 0 1 0 0]     [0],
     
               [1 0 0 0 0]     [1]
               [0 0 0 1 0]     [0]
     [a](x0) = [0 0 1 0 0]x0 + [0]
               [0 0 0 1 0]     [0]
               [0 0 0 0 1]     [0],
     
               [0 0 0 0 1]     [0]
               [0 1 0 0 0]     [0]
     [b](x0) = [0 0 0 0 1]x0 + [0]
               [0 0 1 1 1]     [1]
               [0 0 1 0 0]     [0]
    orientation:
     a#(b(x)) = [0 0 1 1 1]x + [1] >= [0 0 0 1 0]x = a#(x)
     
     a#(b(x)) = [0 0 1 1 1]x + [1] >= [0 0 0 1 0]x = a#(a(x))
     
     a#(b(x)) = [0 0 1 1 1]x + [1] >= [0 0 0 1 1]x = b#(a(a(x)))
     
     b#(c(x)) = [0 1 2 0 1]x + [1] >= [0 1 0 0 1]x = b#(x)
     
     b#(c(x)) = [0 1 2 0 1]x + [1] >= [0 1 1 0 0]x = b#(b(x))
     
     b#(c(x)) = [0 1 2 0 1]x + [1] >= [0 0 2 0 0]x = c#(b(b(x)))
     
     c#(a(x)) = [1 0 1 0 0]x + [1] >= [1 0 1 0 0]x = c#(x)
     
     c#(a(x)) = [1 0 1 0 0]x + [1] >= [1 0 1 0 0]x = c#(c(x))
     
     c#(a(x)) = [1 0 1 0 0]x + [1] >= [0 0 1 0 0]x = a#(c(c(x)))
     
               [0 0 0 0 1]    [1]    [0 0 0 0 1]    [0]             
               [0 0 1 1 1]    [1]    [0 0 0 1 0]    [0]             
     a(b(x)) = [0 0 0 0 1]x + [0] >= [0 0 0 0 1]x + [0] = b(a(a(x)))
               [0 0 1 1 1]    [1]    [0 0 1 1 1]    [1]             
               [0 0 1 0 0]    [0]    [0 0 1 0 0]    [0]             
     
               [1 1 0 1 1]    [2]         
               [1 1 0 1 1]    [1]         
     a(u(x)) = [0 1 1 0 1]x + [0] >= x = x
               [1 1 0 1 1]    [1]         
               [1 1 1 0 1]    [0]         
     
               [0 0 1 0 0]    [0]    [0 0 1 0 0]    [0]             
               [0 1 1 0 1]    [1]    [0 1 1 0 1]    [1]             
     b(c(x)) = [0 0 1 0 0]x + [0] >= [0 0 1 0 0]x + [0] = c(b(b(x)))
               [0 0 3 0 0]    [1]    [0 0 1 0 0]    [0]             
               [0 0 1 0 0]    [0]    [0 0 1 0 0]    [0]             
     
               [1 1 1 1 0]    [0]         
               [0 1 1 1 1]    [0]         
     b(v(x)) = [1 1 1 1 0]x + [0] >= x = x
               [1 1 1 1 2]    [2]         
               [0 0 0 0 1]    [0]         
     
               [1 0 0 0 0]    [1]    [1 0 0 0 0]    [1]             
               [0 0 1 1 1]    [1]    [0 0 1 0 0]    [0]             
     c(a(x)) = [0 0 1 0 0]x + [0] >= [0 0 1 0 0]x + [0] = a(c(c(x)))
               [0 0 1 0 0]    [0]    [0 0 1 0 0]    [0]             
               [0 0 1 0 0]    [0]    [0 0 1 0 0]    [0]             
     
               [1 0 1 1 0]    [0]         
               [0 1 1 2 1]    [1]         
     c(w(x)) = [0 1 1 1 1]x + [0] >= x = x
               [0 1 1 1 1]    [0]         
               [0 1 1 1 1]    [0]         
    problem:
     DPs:
      
     TRS:
      a(b(x)) -> b(a(a(x)))
      a(u(x)) -> x
      b(c(x)) -> c(b(b(x)))
      b(v(x)) -> x
      c(a(x)) -> a(c(c(x)))
      c(w(x)) -> x
    Qed