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
   
   usable rules:
    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)
   interpretation:
    [b#](x0, x1) = [0 2]x0 + [0 2]x1 + [1],
    
    [f#](x0) = [2 0]x0,
    
                      [0 1]     [0 0]     [0 0]     [1]
    [c](x0, x1, x2) = [2 0]x0 + [3 0]x1 + [0 1]x2 + [0],
    
              [1 1]  
    [f](x0) = [1 0]x0,
    
                  [0 2]     [2 1]     [0]
    [b](x0, x1) = [0 2]x0 + [2 0]x1 + [1],
    
          [0]
    [a] = [1]
   orientation:
    b#(y,b(a(),z)) = [0 2]y + [4 0]z + [7] >= [2 0]z = f#(z)
    
    b#(y,b(a(),z)) = [0 2]y + [4 0]z + [7] >= [2 0]z + [3] = b#(f(z),a())
    
    b#(y,b(a(),z)) = [0 2]y + [4 0]z + [7] >= [0 2]y + [2] = f#(c(y,y,a()))
    
    b#(y,b(a(),z)) = [0 2]y + [4 0]z + [7] >= [0 2]y + [4 0]z + [5] = b#(f(c(y,y,a())),b(f(z),a()))
    
    f#(f(f(c(z,x,a())))) = [6 0]x + [4 4]z + [6] >= [2 0]x = f#(x)
    
    f#(f(f(c(z,x,a())))) = [6 0]x + [4 4]z + [6] >= [2 0]x + [0 2]z + [1] = b#(f(x),z)
    
                  [4 1]    [5]         
    f(b(a(),z)) = [2 1]z + [2] >= z = z
    
                    [0 2]    [6 2]    [7]    [0 2]    [6 0]    [5]                               
    b(y,b(a(),z)) = [0 2]y + [4 2]z + [5] >= [0 2]y + [4 0]z + [5] = b(f(c(y,y,a())),b(f(z),a()))
    
                          [6 0]    [4 3]    [5]    [2 0]    [2 1]    [0]            
    f(f(f(c(z,x,a())))) = [3 0]x + [2 2]z + [3] >= [2 0]x + [2 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