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)))))))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [b#](x0) = x0,
      
      [a](x0) = x0,
      
      [b](x0) = 1x0
     orientation:
      b#(a(a(b(a(b(x1)))))) = 2x1 >= 2x1 = b#(a(a(b(b(a(x1))))))
      
      b#(a(a(b(a(b(x1)))))) = 2x1 >= x1 = b#(a(x1))
      
      b(a(a(b(a(b(x1)))))) = 3x1 >= 3x1 = a(b(a(a(b(b(a(x1)))))))
     problem:
      DPs:
       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)))))))
     EDG Processor:
      DPs:
       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(a(b(b(a(x1))))))
      Matrix Interpretation Processor: dim=4
       
       interpretation:
        [b#](x0) = [1 0 0 0]x0,
        
                  [0 1 0 0]  
                  [1 0 0 0]  
        [a](x0) = [0 0 0 1]x0
                  [0 0 0 0]  ,
        
                  [0 0 1 0]     [0]
                  [0 0 0 0]     [0]
        [b](x0) = [1 0 0 1]x0 + [0]
                  [0 1 0 0]     [1]
       orientation:
        b#(a(a(b(a(b(x1)))))) = [0 1 0 0]x1 + [1] >= [0 1 0 0]x1 = b#(a(a(b(b(a(x1))))))
        
                               [0 0 0 0]     [0]    [0]                          
                               [0 0 0 0]     [0]    [0]                          
        b(a(a(b(a(b(x1)))))) = [0 1 0 0]x1 + [1] >= [1] = 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