YES

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

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