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