Exercise 7.25 [convert-clausal-exercise]

Convert the following set of sentences to clausal form.

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

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

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

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

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

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

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