YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   c(b(a(X))) -> a(a(b(b(c(c(X))))))
   a(X) -> e()
   b(X) -> e()
   c(X) -> e()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [e] = 0,
    
    [c](x0) = x0 + 2,
    
    [b](x0) = x0,
    
    [a](x0) = x0 + 2
   orientation:
    c(b(a(X))) = X + 4 >= X + 8 = a(a(b(b(c(c(X))))))
    
    a(X) = X + 2 >= 0 = e()
    
    b(X) = X >= 0 = e()
    
    c(X) = X + 2 >= 0 = e()
   problem:
    strict:
     c(b(a(X))) -> a(a(b(b(c(c(X))))))
     b(X) -> e()
    weak:
     a(X) -> e()
     c(X) -> e()
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [e] = 0,
     
     [c](x0) = x0,
     
     [b](x0) = x0 + 1,
     
     [a](x0) = x0
    orientation:
     c(b(a(X))) = X + 1 >= X + 2 = a(a(b(b(c(c(X))))))
     
     b(X) = X + 1 >= 0 = e()
     
     a(X) = X >= 0 = e()
     
     c(X) = X >= 0 = e()
    problem:
     strict:
      c(b(a(X))) -> a(a(b(b(c(c(X))))))
     weak:
      b(X) -> e()
      a(X) -> e()
      c(X) -> e()
    Bounds Processor:
     bound: 1
     enrichment: match-rt
     automaton:
      final states: {5}
      transitions:
       a1(17) -> 18*
       a1(18) -> 19*
       b1(15) -> 16*
       b1(16) -> 17*
       c1(20) -> 21*
       c1(14) -> 15*
       c1(13) -> 14*
       e1() -> 26*
       c0(5) -> 5*
       b0(5) -> 5*
       a0(5) -> 5*
       e0() -> 5*
       5 -> 13*
       18 -> 20*
       19 -> 14,5
       21 -> 14*
       26 -> 21,15,18,19,5,13,14,20,16,17
     problem:
      strict:
       
      weak:
       c(b(a(X))) -> a(a(b(b(c(c(X))))))
       b(X) -> e()
       a(X) -> e()
       c(X) -> e()
     Qed