\section{Constraint Simplification}
\label{sec:simplify}

In this section we hint on how to bring clauses stemming from
complementation into their final format by simplifying, whenever
possible, the disequation introduced by the $\mnota\Imp$ rule. This
entails the following:
\begin{itemize}
\item Solving  disequations existential variable-ground term by
  computing the complement of the latter.
\item Removing unsatisfiable variable-variable disequations.
\end{itemize}

In a final pass we will also:
\begin{itemize}
\item Remove irrelevant occurrences of $\top$'.
\item Remove failing clauses, \ie with $\perp$ in the body.
\item Hide the residual augmentation in the final negative clause.
\end{itemize}



\begin{Example}
\label{ex:closedfinal} 
Continuing Example \ref{ex:closed} and \ref{ex:closedatensor}...
\end{Example}