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

% D-0.IN                  Revised 1998 January 3
% Selfdual version of Distributive Law 

formula_list(sos).
% negation of theorem D-0 
-(all x y z subclass(intersection(union(x,y),z),
                     union(x,intersection(y,z)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sat Jan 03 13:04:27 1998

Length of proof is 8. Level of proof is 4.

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

2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
21 [] -member(z,intersection(x,y)) | member(z,x).
22 [] -member(z,intersection(x,y)) | member(z,y).
23 [] -member(z,x) | -member(z,y) | member(z,intersection(x,y)).
178 [] -member(x,union(y,z)) | member(x,y) | member(x,z).
179 [] -member(x,y) | member(x,union(y,z)).
180 [] -member(x,z) | member(x,union(y,z)).
199 [] -subclass(intersection(union($c3,$c2),
          $c1),union($c3,intersection($c2,$c1))).
201 [] equal(intersection(x,y),intersection(y,x)).
217 [ur,199,3,demod,201] 
          -member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),
          union($c3,intersection($c2,$c1))).
218 [ur,199,2,demod,201,201] 
          member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),
          intersection($c1,union($c3,$c2))).
219 [ur,217,180] -member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),intersection($c2,$c1)).
220 [ur,217,179] -member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),$c3).
221 [ur,218,22] member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),union($c3,$c2)).
222 [ur,218,21] member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),$c1).
223 [ur,222,23,219] -member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),$c2).
224 [ur,223,178,220] -member(notsub(intersection($c1,union($c3,$c2)),
          union($c3,intersection($c2,$c1))),union($c3,$c2)).
225 [binary,224.1,221.1] $F.

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

clauses generated     161
Kbytes malloced       255
user CPU time           0.83  seconds