YES

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

Proof:
 DP Processor:
  DPs:
   b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(x1)))
   b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
   b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1))))))
   b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(b(b(a(b(a(c(x1)))))))))
  TRS:
   b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
  EDG Processor:
   DPs:
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(x1)))
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1))))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(b(b(a(b(a(c(x1)))))))))
   TRS:
    b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
   graph:
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1)))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(x1)))
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1)))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1)))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1))))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1)))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(b(b(a(b(a(c(x1)))))))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(x1)))
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1))))))
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1))))) ->
    b#(a(b(a(c(b(a(x1))))))) -> b#(a(c(b(b(a(b(a(c(x1)))))))))
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 8/16
    DPs:
     b#(a(b(a(c(b(a(x1))))))) -> b#(b(a(b(a(c(x1))))))
     b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
    TRS:
     b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
    Matrix Interpretation Processor: dim=4
     
     interpretation:
      [b#](x0) = [0 1 0 0]x0,
      
                [1 0 0 0]  
                [0 0 1 1]  
      [c](x0) = [0 0 0 0]x0
                [0 0 0 1]  ,
      
                [1 0 0 0]     [0]
                [0 0 0 1]     [0]
      [b](x0) = [1 0 0 0]x0 + [1]
                [0 1 0 0]     [0],
      
                [1 0 0 0]  
                [0 0 1 1]  
      [a](x0) = [0 0 0 0]x0
                [0 1 0 0]  
     orientation:
      b#(a(b(a(c(b(a(x1))))))) = [1 0 1 1]x1 + [1] >= [0 0 1 1]x1 = b#(b(a(b(a(c(x1))))))
      
      b#(a(b(a(c(b(a(x1))))))) = [1 0 1 1]x1 + [1] >= [1 0 0 1]x1 + [1] = b#(a(b(a(c(x1)))))
      
                                [1 0 0 0]     [0]    [1 0 0 0]     [0]                                   
                                [1 0 1 1]     [1]    [1 0 1 1]     [1]                                   
      b(a(b(a(c(b(a(x1))))))) = [1 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = a(b(a(c(b(b(a(b(a(c(x1))))))))))
                                [1 0 1 1]     [1]    [1 0 1 1]     [1]                                   
     problem:
      DPs:
       b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
      TRS:
       b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
     EDG Processor:
      DPs:
       b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
      TRS:
       b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
      graph:
       b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1))))) ->
       b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
      CDG Processor:
       DPs:
        b#(a(b(a(c(b(a(x1))))))) -> b#(a(b(a(c(x1)))))
       TRS:
        b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(x1))))))))))
       graph:
        
       Qed