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