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

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

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


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

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

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

98 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
196 [] subclass(x,union(x,y)).
197 [] subclass(y,union(x,y)).
199 [] subclass(intersection(x,y),y).
200 [] -subclass(x,z) | -subclass(y,z) | subclass(union(x,y),z).
217 [] -subclass(union($c3,intersection($c2,$c1)),union($c3,$c1)).
241 [ur,217,200,196] -subclass(intersection($c2,$c1),union($c3,$c1)).
246 [ur,241,98,197] -subclass(intersection($c2,$c1),$c1).
247 [binary,246.1,199.1] $F.

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

clauses generated      46
Kbytes malloced       287
user CPU time           0.49  seconds