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.