Exercise 7.26 [convert-clausal-exercise]

Convert the following set of sentences to clausal form.

S1: $A {\;\;{\Leftrightarrow}\;\;}(C \lor E)$.

S2: $E {:\;{\Rightarrow}:\;}D$.

S3: $B \land F {:\;{\Rightarrow}:\;}\lnot C$.

S4: $E {:\;{\Rightarrow}:\;}C$.

S5: $C {:\;{\Rightarrow}:\;}F$.

S6: $C {:\;{\Rightarrow}:\;}B$

Give a trace of the execution of DPLL on the conjunction of these clauses.