2. (This exercise is a variation of Exercise 4.5 in Chapter 4 of the textbook) Consider the set of formulas S = { p, p ((q r) (q r)), p ((s t) (s t)), s q, r t, t s } (a) Transform S into a set of formulas in CNF, S'

(b) Transform S' into a set of formulas in clausal form, S''

c) Prove using resolution that S'' is unsatisfiable.

3. (Exercise 4.4 in Chapter 4 of the textbook) Given the set of clauses {pqr, pr, qr, r}, construct two refutations (i.e. demonstrate using the resolution procedure that the set of clauses is unsatisfiable): (a) one by resolving the literals in the order {p, q, r} (b) and the other in the order {r, q, p}