I’m working on a Closed-Tape-Language based decider and it found a proof for Skelet’s machine #32.
After some tweaking of parameters to get a proof that is vaguely human readable I managed to produce a proof file that can be verified with SymbolicTM by @Frans_Faase.
Or one can check by hand, as after removing unnecessary configurations only 10 are left.