YES

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

Proof:
 DP Processor:
  DPs:
   b#(y,z) -> c#(y,z,z)
   b#(y,z) -> c#(c(y,z,z),a(),a())
   c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
   c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
   c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
  TRS:
   b(y,z) -> f(c(c(y,z,z),a(),a()))
   b(b(z,y),a()) -> z
   c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
  TDG Processor:
   DPs:
    b#(y,z) -> c#(y,z,z)
    b#(y,z) -> c#(c(y,z,z),a(),a())
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
    c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
   TRS:
    b(y,z) -> f(c(c(y,z,z),a(),a()))
    b(b(z,y),a()) -> z
    c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
   graph:
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
    c#(f(z),f(c(a(),x,a())),y) -> b#(x,z) ->
    b#(y,z) -> c#(c(y,z,z),a(),a())
    c#(f(z),f(c(a(),x,a())),y) -> b#(x,z) -> b#(y,z) -> c#(y,z,z)
    b#(y,z) -> c#(c(y,z,z),a(),a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
    b#(y,z) -> c#(c(y,z,z),a(),a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
    b#(y,z) -> c#(c(y,z,z),a(),a()) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
    b#(y,z) -> c#(y,z,z) ->
    c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
    b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
    b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
   EDG Processor:
    DPs:
     b#(y,z) -> c#(y,z,z)
     b#(y,z) -> c#(c(y,z,z),a(),a())
     c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
     c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
     c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
    TRS:
     b(y,z) -> f(c(c(y,z,z),a(),a()))
     b(b(z,y),a()) -> z
     c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
    graph:
     c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a()) ->
     c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
     c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a()) ->
     c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
     c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a()) ->
     c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
     c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
     c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
     c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
     c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
     c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
     c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
     c#(f(z),f(c(a(),x,a())),y) -> b#(x,z) ->
     b#(y,z) -> c#(y,z,z)
     c#(f(z),f(c(a(),x,a())),y) -> b#(x,z) -> b#(y,z) -> c#(c(y,z,z),a(),a())
     b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
     b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
     b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
    CDG Processor:
     DPs:
      b#(y,z) -> c#(y,z,z)
      b#(y,z) -> c#(c(y,z,z),a(),a())
      c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
      c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
      c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
     TRS:
      b(y,z) -> f(c(c(y,z,z),a(),a()))
      b(b(z,y),a()) -> z
      c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
     graph:
      c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
      c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
      c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
      c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
      c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a()) ->
      c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
      c#(f(z),f(c(a(),x,a())),y) -> b#(x,z) ->
      b#(y,z) -> c#(c(y,z,z),a(),a())
      c#(f(z),f(c(a(),x,a())),y) -> b#(x,z) -> b#(y,z) -> c#(y,z,z)
      b#(y,z) -> c#(y,z,z) ->
      c#(f(z),f(c(a(),x,a())),y) -> c#(f(b(x,z)),c(z,y,a()),a())
      b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
      b#(y,z) -> c#(y,z,z) -> c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 8/25
      DPs:
       c#(f(z),f(c(a(),x,a())),y) -> c#(z,y,a())
       c#(f(z),f(c(a(),x,a())),y) -> b#(x,z)
       b#(y,z) -> c#(y,z,z)
      TRS:
       b(y,z) -> f(c(c(y,z,z),a(),a()))
       b(b(z,y),a()) -> z
       c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [c#](x0, x1, x2) = 2x0 + x1 + x2 + 5,
        
        [b#](x0, x1) = 2x0 + 2x1 + 6,
        
        [f](x0) = x0,
        
        [a] = 0,
        
        [c](x0, x1, x2) = 2x1 + 4x2 + 4,
        
        [b](x0, x1) = x0 + 4
       orientation:
        c#(f(z),f(c(a(),x,a())),y) = 2x + y + 2z + 9 >= y + 2z + 5 = c#(z,y,a())
        
        c#(f(z),f(c(a(),x,a())),y) = 2x + y + 2z + 9 >= 2x + 2z + 6 = b#(x,z)
        
        b#(y,z) = 2y + 2z + 6 >= 2y + 2z + 5 = c#(y,z,z)
        
        b(y,z) = y + 4 >= 4 = f(c(c(y,z,z),a(),a()))
        
        b(b(z,y),a()) = z + 8 >= z = z
        
        c(f(z),f(c(a(),x,a())),y) = 4x + 4y + 12 >= 4y + 12 = c(f(b(x,z)),c(z,y,a()),a())
       problem:
        DPs:
         
        TRS:
         b(y,z) -> f(c(c(y,z,z),a(),a()))
         b(b(z,y),a()) -> z
         c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
       Qed