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

% D-4COR2.IN               1997 January 3
% Corollary 2 of absorptive law for union
% Quaife, page 162.

formula_list(sos).
% negation of Corollary D-4COR2
-(all x y z equal(union(x,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 17:06:48 1998

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

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

186 [] equal(union(x,y),union(y,x)).
221 [] equal(union(x,union(y,intersection(x,z))),union(x,y)).
222 [] -equal(union($c3,union(intersection($c3,$c2),$c1)),
          union($c3,$c1)).
224 [para_into,222.1.1.2,186.1.2] 
          -equal(union($c3,union($c1,intersection($c3,$c2))),
          union($c3,$c1)).
225 [binary,224.1,221.1] $F.

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

clauses generated      18
Kbytes malloced       255
user CPU time           0.27  seconds