----- SUMMARY FOR THEOREM AC-SG-1 IN DIRECTORY Q:\ax-e ----- % AC-SG-1.IN 1997 August 14 formula_list(sos). % negation of Theorem AC-SG-1 -(AxCh -> subclass(inverse(SINGLETON),CHOICE)). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Thu Aug 14 07:09:33 1997 Length of proof is 13. Level of proof is 7. ---------------- PROOF ---------------- 1 [] -subclass(x,y) | -member(u,x) | member(u,y). 2 [] member(notsub(x,y),x) | subclass(x,y). 3 [] -member(notsub(x,y),y) | subclass(x,y). 17 [] -member(z,cart(x,y)) | equal(z,pair(first(z),second(z))). 26 [] -member(z,complement(x)) | -member(z,x). 27 [] member(z,complement(x)) | -member(z,V) | member(z,x). 135 [] member(pair(x,y),V). 218 [] -member(z,cart(x,y)) | member(second(z),y). 304 [] subclass(inverse(x),cart(V,V)). 305 [] -member(pair(u,v),inverse(x)) | member(pair(v,u),x). 564 [] -member(pair(x,y),SINGLETON) | equal(singleton(x),y). 673 [] -AxCh | -member(x,V) | member(pair(singleton(x),x),CHOICE). 674 [] AxCh. 675 [] -subclass(inverse(SINGLETON),CHOICE). 768 [] equal(notsub(inverse(SINGLETON),CHOICE),n$). 769 [] equal(first(n$),f$). 770 [] equal(second(n$),s$). 775 [ur,675,3,demod,768] -member(n$,CHOICE). 776 [ur,675,2,demod,768] member(n$,inverse(SINGLETON)). 787 [ur,776,1,304] member(n$,cart(V,V)). 812 [ur,787,218,demod,770] member(s$,V). 814,813 [ur,787,17,demod,769,770] equal(n$,pair(f$,s$)). 818 [back_demod,776,demod,814] member(pair(f$,s$),inverse(SINGLETON)). 819 [back_demod,775,demod,814] -member(pair(f$,s$),CHOICE). 837 [ur,812,673,674] member(pair(singleton(s$),s$),CHOICE). 847 [ur,818,305] member(pair(s$,f$),SINGLETON). 849 [ur,819,27,135] member(pair(f$,s$),complement(CHOICE)). 919 [ur,837,26] -member(pair(singleton(s$),s$),complement(CHOICE)). 996,995 [ur,847,564] equal(singleton(s$),f$). 1011 [back_demod,919,demod,996] -member(pair(f$,s$),complement(CHOICE)). 1012 [binary,1011.1,849.1] $F. ------------ end of proof ------------- clauses generated 12510 Kbytes malloced 734 user CPU time 3.79 seconds