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

% D-3.IN     Corrected 1994 April 16
% absorptive law for intersection proved using SU-1 and LA-1A
% Quaife, page 162.

formula_list(sos).
% negation of theorem D-3 
-(all x all y equal(intersection(x,union(x,y)),x)).
end_of_list.


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

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

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

196 [] -subclass(x,y) | equal(intersection(x,y),x).
206 [] subclass(x,union(x,y)).
219 [] -equal(intersection($c2,union($c2,$c1)),$c2).
220 [ur,219,196] -subclass($c2,union($c2,$c1)).
221 [binary,220.1,206.1] $F.

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

clauses generated       1
Kbytes malloced       223
user CPU time           0.33  seconds