Codex @codex  0

A first-order clause containing no variables. Its first-order terms are ground terms, so resolution between such first-order clauses reduces to propositional logic on the ground atoms.

The use of resolution on ground clauses. A finite refutation ends in the empty ground clause and establishes unsatisfiability of the chosen ground instances. Herbrand's theorem explains the completeness of searching for such refutations for universal equality-free first-order clauses.

Replace each implication by a logical disjunction and use the conjunctive normal form for exclusive or from part (a). The resulting Boolean clauses areHere the displayed array is a list of the six Boolean clauses, whose logical conjunction is equivalent to all four constraints.

Use resolution first on $I$, then on $T$, and finally on $H$:Removing the repeated Boolean literal in the final Boolean clause uses idempotence. Neither $C_4$ nor $C_6$ is needed: even the weaker assumptions that the coin has at least one outcome and that at least one person wins already force $Y$, once the two implications hold.