YES

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

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