----- SUMMARY FOR THEOREM AC-RA IN DIRECTORY Q:\choice -----

% AC-RA.IN                 2000 June 4

formula_list(sos).
% negation of Theorem AC-RA
-(AxCh -> equal(R(CHOICE),V)).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Jun 04 19:00:11 2000

Length of proof is 3. Level of proof is 2.

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

300 [] -equal(cart(V,V),0).
451 [] -subclass(x,y) | subclass(R(x),R(y)).
555 [] -subclass(image(V,x),y) | equal(x,0) | equal(y,V).
1843 [] -AxCh | subclass(inverse(SINGLETON),CHOICE).
1844 [] AxCh.
1845 [] -equal(R(CHOICE),V).
1874 [] equal(intersection(x,x),x).
1946 [] equal(R(inverse(x)),D(x)).
1949 [] equal(R(V),V).
1961 [] equal(image(x,V),R(x)).
1978 [] equal(image(V,cart(x,y)),intersection(image(V,x),
          image(V,y))).
2231 [] equal(D(SINGLETON),V).
2405 [ur,1844,1843] subclass(inverse(SINGLETON),CHOICE).
2406 [ur,1845,555,300,demod,1978,1961,1949,1961,1949,1874] 
          -subclass(V,R(CHOICE)).
2407 [ur,2405,451,demod,1946,2231] subclass(V,R(CHOICE)).
2408 [binary,2407.1,2406.1] $F.

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

clauses generated     529
Kbytes malloced      1756
user CPU time           2.81  seconds