----- SUMMARY FOR THEOREM AC-IM-SC IN DIRECTORY Q:\choice -----

% AC-IM-SC.IN                 2000 June 5

formula_list(sos).
% negation of Theorem AC-IM-SC
-(AxCh -> (all x subclass(image(CHOICE,x),U(x)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Tue Jun 06 00:01:36 2000

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

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

70 [] -AxCh | subclass(CHOICE,inverse(E)).
519 [] -subclass(x,y) | subclass(image(x,z),image(y,z)).
2722 [] AxCh.
2723 [] -subclass(image(CHOICE,$c1),U($c1)).
2871 [] equal(image(inverse(E),x),U(x)).
3634 [ur,2722,70] subclass(CHOICE,inverse(E)).
3640 [ur,3634,519,demod,2871] subclass(image(CHOICE,x),U(x)).
3641 [binary,3640.1,2723.1] $F.

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

clauses generated    1260
Kbytes malloced      2618
user CPU time           2.09  seconds