Davis-Putnam empty cls. vs no cls.

Question

Lets have

$$ S = \{qr\bar t, q\bar r, pr \bar s, t, \bar pqr, r\bar u, q\bar s t, r \bar tu, \bar qr, p\bar s \bar t\}$$

Unit-literal rule ( t )

$$ S_2 = \{q\bar r, pr \bar s, \bar pqr, r\bar u, ru, \bar qr, p\bar s\}$$

Pure-literal rule ( $ \bar s$ )

$$ S_3 = \{q\bar r, \bar pqr, r\bar u, ru, \bar qr\}$$

Pure-literal rule ( $ \bar p$ )

$$ S_4 = \{q\bar r, r\bar u, ru, \bar qr\}$$

Eliminate a variable by resolution for collision literal q

$$ Res(\{q\bar r\}, \{\bar qr\}) = \{r\bar r\} = \emptyset $$

$$ S_5 = \{r\bar u, ru\}$$

Pure-literal rule ( $r$ )

Do I get $$S_6 = \emptyset \;\;\text{satisfiable}$$ or $$S_6 = \{\square\} \;\;\text{not satisfiable}$$

How do I prove that $S \approx S_6$ ? (in case of $S_6$ not satisfiable, does it even make sense?)

Answer 1

Pure-literal rule: If there is a pure literal l, delete all clauses containing l.

($S_5$) So by deleting all clauses that contain $r$ I get $\emptyset$ not $\{\square\}$ therefore $$S_6 = \emptyset$$

Wolframalpha agrees.

---

Unit-literal rule: If there is a unit clause {l}, delete all clauses containing l and delete all occurrences of lc from all other clauses.

For clarification (as I understand) you can get $\{\square\}$ by having $$S = \{r, \bar r\}$$ and applying Unit-literal rule ( $r$ ) you get $$S^{'} = \{\emptyset, \{\}\}$$ which ultimately is $$S^{'} = \{\square\}$$

Wolframalpha agrees again.