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

% D-2B2.IN    Corrected 1994 April 16

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


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Jul 12 03:54:21 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)).
216 [] -subclass(x,y) | subclass(union(x,z),union(y,z)).
217 [] -subclass(union(intersection($c3,$c2),
          $c1),intersection(union($c3,$c1),union($c2,$c1))).
218 [ur,216,209] subclass(union(intersection(x,y),z),union(y,z)).
219 [ur,216,208] subclass(union(intersection(x,y),z),union(x,z)).
246 [ur,219,211,218] 
          subclass(union(intersection(x,y),
          z),intersection(union(x,z),union(y,z))).
247 [binary,246.1,217.1] $F.

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

clauses generated     112
Kbytes malloced       255
user CPU time           0.33  seconds