YES(?,O(n^1))

Problem:
 c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
 c(c(b(c(y),0()))) -> a(0(),c(c(a(y,0()))))
 c(c(a(a(y,0()),x))) -> c(y)

Proof:
 RT Transformation Processor:
  strict:
   c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
   c(c(b(c(y),0()))) -> a(0(),c(c(a(y,0()))))
   c(c(a(a(y,0()),x))) -> c(y)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0] = 17,
    
    [b](x0, x1) = x0 + x1 + 15,
    
    [c](x0) = x0,
    
    [a](x0, x1) = x0 + x1 + 9
   orientation:
    c(c(c(a(x,y)))) = x + y + 9 >= x + y + 15 = b(c(c(c(c(y)))),x)
    
    c(c(b(c(y),0()))) = y + 32 >= y + 52 = a(0(),c(c(a(y,0()))))
    
    c(c(a(a(y,0()),x))) = x + y + 35 >= y = c(y)
   problem:
    strict:
     c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
     c(c(b(c(y),0()))) -> a(0(),c(c(a(y,0()))))
    weak:
     c(c(a(a(y,0()),x))) -> c(y)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [0] = 26,
     
     [b](x0, x1) = x0 + x1,
     
     [c](x0) = x0 + 2,
     
     [a](x0, x1) = x0 + x1 + 3
    orientation:
     c(c(c(a(x,y)))) = x + y + 9 >= x + y + 8 = b(c(c(c(c(y)))),x)
     
     c(c(b(c(y),0()))) = y + 32 >= y + 62 = a(0(),c(c(a(y,0()))))
     
     c(c(a(a(y,0()),x))) = x + y + 36 >= y + 2 = c(y)
    problem:
     strict:
      c(c(b(c(y),0()))) -> a(0(),c(c(a(y,0()))))
     weak:
      c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
      c(c(a(a(y,0()),x))) -> c(y)
    Bounds Processor:
     bound: 3
     enrichment: match-rt
     automaton:
      final states: {5}
      transitions:
       b3(73,5) -> 78,63
       b3(73,16) -> 78,63
       b3(81,29) -> 81,66,40
       a1(10,88) -> 80,65
       a1(10,13) -> 78,32,63,39,17,40,38,16,21,20,15,37,13,14,18,19,5
       a1(61,10) -> 49*
       a1(16,10) -> 11*
       a1(10,51) -> 79,64,66,65,81,80,40,39,20,16,21,17,38,15
       a1(20,10) -> 26*
       a1(15,10) -> 49*
       a1(5,10) -> 11*
       a1(10,28) -> 81,66,80,65,79,64,78,32,63,40,39,17,38,16,21,20,15,37,13,14,18,5,19
       a1(72,10) -> 86*
       c3(80) -> 81*
       c3(70) -> 71*
       c3(72) -> 73*
       c3(32) -> 78*
       c3(79) -> 80*
       c3(29) -> 70*
       c3(71) -> 72*
       c3(78) -> 79*
       01() -> 10*
       c1(50) -> 51*
       c1(20) -> 21*
       c1(15) -> 16*
       c1(5) -> 81,66,80,65,79,64,78,63,40,32,39,17,38,16,21,37,15,20,19,14,13,18
       c1(87) -> 88*
       c1(27) -> 28*
       c1(12) -> 13*
       c1(49) -> 50*
       c1(19) -> 20*
       c1(14) -> 15*
       c1(86) -> 87*
       c1(26) -> 27*
       c1(16) -> 17*
       c1(11) -> 12*
       c1(28) -> 14*
       c1(18) -> 19*
       c1(13) -> 14*
       b1(21,5) -> 5*
       b1(16,5) -> 81,66,80,65,32,64,63,79,78,40,39,17,38,37,16,21,18,20,14,19,15,13
       b1(17,10) -> 32,63,78,37,18,14,19,13,5
       a2(29,32) -> 79,64,66,65,81,80,78,63,40,17,39,20,16,21,38,15,37,14,19
       a2(5,29) -> 30*
       a2(29,54) -> 66,81,40,17
       a2(39,29) -> 52*
       a2(16,29) -> 30*
       c0(5) -> 5*
       02() -> 29*
       b0(5,5) -> 5*
       c2(65) -> 66*
       c2(60) -> 61*
       c2(30) -> 31*
       c2(10) -> 59*
       c2(52) -> 53*
       c2(37) -> 38*
       c2(32) -> 63*
       c2(64) -> 65*
       c2(59) -> 60*
       c2(39) -> 40*
       c2(61) -> 62*
       c2(31) -> 32*
       c2(63) -> 64*
       c2(53) -> 54*
       c2(38) -> 39*
       c2(28) -> 37*
       c2(13) -> 37*
       00() -> 5*
       b2(62,5) -> 37,14
       b2(40,10) -> 81,80,66,65,64,79,38,40,39,21,20,17,15,16
       b2(66,29) -> 17*
       b2(62,16) -> 37,14
       b2(62,20) -> 37,14
       a0(5,5) -> 5*
     problem:
      strict:
       
      weak:
       c(c(b(c(y),0()))) -> a(0(),c(c(a(y,0()))))
       c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
       c(c(a(a(y,0()),x))) -> c(y)
     Qed