YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   b(b(0(),y),x) -> y
   c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
   a(y,0()) -> b(y,0())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [a](x0, x1) = x0 + x1 + 5,
    
    [c](x0) = x0 + 8,
    
    [b](x0, x1) = x0 + x1,
    
    [0] = 0
   orientation:
    b(b(0(),y),x) = x + y >= y = y
    
    c(c(c(y))) = y + 24 >= y + 34 = c(c(a(a(c(b(0(),y)),0()),0())))
    
    a(y,0()) = y + 5 >= y = b(y,0())
   problem:
    strict:
     b(b(0(),y),x) -> y
     c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
    weak:
     a(y,0()) -> b(y,0())
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5}
     transitions:
      c1(10) -> 11*
      c1(7) -> 8*
      c1(11) -> 5*
      a1(9,6) -> 10*
      a1(8,6) -> 9*
      b1(9,6) -> 10*
      b1(6,10) -> 7*
      b1(8,6) -> 9*
      b1(6,5) -> 7*
      b1(6,11) -> 7*
      01() -> 6*
      b0(5,5) -> 5*
      00() -> 5*
      c0(5) -> 5*
      a0(5,5) -> 5*
    problem:
     strict:
      c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
     weak:
      b(b(0(),y),x) -> y
      a(y,0()) -> b(y,0())
    Bounds Processor:
     bound: 1
     enrichment: match-rt
     automaton:
      final states: {5}
      transitions:
       c1(17) -> 5*
       c1(16) -> 17*
       c1(13) -> 14*
       a1(14,12) -> 15*
       a1(15,12) -> 16*
       b1(12,16) -> 13*
       b1(14,12) -> 15*
       b1(12,5) -> 13*
       b1(12,17) -> 13*
       b1(15,12) -> 16*
       01() -> 12*
       b0(5,5) -> 5*
       00() -> 5*
       c0(5) -> 5*
       a0(5,5) -> 5*
     problem:
      strict:
       
      weak:
       c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
       b(b(0(),y),x) -> y
       a(y,0()) -> b(y,0())
     Qed