YES

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

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