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

% D-2A2.IN    Corrected 1994 April 16
% Left Semi-Distributive Inequality for union over intersection.
% Quaife, page 161.

formula_list(sos).
(all x all y all z (subclass(x,y) -> 
                    subclass(union(z,x),union(z,y)))).           % LA-3A'
% Negation of Semi-Distributive Inequality D-2A2
-(all x all y all z subclass(union(x,intersection(y,z)),
                    intersection(union(x,y),union(x,z)))).
end_of_list.


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

Length of proof is 3. Level of proof is 2.

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

208 [] subclass(intersection(x,y),x).
209 [] subclass(intersection(x,y),y).
211 [] -subclass(z,x) | -subclass(z,y) | subclass(z,
          intersection(x,y)).
215 [] -subclass(x,y) | subclass(union(z,x),union(z,y)).
216 [] -subclass(union($c3,intersection($c2,$c1)),
          intersection(union($c3,$c2),union($c3,$c1))).
217 [ur,215,209] subclass(union(x,intersection(y,z)),union(x,z)).
218 [ur,215,208] subclass(union(x,intersection(y,z)),union(x,y)).
245 [ur,218,211,217] 
          subclass(union(x,intersection(y,z)),
          intersection(union(x,y),union(x,z))).
246 [binary,245.1,216.1] $F.

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

clauses generated     112
Kbytes malloced       255
user CPU time           0.33  seconds