This post summarizes a family of 5 decider holdouts (proved infinite by hand).

They are:

`1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA`

= 7763480 proof`1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD`

= 8120967 proof`1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA`

= 10756090 proof`1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE`

= 11017998 proof`1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE`

= 11018487 proof

Years ago, Skelet noticed them and wrote: " **N_2N** and **3N** machines are 3-linear sequences, but with little complex behavior than the machines, proved by methods TryL1Cnt and TryModFin. They are easy provable by hand." (â€śN_2Nâ€ť corresponds to these five; â€ś3Nâ€ť corresponds to a holdout family Iâ€™ve called â€śhelixâ€ť.)

I called them â€śfinnedâ€ť cubic machines when I noticed them as CTL holdouts.

They are *provably* CTL holdouts, as illustrated by @Iijil: 10756090 is irregular.

Analysis has shown theyâ€™ll likely remain holdouts for any Weighted Finite Automata decider (using a single integer weight): a closed language of configs can be described in this way (and the linked proofs effectively do that), but the transitions do not vary the weights smoothly.

However, @mxdys has reported being able to extend a Repeated-Word List CTL decider in a way that allows linear equalities between repeater counts, and it was effective at solving these machines.

@meithecatte has also at least started to explore automatic deciders that could cover this class

Therefore, these machines may soon lose their status as special cases.