Assume that R-Rule 2 is not applicable to \(F\) , then \(F\)  has no pure literals,
i.e., literals whose negation does not appear in \(F\) . Thus, all variables are
\(2^+\) -variables. Under this condition, we can process 2-variables based on
the resolution principle [1]}, whose correctness can be easily verified.
