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

% D-4COR1.IN      Corrected 1994 April 16
% Corollary of absorptive law for union
% Quaife, page 162.

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


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

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

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

186 [] equal(union(x,y),union(y,x)).
187 [] equal(union(x,union(y,z)),union(y,union(x,z))).
220 [] equal(union(x,intersection(x,y)),x).
221 [] -equal(union($c3,union($c2,intersection($c3,$c1))),
          union($c3,$c2)).
224 [para_into,221.1.1,187.1.2] 
          -equal(union($c2,union($c3,intersection($c3,$c1))),
          union($c3,$c2)).
237 [para_into,224.1.1.2,220.1.1] 
          -equal(union($c2,$c3),union($c3,$c2)).
238 [binary,237.1,186.1] $F.

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

clauses generated     125
Kbytes malloced       255
user CPU time           0.32  seconds