  We will find a lower bound on the recognition complexity of the theories that
are nontrivial relative to some equivalence relation (this relation may be
equality), namely, each of these theories is consistent with the formula, whose
sense is that there exist two non-equivalent elements. However, at first, we
will obtain a lower bound on the computational complexity for the first-order
theory of Boolean algebra that has only two elements. For this purpose, we will
code the long-continued deterministic Turing machine computations by the
relatively short-length quantified Boolean formulae; the modified Stockmeyer
and Meyer method will appreciably be used for this simulation. Then, we will
transform the modeling formulae of the theory of this Boolean algebra to the
simulation ones of the first-order theory of the only equivalence relation in
polynomial time. Since the computational complexity of these theories is not
polynomial, we obtain that the class $\mathbf{P}$ is a proper subclass of
$\mathbf{PSPACE}$ (Polynomial Time is a proper subset of Polynomial Space).
  Keywords: Computational complexity, the theory of equality, the coding of
computations, simulation by means formulae, polynomial time, polynomial space,
lower complexity bound
