YES

Problem:
 c(b(a(X))) -> a(a(b(b(c(c(X))))))
 a(X) -> e()
 b(X) -> e()
 c(X) -> e()

Proof:
 DP Processor:
  DPs:
   c#(b(a(X))) -> c#(X)
   c#(b(a(X))) -> c#(c(X))
   c#(b(a(X))) -> b#(c(c(X)))
   c#(b(a(X))) -> b#(b(c(c(X))))
   c#(b(a(X))) -> a#(b(b(c(c(X)))))
   c#(b(a(X))) -> a#(a(b(b(c(c(X))))))
  TRS:
   c(b(a(X))) -> a(a(b(b(c(c(X))))))
   a(X) -> e()
   b(X) -> e()
   c(X) -> e()
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    c(b(a(X))) -> a(a(b(b(c(c(X))))))
    a(X) -> e()
    b(X) -> e()
    c(X) -> e()
   interpretation:
    [a#](x0) = 0,
    
    [b#](x0) = -4x0 + 0,
    
    [c#](x0) = -1x0 + 4,
    
    [e] = 0,
    
    [c](x0) = -2x0 + 1,
    
    [b](x0) = 3x0 + 1,
    
    [a](x0) = -2x0 + 4
   orientation:
    c#(b(a(X))) = X + 6 >= -1X + 4 = c#(X)
    
    c#(b(a(X))) = X + 6 >= -3X + 4 = c#(c(X))
    
    c#(b(a(X))) = X + 6 >= -8X + 0 = b#(c(c(X)))
    
    c#(b(a(X))) = X + 6 >= -5X + 0 = b#(b(c(c(X))))
    
    c#(b(a(X))) = X + 6 >= 0 = a#(b(b(c(c(X)))))
    
    c#(b(a(X))) = X + 6 >= 0 = a#(a(b(b(c(c(X))))))
    
    c(b(a(X))) = -1X + 5 >= -2X + 4 = a(a(b(b(c(c(X))))))
    
    a(X) = -2X + 4 >= 0 = e()
    
    b(X) = 3X + 1 >= 0 = e()
    
    c(X) = -2X + 1 >= 0 = e()
   problem:
    DPs:
     
    TRS:
     c(b(a(X))) -> a(a(b(b(c(c(X))))))
     a(X) -> e()
     b(X) -> e()
     c(X) -> e()
   Qed