YES

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

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