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