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