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
  TDG 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
   graph:
    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)))
    b#(x,b(z,y)) -> b#(f(f(z)),c(x,z,y)) ->
    b#(x,b(z,y)) -> b#(f(f(z)),c(x,z,y))
    b#(x,b(z,y)) -> b#(f(f(z)),c(x,z,y)) ->
    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#(z)
    b#(x,b(z,y)) -> f#(b(f(f(z)),c(x,z,y))) -> f#(c(a(),z,x)) -> b#(a(),z)
    b#(x,b(z,y)) -> f#(f(z)) -> f#(c(a(),z,x)) -> b#(a(),z)
    b#(x,b(z,y)) -> f#(z) -> f#(c(a(),z,x)) -> b#(a(),z)
    f#(c(a(),z,x)) -> b#(a(),z) ->
    b#(x,b(z,y)) -> f#(b(f(f(z)),c(x,z,y)))
    f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> b#(f(f(z)),c(x,z,y))
    f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> f#(f(z))
    f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> f#(z)
   EDG 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
    graph:
     b#(x,b(z,y)) -> f#(b(f(f(z)),c(x,z,y))) -> f#(c(a(),z,x)) -> b#(a(),z)
     b#(x,b(z,y)) -> f#(f(z)) -> f#(c(a(),z,x)) -> b#(a(),z)
     b#(x,b(z,y)) -> f#(z) -> f#(c(a(),z,x)) -> b#(a(),z)
     f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> f#(z)
     f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> f#(f(z))
     f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> b#(f(f(z)),c(x,z,y))
     f#(c(a(),z,x)) -> b#(a(),z) -> b#(x,b(z,y)) -> f#(b(f(f(z)),c(x,z,y)))
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 7/25
     DPs:
      b#(x,b(z,y)) -> f#(b(f(f(z)),c(x,z,y)))
      f#(c(a(),z,x)) -> b#(a(),z)
      b#(x,b(z,y)) -> f#(f(z))
      b#(x,b(z,y)) -> f#(z)
     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=1
      
      interpretation:
       [b#](x0, x1) = 5x1 + 4,
       
       [f#](x0) = 2x0 + 1,
       
       [b](x0, x1) = 6x0 + 2x1 + 2,
       
       [f](x0) = x0,
       
       [c](x0, x1, x2) = 3x1 + x2 + 2,
       
       [a] = 0
      orientation:
       b#(x,b(z,y)) = 10y + 30z + 14 >= 4y + 24z + 13 = f#(b(f(f(z)),c(x,z,y)))
       
       f#(c(a(),z,x)) = 2x + 6z + 5 >= 5z + 4 = b#(a(),z)
       
       b#(x,b(z,y)) = 10y + 30z + 14 >= 2z + 1 = f#(f(z))
       
       b#(x,b(z,y)) = 10y + 30z + 14 >= 2z + 1 = f#(z)
       
       f(c(a(),z,x)) = x + 3z + 2 >= 2z + 2 = b(a(),z)
       
       b(x,b(z,y)) = 6x + 4y + 12z + 6 >= 2y + 12z + 6 = f(b(f(f(z)),c(x,z,y)))
       
       b(y,z) = 6y + 2z + 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