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]]