{\leftarrow}y,\overline{y};\;
w {\leftarrow}y,\overline{y};\;
y {\leftarrow}u,w;\; \nonumber \\
\label{eq:red:second}
&&\hphantom{\{}
\overline{y} {\leftarrow}u,w;\;
v {\leftarrow}y;\;
v {\leftarrow}\overline{y}
\mid y\in Y\}\cup{}\\
&&
\{  z \lor \overline{z} {\leftarrow}v;\;
u {\leftarrow}z,{{\mathit not}}\ w;\;
u {\leftarrow}\overline{z},{{\mathit not}}\ w;\;
v {\leftarrow}z;\;
v {\leftarrow}\overline{z};\; \nonumber \\
&&\hphantom{\{}
\label{eq:red:third}
z {\leftarrow}w;\;
\overline{z} {\leftarrow}w;\;
z {\leftarrow}u;\;
\overline{z} {\leftarrow}u;\;
w \vee u \leftarrow z, \overline{z}
\mid z\in Z\}\cup{}\\
\label{eq:red:fourth}
&& \{ w \vee u {\leftarrow}l_{i,1},\ldots,l_{i,m_i} \mid 1\leq i \leq  n\} \\
\label{eq:red:fifth}
&& \{
  v {\leftarrow}w;\;
  v {\leftarrow}u;\;
  v {\leftarrow}{{\mathit not}}\ u\}.\end{aligned}$$

The program above contains atoms associated with literals in $\Phi$ and three auxiliary atoms $u,v,w$. Intuitively, truth values for variables in $X$ are guessed by rules in (\[eq:red:first\]), and truth values for variables in $Y \cup Z$ are guessed by rules in (\[eq:red:second\])–(\[eq:red:third\]) provided that $v$ is true. Moreover, rules in (\[eq:red:first\])–(\[eq:red:second\]) derive all atoms in $X \cup \overline{X} \cup Y \cup \overline{Y} \cup \{u,w\}$ whenever both $u$ and $w$ are true, or in case an inconsistent assignment for some propositional variable in $X \cup Y$ is forced by the addition of a set of facts to the program. On the other hand, all atoms associated with variables $Z$ are inferred by rules in (\[eq:red:third\]) if one of $u$ 