The 30 to 34 CTL holdouts from BB(5)

Individual machines
4

Possibly slightly off topic, it would be good to give a clear Skelet status list here. UncombedCoconut pointed me on discord to his list: https://cdn.discordapp.com/attachments/960643023530762341/1073801475291099207/skelet_annotated_v2.txt and apparently all undecideds have been since decided, #1 and #17 manually and #3 and #7 by automata as mentioned by Justin on Discord. The list is reproduced here:

1	1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC	** UNDECIDED **
2	1RB0LD_1LC0RA_1LA1LC_1RA0LE_---0LB	Decided by: bbchallenge.org
3	1RB0LA_1LC0RD_1LA1LB_---1RE_0RB1RC	** UNDECIDED ** ~7
4	1RB0LC_1LC1RB_1RD1LA_1RE0RC_---0RD	Decided by: Justin, [CPS untested]
5	1RB1RA_1LC0RD_1RA0LB_1LB0RE_---0RC	Decided by: bbchallenge.org
6	1RB0LE_1RC0LA_1LD0RB_1LB1LD_---0LC	Decided by: bbchallenge.org
7	1RB0LD_1RC1RA_1LA0RC_---1LE_0LA1LB	** UNDECIDED ** ~3
8	1RB0LE_1RC0RB_0LD1RB_0LA1LD_---0LB	Decided by: Justin, bouncers, shawn_oct3, [CPS untested]
9	1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB	Decided by: Justin, [CPS untested]
10	1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB	[manual: D. Briggs]
11	1RB0RA_0LC1RA_0LD1LC_1RA0LE_---0LA	Decided by: Justin, bouncers, shawn_oct3, [CPS untested]
12	1RB0RD_0LC1RA_0RA1LB_1LB0RE_---1RD	Decided by: Justin, [CPS untested]
13	1RB0LE_0RC1LD_0LD1RB_1LB0LA_---1LA	Decided by: Justin, [CPS untested]
14	1RB---_1LC0LE_1RD0LB_0RD1RA_0LC0RA	Decided by: bbchallenge.org
15	1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC	[manual: S. Ligocki]
16	1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB	Decided by: Justin, [CPS untested]
17	1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA	** UNDECIDED **
18	1RB---_0RC0LD_1RD0LE_1RE0RA_1LC0LD	Decided by: bbchallenge.org
19	1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE	Decided by: Justin, [CPS untested]
20	1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
21	1RB1RD_1LC0LD_1LE1LD_1LB0RA_1RA---	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
22	1RB0RE_1LC0RA_0LC1LD_1LA---_0RB0LD	Decided by: bbchallenge.org
23	1RB0LB_1LC0RD_1RB0LD_1LA1RE_0RC---	Decided by: Justin, [CPS untested]
24	1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD---	Decided by: Justin, [CPS untested]
25	1RB0LA_1LC1RD_1LA0LC_0RD0LE_1RA---	Decided by: bbchallenge.org
26	1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---	[manual: S. Ligocki]
27	1RB0LD_1RC0RE_1LA0RA_0LA1LD_0RD---	Decided by: Justin, [CPS untested]
28	1RB0RE_1RC1RE_1LD---_1LA1LE_1RA0LD	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
29	1RB0LC_1LA0RC_1LD1RE_1RB0LB_0RA---	Decided by: Justin, [CPS untested]
30	1RB0RD_0LC1RA_1LA0LD_1LE0RD_1LB---	Decided by: CPS:(w,s)≤(54,27)
31	1RB0LE_0RC1RB_1RD0RB_1LA0LB_0LD---	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
32	1RB0LD_0RC0RE_1LC0LA_1LA1RC_0RB---	Decided by: Justin, [CPS untested]
33	1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE	[manual: S. Ligocki]
34	1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA	[manual: S. Ligocki]
35	1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA	[manual: S. Ligocki]
36	1RB1LE_0RC0RB_1LD1RA_1LC---_1RC0LA	Decided by: Justin, [CPS untested]
37	1RB0LE_0RC0LC_1LA0RD_1RC1RD_1LB---	Decided by: Justin, [CPS untested]
38	1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE	Decided by: Justin, [CPS untested]
39	1RB1RD_1LC---_1LE1LD_1RE0LC_1RA0RD	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
40	1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA	Decided by: Justin, [CPS untested]
41	1RB0LA_1RC---_0RD1LE_1RE0RA_1LC0LA	Decided by: CPS:(w,s)≤(54,27)
42	1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE	Decided by: Justin, [CPS untested]
43	1RB0LA_0RC---_1LC1RD_1RE1LA_0RB0LD	Decided by: CPS:(w,s)≤(54,27)

I was curious about some things of the list:

  • what is Justin, [CPS untested]? Is there a database or paintext list somewhere of all the machines that were proven by that decider, possibly with the DFA or DFA size?
  • what is CPS:(w,s)≤(54,27)
  • what is shawn_oct3. Presumably some work by Sligoki.

The rest I understand.

It is also interesting that some of the machines that were not caught by deciders as mentioned at: The 30 to 34 CTL holdouts from BB(5) - #3 by chxu were decided by Skelet apparently. It would be interesting to find out if this was a bug on his side, of if he had some specialized deciders for those cases.

I also started to compile a more direct HTML Skelet list with links for copy paste at: halting problem - What is the smallest Turing machine where it is unknown if it halts or not? - Theoretical Computer Science Stack Exchange and I’ll update that as I understand things a bit more clearly.

| # | #BBC | proofs | comments |
|-|-|-|-|-|
| 1 | 68329601 | TC: Coq, manual | |
| 2 | 55767995 | TC: BBC decider | |
| 3 | 5950405 | FAR: decider | |
| 4 | 6897876 | FAR: BBC decider | |
| 5 | 60581745 | TC: BBC decider | |
| 6 | 58211439 | TC: BBC decider | |
| 7 | 7196989 | FAR: decider | |
| 8 | 7728246 | FAR: decider, manual | |
| 9 | 12554268 | FAR: decider, manual | |
| 10 | 3810716 | manual by D. Briggs | interpretation |
| 11 | 3810169 | FAR: decider, manual | |
| 12 | 4982511 | FAR: decider, manual | |
| 13 | 7566785 | FAR: decider, manual | |
| 14 | 31357173 | TC: BBC decider | |
| 15 | 2204428 | SOC: manual | |
| 16 | 20569060 | FAR: decider | |
| 17 | 1365166 | manual by C. Xu | |
| 18 | 15439451 | TC: BBC decider | |
| 19 | 14536286 | FAR: decider | |
| 20 | 347505 | BNC | |
| 21 | 9980689 | BNC, manual by D. Briggs | |
| 22 | 45615747 | TC: BBC decider | |
| 23 | 6237150 | FAR: BBC decider |
| 24 | 60658955 | FAR: decider | |
| 25 | 47260245 | TC: BBC decider | |
| 26 | 13134219 | SOC: manual by S. Ligocki | |
| 27 | 7163434 | FAR: decider | |
| 28 | 5657318 | BNC, manual by D. Briggs | |
| 29 | 6626162 | FAR: BBC decider | |
| 30 | 4986661 | FAR: decider | =41 |
| 31 | 56967673 | manual by D. Briggs | |
| 32 | 6957734 | FAR: BBC decider, manual | |
| 33 | 11896833 | SOC: manual by S. Sligocki | |
| 34 | 11896832 | SOC: manual by S. Sligocki, Coq | |
| 35 | 11896831 | SOC: manual by S. Sligocki, Coq | |
| 36 | 13609549 | FAR: BBC decider | |
| 37 | 7512832 | FAR: BBC decider | |
| 38 | 35771936 | ? | |
| 39 | 9914965 | BNC, manual by D. Briggs | |
| 40 | 3841616 | FAR: BBC decider | |
| 41 | 5915217 | FAR: decider | =30 |
| 42 | 57874080 | FAR: decider | |
| 43 | 5878998 | FAR: decider |

1 Like