Update based on Discord conversations and better searching:
- @univerz’s prover matters only as a benchmark. (“its under continuous construction for breaking BB6 record; but i do not think we can get that code to bbchallenge replicability standards, its too complicated”)
- Bruteforce-CTL probably isn’t needed (still interesting though)
- “Rule-proving simulation acceleration” by @sligocki (thread: Shawn's Holdouts) has the potential to generalize/subsume the “bouncers” decider, based on reported results. I haven’t yet checked its performance, ease of reproduction, and ease of proof. Your decider looks good on those fronts…