Proving BB(5) in Coq

I’m working on proving correctness of deciders in Coq.
Now only some simple deciders are proved, and there are 82 holdouts (58 of them write 1 at the first step).
Used deciders:

  1. translated cycle
  2. n-gram-CPS with local update history
  3. CTL limited to fixed word length and no “|”
    See readme code for more details.
2 Likes

Wow, this looks like a very fresh approach to piecing together BB(5) from available techniques. You’ve got my interest.
If I may ask, have you been active here for a while? I’m not aware of Nathan’s nice CPS variant being well advertised outside of Discord?
Also, would you mind sharing a holdout list (with the caveat that more compute might change things)? Are they likely TNF leaves or interior nodes corresponding to many individual TMs?

Here is the holdout list, they are all TNF leaves.
holdouts.txt (3.3 KB)

[upd 2024.4.30]:
23 TMs are solved by a FAR verifier
17 TMs are solved by a Weighted Automata verifier
347505 is solved by limited CTL
5877285,6244297,7174252,7174254 are solved by n-gram-CPS

[upd 2024.5.10]:
The proof is finished.

2 Likes

I found this website two weeks ago, and read n-gram-CPS from https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/2.
Since n-gram-CPS seems easy to implement, I reimplement the version described in readme and found that it fails on many trivial cases (e.g. cannot distinguish the length of 1111…1 mod 2).
Add more history information to the tape helps a lot in many cases.
For example, if 1111…11 is generated by a translated cycle of shift 2, and the transition of last update of each position is recorded on the tape, it may look like (1,(A,0))(1,(B,1))(1,(A,0))(1,(B,1))…(1,(A,0))(1,(B,1)).
However, fixed length historical information is not enough, as nested loops may overwrite all useful historical information. LRU cache is a solution (but not perfect) for this: we can record the order of the last occurrence of all 10 possible transitions in each position.

2 Likes

I’ve translated your list to terms more familiar to us, below.
Let me reiterate how impressive these results are. A limitation is that machines not marked as “Regular” below cannot be solved by the techniques you’ve described (we think). However, we know how to solve them between individual proofs in @meithecatte’s BusyCoq repo and a weighted automata technique in @Iijil’s MITMWFAR repo. [EDIT: except Skelet #17, whose BusyCoq proof is under construction. Proof write-ups have been posted to our Discord.]

The “Regular” ones are solvable with CTL/FAR techniques, perhaps including your own with more compute. Let me know if you’d like me to dig up more info about the proofs we know about for these ones.

Holdout BBChallenge Text BBChallenge ID Type
BR0 AL0 CR1 HR1 DR0 EL1 ER1 DR1 AL1 CL1 1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE 572659 Shift Recursive
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 DL1 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD 3841643 Regular
BR1 CL1 AL1 BR1 DL1 AL0 ER1 DR0 HR1 BR0 1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB 12554268 Regular (Sk. 9)
BR0 BL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA 8210684 Shift Recursive
BR0 EL0 CL1 BR1 BR1 DL1 HR1 AL0 AR0 EL1 1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE 11218583 Regular
BR1 HR1 CR0 BR0 CL1 DL0 AR1 EL0 AL0 EL0 1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE 14536286 Regular (Sk. 19)
BR1 HR1 CR0 BL1 DR1 CR1 EL1 DL1 AR0 EL0 1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE 472097 Shift Recursive
BR0 AL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE 8210685 Shift Recursive
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AL1 HR1 1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA 10818510 Shift Recursive
BR1 DL0 CR1 BL0 DR0 HR1 ER1 BL0 AL1 AR0 1RB0LD_1RC0LB_0RD---_1RE0LB_1LA0RA 7174254 Regular
BR0 CL0 CR1 BR1 DL1 EL0 HR1 EL1 AR1 AL1 1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB 8176549 Regular
BR1 CR0 CL1 EL0 DL0 BL0 AR1 HR1 BL1 DR0 1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD 4817065 3N (“Helix”)
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 ER1 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE 11896833 Shift-Overflow
BR1 BL0 CL1 ER0 DL1 CR0 EL0 HR1 AL1 AL0 1RB0LB_1LC0RE_1LD0RC_0LE---_1LA0LA 6244297 Regular
BR1 BL1 CR0 DL0 DR1 CR1 EL1 AL0 HR1 AL1 1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA 11414657 Regular
BR1 AL1 CR1 DR1 AL0 ER0 HR1 CR0 CL0 ER1 1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE 11143983 Regular
BR0 AL0 CR1 HR1 DR0 DL1 ER1 DR1 AL1 EL1 1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE 523280 Shift Recursive
BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE 347505 Regular (Sk. 20)
BR1 AR1 CL1 CL0 EL0 DR0 AR0 BL1 DL1 HR1 1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- 60658955 Regular (Sk. 24)
BR1 AL1 CL0 ER0 HR1 DL1 AR1 CL0 AR1 ER1 1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE 11017998 N_2N (“Finned”)
BR1 DL0 CR1 AR0 DR0 BR0 EL1 HR1 BL1 CL0 1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC 7138511 3N (“Helix”)
BR0 AR0 CL1 HR1 DL0 CL0 ER0 BR1 ER1 AR1 1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE 35346 Regular
BR0 DL0 CR1 ER1 AL1 CR1 CL1 DL1 HR1 BR0 1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA 10756090 N_2N (“Finned”)
BR1 AR1 CR1 BL1 DL0 AR0 AR1 EL1 HR1 DL0 1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD 8120967 N_2N (“Finned”)
BR1 DR0 CR1 HR1 DL1 EL1 ER1 DL1 AR1 CL0 1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC 5057577 Regular
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA 3841642 Regular
BR1 AR0 CL0 AR1 ER1 DL1 CL1 DL0 HR1 BR0 1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB 3810716 Skelet #10
BR0 CL0 CR1 HR1 DL0 ER1 EL1 DL1 AR1 AR0 1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB 20569060 Regular (Sk. 16)
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AR1 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA 11896832 Shift-Overflow
BR1 HR1 CR1 BL1 DL1 ER1 BL1 DL0 AR1 CR0 1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC 2204428 Shift-Overflow
BR1 BR0 CR0 DL0 DR1 HR1 EL0 AR1 AL1 EL1 1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE 35771936 Regular (Sk. 38)
BR0 AL0 CR1 HR1 DR0 DR1 ER1 DR1 AL1 EL1 1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE 321080 Shift Recursive
BR1 HR1 CL0 CL1 DL1 BL1 ER1 DR1 AL0 ER0 1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE 1465912 Shift Recursive
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 CR1 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC 36287 Regular
BR1 CR1 CL1 BR1 DL1 AR0 EL1 BL0 AL1 HR1 1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- 9393627 Regular
BR1 EL0 CR1 BR1 DR1 CL1 EL0 BR0 HR1 AL1 1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA 7763480 N_2N (“Finned”)
BR1 AR1 CL1 BL1 DR0 CL0 ER1 HR1 AR0 AR1 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA 8210683 Shift Recursive
BR1 DL1 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA 13357563 Regular
BR0 AR1 CR1 DL1 DL1 BR1 EL0 AL0 HR1 DL0 1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC 12781955 Shift Recursive
BR1 AL1 CR1 EL0 DR1 AR0 ER1 HR1 AL1 BL1 1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB 11128264 Regular
BR1 HR1 CL0 ER1 DL0 CL1 AR1 BL1 BR0 AR0 1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA 1365166 Skelet #17
BR1 DL0 CR1 BL0 DR0 HR1 ER1 ER0 AL1 AR0 1RB0LD_1RC0LB_0RD---_1RE0RE_1LA0RA 7174252 Regular
BR0 AR1 CR1 DL1 CL1 BR1 EL0 AL0 HR1 DL0 1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC 12699987 Shift Recursive
BR1 AR1 CL1 EL1 DR0 CL0 ER1 HR1 AR0 BL1 1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB 8226493 Shift Recursive
BR1 DR1 CL1 CR0 AR1 DL1 ER0 BL0 HR1 CR1 1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC 68329601 Skelet # 1
BR1 HR1 CR0 CR1 DR1 BR1 EL1 DL1 AR0 EL0 1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE 320969 Shift Recursive
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 EL0 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE 36285 Regular
BR1 ER0 CR0 AR0 DL1 HR1 AL1 BL0 AR1 CL0 1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC 5377178 3N (“Helix”)
BR1 AL0 CR0 HR1 DR1 DR0 EL1 ER0 AR1 CL0 1RB0LA_0RC---_1RD0RD_1LE0RE_1RA0LC 5877285 Regular
BR1 EL0 CR1 HR1 DR0 CR0 DL1 AL0 BL0 EL0 1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE 57874080 Regular (Sk. 42)
BR1 AR0 CL1 HR1 CL0 DL0 ER1 BR0 ER0 AR1 1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA 3841616 Regular (Sk. 40)
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AL0 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA 11896831 Shift-Overflow
BR1 HR1 CL1 DL1 DR1 CL1 ER1 BL0 AR1 CR0 1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC 3656280 Regular
BR1 DL1 CR1 BR0 AL1 CR1 EL1 AL0 CL1 HR1 1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC--- 13134219 Shift-Overflow
BR1 HR1 CR0 BR0 DL0 EL1 DL1 CR1 AL1 EL0 1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE 36299 Regular
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AR1 HR1 1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA 10818491 Shift Recursive
BR1 DL0 CR1 ER0 DR1 HR1 EL1 AL1 AR1 EL1 1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE 7161825 Regular
BR1 AL1 CL0 ER0 HR1 DL1 AL1 CL0 AR1 ER1 1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE 11018487 N_2N (“Finned”)
3 Likes

Here’s the info about known proofs of the above holdouts.

This subset is solved by individual proofs alone (sometimes with common techniques/lemmas). We’re confident these aren’t regular, except technically Skelet 1 (becomes a translated cycler at ludicrous scales).

Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 ER1 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE 11896833 Shift-Overflow Skelet33.v
BR1 AL1 CL0 ER0 HR1 DL1 AR1 CL0 AR1 ER1 1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE 11017998 N_2N (“Finned”) Finned4.v
BR0 DL0 CR1 ER1 AL1 CR1 CL1 DL1 HR1 BR0 1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA 10756090 N_2N (“Finned”) Finned3.v
BR1 AR1 CR1 BL1 DL0 AR0 AR1 EL1 HR1 DL0 1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD 8120967 N_2N (“Finned”) Finned2.v
BR1 AR0 CL0 AR1 ER1 DL1 CL1 DL0 HR1 BR0 1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB 3810716 Skelet #10 Skelet10.v
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AR1 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA 11896832 Shift-Overflow Skelet34.v
BR1 HR1 CR1 BL1 DL1 ER1 BL1 DL0 AR1 CR0 1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC 2204428 Shift-Overflow Skelet15.v
BR1 EL0 CR1 BR1 DR1 CL1 EL0 BR0 HR1 AL1 1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA 7763480 N_2N (“Finned”) Finned1.v
BR1 HR1 CL0 ER1 DL0 CL1 AR1 BL1 BR0 AR0 1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA 1365166 Skelet #17 WIP / Discord
BR1 DR1 CL1 CR0 AR1 DL1 ER0 BL0 HR1 CR1 1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC 68329601 Skelet # 1 Skelet1.v
BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AL0 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA 11896831 Shift-Overflow Skelet35.v
BR1 DL1 CR1 BR0 AL1 CR1 EL1 AL0 CL1 HR1 1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC--- 13134219 Shift-Overflow Skelet26.v
BR1 AL1 CL0 ER0 HR1 DL1 AL1 CL0 AR1 ER1 1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE 11018487 N_2N (“Finned”) Finned5.v

This subset is solved by weighted automata, and listed (by bbchallenge text) in the cert files of MITMWFAR.
We’re confident these aren’t regular. The solution is CTL flavored, but the language class allows counting. The program can solve the 11 “shift recursive” ones by search. The 3N/helix ones, I solved by hand and translated.

Holdout BBChallenge Text BBChallenge ID Type Proof
BR0 AL0 CR1 HR1 DR0 EL1 ER1 DR1 AL1 CL1 1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE 572659 Shift Recursive Weighted Automata
BR0 BL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA 8210684 Shift Recursive Weighted Automata
BR1 HR1 CR0 BL1 DR1 CR1 EL1 DL1 AR0 EL0 1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE 472097 Shift Recursive Weighted Automata
BR0 AL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE 8210685 Shift Recursive Weighted Automata
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AL1 HR1 1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA 10818510 Shift Recursive Weighted Automata
BR1 CR0 CL1 EL0 DL0 BL0 AR1 HR1 BL1 DR0 1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD 4817065 3N (“Helix”) Weighted Automata
BR0 AL0 CR1 HR1 DR0 DL1 ER1 DR1 AL1 EL1 1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE 523280 Shift Recursive Weighted Automata
BR1 DL0 CR1 AR0 DR0 BR0 EL1 HR1 BL1 CL0 1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC 7138511 3N (“Helix”) Weighted Automata
BR0 AL0 CR1 HR1 DR0 DR1 ER1 DR1 AL1 EL1 1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE 321080 Shift Recursive Weighted Automata
BR1 HR1 CL0 CL1 DL1 BL1 ER1 DR1 AL0 ER0 1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE 1465912 Shift Recursive Weighted Automata
BR1 AR1 CL1 BL1 DR0 CL0 ER1 HR1 AR0 AR1 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA 8210683 Shift Recursive Weighted Automata
BR0 AR1 CR1 DL1 DL1 BR1 EL0 AL0 HR1 DL0 1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC 12781955 Shift Recursive Weighted Automata
BR0 AR1 CR1 DL1 CL1 BR1 EL0 AL0 HR1 DL0 1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC 12699987 Shift Recursive Weighted Automata
BR1 AR1 CL1 EL1 DR0 CL0 ER1 HR1 AR0 BL1 1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB 8226493 Shift Recursive Weighted Automata
BR1 HR1 CR0 CR1 DR1 BR1 EL1 DL1 AR0 EL0 1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE 320969 Shift Recursive Weighted Automata
BR1 ER0 CR0 AR0 DL1 HR1 AL1 BL0 AR1 CL0 1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC 5377178 3N (“Helix”) Weighted Automata
BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AR1 HR1 1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA 10818491 Shift Recursive Weighted Automata

This holdout, Skelet 20, is both an extreme bouncer and an extreme CPS-solvable TM.
BusyCoq certifies it as a bouncer as follows. (More info here.)

dir=L,
n0=55144,
n1=41010,
split=[(80, 80), (6, 10), (75, 70)],
shifts=[(0, 144), (2, 20), (1, 34), (1, 28), (5, 392), (1, 196), (3, 34), (13, 816), (2, 144), (2, 22), (5, 392), (2, 196), (9, 102), (13, 816), (0, 144), (0, 16), (5, 392), (1, 196), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (1, 196), (5, 392), (2, 196), (12, 102), (13, 816), (0, 144), (0, 20), (5, 392), (1, 196), (1, 34), (2, 28), (3, 34), (13, 816), (2, 144), (0, 22), (5, 392), (2, 196), (5, 392), (1, 196), (9, 102), (13, 816), (0, 144), (0, 16), (5, 392), (0, 196), (5, 392), (1, 196), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (3, 196), (12, 102), (13, 816), (0, 144), (0, 20), (5, 392), (2, 196), (1, 34), (0, 28), (5, 392), (1, 196), (3, 34), (13, 816), (2, 144), (0, 22), (5, 392), (2, 196), (9, 102), (13, 816), (0, 144), (0, 16), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (1, 196), (12, 102), (13, 816), (0, 144), (2, 20), (1, 34), (1, 28), (3, 34), (13, 816), (2, 144), (0, 22), (9, 102), (13, 816), (0, 144), (0, 16), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (2, 196), (12, 102), (13, 816)]
Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE 347505 Regular (Sk. 20) Bouncers

This subset is solved by CPS, with the given left/center/right segment sizes. (More info here.) I re-list Sk. 20.

Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 DL0 CR1 BL0 DR0 HR1 ER1 BL0 AL1 AR0 1RB0LD_1RC0LB_0RD---_1RE0LB_1LA0RA 7174254 Regular CPS3(12-12-11)
BR1 BL0 CL1 ER0 DL1 CR0 EL0 HR1 AL1 AL0 1RB0LB_1LC0RE_1LD0RC_0LE---_1LA0LA 6244297 Regular CPS3(12-12-11)
BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE 347505 Regular (Sk. 20) CPS3(8-24-7)
BR1 DL0 CR1 BL0 DR0 HR1 ER1 ER0 AL1 AR0 1RB0LD_1RC0LB_0RD---_1RE0RE_1LA0RA 7174252 Regular CPS3(12-12-11)
BR1 AL0 CR0 HR1 DR1 DR0 EL1 ER0 AR1 CL0 1RB0LA_0RC---_1RD0RD_1LE0RE_1RA0LC 5877285 Regular CPS3(12-12-11)

The rest are solved by FAR. In this table I give minimal left/right DFA sizes.
Where I show ‘??’ on the right, only FAR-direct realistically gets it (using an NFA on the right). A DFA size in the 80s is possible…

Holdout BBChallenge Text BBChallenge ID Type Proof
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 DL1 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD 3841643 Regular FAR: 3x4
BR1 CL1 AL1 BR1 DL1 AL0 ER1 DR0 HR1 BR0 1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB 12554268 Regular (Sk. 9) FAR: 13x16
BR0 EL0 CL1 BR1 BR1 DL1 HR1 AL0 AR0 EL1 1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE 11218583 Regular FAR: 4x4
BR1 HR1 CR0 BR0 CL1 DL0 AR1 EL0 AL0 EL0 1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE 14536286 Regular (Sk. 19) FAR: 11x11
BR0 CL0 CR1 BR1 DL1 EL0 HR1 EL1 AR1 AL1 1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB 8176549 Regular FAR: 10x??
BR1 BL1 CR0 DL0 DR1 CR1 EL1 AL0 HR1 AL1 1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA 11414657 Regular FAR: 10x??
BR1 AL1 CR1 DR1 AL0 ER0 HR1 CR0 CL0 ER1 1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE 11143983 Regular FAR: 4x4
BR1 AR1 CL1 CL0 EL0 DR0 AR0 BL1 DL1 HR1 1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- 60658955 Regular (Sk. 24) FAR: 11x11
BR0 AR0 CL1 HR1 DL0 CL0 ER0 BR1 ER1 AR1 1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE 35346 Regular FAR: 4x3
BR1 DR0 CR1 HR1 DL1 EL1 ER1 DL1 AR1 CL0 1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC 5057577 Regular FAR: 11x9
BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA 3841642 Regular FAR: 3x4
BR0 CL0 CR1 HR1 DL0 ER1 EL1 DL1 AR1 AR0 1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB 20569060 Regular (Sk. 16) FAR: 12x11
BR1 BR0 CR0 DL0 DR1 HR1 EL0 AR1 AL1 EL1 1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE 35771936 Regular (Sk. 38) FAR: 11x11
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 CR1 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC 36287 Regular FAR: 4x4
BR1 CR1 CL1 BR1 DL1 AR0 EL1 BL0 AL1 HR1 1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- 9393627 Regular FAR: 9x11
BR1 DL1 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA 13357563 Regular FAR: 3x4
BR1 AL1 CR1 EL0 DR1 AR0 ER1 HR1 AL1 BL1 1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB 11128264 Regular FAR: 11x9
BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 EL0 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE 36285 Regular FAR: 4x4
BR1 EL0 CR1 HR1 DR0 CR0 DL1 AL0 BL0 EL0 1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE 57874080 Regular (Sk. 42) FAR: 10x11
BR1 AR0 CL1 HR1 CL0 DL0 ER1 BR0 ER0 AR1 1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA 3841616 Regular (Sk. 40) FAR: 4x4
BR1 HR1 CL1 DL1 DR1 CL1 ER1 BL0 AR1 CR0 1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC 3656280 Regular FAR: 11x9
BR1 HR1 CR0 BR0 DL0 EL1 DL1 CR1 AL1 EL0 1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE 36299 Regular FAR: 4x4
BR1 DL0 CR1 ER0 DR1 HR1 EL1 AL1 AR1 EL1 1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE 7161825 Regular FAR: 11x9

Here are the DFA tables for those:

1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB [[0, 1], [2, 3], [4, 5], [4, 6], [4, 4], [4, 7], [4, 8], [4, 9], [4, 10], [4, 11], [4, 3], [4, 12], [4, 7]], [[0, 1], [2, 3], [4, 5], [6, 7], [4, 4], [0, 1], [4, 8], [9, 5], [10, 11], [4, 12], [4, 13], [4, 14], [3, 15], [6, 2], [3, 6], [4, 8]]
1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE [[0, 1], [2, 3], [2, 2], [0, 1]], [[0, 1], [2, 3], [2, 2], [0, 1]]
1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE [[0, 1], [2, 3], [4, 4], [5, 6], [4, 4], [7, 4], [8, 4], [9, 10], [4, 4], [5, 6], [4, 3]], [[0, 1], [2, 1], [3, 4], [5, 6], [6, 7], [6, 6], [6, 6], [8, 9], [10, 6], [10, 4], [3, 4]]
1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB [[0, 1], [2, 3], [4, 5], [6, 0], [4, 4], [4, 7], [4, 8], [4, 2], [4, 9], [4, 6]], ??
1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA [[0, 1], [2, 3], [4, 5], [6, 0], [4, 4], [4, 7], [4, 8], [4, 2], [4, 9], [4, 6]], ??
1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE [[0, 1], [2, 3], [2, 2], [0, 1]], [[0, 1], [2, 3], [2, 2], [2, 1]]
1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- [[0, 1], [2, 3], [4, 5], [5, 5], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]], [[0, 1], [2, 1], [3, 4], [5, 6], [5, 7], [5, 5], [5, 7], [8, 9], [3, 5], [10, 6], [5, 4]]
1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [2, 0], [2, 2]]
1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC [[0, 1], [2, 3], [4, 5], [2, 3], [6, 7], [8, 8], [9, 6], [9, 6], [4, 10], [9, 9], [8, 8]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB [[0, 1], [2, 3], [4, 5], [2, 3], [6, 7], [6, 8], [6, 6], [6, 8], [9, 10], [4, 6], [11, 7], [6, 5]], [[0, 1], [2, 3], [4, 5], [5, 5], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]]
1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE [[0, 1], [2, 1], [3, 4], [5, 6], [5, 7], [5, 5], [5, 7], [8, 9], [3, 5], [10, 6], [5, 4]], [[0, 1], [2, 3], [4, 5], [5, 6], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]]
1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]], [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]]
1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE [[0, 1], [2, 3], [4, 4], [5, 6], [4, 4], [7, 4], [2, 4], [8, 9], [5, 6], [4, 3]], [[0, 1], [2, 1], [3, 4], [5, 6], [6, 7], [6, 6], [6, 6], [8, 9], [10, 6], [10, 4], [3, 4]]
1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA [[0, 1], [2, 3], [1, 0], [3, 3]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC [[0, 1], [2, 3], [4, 5], [2, 3], [6, 4], [6, 7], [6, 6], [8, 9], [6, 10], [7, 7], [6, 4]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
2 Likes