----- SUMMARY FOR THEOREM D-2B1 IN DIRECTORY Q:\D\1 -----

% D-2B1.IN      Corrected 1994 April 16
% half of right distributive law for union over intersection
% Quaife, page 161.

formula_list(sos).
% negation of theorem D-2B1
-(all x all y all z subclass(intersection(union(x,z),union(y,z)),
                    union(intersection(x,y),z))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Jul 12 03:54:17 1997

Length of proof is 1. Level of proof is 1.

---------------- PROOF ----------------

6 [] -equal(x,y) | subclass(y,x).
201 [] equal(union(x,intersection(y,z)),intersection(union(x,y),
          union(x,z))).
202 [] -subclass(intersection(union($c3,$c1),union($c2,$c1)),
          union(intersection($c3,$c2),$c1)).
204 [] equal(intersection(x,y),intersection(y,x)).
211 [] equal(union(x,y),union(y,x)).
218 [ur,202,6,demod,204,211,211,211,204] 
          -equal(union($c1,intersection($c2,$c3)),
          intersection(union($c1,$c2),union($c1,$c3))).
219 [binary,218.1,201.1] $F.

------------ end of proof -------------

clauses generated      18
Kbytes malloced       255
user CPU time           0.28  seconds