We will show \(\Pi _{\mathit {3}}^{\mathit {P}}\) -hardness via reduction from
3-QBF solving. We will construct two ELPs \(\Pi _1\)  and \(\Pi _2\)  such that they
are uniformly equivalent iff a given 3-QBF is unsatisfiable. To this end, we
will make use of the reduction from 3-QBF solving to CWV existence offered in
[1]}, on which our reduction is based. Let
\(\exists {\mathbf {X}}\forall {\mathbf {Y}}\exists {\mathbf {Z}}\; \Psi ({\mathbf {X}}, {\mathbf {Y}}, {\mathbf {Z}})\) 
be a 3-QBF formula in conjunctive normal form, where each clause has the form
\(\ell _1 \vee \ell _2 \vee \ell _3\) , where each \(\ell \)  is a literal over the
variables in \({\mathbf {X}}\cup {\mathbf {Y}}\cup {\mathbf {Z}}\) . In [1]}, it is
assumed w.l.o.g. that the 3-QBF evaluates to true whenever all variables in
\({\mathbf {Y}}\)  are replaced by \(\top \) . This does not change the hardness of the
problem, and we make use of the same assumption. For a 3-QBF formula as above,
we construct the ELP \(\Pi _1 = (\mathcal {A}, \mathcal {E}, \mathcal {R}_1)\)  over the atoms \(\mathcal {A}=\lbrace  w, \overline{w} \mid w \in {\mathbf {X}}\cup {\mathbf {Y}}\cup {\mathbf {Z}}\rbrace  \cup \lbrace {\mathit {false}}, {\mathit {sat}} \rbrace \)  using the well-known technique of
saturation [3]}. \(\Pi _1\)  contains the following set of rules,
where \(\ell ^*\)  converts a literal \(a\)  into atom \(\overline{a}\)  and literal
\(\lnot a\)  into atom \(a\) :
