YES

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

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