----- SUMMARY FOR THEOREM D-SU2 IN DIRECTORY Q:\D\1 -----

% D-SU2.IN               1998 January 3
% Theorem suggested by examining output of ALL.CLS
% This theorem subsumes others.

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


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Jan 03 16:24:40 1998

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

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

198 [] subclass(intersection(x,y),x).
202 [] -subclass(x,y) | subclass(union(x,z),union(y,z)).
217 [] -subclass(union(intersection($c3,$c2),$c1),union($c3,$c1)).
241 [ur,217,202] -subclass(intersection($c3,$c2),$c3).
242 [binary,241.1,198.1] $F.

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

clauses generated       1
Kbytes malloced       287
user CPU time           0.55  seconds