----- SUMMARY FOR THEOREM AC-SG-2 IN DIRECTORY Q:\choice -----

% AC-SG-2.IN                 2000 June 4

formula_list(sos).
% negation of Theorem AC-SG-2
-(AxCh -> equal(composite(CHOICE,SINGLETON),Id)).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Jun 04 14:47:37 2000

Length of proof is 8. Level of proof is 4.

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

5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
70 [] -AxCh | subclass(CHOICE,inverse(E)).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
744 [] -subclass(x,y) | subclass(composite(x,z),composite(y,z)).
1225 [] subclass(id(R(x)),composite(x,inverse(x))).
1260 [] equal(composite(inverse(E),SINGLETON),Id).
1843 [] -AxCh | subclass(inverse(SINGLETON),CHOICE).
1844 [] AxCh.
1845 [] -equal(composite(CHOICE,SINGLETON),Id).
1946 [] equal(R(inverse(x)),D(x)).
2117 [] equal(inverse(inverse(x)),composite(Id,x)).
2126 [] equal(composite(x,composite(Id,y)),composite(x,y)).
2197 [] equal(id(V),Id).
2231 [] equal(D(SINGLETON),V).
2405 [binary,1844.1,1843.1] subclass(inverse(SINGLETON),CHOICE).
2406 [binary,1844.1,70.1] subclass(CHOICE,inverse(E)).
2408 [binary,1845.1,5.3] 
          -subclass(composite(CHOICE,SINGLETON),Id)
           | -subclass(Id,composite(CHOICE,SINGLETON)).
2411 [binary,2405.1,744.1] 
          subclass(composite(inverse(SINGLETON),
          x),composite(CHOICE,x)).
2421 [binary,2406.1,744.1] 
          subclass(composite(CHOICE,x),composite(inverse(E),x)).
2448 [ur,2411,77,1225,demod,1946,2231,2197,2117,2126] 
          subclass(Id,composite(CHOICE,SINGLETON)).
2519 [para_into,2421.1.2,1260.1.1] 
          subclass(composite(CHOICE,SINGLETON),Id).
2592 [binary,2448.1,2408.2] 
          -subclass(composite(CHOICE,SINGLETON),Id).
2593 [binary,2592.1,2519.1] $F.

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

clauses generated   20902
Kbytes malloced      1852
user CPU time           3.40  seconds