----- SUMMARY FOR THEOREM AC-SS-2 IN DIRECTORY Q:\ax-e -----

% AC-SS-2.IN            1997 August 13

formula_list(sos).
% negation of Theorem AC-SS-2
-(AxCh -> (all x (member(x,V) -> member(pair(singleton(x),x),CHOICE)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Aug 14 03:59:05 1997

Length of proof is 5. Level of proof is 5.

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

119 [] -member(y,singleton(x)) | equal(y,x).
272 [] -member(x,D(xr)) | member(pair(x,ran(xr,x,V)),xr).
659 [] -AxCh | -member(pair(x,y),CHOICE) | member(y,x).
660 [] -AxCh | -member(x,V) | member(singleton(x),D(CHOICE)).
661 [] AxCh.
662 [] member($c1,V).
663 [] -member(pair(singleton($c1),$c1),CHOICE).
753 [] equal(ran(CHOICE,singleton(x),V),r$(x)).
755 [ur,662,660,661] member(singleton($c1),D(CHOICE)).
761 [ur,755,272,demod,753] 
          member(pair(singleton($c1),r$($c1)),CHOICE).
787 [ur,761,659,661] member(r$($c1),singleton($c1)).
864,863 [ur,787,119] equal(r$($c1),$c1).
865 [back_demod,761,demod,864] 
          member(pair(singleton($c1),$c1),CHOICE).
866 [binary,865.1,663.1] $F.

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

clauses generated    8839
Kbytes malloced       766
user CPU time           4.55  seconds