oriented_eq(<A HREF="term.html">Term</A> atom);
</B></PRE>This routine marks an atom as an oriented equality.
<A NAME="mark_renamable_flip"></A><HR><PRE><B>void mark_renamable_flip(<A HREF="term.html">Term</A> atom);
</B></PRE>This routine marks an atom as "renamable_flip".
<A NAME="new_constant"></A><HR><PRE><B>Topform new_constant(Topform c, int new_sn);
</B></PRE>If the Topform is a positive equality unit a(x) = b(y) with two variables
in which one variable occurs in each side, infer a clause
a(x) = c wi