Tested Closed state/transition cluster since it was added to busycoq. It’d be used at an early stage: it’s over in a few seconds, and you can explain how it works in a few seconds too.
Though weaker than FAR, this method exploits work from the TNF (DB construction) stage to define only reachable transitions. The first FAR iteration misses 8% of this method’s decided TMs because machines like this can delay entering the closed transition cluster until after several steps on the tape.
Here’s the decided set:
Syntactic.bs.zst (2.6 MB)
And here’s a fair-ish Venn diagram that includes very-fast methods.
If your goal is a simple decider pipeline: you need Cyclers/TCyclers/Bouncers anyway, at which point BackwardReasoning is exhausted by adding FAR-Direct-6 and Syntactic is exhausted by adding FAR-Direct-3. But that is not the end of the story when speed is a priority.