This is very impressive work, you are really pushing bbchallenge on the tracks of automatic proofs at a faster rate than what I could have imagined in my dreams!!
I am going to read your code in depth as well as starting to write about bouncers in parallel.
Thank you!
Earlier in May @Iijil also proposed an implementation of bouncers: GitHub - Iijil1/Bouncers: A bouncer decider. Proving that some turing machines don't halt.