YES

Problem:
 c(z,x,a()) -> f(b(b(f(z),z),x))
 b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
 f(c(c(z,a(),a()),x,a())) -> z

Proof:
 DP Processor:
  DPs:
   c#(z,x,a()) -> f#(z)
   c#(z,x,a()) -> b#(f(z),z)
   c#(z,x,a()) -> b#(b(f(z),z),x)
   c#(z,x,a()) -> f#(b(b(f(z),z),x))
   b#(y,b(z,a())) -> f#(a())
   b#(y,b(z,a())) -> c#(f(a()),y,z)
   b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
   b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
  TRS:
   c(z,x,a()) -> f(b(b(f(z),z),x))
   b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
   f(c(c(z,a(),a()),x,a())) -> z
  TDG Processor:
   DPs:
    c#(z,x,a()) -> f#(z)
    c#(z,x,a()) -> b#(f(z),z)
    c#(z,x,a()) -> b#(b(f(z),z),x)
    c#(z,x,a()) -> f#(b(b(f(z),z),x))
    b#(y,b(z,a())) -> f#(a())
    b#(y,b(z,a())) -> c#(f(a()),y,z)
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
   TRS:
    c(z,x,a()) -> f(b(b(f(z),z),x))
    b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
    f(c(c(z,a(),a()),x,a())) -> z
   graph:
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> c#(f(a()),y,z)
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> f#(a())
    b#(y,b(z,a())) -> c#(f(a()),y,z) ->
    c#(z,x,a()) -> f#(b(b(f(z),z),x))
    b#(y,b(z,a())) -> c#(f(a()),y,z) ->
    c#(z,x,a()) -> b#(b(f(z),z),x)
    b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> b#(f(z),z)
    b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> f#(z)
    c#(z,x,a()) -> b#(b(f(z),z),x) ->
    b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    c#(z,x,a()) -> b#(b(f(z),z),x) ->
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    c#(z,x,a()) -> b#(b(f(z),z),x) ->
    b#(y,b(z,a())) -> c#(f(a()),y,z)
    c#(z,x,a()) -> b#(b(f(z),z),x) -> b#(y,b(z,a())) -> f#(a())
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> c#(f(a()),y,z)
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> f#(a())
   SCC Processor:
    #sccs: 1
    #rules: 4
    #arcs: 16/64
    DPs:
     b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
     b#(y,b(z,a())) -> c#(f(a()),y,z)
     c#(z,x,a()) -> b#(f(z),z)
     c#(z,x,a()) -> b#(b(f(z),z),x)
    TRS:
     c(z,x,a()) -> f(b(b(f(z),z),x))
     b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
     f(c(c(z,a(),a()),x,a())) -> z
    Arctic Interpretation Processor:
     dimension: 1
     usable rules:
      c(z,x,a()) -> f(b(b(f(z),z),x))
      b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
      f(c(c(z,a(),a()),x,a())) -> z
     interpretation:
      [b#](x0, x1) = -2x0 + -2x1 + 0,
      
      [c#](x0, x1, x2) = 1x0 + -2x1 + -8x2 + 0,
      
      [b](x0, x1) = 1x0 + 1x1 + 2,
      
      [f](x0) = -2x0 + 0,
      
      [c](x0, x1, x2) = 1x0 + -1x1 + -2x2 + 0,
      
      [a] = 3
     orientation:
      b#(y,b(z,a())) = -2y + -1z + 2 >= -3y + -2z + 0 = b#(c(f(a()),y,z),z)
      
      b#(y,b(z,a())) = -2y + -1z + 2 >= -2y + -8z + 2 = c#(f(a()),y,z)
      
      c#(z,x,a()) = -2x + 1z + 0 >= -2z + 0 = b#(f(z),z)
      
      c#(z,x,a()) = -2x + 1z + 0 >= -2x + -1z + 0 = b#(b(f(z),z),x)
      
      c(z,x,a()) = -1x + 1z + 1 >= -1x + z + 1 = f(b(b(f(z),z),x))
      
      b(y,b(z,a())) = 1y + 2z + 5 >= -2y + -1z + 1 = f(b(c(f(a()),y,z),z))
      
      f(c(c(z,a(),a()),x,a())) = -3x + z + 1 >= z = z
     problem:
      DPs:
       b#(y,b(z,a())) -> c#(f(a()),y,z)
       c#(z,x,a()) -> b#(f(z),z)
       c#(z,x,a()) -> b#(b(f(z),z),x)
      TRS:
       c(z,x,a()) -> f(b(b(f(z),z),x))
       b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
       f(c(c(z,a(),a()),x,a())) -> z
     Restore Modifier:
      DPs:
       b#(y,b(z,a())) -> c#(f(a()),y,z)
       c#(z,x,a()) -> b#(f(z),z)
       c#(z,x,a()) -> b#(b(f(z),z),x)
      TRS:
       c(z,x,a()) -> f(b(b(f(z),z),x))
       b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
       f(c(c(z,a(),a()),x,a())) -> z
      Arctic Interpretation Processor:
       dimension: 1
       usable rules:
        c(z,x,a()) -> f(b(b(f(z),z),x))
        b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
        f(c(c(z,a(),a()),x,a())) -> z
       interpretation:
        [b#](x0, x1) = 1x0 + -1x1 + 0,
        
        [c#](x0, x1, x2) = x0 + 1x1 + x2 + 1,
        
        [b](x0, x1) = 1x0 + -1x1 + 2,
        
        [f](x0) = -4x0 + 0,
        
        [c](x0, x1, x2) = 2x0 + x1 + x2 + 3,
        
        [a] = 3
       orientation:
        b#(y,b(z,a())) = 1y + z + 1 >= 1y + z + 1 = c#(f(a()),y,z)
        
        c#(z,x,a()) = 1x + z + 3 >= -1z + 1 = b#(f(z),z)
        
        c#(z,x,a()) = 1x + z + 3 >= -1x + z + 3 = b#(b(f(z),z),x)
        
        c(z,x,a()) = x + 2z + 3 >= -5x + -4z + 0 = f(b(b(f(z),z),x))
        
        b(y,b(z,a())) = 1y + z + 2 >= -3y + -3z + 0 = f(b(c(f(a()),y,z),z))
        
        f(c(c(z,a(),a()),x,a())) = -4x + z + 1 >= z = z
       problem:
        DPs:
         b#(y,b(z,a())) -> c#(f(a()),y,z)
         c#(z,x,a()) -> b#(b(f(z),z),x)
        TRS:
         c(z,x,a()) -> f(b(b(f(z),z),x))
         b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
         f(c(c(z,a(),a()),x,a())) -> z
       Restore Modifier:
        DPs:
         b#(y,b(z,a())) -> c#(f(a()),y,z)
         c#(z,x,a()) -> b#(b(f(z),z),x)
        TRS:
         c(z,x,a()) -> f(b(b(f(z),z),x))
         b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
         f(c(c(z,a(),a()),x,a())) -> z
        Arctic Interpretation Processor:
         dimension: 1
         usable rules:
          c(z,x,a()) -> f(b(b(f(z),z),x))
          b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
          f(c(c(z,a(),a()),x,a())) -> z
         interpretation:
          [b#](x0, x1) = 3x0 + 2x1 + 5,
          
          [c#](x0, x1, x2) = 5x0 + 3x1 + 4x2 + 0,
          
          [b](x0, x1) = 2x0 + x1 + 0,
          
          [f](x0) = -2x0 + 0,
          
          [c](x0, x1, x2) = 1x0 + -1x1 + -10x2 + 2,
          
          [a] = 2
         orientation:
          b#(y,b(z,a())) = 3y + 4z + 5 >= 3y + 4z + 5 = c#(f(a()),y,z)
          
          c#(z,x,a()) = 3x + 5z + 6 >= 2x + 3z + 5 = b#(b(f(z),z),x)
          
          c(z,x,a()) = -1x + 1z + 2 >= -2x + z + 2 = f(b(b(f(z),z),x))
          
          b(y,b(z,a())) = 2y + 2z + 2 >= -1y + -2z + 2 = f(b(c(f(a()),y,z),z))
          
          f(c(c(z,a(),a()),x,a())) = -3x + z + 1 >= z = z
         problem:
          DPs:
           b#(y,b(z,a())) -> c#(f(a()),y,z)
          TRS:
           c(z,x,a()) -> f(b(b(f(z),z),x))
           b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
           f(c(c(z,a(),a()),x,a())) -> z
         Restore Modifier:
          DPs:
           b#(y,b(z,a())) -> c#(f(a()),y,z)
          TRS:
           c(z,x,a()) -> f(b(b(f(z),z),x))
           b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
           f(c(c(z,a(),a()),x,a())) -> z
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 8/1