The Busy Beaver Challenge

bbchallenge.org

It looks like Skelet 17 is not CTL-able, then. Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.