Given a set of clauses
*F _{1} &and F_{2} &and ... &and F_{n} &and ¬ G*,
each clause restricts the portion of the space in which an
interpretation satisfying the formula could lie.

A resolution step defines a new (perhaps
better described) space in which any solution must lie; if the
space is empty (*□*), the formula must be unsatisfiable.

Resolution step: *(P &or &alpha) &and (¬ P &or &beta) &rarr
(&alpha &or &beta)*