FWIW, here is a list of 5 state BB holdouts (unproven TMs) from my codebase: GitHub - sligocki/busy-beaver: Tools for finding Busy Beaver Turing Machines and Proving others as non-halting
It is 7565 TMs. All others were decided using my deciders:
Thank you very much for sharing! I have just enabled the upload of txt files, hopefully it should be working now!
I’ve turned my experimental CTL decider loose on these things – on a laptop, using 1 thread.
Hopefully there are no bugs, in which case this helps show the time/power tradeoffs at play.
Results:
| opts | user time | ms/TM | solved | pct |
|---|---|---|---|---|
| -l 1 | 2.453s | 0.3 | 1521 | 20% |
| -l 2 | 4.060s | 0.5 | 2372 | 31% |
| -l 3 | 16.317s | 2.2 | 3412 | 45% |
| -l 4 | 4m14.293s | 33.6 | 4526 | 60% |
| -l 5 | 112m11.305s | 889.8 | 5421 | 72% |
Purported solutions (beware of “CTL”/“co-CTL” conventions, note the state-precedes-current-bit convention, beware of bad RE simplification) attached.
holdouts_ctl_l5.txt.xz (360.3 KB)
Progress:
The mere output of a decision has a dramatically faster implementation.
The ability to try left-to-right and right-to-left constructions halves the order-of-magnitude speedup, but it gets machines solved significantly faster.
The Python version with regexp output is actually slower, but clearer.
(I’ll let it rerun the limit-5 search and provide updated expressions… eventually. Regexps just aren’t this decider’s native certificate format, apparently.)
| limit | 1-side, CPP | 2-side, CPP | ms/TM | solved | pct |
|---|---|---|---|---|---|
| 1 | 0.008s | 0.017s | <0.1 | 2086 | 28% |
| 1 | 0.055s | 0.096s | <0.1 | 3481 | 46% |
| 2 | 0.701s | 1.135s | 0.2 | 4371 | 58% |
| 3 | 16.376s | 26.572s | 3.5 | 5082 | 67% |
| 4 | 8m05.696s | 13m10.464s | 104.5 | 5925 | 78% |
This time Python needed 178m for -l5 with details.
The certifying regexps now use the angle-bracket convention to clarify the head position (A>0 or [01]<B). I think they’re still “co-CTL” in Shawn’s terms? [EDIT: I misremembered, correct that to – I think these languages are complements of CTLs in Shawn’s terms] In most cases they’re cleaner than before, but there are still some absolute stinkers. The record is “2376, infinite, [78,627 char regexp]”.
I’m now attaching both the decider output and the collection of 1640 stubborn holdouts in seeddb format.
holdouts_ctl_l5.txt.xz (375.9 KB)
stubborn_holdouts.db (48.1 KB)
So far I have no sense of when CTL techniques fail (basically when a regular language can fail to be separated from a word by any regular language). Pushing the depth higher still solves more machines, but it’s diminishing returns on a large investment.
Cool to see @UncombedCoconut . This is very exciting. I mentioned on Discord that CPS has also been pretty effective, categorizing around 50% of my original holdouts. But it looks like your CTL technique is still more effective. I’m downloading the holdouts now to compare and see what sort of overlap we’re seeing.
It looks like CPS decides 523 / 1640 (31%) from @UncombedCoconut’s stubborn_holdouts.db. So it looks like your CTL and my CPS are not totally overlapping in what they find. Woohoo!
FWIW, here is my new holdouts file. This is basically the original file filtered by CPS up to block size 16. I have not included the reductions from @UncombedCoconut or halting segment or any other recent decider. Only ones I’ve written myself. But I’m glad to see that others are finding my list useful 
I’m down to 3,166 holdouts: unknown.txt (108.2 KB) (As commented earlier, with @UncombedCoconut’s filter additionally, that’s down further to 1,117!)