----- SUMMARY FOR THEOREM AC-Z-COR IN DIRECTORY Q:\choice -----

% AC-Z-COR.IN                 2001 May 7
% Reformulation of AC-Z without set-variables.

formula_list(sos).
% negation of Corollary AC-Z-COR
-(AxCh -> (all x (subclass(cart(x,x),union(Id,DISJOINT)) ->
 (member(0,x) | subclass(image(IMAGE(id(image(CHOICE,x))),x),R(SINGLETON)))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon May 07 21:21:09 2001

Length of proof is 12. Level of proof is 4.

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

2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
86 [] -subclass(x,0) | equal(x,0).
142 [] -equal(intersection(x,y),x) | subclass(x,y).
505 [] -member(x,image(y,z)) | member(dom(y,z,x),z).
518 [] -member(x,image(y,z)) | member(pair(dom(y,z,x),x),y).
540 [] -member(x,image(y,z)) | member(dom(y,z,x),D(y)).
599 [] -member(x,y) | -member(y,z) | member(x,U(z)).
1359 [] -member(x,V) | member(singleton(x),R(SINGLETON)).
2901 [] -member(pair(x,y),IMAGE(id(z))) | equal(intersection(x,z),y).
3163 [] -AxCh | -member(x,V) | equal(0,x)
           | member(apply(CHOICE,x),x).
3167 [] -AxCh | -member(x,y) | -subclass(cart(y,y),union(Id,DISJOINT))
           | equal(x,0) | equal(intersection(x,image(CHOICE,y)),
          singleton(apply(CHOICE,x))).
3168 [] AxCh.
3169 [] subclass(cart($c1,$c1),union(Id,DISJOINT)).
3170 [] -member(0,$c1).
3171 [] -subclass(image(IMAGE(id(image(CHOICE,$c1))),
          $c1),R(SINGLETON)).
3194 [] equal(intersection(x,0),0).
3323 [] equal(U(V),V).
4116 [] equal(D(IMAGE(id(x))),V).
4220 [] equal(notsub(image(IMAGE(id(image(CHOICE,x))),
          x),R(SINGLETON)),n$(x)).
4221 [] equal(dom(IMAGE(id(image(CHOICE,x))),x,n$(x)),d$(x)).
4225 [para_into,3170.1.1,86.2.2] -member(x,$c1) | -subclass(x,0).
4228 [binary,3171.1,3.2,demod,4220] -member(n$($c1),R(SINGLETON)).
4229 [binary,3171.1,2.2,demod,4220] 
          member(n$($c1),image(IMAGE(id(image(CHOICE,$c1))),$c1)).
4236 [binary,4225.2,142.2,demod,3194] -member(x,$c1) | -equal(0,x).
4240 [binary,4229.1,540.1,demod,4221,4116] member(d$($c1),V).
4241 [binary,4229.1,518.1,demod,4221] 
          member(pair(d$($c1),n$($c1)),IMAGE(id(image(CHOICE,$c1)))).
4242 [binary,4229.1,505.1,demod,4221] member(d$($c1),$c1).
4254 [binary,4240.1,599.2,demod,3323] 
          -member(x,d$($c1)) | member(x,V).
4259,4258 [binary,4241.1,2901.1] 
          equal(intersection(d$($c1),image(CHOICE,$c1)),n$($c1)).
4265 [binary,4242.1,4236.1,flip.1] -equal(d$($c1),0).
4267 [binary,4242.1,3167.2,demod,4259,unit_del,3168,3169,4265,flip.1] 
          equal(singleton(apply(CHOICE,d$($c1))),n$($c1)).
4291 [binary,4254.1,3163.4,unit_del,3168,4240,4265] 
          member(apply(CHOICE,d$($c1)),V).
4323 [para_from,4267.1.1,1359.2.1,unit_del,4291,4228] $F.

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

clauses generated   43774
Kbytes malloced      3129
user CPU time           7.97  seconds