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
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [b#](x0, x1) = x1 + 0,
       
       [f#](x0) = x0 + 0,
       
       [b](x0, x1) = 1x0 + x1 + 1,
       
       [f](x0) = x0 + 0,
       
       [c](x0, x1, x2) = x1 + 1,
       
       [a] = 0
      orientation:
       b#(x,b(z,y)) = y + 1z + 1 >= 1z + 1 = f#(b(f(f(z)),c(x,z,y)))
       
       f#(c(a(),z,x)) = z + 1 >= z + 0 = b#(a(),z)
       
       b#(x,b(z,y)) = y + 1z + 1 >= z + 0 = f#(f(z))
       
       b#(x,b(z,y)) = y + 1z + 1 >= z + 0 = f#(z)
       
       f(c(a(),z,x)) = z + 1 >= z + 1 = b(a(),z)
       
       b(x,b(z,y)) = 1x + y + 1z + 1 >= 1z + 1 = f(b(f(f(z)),c(x,z,y)))
       
       b(y,z) = 1y + z + 1 >= z = z
      problem:
       DPs:
        b#(x,b(z,y)) -> f#(b(f(f(z)),c(x,z,y)))
        f#(c(a(),z,x)) -> b#(a(),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
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [b#](x0, x1) = 2x0 + x1 + 0,
        
        [f#](x0) = x0 + 0,
        
        [b](x0, x1) = 3x0 + x1 + 7,
        
        [f](x0) = x0 + 4,
        
        [c](x0, x1, x2) = 2x0 + 3x1 + x2 + 7,
        
        [a] = 0
       orientation:
        b#(x,b(z,y)) = 2x + y + 3z + 7 >= 2x + y + 3z + 7 = f#(b(f(f(z)),c(x,z,y)))
        
        f#(c(a(),z,x)) = x + 3z + 7 >= z + 2 = b#(a(),z)
        
        f(c(a(),z,x)) = x + 3z + 7 >= z + 7 = b(a(),z)
        
        b(x,b(z,y)) = 3x + y + 3z + 7 >= 2x + y + 3z + 7 = f(b(f(f(z)),c(x,z,y)))
        
        b(y,z) = 3y + z + 7 >= z = z
       problem:
        DPs:
         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
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 6/1