----- SUMMARY FOR THEOREM D-2B IN DIRECTORY Q:\D\1 -----

% D-2B.IN            1998 January 3
% right distributive law for union over intersection
% Quaife, page 161.

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


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Jan 03 15:55:08 1998

Length of proof is 3. Level of proof is 3.

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

191 [] equal(union(x,y),union(y,x)).
220 [] equal(union(x,intersection(y,z)),intersection(union(x,y),
          union(x,z))).
221 [] -equal(union(intersection($c3,$c2),
          $c1),intersection(union($c3,$c1),union($c2,$c1))).
249 [para_into,221.1.2.1,191.1.2,flip.1] 
          -equal(intersection(union($c1,$c3),union($c2,$c1)),
          union(intersection($c3,$c2),$c1)).
259 [para_into,249.1.1.2,191.1.2] 
          -equal(intersection(union($c1,$c3),union($c1,$c2)),
          union(intersection($c3,$c2),$c1)).
271 [para_into,259.1.1,220.1.2,flip.1] 
          -equal(union(intersection($c3,$c2),
          $c1),union($c1,intersection($c3,$c2))).
272 [binary,271.1,191.1] $F.

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

clauses generated     438
Kbytes malloced       319
user CPU time           0.49  seconds