----- SUMMARY FOR THEOREM D-5' IN DIRECTORY Q:\D\1 -----

% D-5'.IN              1995 August 24
% Variant of Theorem D-5
% Quaife, page 162.

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


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Aug 24 22:56:32 1997

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

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

167 [] equal(intersection(x,y),intersection(y,x)).
221 [] equal(union(x,intersection(complement(x),y)),union(x,y)).
222 [] -equal(union($c2,intersection($c1,complement($c2))),
          union($c2,$c1)).
225 [para_into,222.1.1.2,167.1.2] 
          -equal(union($c2,intersection(complement($c2),$c1)),
          union($c2,$c1)).
226 [binary,225.1,221.1] $F.

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

clauses generated       9
Kbytes malloced       255
user CPU time           0.44  seconds