YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   a(x,y) -> b(x,b(0(),c(y)))
   c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
   b(y,0()) -> y
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [b](x0, x1) = x0 + x1 + 5,
    
    [c](x0) = x0 + 9,
    
    [0] = 10,
    
    [a](x0, x1) = x0 + x1 + 9
   orientation:
    a(x,y) = x + y + 9 >= x + y + 29 = b(x,b(0(),c(y)))
    
    c(b(y,c(x))) = x + y + 23 >= y + 52 = c(c(b(a(0(),0()),y)))
    
    b(y,0()) = y + 15 >= y = y
   problem:
    strict:
     a(x,y) -> b(x,b(0(),c(y)))
     c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
    weak:
     b(y,0()) -> y
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [b](x0, x1) = x0 + x1 + 4,
     
     [c](x0) = x0,
     
     [0] = 4,
     
     [a](x0, x1) = x0 + x1 + 27
    orientation:
     a(x,y) = x + y + 27 >= x + y + 12 = b(x,b(0(),c(y)))
     
     c(b(y,c(x))) = x + y + 4 >= y + 39 = c(c(b(a(0(),0()),y)))
     
     b(y,0()) = y + 8 >= y = y
    problem:
     strict:
      c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
     weak:
      a(x,y) -> b(x,b(0(),c(y)))
      b(y,0()) -> y
    Bounds Processor:
     bound: 3
     enrichment: match-rt
     automaton:
      final states: {5}
      transitions:
       b3(14,32) -> 15*
       b3(31,30) -> 32*
       c1(5) -> 25*
       c1(12) -> 13*
       c1(18) -> 12*
       c1(13) -> 25,5
       03() -> 31*
       b1(10,25) -> 26*
       b1(11,5) -> 12*
       b1(5,26) -> 5*
       b1(11,11) -> 18*
       c3(14) -> 30*
       a1(10,10) -> 11*
       01() -> 10*
       c2(10) -> 19*
       c2(17) -> 13*
       c2(16) -> 17*
       c0(5) -> 5*
       b2(15,11) -> 16*
       b2(14,19) -> 20*
       b2(10,20) -> 11*
       b0(5,5) -> 5*
       a2(14,14) -> 15*
       a0(5,5) -> 5*
       02() -> 14*
       00() -> 5*
       11 -> 12*
     problem:
      strict:
       
      weak:
       c(b(y,c(x))) -> c(c(b(a(0(),0()),y)))
       a(x,y) -> b(x,b(0(),c(y)))
       b(y,0()) -> y
     Qed