Q:\D\1\D-3COR2.TXT          1998 January 3

We completely revamped the D group, related to the distributive law.
Previously we had only proven certain theorems with a stripped down
input file, and for this reason they had not been placed in the main
directory, but only in the D\1\BINARY subdirectory.  New proofs were
obtained for Theorems D-1B, D-2A and D-2B.

Once the version D-1A of the distributive law has been proved, it is
very easy to obtain the variant D-1B.  The ALL.CLS file for the D
group shrank dramatically when we added the variant D-1B of the
distributive law.  The same happened when we added D-2A and D-2B.

When we examined the output file with these changes made we found
it had eliminated all but two theorems involving subclass(*,*).
These two theorems are subsumed by new theorems D-SU1 and D-SU2
which were added to the D group.  

After all these changes were made, we found that all but one single
clause from the D\1\BINARY group were subsumed by those in the main
D\1 group.  Using answer literals, that last one was traced to
Quaife's corollary D-3-COR.  But the strange thing is that we did
have this corollary already in the main directory.  This involves a
double application of intersection to a union.  In simplifying this,
several demodulators are used, and the result appears to depend on
the order in which they are applied. We were therefore left with one
complicated orphan clause from D\1\BINARY which did not get subsumed.
We obtained a new proof of this orphan clause, which we are calling
Corollary D-3COR2.  To accommodate this new theorem, the old D-3-COR
was renamed D-3COR1.  The other strange thing is that we got a new
lrpo-dependent demodulator for commutativity of unions, ostensibly
related to D-2B.  We did not keep this, as it seems to be subsumed
by the more general lrpo-dependent demodulator U-2.  But for some
reason it technically was not subsumed.