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

% D-4.IN      Corrected 1995 August 23
% Absorptive law for union
% Quaife, page 162.

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


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

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

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

7 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
97 [] subclass(x,x).
206 [] subclass(x,union(x,y)).
208 [] subclass(intersection(x,y),x).
210 [] -subclass(x,z) | -subclass(y,z) | subclass(union(x,y),z).
220 [] -equal(union($c2,intersection($c2,$c1)),$c2).
221 [ur,220,7,206] -subclass(union($c2,intersection($c2,$c1)),$c2).
222 [ur,221,210,208] -subclass($c2,$c2).
223 [binary,222.1,97.1] $F.

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

clauses generated       5
Kbytes malloced       223
user CPU time           0.38  seconds