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

% AC-VS.IN                 2000 June 4

formula_list(sos).
% negation of Theorem AC-VS
-(AxCh -> (all x subclass(composite(CHOICE,VERTSECT(x)),x))).
end_of_list.


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

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

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

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)).
1162 [] subclass(composite(x,id(y)),x).
2071 [] equal(composite(inverse(E),VERTSECT(x)),
          composite(x,id(D(VERTSECT(x))))).
2074 [] AxCh.
2075 [] -subclass(composite(CHOICE,VERTSECT($c1)),$c1).
2743 [binary,2074.1,70.1] subclass(CHOICE,inverse(E)).
2745 [binary,2075.1,77.3] 
          -subclass(composite(CHOICE,VERTSECT($c1)),x)
           | -subclass(x,$c1).
2756 [binary,2745.1,744.2] 
          -subclass(composite(x,VERTSECT($c1)),$c1)
           | -subclass(CHOICE,x).
2780 [para_into,2756.1.1,2071.1.1,unit_del,1162,2743] $F.

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

clauses generated    8068
Kbytes malloced      1979
user CPU time           2.25  seconds