In his regular column in the AAR Newsletter, Larry Wos typically posed challenges to the automated reasoning community. Some of these challenges concern general research objectives, but several of them concern specific problems relevant to his own experience and attempts to solve especially difficult problems, including open questions, with an automated theorem prover. This note honors Larry’s memory by working through a solution to one of these challenges.
Larry also mentions an interest in having derivations of the goal clauses that are equality ordered exactly as given in the problem description. Comments about this aspect of the challenge are included at the end of this article.