YES

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

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