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)
  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:
     dimension: 1
     interpretation:
      [b#](x0, x1) = x1 + 1,
      
      [f#](x0) = x0 + 1,
      
      [c](x0, x1, x2) = x0 + x1 + 1,
      
      [f](x0) = x0,
      
      [b](x0, x1) = x1,
      
      [a] = 0
     orientation:
      b#(y,b(a(),z)) = z + 1 >= 1 = b#(f(c(y,y,a())),b(f(z),a()))
      
      b#(y,b(a(),z)) = z + 1 >= z + 1 = f#(z)
      
      f#(f(f(c(z,x,a())))) = x + z + 2 >= z + 1 = b#(f(x),z)
      
      f#(f(f(c(z,x,a())))) = x + z + 2 >= x + 1 = f#(x)
      
      f(b(a(),z)) = z >= z = z
      
      b(y,b(a(),z)) = z >= 0 = b(f(c(y,y,a())),b(f(z),a()))
      
      f(f(f(c(z,x,a())))) = x + z + 1 >= z = 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)
      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:
      dimension: 1
      interpretation:
       [b#](x0, x1) = 1,
       
       [f#](x0) = 0,
       
       [c](x0, x1, x2) = x0,
       
       [f](x0) = x0,
       
       [b](x0, x1) = x1,
       
       [a] = 0
      orientation:
       b#(y,b(a(),z)) = 1 >= 1 = b#(f(c(y,y,a())),b(f(z),a()))
       
       b#(y,b(a(),z)) = 1 >= 0 = f#(z)
       
       f(b(a(),z)) = z >= z = z
       
       b(y,b(a(),z)) = z >= 0 = b(f(c(y,y,a())),b(f(z),a()))
       
       f(f(f(c(z,x,a())))) = z >= z = b(f(x),z)
      problem:
       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)
      Bounds Processor:
       bound: 1
       enrichment: top-dp
       automaton:
        final states: {6}
        transitions:
         c0(14,16,15) -> 14*
         c0(18,12,14) -> 14*
         c0(14,18,15) -> 14*
         c0(18,14,14) -> 14*
         c0(18,16,14) -> 14*
         c0(15,11,18) -> 14*
         c0(18,18,14) -> 14*
         c0(14,12,12) -> 16*
         c0(14,14,12) -> 16*
         c0(15,15,18) -> 14*
         c0(16,11,16) -> 14*
         c0(14,11,17) -> 14*
         c0(14,16,12) -> 16*
         c0(18,12,11) -> 14*
         c0(15,17,18) -> 14*
         c0(11,11,16) -> 14*
         c0(14,18,12) -> 16*
         c0(18,14,11) -> 14*
         c0(16,15,16) -> 14*
         c0(14,15,17) -> 14*
         c0(18,16,11) -> 14*
         c0(11,15,16) -> 14*
         c0(15,11,15) -> 14*
         c0(16,17,16) -> 14*
         c0(14,17,17) -> 14*
         c0(18,18,11) -> 14*
         c0(11,17,16) -> 14*
         c0(15,15,15) -> 14*
         c0(14,11,14) -> 14*
         c0(15,17,15) -> 14*
         c0(14,15,14) -> 14*
         c0(15,11,12) -> 16*
         c0(16,12,18) -> 14*
         c0(14,17,14) -> 14*
         c0(11,12,18) -> 14*
         c0(16,14,18) -> 14*
         c0(11,14,18) -> 14*
         c0(15,15,12) -> 16*
         c0(16,16,18) -> 14*
         c0(14,11,11) -> 14*
         c0(11,16,18) -> 14*
         c0(17,12,16) -> 14*
         c0(15,12,17) -> 14*
         c0(15,17,12) -> 16*
         c0(16,18,18) -> 14*
         c0(12,12,16) -> 14*
         c0(17,14,16) -> 14*
         c0(11,18,18) -> 14*
         c0(15,14,17) -> 14*
         c0(12,14,16) -> 14*
         c0(14,15,11) -> 14*
         c0(17,16,16) -> 14*
         c0(15,16,17) -> 14*
         c0(12,16,16) -> 14*
         c0(16,12,15) -> 14*
         c0(14,17,11) -> 14*
         c0(17,18,16) -> 14*
         c0(15,18,17) -> 14*
         c0(11,12,15) -> 14*
         c0(12,18,16) -> 14*
         c0(16,14,15) -> 14*
         c0(11,14,15) -> 14*
         c0(16,16,15) -> 14*
         c0(11,16,15) -> 14*
         c0(15,12,14) -> 14*
         c0(16,18,15) -> 14*
         c0(11,18,15) -> 14*
         c0(15,14,14) -> 14*
         c0(17,11,18) -> 14*
         c0(15,16,14) -> 14*
         c0(12,11,18) -> 14*
         c0(16,12,12) -> 16*
         c0(15,18,14) -> 14*
         c0(11,12,12) -> 16*
         c0(16,14,12) -> 16*
         c0(17,15,18) -> 14*
         c0(11,14,12) -> 16*
         c0(12,15,18) -> 14*
         c0(18,11,16) -> 14*
         c0(16,11,17) -> 14*
         c0(16,16,12) -> 16*
         c0(17,17,18) -> 14*
         c0(11,11,17) -> 14*
         c0(11,16,12) -> 16*
         c0(15,12,11) -> 14*
         c0(12,17,18) -> 14*
         c0(16,18,12) -> 16*
         c0(11,18,12) -> 16*
         c0(15,14,11) -> 14*
         c0(18,15,16) -> 14*
         c0(16,15,17) -> 14*
         c0(11,15,17) -> 14*
         c0(17,11,15) -> 14*
         c0(15,16,11) -> 14*
         c0(18,17,16) -> 14*
         c0(16,17,17) -> 14*
         c0(12,11,15) -> 14*
         c0(11,17,17) -> 14*
         c0(15,18,11) -> 14*
         c0(17,15,15) -> 14*
         c0(12,15,15) -> 14*
         c0(16,11,14) -> 14*
         c0(17,17,15) -> 14*
         c0(11,11,14) -> 14*
         c0(12,17,15) -> 14*
         c0(16,15,14) -> 14*
         c0(17,11,12) -> 16*
         c0(11,15,14) -> 14*
         c0(18,12,18) -> 14*
         c0(16,17,14) -> 14*
         c0(12,11,12) -> 16*
         c0(11,17,14) -> 14*
         c0(18,14,18) -> 14*
         c0(17,15,12) -> 16*
         c0(18,16,18) -> 14*
         c0(12,15,12) -> 16*
         c0(16,11,11) -> 14*
         c0(17,12,17) -> 14*
         c0(17,17,12) -> 16*
         c0(11,11,11) -> 14*
         c0(18,18,18) -> 14*
         c0(14,12,16) -> 14*
         c0(12,12,17) -> 14*
         c0(12,17,12) -> 16*
         c0(17,14,17) -> 14*
         c0(14,14,16) -> 14*
         c0(12,14,17) -> 14*
         c0(16,15,11) -> 14*
         c0(17,16,17) -> 14*
         c0(11,15,11) -> 14*
         c0(14,16,16) -> 14*
         c0(12,16,17) -> 14*
         c0(18,12,15) -> 14*
         c0(16,17,11) -> 14*
         c0(17,18,17) -> 14*
         c0(11,17,11) -> 14*
         c0(14,18,16) -> 14*
         c0(18,14,15) -> 14*
         c0(12,18,17) -> 14*
         c0(18,16,15) -> 14*
         c0(17,12,14) -> 14*
         c0(18,18,15) -> 14*
         c0(12,12,14) -> 14*
         c0(17,14,14) -> 14*
         c0(12,14,14) -> 14*
         c0(17,16,14) -> 14*
         c0(14,11,18) -> 14*
         c0(18,12,12) -> 16*
         c0(12,16,14) -> 14*
         c0(17,18,14) -> 14*
         c0(18,14,12) -> 16*
         c0(12,18,14) -> 14*
         c0(14,15,18) -> 14*
         c0(18,11,17) -> 14*
         c0(18,16,12) -> 16*
         c0(15,11,16) -> 14*
         c0(17,12,11) -> 14*
         c0(14,17,18) -> 14*
         c0(18,18,12) -> 16*
         c0(12,12,11) -> 14*
         c0(17,14,11) -> 14*
         c0(18,15,17) -> 14*
         c0(12,14,11) -> 14*
         c0(15,15,16) -> 14*
         c0(17,16,11) -> 14*
         c0(18,17,17) -> 14*
         c0(14,11,15) -> 14*
         c0(12,16,11) -> 14*
         c0(15,17,16) -> 14*
         c0(17,18,11) -> 14*
         c0(12,18,11) -> 14*
         c0(14,15,15) -> 14*
         c0(18,11,14) -> 14*
         c0(14,17,15) -> 14*
         c0(18,15,14) -> 14*
         c0(18,17,14) -> 14*
         c0(14,11,12) -> 16*
         c0(15,12,18) -> 14*
         c0(15,14,18) -> 14*
         c0(14,15,12) -> 16*
         c0(18,11,11) -> 14*
         c0(15,16,18) -> 14*
         c0(16,12,16) -> 14*
         c0(14,12,17) -> 14*
         c0(14,17,12) -> 16*
         c0(15,18,18) -> 14*
         c0(11,12,16) -> 14*
         c0(16,14,16) -> 14*
         c0(14,14,17) -> 14*
         c0(18,15,11) -> 14*
         c0(11,14,16) -> 14*
         c0(16,16,16) -> 14*
         c0(14,16,17) -> 14*
         c0(18,17,11) -> 14*
         c0(11,16,16) -> 14*
         c0(15,12,15) -> 14*
         c0(16,18,16) -> 14*
         c0(14,18,17) -> 14*
         c0(11,18,16) -> 14*
         c0(15,14,15) -> 14*
         c0(15,16,15) -> 14*
         c0(14,12,14) -> 14*
         c0(15,18,15) -> 14*
         c0(14,14,14) -> 14*
         c0(16,11,18) -> 14*
         c0(14,16,14) -> 14*
         c0(11,11,18) -> 14*
         c0(15,12,12) -> 16*
         c0(14,18,14) -> 14*
         c0(15,14,12) -> 16*
         c0(16,15,18) -> 14*
         c0(17,11,16) -> 14*
         c0(11,15,18) -> 14*
         c0(15,11,17) -> 14*
         c0(15,16,12) -> 16*
         c0(16,17,18) -> 14*
         c0(12,11,16) -> 14*
         c0(14,12,11) -> 14*
         c0(11,17,18) -> 14*
         c0(15,18,12) -> 16*
         c0(14,14,11) -> 14*
         c0(17,15,16) -> 14*
         c0(15,15,17) -> 14*
         c0(12,15,16) -> 14*
         c0(16,11,15) -> 14*
         c0(14,16,11) -> 14*
         c0(17,17,16) -> 14*
         c0(15,17,17) -> 14*
         c0(11,11,15) -> 14*
         c0(12,17,16) -> 14*
         c0(14,18,11) -> 14*
         c0(16,15,15) -> 14*
         c0(11,15,15) -> 14*
         c0(15,11,14) -> 14*
         c0(16,17,15) -> 14*
         c0(11,17,15) -> 14*
         c0(15,15,14) -> 14*
         c0(16,11,12) -> 16*
         c0(17,12,18) -> 14*
         c0(15,17,14) -> 14*
         c0(11,11,12) -> 16*
         c0(12,12,18) -> 14*
         c0(17,14,18) -> 14*
         c0(12,14,18) -> 14*
         c0(16,15,12) -> 16*
         c0(17,16,18) -> 14*
         c0(11,15,12) -> 16*
         c0(15,11,11) -> 14*
         c0(12,16,18) -> 14*
         c0(18,12,16) -> 14*
         c0(16,12,17) -> 14*
         c0(16,17,12) -> 16*
         c0(17,18,18) -> 14*
         c0(11,12,17) -> 14*
         c0(11,17,12) -> 16*
         c0(12,18,18) -> 14*
         c0(18,14,16) -> 14*
         c0(16,14,17) -> 14*
         c0(11,14,17) -> 14*
         c0(15,15,11) -> 14*
         c0(18,16,16) -> 14*
         c0(16,16,17) -> 14*
         c0(17,12,15) -> 14*
         c0(11,16,17) -> 14*
         c0(15,17,11) -> 14*
         c0(18,18,16) -> 14*
         c0(16,18,17) -> 14*
         c0(12,12,15) -> 14*
         c0(17,14,15) -> 14*
         c0(11,18,17) -> 14*
         c0(12,14,15) -> 14*
         c0(17,16,15) -> 14*
         c0(12,16,15) -> 14*
         c0(16,12,14) -> 14*
         c0(17,18,15) -> 14*
         c0(11,12,14) -> 14*
         c0(12,18,15) -> 14*
         c0(16,14,14) -> 14*
         c0(11,14,14) -> 14*
         c0(18,11,18) -> 14*
         c0(16,16,14) -> 14*
         c0(17,12,12) -> 16*
         c0(11,16,14) -> 14*
         c0(16,18,14) -> 14*
         c0(12,12,12) -> 16*
         c0(17,14,12) -> 16*
         c0(11,18,14) -> 14*
         c0(18,15,18) -> 14*
         c0(12,14,12) -> 16*
         c0(17,11,17) -> 14*
         c0(17,16,12) -> 16*
         c0(18,17,18) -> 14*
         c0(14,11,16) -> 14*
         c0(12,11,17) -> 14*
         c0(12,16,12) -> 16*
         c0(16,12,11) -> 14*
         c0(17,18,12) -> 16*
         c0(11,12,11) -> 14*
         c0(12,18,12) -> 16*
         c0(16,14,11) -> 14*
         c0(17,15,17) -> 14*
         c0(11,14,11) -> 14*
         c0(14,15,16) -> 14*
         c0(18,11,15) -> 14*
         c0(12,15,17) -> 14*
         c0(16,16,11) -> 14*
         c0(17,17,17) -> 14*
         c0(11,16,11) -> 14*
         c0(14,17,16) -> 14*
         c0(12,17,17) -> 14*
         c0(16,18,11) -> 14*
         c0(11,18,11) -> 14*
         c0(18,15,15) -> 14*
         c0(17,11,14) -> 14*
         c0(18,17,15) -> 14*
         c0(12,11,14) -> 14*
         c0(17,15,14) -> 14*
         c0(18,11,12) -> 16*
         c0(12,15,14) -> 14*
         c0(17,17,14) -> 14*
         c0(14,12,18) -> 14*
         c0(12,17,14) -> 14*
         c0(14,14,18) -> 14*
         c0(18,15,12) -> 16*
         c0(17,11,11) -> 14*
         c0(14,16,18) -> 14*
         c0(18,12,17) -> 14*
         c0(18,17,12) -> 16*
         c0(12,11,11) -> 14*
         c0(15,12,16) -> 14*
         c0(14,18,18) -> 14*
         c0(18,14,17) -> 14*
         c0(15,14,16) -> 14*
         c0(17,15,11) -> 14*
         c0(18,16,17) -> 14*
         c0(12,15,11) -> 14*
         c0(15,16,16) -> 14*
         c0(17,17,11) -> 14*
         c0(18,18,17) -> 14*
         c0(14,12,15) -> 14*
         c0(12,17,11) -> 14*
         c0(15,18,16) -> 14*
         c0(14,14,15) -> 14*
         b{#,1}(23,21) -> 6*
         f1(22) -> 23*
         f1(12) -> 20*
         c1(18,18,19) -> 22*
         a1() -> 19*
         b1(20,19) -> 21*
         b{#,0}(18,17) -> 6*
         b0(12,14) -> 11*
         b0(17,16) -> 11*
         b0(12,16) -> 11*
         b0(17,18) -> 11*
         b0(12,18) -> 11*
         b0(18,11) -> 11*
         b0(18,15) -> 11*
         b0(18,17) -> 11*
         b0(14,12) -> 11*
         b0(14,14) -> 11*
         b0(14,16) -> 11*
         b0(14,18) -> 11*
         b0(15,11) -> 11*
         b0(15,15) -> 11*
         b0(15,17) -> 11*
         b0(16,12) -> 11*
         b0(11,12) -> 11*
         b0(16,14) -> 11*
         b0(11,14) -> 11*
         b0(16,16) -> 11*
         b0(11,16) -> 11*
         b0(16,18) -> 11*
         b0(11,18) -> 11*
         b0(17,11) -> 11*
         b0(12,11) -> 11*
         b0(17,15) -> 11*
         b0(12,15) -> 11*
         b0(17,17) -> 11*
         b0(12,17) -> 11*
         b0(18,12) -> 17*
         b0(18,14) -> 11*
         b0(18,16) -> 11*
         b0(18,18) -> 11*
         b0(14,11) -> 11*
         b0(14,15) -> 11*
         b0(14,17) -> 11*
         b0(15,12) -> 17*
         b0(15,14) -> 11*
         b0(15,16) -> 11*
         b0(15,18) -> 11*
         b0(16,11) -> 11*
         b0(11,11) -> 11*
         b0(16,15) -> 11*
         b0(11,15) -> 11*
         b0(16,17) -> 11*
         b0(11,17) -> 11*
         b0(17,12) -> 11*
         b0(12,12) -> 11*
         b0(17,14) -> 11*
         a0() -> 12*
         f0(15) -> 15*
         f0(17) -> 15*
         f0(12) -> 15*
         f0(14) -> 15*
         f0(16) -> 18*
         f0(11) -> 15*
         f0(18) -> 15*
         11 -> 15*
         12 -> 15*
         14 -> 15*
         16 -> 15*
         17 -> 15*
         18 -> 15*
       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