MAYBE

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

Proof:
 DP Processor:
  DPs:
   a#(a(a(b(x1)))) -> a#(x1)
   a#(a(a(b(x1)))) -> a#(a(x1))
   a#(a(a(b(x1)))) -> a#(a(a(x1)))
   a#(a(a(b(x1)))) -> a#(a(a(a(x1))))
  TRS:
   a(x1) -> x1
   a(a(a(b(x1)))) -> b(b(b(a(a(a(a(x1)))))))
  Open