YES

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

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