Plist back_subsume(Topform c, Lindex idx);Look in the index and return the list of clauses subsumed by c.
Topform back_subsume_one(Topform c, Lindex idx);Look in the index for a clause subsumed by c. The first one found is returned. (It is not necessarily the first of the subsumees that was inserted into the index.)
Plist back_unit_del_by_index(Topform unit, Lindex idx);Given a unit clause and a literal index, return the Plist of clauses containing literals that are instances of the negation of the unit clause.
Such clauses can be "back unit deleted".
BOOL eq_removable_literal(Topform c, Literals lit);Can a literal in a clause be removed by resolution with x=x without instantiating any other literal in the clause?
If so, instantiate any inheritable (e.g., answer) attributes with the corresponding substitution.
Topform forward_subsume(Topform d, Lindex idx);
int nonunit_subsumption_tests(void);
void simplify_literals(Topform c);Remove any literals t!=t.
void simplify_literals2(Topform c);1. If there are any literals t=t, the clause becomes true_sym(). 2. Remove any literals t!=t. 3. If there are any literals s!=t, where unify(s,t), without instantiating any other literals, remove the literal.
BOOL subsumes(Topform c, Topform d);This routine checks if Topform c subsumes Topform d. Ordinary unification is used; in particular, symmetry of equality is not built in.
BOOL subsumes_bt(Topform c, Topform d);This routine checks if Topform c subsumes Topform d. Backtrack unification is used; in particular, AC and commutative/symmetric matching are applied where appropriate.
Topform try_unit_conflict(Topform a, Topform b);
void unit_conflict_by_index(Topform c, Lindex idx, void (*empty_proc) (Topform));Look in idx for unit conflicts
void unit_delete(Topform c, Lindex idx);Given a clause and a literal index, remove the literals that can be removed by "unit deletion" with units in the index. Update the clause's justification for each removed literal.