@@ -54,18 +54,18 @@ The general case is dealt with in Section~\ref{ssec:ent-all};

We show how to derive the coNP upper bound from the aforementioned decision procedure. We first observe the following facts.

\begin{enumerate}

\item The original entailment problem is valid iff all of at most exponentially many

\emph{ordered entailment problems} are valid, since there are exponentially many total preorders.

\itemFor each ordered entailment problem, it is valid iff all of at most exponentially many \emph{special ordered entailment problems}, where the consequent contains only one spatial atom, are valid.

\emph{ordered entailment problems} are valid, since there are at most exponentially many total preorders.

\itemEach ordered entailment problem is valid iff all of at most exponentially many \emph{special ordered entailment problems}, where the consequent contains only one spatial atom, are valid.

%\item The original entailment problem is invalid iff there is an invalid special ordered entailment problem instance.

\item The special ordered entailment problem is in coNP.

\end{enumerate}

Therefore, to show that $\varphi\models\psi$ is not valid, we

\begin{itemize}

\item first guess a total preorder and obtain an ordered entailment problem,

\item then guess for the ordered entailment problem one special ordered entailment problem where the consequent contains only one spatial atom,

\itemand finally guess and verify in polynomial time a polynomial-size witness for the invalidity of the special ordered entailment problem.

\item first guess a total preorder and obtain an ordered entailment problem (of polynomial size),

\item then guess for the ordered entailment problem one special ordered entailment problem (of polynomial size) where the consequent contains only one spatial atom,

\item finally guess and verify in polynomial time a polynomial-size witness for the invalidity of the special ordered entailment problem.

\end{itemize}

The above procedure runs in nondeterministic polynomial time, thus showing the invalidity of the entailment problem is in NP. From this, we conclude that the entailment problem of {\slah} is in coNP.

The above procedure runs in nondeterministic polynomial time, thus showing the invalidity of the entailment problem is in NP. From this, we deduce that the entailment problem of {\slah} is in coNP.

%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,

%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,