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
  TDG 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
   graph:
    c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> a#(c(c(x)))
    c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> c#(c(x))
    c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> c#(x)
    c#(a(x)) -> c#(x) -> c#(a(x)) -> a#(c(c(x)))
    c#(a(x)) -> c#(x) -> c#(a(x)) -> c#(c(x))
    c#(a(x)) -> c#(x) -> c#(a(x)) -> c#(x)
    c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> b#(a(a(x)))
    c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> a#(a(x))
    c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> a#(x)
    b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> a#(c(c(x)))
    b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> c#(c(x))
    b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> c#(x)
    b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> c#(b(b(x)))
    b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> b#(b(x))
    b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> b#(x)
    b#(c(x)) -> b#(x) -> b#(c(x)) -> c#(b(b(x)))
    b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(b(x))
    b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(x)
    a#(b(x)) -> b#(a(a(x))) -> b#(c(x)) -> c#(b(b(x)))
    a#(b(x)) -> b#(a(a(x))) -> b#(c(x)) -> b#(b(x))
    a#(b(x)) -> b#(a(a(x))) -> b#(c(x)) -> b#(x)
    a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> b#(a(a(x)))
    a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> a#(a(x))
    a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> a#(x)
    a#(b(x)) -> a#(x) -> a#(b(x)) -> b#(a(a(x)))
    a#(b(x)) -> a#(x) -> a#(b(x)) -> a#(a(x))
    a#(b(x)) -> a#(x) -> a#(b(x)) -> a#(x)
   Arctic Interpretation Processor:
    dimension: 2
    interpretation:
     [c#](x0) = [-& 3 ]x0 + [0],
     
     [b#](x0) = [-& 3 ]x0 + [3],
     
     [a#](x0) = [3 0]x0 + [0],
     
               [3  -4]     [-1]
     [w](x0) = [3  3 ]x0 + [-2],
     
               [0  3 ]  
     [v](x0) = [-4 1 ]x0,
     
               [0  2 ]     [-&]
     [u](x0) = [0  -&]x0 + [0 ],
     
               [-3 0 ]     [0 ]
     [c](x0) = [-& 0 ]x0 + [-&],
     
               [0  0 ]     [-&]
     [a](x0) = [-2 0 ]x0 + [1 ],
     
               [0  1 ]     [2]
     [b](x0) = [-& 0 ]x0 + [0]
    orientation:
     a#(b(x)) = [3 4]x + [5] >= [3 0]x + [0] = a#(x)
     
     a#(b(x)) = [3 4]x + [5] >= [3 3]x + [1] = a#(a(x))
     
     a#(b(x)) = [3 4]x + [5] >= [1 3]x + [4] = b#(a(a(x)))
     
     b#(c(x)) = [-& 3 ]x + [3] >= [-& 3 ]x + [3] = b#(x)
     
     b#(c(x)) = [-& 3 ]x + [3] >= [-& 3 ]x + [3] = b#(b(x))
     
     b#(c(x)) = [-& 3 ]x + [3] >= [-& 3 ]x + [3] = c#(b(b(x)))
     
     c#(a(x)) = [1 3]x + [4] >= [-& 3 ]x + [0] = c#(x)
     
     c#(a(x)) = [1 3]x + [4] >= [-& 3 ]x + [0] = c#(c(x))
     
     c#(a(x)) = [1 3]x + [4] >= [-3 3 ]x + [3] = a#(c(c(x)))
     
               [0  1 ]    [2]    [0  1 ]    [2]             
     a(b(x)) = [-2 0 ]x + [1] >= [-2 0 ]x + [1] = b(a(a(x)))
     
               [-3 1 ]    [2]    [-3 0 ]    [0]             
     b(c(x)) = [-& 0 ]x + [0] >= [-& 0 ]x + [0] = c(b(b(x)))
     
               [-2 0 ]    [1]    [-6 0 ]    [0]             
     c(a(x)) = [-2 0 ]x + [1] >= [-8 0 ]x + [1] = a(c(c(x)))
     
               [0 2]    [3]         
     u(a(x)) = [0 0]x + [0] >= x = x
     
               [0  3 ]    [3]         
     v(b(x)) = [-4 1 ]x + [1] >= x = x
     
               [0 3]    [3]         
     w(c(x)) = [0 3]x + [3] >= x = x
     
               [0 2]    [0]         
     a(u(x)) = [0 0]x + [1] >= x = x
     
               [0  3 ]    [2]         
     b(v(x)) = [-4 1 ]x + [0] >= x = x
     
               [3 3]    [0 ]         
     c(w(x)) = [3 3]x + [-2] >= x = x
    problem:
     DPs:
      a#(b(x)) -> a#(x)
      a#(b(x)) -> 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
    EDG Processor:
     DPs:
      a#(b(x)) -> a#(x)
      a#(b(x)) -> 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
     graph:
      c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> c#(x)
      c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> c#(c(x))
      c#(a(x)) -> c#(c(x)) -> c#(a(x)) -> a#(c(c(x)))
      c#(a(x)) -> c#(x) -> c#(a(x)) -> c#(x)
      c#(a(x)) -> c#(x) -> c#(a(x)) -> c#(c(x))
      c#(a(x)) -> c#(x) -> c#(a(x)) -> a#(c(c(x)))
      c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> a#(x)
      c#(a(x)) -> a#(c(c(x))) -> a#(b(x)) -> a#(a(x))
      b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> c#(x)
      b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> c#(c(x))
      b#(c(x)) -> c#(b(b(x))) -> c#(a(x)) -> a#(c(c(x)))
      b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> b#(x)
      b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> b#(b(x))
      b#(c(x)) -> b#(b(x)) -> b#(c(x)) -> c#(b(b(x)))
      b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(x)
      b#(c(x)) -> b#(x) -> b#(c(x)) -> b#(b(x))
      b#(c(x)) -> b#(x) -> b#(c(x)) -> c#(b(b(x)))
      a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> a#(x)
      a#(b(x)) -> a#(a(x)) -> a#(b(x)) -> a#(a(x))
      a#(b(x)) -> a#(x) -> a#(b(x)) -> a#(x)
      a#(b(x)) -> a#(x) -> a#(b(x)) -> a#(a(x))
     SCC Processor:
      #sccs: 3
      #rules: 6
      #arcs: 21/64
      DPs:
       b#(c(x)) -> b#(b(x))
       b#(c(x)) -> b#(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
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b#](x0) = 2x0 + 1,
        
        [w](x0) = 4x0 + 2,
        
        [v](x0) = 2x0 + 7,
        
        [u](x0) = 4x0 + 1,
        
        [c](x0) = x0 + 1/2,
        
        [a](x0) = 1/2x0,
        
        [b](x0) = x0
       orientation:
        b#(c(x)) = 2x + 2 >= 2x + 1 = b#(b(x))
        
        b#(c(x)) = 2x + 2 >= 2x + 1 = b#(x)
        
        a(b(x)) = 1/2x >= 1/4x = b(a(a(x)))
        
        b(c(x)) = x + 1/2 >= x + 1/2 = c(b(b(x)))
        
        c(a(x)) = 1/2x + 1/2 >= 1/2x + 1/2 = a(c(c(x)))
        
        u(a(x)) = 2x + 1 >= x = x
        
        v(b(x)) = 2x + 7 >= x = x
        
        w(c(x)) = 4x + 4 >= x = x
        
        a(u(x)) = 2x + 1/2 >= x = x
        
        b(v(x)) = 2x + 7 >= x = x
        
        c(w(x)) = 4x + 5/2 >= x = x
       problem:
        DPs:
         
        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
       Qed
      
      DPs:
       c#(a(x)) -> c#(c(x))
       c#(a(x)) -> 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
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [c#](x0) = 1/2x0 + 6,
        
        [w](x0) = 4x0 + 2,
        
        [v](x0) = 2x0 + 5,
        
        [u](x0) = 2x0,
        
        [c](x0) = x0,
        
        [a](x0) = x0 + 1/2,
        
        [b](x0) = 1/2x0
       orientation:
        c#(a(x)) = 1/2x + 25/4 >= 1/2x + 6 = c#(c(x))
        
        c#(a(x)) = 1/2x + 25/4 >= 1/2x + 6 = c#(x)
        
        a(b(x)) = 1/2x + 1/2 >= 1/2x + 1/2 = b(a(a(x)))
        
        b(c(x)) = 1/2x >= 1/4x = c(b(b(x)))
        
        c(a(x)) = x + 1/2 >= x + 1/2 = a(c(c(x)))
        
        u(a(x)) = 2x + 1 >= x = x
        
        v(b(x)) = x + 5 >= x = x
        
        w(c(x)) = 4x + 2 >= x = x
        
        a(u(x)) = 2x + 1/2 >= x = x
        
        b(v(x)) = x + 5/2 >= x = x
        
        c(w(x)) = 4x + 2 >= x = x
       problem:
        DPs:
         
        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
       Qed
      
      DPs:
       a#(b(x)) -> a#(a(x))
       a#(b(x)) -> a#(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
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [a#](x0) = 4x0,
        
        [w](x0) = 3x0 + 1,
        
        [v](x0) = 4x0 + 5/2,
        
        [u](x0) = 4x0 + 15/2,
        
        [c](x0) = 1/2x0,
        
        [a](x0) = x0,
        
        [b](x0) = x0 + 1/2
       orientation:
        a#(b(x)) = 4x + 2 >= 4x = a#(a(x))
        
        a#(b(x)) = 4x + 2 >= 4x = a#(x)
        
        a(b(x)) = x + 1/2 >= x + 1/2 = b(a(a(x)))
        
        b(c(x)) = 1/2x + 1/2 >= 1/2x + 1/2 = c(b(b(x)))
        
        c(a(x)) = 1/2x >= 1/4x = a(c(c(x)))
        
        u(a(x)) = 4x + 15/2 >= x = x
        
        v(b(x)) = 4x + 9/2 >= x = x
        
        w(c(x)) = 3/2x + 1 >= x = x
        
        a(u(x)) = 4x + 15/2 >= x = x
        
        b(v(x)) = 4x + 3 >= x = x
        
        c(w(x)) = 3/2x + 1/2 >= x = x
       problem:
        DPs:
         
        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
       Qed