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

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

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


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

Length of proof is 7. Level of proof is 7.

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

191 [] equal(union(x,y),union(y,x)).
202 [] -subclass(x,y) | equal(union(x,y),y).
212 [] subclass(intersection(x,y),x).
213 [] subclass(intersection(x,y),y).
218 [] equal(intersection(x,union(y,z)),union(intersection(x,y),
          intersection(x,z))).
219 [] equal(intersection(union(x,y),z),union(intersection(x,z),
          intersection(y,z))).
220 [] -equal(union($c3,intersection($c2,$c1)),
          intersection(union($c3,$c2),union($c3,$c1))).
227 [] equal(intersection(x,x),x).
237 [] equal(union(union(x,y),z),union(x,union(y,z))).
245 [para_into,220.1.2,218.1.1,flip.1] 
          -equal(union(intersection(union($c3,$c2),
          $c3),intersection(union($c3,$c2),$c1)),
          union($c3,intersection($c2,$c1))).
246 [para_into,245.1.1.1.1,191.1.2] 
          -equal(union(intersection(union($c2,$c3),
          $c3),intersection(union($c3,$c2),$c1)),
          union($c3,intersection($c2,$c1))).
254 [para_into,246.1.1,191.1.2] 
          -equal(union(intersection(union($c3,$c2),
          $c1),intersection(union($c2,$c3),$c3)),
          union($c3,intersection($c2,$c1))).
277 [para_into,254.1.1.2,219.1.1,demod,227] 
          -equal(union(intersection(union($c3,$c2),
          $c1),union(intersection($c2,$c3),$c3)),
          union($c3,intersection($c2,$c1))).
314 [para_into,277.1.1.2,202.2.1,unit_del,213] 
          -equal(union(intersection(union($c3,$c2),
          $c1),$c3),union($c3,intersection($c2,$c1))).
317 [para_into,314.1.1.1.1,191.1.2] 
          -equal(union(intersection(union($c2,$c3),
          $c1),$c3),union($c3,intersection($c2,$c1))).
322 [para_into,317.1.1.1,219.1.1,demod,237] 
          -equal(union(intersection($c2,$c1),
          union(intersection($c3,$c1),$c3)),
          union($c3,intersection($c2,$c1))).
354 [para_into,322.1.1.2,202.2.1,unit_del,191,212] $F.

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

clauses generated    1933
Kbytes malloced       351
user CPU time           1.21  seconds