YES

Problem:
 b(d(b(x1))) -> c(d(b(x1)))
 b(a(c(x1))) -> b(c(x1))
 a(d(x1)) -> d(c(x1))
 b(b(b(x1))) -> a(b(c(x1)))
 d(c(x1)) -> b(d(x1))
 d(c(x1)) -> d(b(d(x1)))
 d(a(c(x1))) -> b(b(x1))

Proof:
 DP Processor:
  DPs:
   b#(a(c(x1))) -> b#(c(x1))
   a#(d(x1)) -> d#(c(x1))
   b#(b(b(x1))) -> b#(c(x1))
   b#(b(b(x1))) -> a#(b(c(x1)))
   d#(c(x1)) -> d#(x1)
   d#(c(x1)) -> b#(d(x1))
   d#(c(x1)) -> d#(b(d(x1)))
   d#(a(c(x1))) -> b#(x1)
   d#(a(c(x1))) -> b#(b(x1))
  TRS:
   b(d(b(x1))) -> c(d(b(x1)))
   b(a(c(x1))) -> b(c(x1))
   a(d(x1)) -> d(c(x1))
   b(b(b(x1))) -> a(b(c(x1)))
   d(c(x1)) -> b(d(x1))
   d(c(x1)) -> d(b(d(x1)))
   d(a(c(x1))) -> b(b(x1))
  Matrix Interpretation Processor: dim=5
   
   interpretation:
    [d#](x0) = [1 0 0 0 0]x0,
    
    [a#](x0) = [1 1 0 0 0]x0 + [1],
    
    [b#](x0) = [0 0 0 1 1]x0,
    
              [1 1 1 0 0]     [0]
              [1 1 0 0 0]     [1]
    [a](x0) = [1 1 1 0 0]x0 + [0]
              [1 1 0 0 0]     [0]
              [1 1 0 0 0]     [0],
    
              [1 0 1 0 0]     [1]
              [0 0 0 1 1]     [0]
    [c](x0) = [1 0 1 0 0]x0 + [1]
              [0 0 0 0 0]     [0]
              [0 0 0 0 0]     [0],
    
              [1 0 0 0 0]     [0]
              [0 0 1 0 0]     [1]
    [d](x0) = [1 0 0 0 0]x0 + [0]
              [0 0 1 0 0]     [0]
              [1 0 0 0 0]     [0],
    
              [0 0 0 1 1]     [0]
              [0 0 0 1 1]     [0]
    [b](x0) = [0 0 0 1 1]x0 + [1]
              [0 0 1 0 0]     [0]
              [0 0 1 0 0]     [0]
   orientation:
    b#(a(c(x1))) = [2 0 2 2 2]x1 + [2] >= [0] = b#(c(x1))
    
    a#(d(x1)) = [1 0 1 0 0]x1 + [2] >= [1 0 1 0 0]x1 + [1] = d#(c(x1))
    
    b#(b(b(x1))) = [0 0 0 2 2]x1 + [2] >= [0] = b#(c(x1))
    
    b#(b(b(x1))) = [0 0 0 2 2]x1 + [2] >= [1] = a#(b(c(x1)))
    
    d#(c(x1)) = [1 0 1 0 0]x1 + [1] >= [1 0 0 0 0]x1 = d#(x1)
    
    d#(c(x1)) = [1 0 1 0 0]x1 + [1] >= [1 0 1 0 0]x1 = b#(d(x1))
    
    d#(c(x1)) = [1 0 1 0 0]x1 + [1] >= [1 0 1 0 0]x1 = d#(b(d(x1)))
    
    d#(a(c(x1))) = [2 0 2 1 1]x1 + [2] >= [0 0 0 1 1]x1 = b#(x1)
    
    d#(a(c(x1))) = [2 0 2 1 1]x1 + [2] >= [0 0 2 0 0]x1 = b#(b(x1))
    
                  [0 0 0 2 2]     [1]    [0 0 0 2 2]     [1]              
                  [0 0 0 2 2]     [1]    [0 0 0 2 2]     [1]              
    b(d(b(x1))) = [0 0 0 2 2]x1 + [2] >= [0 0 0 2 2]x1 + [1] = c(d(b(x1)))
                  [0 0 0 1 1]     [0]    [0 0 0 0 0]     [0]              
                  [0 0 0 1 1]     [0]    [0 0 0 0 0]     [0]              
    
                  [2 0 2 2 2]     [2]    [0 0 0 0 0]     [0]           
                  [2 0 2 2 2]     [2]    [0 0 0 0 0]     [0]           
    b(a(c(x1))) = [2 0 2 2 2]x1 + [3] >= [0 0 0 0 0]x1 + [1] = b(c(x1))
                  [2 0 2 1 1]     [2]    [1 0 1 0 0]     [1]           
                  [2 0 2 1 1]     [2]    [1 0 1 0 0]     [1]           
    
               [2 0 1 0 0]     [1]    [1 0 1 0 0]     [1]           
               [1 0 1 0 0]     [2]    [1 0 1 0 0]     [2]           
    a(d(x1)) = [2 0 1 0 0]x1 + [1] >= [1 0 1 0 0]x1 + [1] = d(c(x1))
               [1 0 1 0 0]     [1]    [1 0 1 0 0]     [1]           
               [1 0 1 0 0]     [1]    [1 0 1 0 0]     [1]           
    
                  [0 0 0 2 2]     [2]    [1]              
                  [0 0 0 2 2]     [2]    [1]              
    b(b(b(x1))) = [0 0 0 2 2]x1 + [3] >= [1] = a(b(c(x1)))
                  [0 0 2 0 0]     [1]    [0]              
                  [0 0 2 0 0]     [1]    [0]              
    
               [1 0 1 0 0]     [1]    [1 0 1 0 0]     [0]           
               [1 0 1 0 0]     [2]    [1 0 1 0 0]     [0]           
    d(c(x1)) = [1 0 1 0 0]x1 + [1] >= [1 0 1 0 0]x1 + [1] = b(d(x1))
               [1 0 1 0 0]     [1]    [1 0 0 0 0]     [0]           
               [1 0 1 0 0]     [1]    [1 0 0 0 0]     [0]           
    
               [1 0 1 0 0]     [1]    [1 0 1 0 0]     [0]              
               [1 0 1 0 0]     [2]    [1 0 1 0 0]     [2]              
    d(c(x1)) = [1 0 1 0 0]x1 + [1] >= [1 0 1 0 0]x1 + [0] = d(b(d(x1)))
               [1 0 1 0 0]     [1]    [1 0 1 0 0]     [1]              
               [1 0 1 0 0]     [1]    [1 0 1 0 0]     [0]              
    
                  [2 0 2 1 1]     [2]    [0 0 2 0 0]     [0]           
                  [2 0 2 1 1]     [3]    [0 0 2 0 0]     [0]           
    d(a(c(x1))) = [2 0 2 1 1]x1 + [2] >= [0 0 2 0 0]x1 + [1] = b(b(x1))
                  [2 0 2 1 1]     [2]    [0 0 0 1 1]     [1]           
                  [2 0 2 1 1]     [2]    [0 0 0 1 1]     [1]           
   problem:
    DPs:
     
    TRS:
     b(d(b(x1))) -> c(d(b(x1)))
     b(a(c(x1))) -> b(c(x1))
     a(d(x1)) -> d(c(x1))
     b(b(b(x1))) -> a(b(c(x1)))
     d(c(x1)) -> b(d(x1))
     d(c(x1)) -> d(b(d(x1)))
     d(a(c(x1))) -> b(b(x1))
   Qed