Find more restrictive strategies in Boolean-ring based methods for resolution-like first-order theorem proving.

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Since the work of Hsiang [Zhang, 1991], several Boolean-ring based methods have been proposed for resolution-like first-order theorem proving. In [Zhang, 1991], superposition rules were defined using multiple overlaps (requiring unifications of products of atoms). It is unknown whether single overlaps (requiring only unifications of atoms) are sufficient in these inference rules. Also, it is not known if unifications of maximal atoms (under a given term ordering) suffice. (The same problem for Hsiang's method was solved positively in [Zhang, 1991].) In other respects, too, the set of inference rules in [Zhang, 1991] may be larger than necessary and the simplification weaker than possible.