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

% D-7.IN     Corrected 1994 April 16

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


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

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

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

171 [] equal(intersection(V,x),x).
181 [] equal(union(x,y),union(y,x)).
206 [] equal(intersection(union(x,y),z),union(intersection(x,z),
          intersection(y,z))).
216 [] -equal(union(intersection(complement($c2),
          $c1),intersection($c2,$c1)),$c1).
221 [] equal(union(x,complement(x)),V).
227 [para_into,216.1.1,206.1.2] 
          -equal(intersection(union(complement($c2),$c2),$c1),$c1).
229 [para_into,227.1.1.1,181.1.2,demod,221] 
          -equal(intersection(V,$c1),$c1).
230 [binary,229.1,171.1] $F.

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

clauses generated      29
Kbytes malloced       255
user CPU time           0.33  seconds