Some machines decided by Skelet's decider

[cosmo]

@savask on discord has given a list of non-halting machines that are decided by Skelet’s program. Each machine is labelled differently in Skelet’s terminology, @mateon1 and I have translated these machines to bbchallenge’s IDs:

• Incremental formula:

  • 1LC0LB_---1LA_1RD1RD_1LB1RE_1LE1RC
  • https://bbchallenge.org/5857873

• Closed position:

  • 1LC0RD_---1RD_1RD0LA_1RA1RE_1LE1RB
  • https://bbchallenge.org/52919616

• Closed transition modulo:

  • 1LC1RB_---0RA_1RD0LD_1LA1RE_1LC1RD
  • https://bbchallenge.org/14168126

• Single exone:

  • 1LC0RA_---0LA_1RD1LE_1RE1RE_1LB0RD
  • https://bbchallenge.org/5960419

• Spec1 exone:

  • 1LC0LC_---0RD_1RD1LA_0RB1RE_1LC0RD
  • https://bbchallenge.org/4225593

• Self-tuning exone:

  • 1LC0LB_---1LD_1RD1LD_0LA1RE_1LD0RE
  • https://bbchallenge.org/5807483

• Huffman:

  • 1LC1RE_---1LA_0RD0LD_1LB1RD_1LA0RA
  • https://bbchallenge.org/86328673

• BL_1:

  • 1LB---_0RC0LC_1LE0RD_1RC1RD_1RB0LA
  • https://bbchallenge.org/936206

• BL_2:

  • 1LC0RE_0LE---_1LD0LB_1RA0LA_0RA1RE
  • https://bbchallenge.org/7163434

[UncombedCoconut]

@cosmo

Spec1 exone:

• 1LC0LC_---0RD_1RD1LA_0RB1RE_1LC0RD
• https://bbchallenge.org/4225593

This one falls easily to closed-language analysis.
Cleaned up output from dumb_dfa_decider looks like 0* 1 (1.)* (1[aAcC] | [bBDE]) .* | 0*[aCd].*
(. representing [01], a/A representing the first state on a 0/1 bit).

FWIW, the others take more than what a 5-state DFA on either side can identify, and I didn’t look into whether this was a lucky example of “Spec1 exone”.
[EDIT: misread my own terminal output: 52919616 falls as well and the others are incomplete. The search found a very messy (0*(1((11|0)1)*((11|0)(a|A|C|E)|(1(C|D)|(b|B|c|d|D|E)))|(a|A|c|C|d|E))1*1|0*(1((11|0)1)*((11|0)(a|A)|(1(C|D)|(b|B|c|D)))|(a|c)))(01*1|0)*.]

[EDIT: The cat also dragged in:

======================================== 5807483 ========================================
((1111*0|(110|(10|0)))*(1111*(d00|(c0|C))|(11((C|d)00|(c0|C))|((1(B|d)|(d|E))00|(1(c0|(B|C|D))|(D0|(a|A|C))))))(100)*1|(1111*0|(110|(10|0)))*(1111*(c|d|D)|(11(c|C|d|D)|(1(b|B|c|d|D)|(a|d|D|E)))))(1(100)*1|0)*

but at this point the searches are expensive for this naive script.]

[UncombedCoconut]

The updated CTL solver (now posted in “Deciders”) gets 4/9 in 20 seconds with default settings.
Its new solution, for “BL_1”, is a monster:

936206, infinite, ((((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*(00|0)|0*1(010*1)*(0(0[01]*D([01]0|[01]|((0[01]*A|D0|E1)0|(0[01]*B|B)))|(1[01]*D([01]0|[01]|((1[01]*A|A)0|1[01]*B))))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*0|0*1(010*1)*(0(0[01]*D[01]|0[01]*C)|(1[01]*D[01]|1[01]*C))))(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*0|1))*(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0)|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*0|[01])|(((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*(00|0)|0*1(010*1)*(0(0[01]*D([01]0|[01]|((0[01]*A|D0|E1)0|(0[01]*B|B)))|(1[01]*D([01]0|[01]|((1[01]*A|A)0|1[01]*B))))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0)|((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*0|0*1(010*1)*(0(0[01]*D[01]|0[01]*E)|(1[01]*D[01]|(1[01]*E|C0))))))((((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|([01]0|0))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0))(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*0|1))*(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0)|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*0|[01])|(((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|([01]0|0))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0)|((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0)))*((((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|([01]0|0))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|0))(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*0|1))*(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((00|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|((00|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|(((00|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|01|0)[01]*|0?)))))|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((10|1)1|1)(110|10)|((101|11|1)0|(1(00|1)|(10|((10|1)0|1)))))(1010|(1(00|1)|0))*1011[01]*|(((10|1)1|1)(111[01]*)?|((101|11|1)1[01]*|((11|11|1)[01]*|1?))))))|(((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|([01]0|0))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((00|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|((00|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|(((00|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|01|0)[01]*|0?)))))|((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((00|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|((00|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|(((00|0)1|0)(111[01]*)?|((001|01|0)1[01]*|(([01]1|01|0)[01]*|[01]?)))))))|((((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*(00|0)|0*1(010*1)*(0(0[01]*D([01]0|[01]|((0[01]*A|D0|E1)0|(0[01]*B|B)))|(1[01]*D([01]0|[01]|((1[01]*A|A)0|1[01]*B))))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*0|0*1(010*1)*(0(0[01]*D[01]|0[01]*C)|(1[01]*D[01]|1[01]*C))))(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*0|[01]|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*0|1))*(((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(00|0)|10|1)((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((00|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|((00|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|(((00|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|01|0)[01]*|0?)))))|((((10|1)1|1)0|1)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((10|1)1|1)(110|10)|((101|11|1)0|(1(00|1)|(10|((10|1)0|1)))))(1010|(1(00|1)|0))*1011[01]*|(((10|1)1|1)(111[01]*)?|((101|11|1)1[01]*|((11|11|1)[01]*|1?))))))|(((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*(00|0)|0*1(010*1)*(0(0[01]*D([01]0|[01]|((0[01]*A|D0|E1)0|(0[01]*B|B)))|(1[01]*D([01]0|[01]|((1[01]*A|A)0|1[01]*B))))((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(00|0)|00|0)*((((00|0)1|0)0|0)((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((((00|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|((00|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|(((00|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|01|0)[01]*|0?)))))|((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))0|(0(0[01]*D[01]|10*E)|1[01]*D[01]))|(0*A010|0*E))((([01]0|0)1|0)0|0)*(((([01]0|0)1|0)(110|10)|((001|01|0)0|(0(00|1)|(00|(([01]0|0)0|0)))))(1010|(1(00|1)|0))*1011[01]*|((([01]0|0)1|0)(111[01]*)?|((001|01|0)1[01]*|((01|([01]1|0))[01]*|0?))))|((0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))(110|10)|((0(0[01]*D([01]01|([01]1|[01])|((10*(D1|C)|E0)01|(10*D0|A)))|(1[01]*D([01]01|([01]1|[01])|(D001|(C1|E)1)))0|(0(0[01]*D([01](00|1)|([01]0|(([01]0|[01]0|[01]))|((10*(D1|C)|E0)(00|1)|(10*(A00|B)|D1)))|(1[01]*D([01](00|1)|([01]0|(([01]0|[01]0|[01]))|(D0(00|1)|((C1|E)0|B0|D1))))))|(0*A01(110|10)|((0*(D1|C)01|0*D0)0|(0*(D1|C)(00|1)|0*(A00|B)))))(1010|(1(00|1)|0))*1011[01]*|(0*1(010*1)*((0(0[01]*D(([01]0|[01]1|[01]|(10*A01|C))|(1[01]*D(([01]0|[01]1|[01]|B1))(111[01]*)?|((0(0[01]*D([01]01|([01]1|[01])|((10*(D1|C)|E0)01|(10*D0|A)))|(1[01]*D([01]01|([01]1|[01])|(D001|(C1|E)1)))1[01]*|((0(0[01]*D([01]1|([01]1|[01])|(10*(A1|D1)|(0[01]*A|D0|E1)1))|(1[01]*D([01]1|([01]1|[01])|((1[01]*A|A)1|C1|D1)))[01]*|(0(0[01]*D[01]?|((0[01]*A|D0|E1)|D))|(1[01]*D[01]?|((1[01]*A|A)|C))))))|(0*A01(111[01]*)?|((0*(D1|C)01|0*D0)1[01]*|0*(A1|D1)[01]*)))))))