YES

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

Proof:
 DP Processor:
  DPs:
   f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
   f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
   f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
   f#(b(b(x,f(y)),z)) -> f#(a())
   f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
   f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
  TRS:
   f(c(c(a(),y,a()),b(x,z),a())) -> b(y,f(c(f(a()),z,z)))
   f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
   c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
  Usable Rule Processor:
   DPs:
    f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
    f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
    f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
    f#(b(b(x,f(y)),z)) -> f#(a())
    f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
    f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
   TRS:
    f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
    c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
     c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
    interpretation:
     [c#](x0, x1, x2) = 0,
     
     [f#](x0) = x0,
     
     [f](x0) = 3x0 + 3,
     
     [b](x0, x1) = x0 + 1x1 + 0,
     
     [c](x0, x1, x2) = 2x1 + x2,
     
     [a] = 0
    orientation:
     f#(c(c(a(),y,a()),b(x,z),a())) = 2x + 3z + 2 >= 0 = f#(a())
     
     f#(c(c(a(),y,a()),b(x,z),a())) = 2x + 3z + 2 >= 0 = c#(f(a()),z,z)
     
     f#(c(c(a(),y,a()),b(x,z),a())) = 2x + 3z + 2 >= 2z = f#(c(f(a()),z,z))
     
     f#(b(b(x,f(y)),z)) = x + 4y + 1z + 4 >= 0 = f#(a())
     
     f#(b(b(x,f(y)),z)) = x + 4y + 1z + 4 >= 1y + 3 = f#(b(b(f(a()),y),y))
     
     f#(b(b(x,f(y)),z)) = x + 4y + 1z + 4 >= 0 = c#(z,x,f(b(b(f(a()),y),y)))
     
     f(b(b(x,f(y)),z)) = 3x + 7y + 4z + 7 >= 2x + 4y + 6 = c(z,x,f(b(b(f(a()),y),y)))
     
     c(b(a(),a()),b(y,z),x) = x + 2y + 3z + 2 >= 2z + 1 = b(a(),b(z,z))
    problem:
     DPs:
      
     TRS:
      f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
      c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
    Qed