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

% D-1B.IN            1998 January 3
% Proof of Distributive Law D-1B using D-1A
% Quaife, page 161.

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


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

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

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

167 [] equal(intersection(x,y),intersection(y,x)).
218 [] equal(intersection(x,union(y,z)),union(intersection(x,y),
          intersection(x,z))).
219 [] -equal(intersection(union($c3,$c2),
          $c1),union(intersection($c3,$c1),intersection($c2,$c1))).
222 [para_into,219.1.1,167.1.2] 
          -equal(intersection($c1,union($c3,$c2)),
          union(intersection($c3,$c1),intersection($c2,$c1))).
230 [para_into,222.1.2.1,167.1.2] 
          -equal(intersection($c1,union($c3,$c2)),
          union(intersection($c1,$c3),intersection($c2,$c1))).
242 [para_into,230.1.2.2,167.1.2] 
          -equal(intersection($c1,union($c3,$c2)),
          union(intersection($c1,$c3),intersection($c1,$c2))).
243 [binary,242.1,218.1] $F.

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

clauses generated     293
Kbytes malloced       287
user CPU time           0.50  seconds