YES

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

Proof:
 DP Processor:
  DPs:
   b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
   b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
   b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
   b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
   b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
  TRS:
   b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1)))))))
  EDG Processor:
   DPs:
    b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
   TRS:
    b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1)))))))
   graph:
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1)))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1)))))) ->
    b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
   CDG Processor:
    DPs:
     b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
    TRS:
     b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1)))))))
    graph:
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(b(a(x1))))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(a(x1))))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) ->
     b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
     b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1))))) -> b#(b(a(b(b(b(x1)))))) -> b#(a(x1))
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 10/25
     DPs:
      b#(b(a(b(b(b(x1)))))) -> b#(b(a(x1)))
      b#(b(a(b(b(b(x1)))))) -> b#(b(b(b(a(x1)))))
     TRS:
      b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1)))))))
     KBO Processor:
      argument filtering:
       pi(b) = [0]
       pi(a) = 0
       pi(b#) = 0
      weight function:
       w0 = 1
       w(b#) = 1
       w(a) = w(b) = 0
      precedence:
       b# ~ a ~ b
      problem:
       DPs:
        
       TRS:
        b(b(a(b(b(b(x1)))))) -> a(b(b(b(b(b(a(x1)))))))
      Qed