  We study the termination of sole combinatory calculus, which consists of only
one combinator. Specifically, the termination for non-erasing combinators is
disproven by finding a desirable tree automaton with a SAT solver as done for
term rewriting systems by Endrullis and Zantema. We improved their technique to
apply to non-erasing sole combinatory calculus, in which it suffices to search
for tree automata with a final sink state. Our method succeeds in disproving
the termination of 8 combinators, whose termination has been an open problem.
