I have implemented my own HaltingSegments Decider in C++, available at bbchallenge/HaltingSegments at main · TonyGuil/bbchallenge · GitHub. It finds all of lijil’s 995,554 machines, plus another 25,080 machines due to its broader segment-matching criterion. I had to run it at depth 1,000 and a node limit of 60,000 to decide all of lijil’s machines; perhaps we are counting nodes differently? This took 160 minutes.
Here is the search tree for one of the newly decided machines (#30414):
(1) . .[.]. . HALT
(2) .[1]. . . A
(3) [1]1 . . . B
(4) 1 1 . . . *
(5) [1]1 . . . C
(6) 1 1 . . . * Duplicate of (4)
(7) 1[1]. . . C
(8) 1 1[1]. . C Duplicate of (7)
(9) [0]1 . . . D
Line (8) curtails the search because it matches line (7), shifted right by 1.
My code is not easy to follow, and I don’t think I’m capable of proving anything about it. So I need to come up with a Decider Verification File format that lets others verify these results. If anybody has any ideas, let me know!