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

% D-6.IN      Corrected 1994 April 16
% Quaife, page 162.

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


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

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

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

99 [] equal(x,x).
211 [] equal(union(x,intersection(complement(x),y)),union(x,y)).
214 [] -equal(union(complement($c2),intersection($c2,$c1)),
          union(complement($c2),$c1)).
215 [] equal(complement(complement(x)),x).
236 [para_into,214.1.2,211.1.2,demod,215] 
          -equal(union(complement($c2),intersection($c2,$c1)),
          union(complement($c2),intersection($c2,$c1))).
237 [binary,236.1,99.1] $F.

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

clauses generated      15
Kbytes malloced       255
user CPU time           0.38  seconds