stification for the XX rule,
which removes literals that are instances of x!=x.
<A NAME="xxres_just"></A><HR><PRE><B>Just xxres_just(Topform c, int lit);
</B></PRE>This routine builds and returns a justification list for resolution with x=x.
<A NAME="zap_just"></A><HR><PRE><B>void zap_just(Just just);
</B></PRE>This routine frees a justification list, including any sublists.
<HR><A NAME=defns></A><H2>Public Definitions in File just.h</H2>
<PRE>
typedef enum {
  INPUT_JUST,         /* Primary                