Consider the propositional formula . We transform this formula using the Tseitin transformation, introducing definitions and . The resulting CNF formula contains 7 clauses; select below the clauses that appear in the CNF formula after Tseitin transformation.

Note that for negation no new definition is introduced. 

Given the following formula

(¬x ∨ z) ∧ (x ∨ ¬y) ∧ (¬x ∨¬y ∨ z) ∧ (y ∨¬z)

Prove with resolution that . 

Given the formula 

 φ = (a ∨ f) ∧ (d ∨ ¬e) ∧ (a ∨ b ∨ ¬d ∨ e) ∧ (d) ∧ (¬a ∨ ¬c) ∧ (b ∨ ¬d ∨ e) ∧ (¬b).

Which of the following clauses can be derived from φ with one resolution step?