English: Two example runs of the Davis-Putnam procedure.

Left: The formula ${\displaystyle (a\vee b\vee c)\wedge (b\vee \mathrm{\neg }c\vee \mathrm{\neg }f)\wedge (\mathrm{\neg }b\vee e)}$ is satisfiable: starting from the given formula (top row), resolving each possible clause pair on the variable ${\displaystyle b}$ yields the middle row, then resolving each pair on ${\displaystyle c}$ yields the bottom row ${\displaystyle a\vee e\vee \mathrm{\neg }f}$. Since no further resolution steps are possible, the algorithm stops; since the empty clause couldn't be derived, the result is "satisfiable". In fact, instantiating e.g. ${\displaystyle a=b=e=\mathit{\text{𝑡𝑟𝑢𝑒}}}$ will make the original formula ${\displaystyle \mathit{\text{𝑡𝑟𝑢𝑒}}}$.

Right: The formula ${\displaystyle (a\vee b)\wedge (a\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }a\vee c)\wedge (\mathrm{\neg }a\vee \mathrm{\neg }c)}$ is unsatisfiable: starting from the given formula (top row), resolving all pairs on ${\displaystyle b}$, then on ${\displaystyle a}$, then on ${\displaystyle c}$ yields the 2nd, 3rd, and 4th row from above, respectively. Since the latter is the empty clause, the algorithm halts with result "unsatisfiable". In fact, each row is a consequence of the row above it, and the bottom row denotes ${\displaystyle \mathit{\text{𝑓𝑎𝑙𝑠𝑒}}}$, which certainly cannot be satisfied.