Transform the set of causes of the given formula are below:
$\overline{x}\lor y.....(1)$
$\overline{y}\lor x.....(2)$
$\overline{z}\lor w.....(3)$
$\overline{w}\lor z.....(4)$
$\overline{s}\lor \overline{t}.....(5)$
$s\lor t.....(6)$
$\overline{x}\lor \overline{z}\lor\overline{s}.....(7)$
$\overline{x}\lor z\lor s.....(8)$
$\overline{z}\lor x\lor s.....(9)$
$\overline{s}\lor x\lor z.....(10)$
$\overline{y}\lor \overline{w}\lor\overline{t}.....(11)$
$\overline{y}\lor w\lor t.....(12)$
$\overline{w}\lor y\lor t.....(13)$
$\overline{t}\lor y\lor w.....(14)$
I need to refute using resolution.
My try:
Resolution of (1) and (9) implies, $\overline{z}\lor y\lor s.....(15)$
Resolution of (2) and (8) implies, $\overline{y}\lor z\lor s.....(16)$
Resolution of (3) and (10) implies, $\overline{s}\lor w\lor x.....(17)$
Resolution of (4) and (7) implies, $\overline{w}\lor \overline{x}\lor\overline{s}.....(18)$
Resolution of (5) and (12) implies, $\overline{s}\lor \overline{y}\lor w.....(19)$
Resolution of (6) and (11) implies, $\overline{y}\lor s\lor \overline{w}.....(20)$
Resolution of (15) and (16) implies, $\overline{z}\lor z\lor s.....(21)$
Resolution of (17) and (18) implies, $\overline{s}\lor \overline {x}\lor x.....(22)$
Resolution of (19) and (14) implies, $\overline{s}\lor \overline {t}\lor w.....(23)$
Resolution of (13) and (20) implies, $s \lor \overline {w} \lor t.....(24)$
My question is how to proceed from here? How to get empty set, $\Phi$, which is unsatisfiable? Is there any easy approach exists to reach $\Phi$?
With these, the best thing to do is to try and decrease the number of variables that you are working with. Fortunately, you can do that here quite nicely. You can use statements 1 through 6 to gradually replace all $x$'s with $y$'s, all $z$'s with $w$'s, and all $s$'s with $t$'s in statements 7 through 10, so that together with statements 11 through 14 you end up with $8$ statements that involve $y$, $w$, and $t$ only. And from there, it's only a few more steps to the contradiction.
Replace all $x$'s with $y$'s:
(15) $\overline{y}\lor \overline{z}\lor\overline{s}.....(2,7)$
(16) $\overline{y}\lor z\lor s.....(2,8)$
(17) $\overline{z}\lor y\lor s.....(1,9)$
(18) $\overline{s}\lor y\lor z.....(1,10)$
Replace all $z$'s with $w$'s
(19) $\overline{y}\lor \overline{w}\lor\overline{s}.....(4,15)$
(20) $\overline{y}\lor w\lor s.....(3,16)$
(21) $\overline{w}\lor y\lor s.....(4,17)$
(22) $\overline{s}\lor y\lor w.....(3,18)$
Replace all $s$'s with $t$'s
(23) $\overline{y}\lor \overline{w}\lor t.....(6,19)$
(24) $\overline{y}\lor w\lor \overline{t}.....(5,20)$
(25) $\overline{w}\lor y\lor \overline{t}.....(5,21)$
(26) $t \lor y\lor w.....(6,22)$
OK, and so now combine these with 11 through 14:
(27) $\overline{y}\lor \overline{w}.....(11,23)$
(28) $\overline{y}\lor w.....(12,24)$
(29) $\overline{w}\lor y.....(13,25)$
(30) $y\lor w.....(14,26)$
Almost there:
(31) $\overline{y}.....(27,28)$
(32) $y .... (29,30)$
(33) $\bot .... (31,32)$