 which forces R to be true. From this process we can recover the assignment (P ← true, Q ← false, R ← true, S ← false) proving that the original formula is satisfiable. A formula may cause the algorithm to branch; the search through a branch reaches a dead end the moment a clause is deemed false—a conflicting clause—and all variations of the assignment that has been partially constructed up to this point can be discarded. To illustrate: