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

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

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


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

Length of proof is 9. Level of proof is 5.

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

2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
21 [] -member(z,intersection(x,y)) | member(z,x).
22 [] -member(z,intersection(x,y)) | member(z,y).
23 [] -member(z,x) | -member(z,y) | member(z,intersection(x,y)).
178 [] -member(x,union(y,z)) | member(x,y) | member(x,z).
179 [] -member(x,y) | member(x,union(y,z)).
180 [] -member(x,z) | member(x,union(y,z)).
201 [] -subclass(intersection(union($c3,$c2),union($c3,$c1)),
          union($c3,intersection($c2,$c1))).
203 [] equal(intersection(x,y),intersection(y,x)).
210 [] equal(union(x,y),union(y,x)).
219 [ur,201,3,demod,210,210,203,203,203] 
          -member(notsub(intersection(union($c1,$c3),union($c2,$c3)),
          union($c3,intersection($c1,$c2))),
          union($c3,intersection($c1,$c2))).
220 [ur,201,2,demod,210,210,203,203,210,210,203] 
          member(notsub(intersection(union($c1,$c3),union($c2,$c3)),
          union($c3,intersection($c1,$c2))),
          intersection(union($c1,$c3),union($c2,$c3))).
221 [ur,219,180] -member(notsub(intersection(union($c1,$c3),
          union($c2,$c3)),union($c3,intersection($c1,$c2))),
          intersection($c1,$c2)).
222 [ur,219,179] -member(notsub(intersection(union($c1,$c3),
          union($c2,$c3)),union($c3,intersection($c1,$c2))),$c3).
223 [ur,220,22] member(notsub(intersection(union($c1,$c3),
          union($c2,$c3)),union($c3,intersection($c1,$c2))),
          union($c2,$c3)).
224 [ur,220,21] member(notsub(intersection(union($c1,$c3),
          union($c2,$c3)),union($c3,intersection($c1,$c2))),
          union($c1,$c3)).
225 [ur,223,178,222] 
          member(notsub(intersection(union($c1,$c3),union($c2,$c3)),
          union($c3,intersection($c1,$c2))),$c2).
226 [ur,225,23,221] -member(notsub(intersection(union($c1,$c3),
          union($c2,$c3)),union($c3,intersection($c1,$c2))),$c1).
228 [ur,226,178,222,demod,210] 
          -member(notsub(intersection(union($c1,$c3),union($c2,$c3)),
          union($c3,intersection($c1,$c2))),union($c1,$c3)).
229 [binary,228.1,224.1] $F.

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

clauses generated     204
Kbytes malloced       255
user CPU time           0.38  seconds