----- SUMMARY FOR THEOREM AC-SS-1 IN DIRECTORY Q:\ax-e -----

% AC-SS-1.IN            1997 August 13
% Lemma 1 for AC-SS

formula_list(sos).
% negation of Lemma AC-SS-1
-(AxCh -> (all x (member(x,V) -> member(singleton(x),D(CHOICE))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Wed Aug 13 17:18:50 1997

Length of proof is 6. Level of proof is 3.

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

1 [] -subclass(x,y) | -member(u,x) | member(u,y).
27 [] member(z,complement(x)) | -member(z,V) | member(z,x).
72 [] -AxCh | equal(D(CHOICE),complement(singleton(0))).
102 [] -member(z,0).
116 [] member(singleton(x),V).
117 [] -member(x,V) | member(x,singleton(x)).
378 [] -member(x,y) | subclass(x,U(y)).
660 [] AxCh.
661 [] member($c1,V).
662 [] -member(singleton($c1),D(CHOICE)).
675 [] equal(complement(complement(x)),x).
728 [] equal(U(singleton(0)),0).
755 [ur,660,72] equal(D(CHOICE),complement(singleton(0))).
761 [ur,661,117] member($c1,singleton($c1)).
766 [ur,662,27,116] member(singleton($c1),complement(D(CHOICE))).
801 [ur,761,1,102] -subclass(singleton($c1),0).
825 [para_into,766.1.2.1,755.1.1,demod,675] 
          member(singleton($c1),singleton(0)).
1115 [ur,825,378,demod,728] subclass(singleton($c1),0).
1116 [binary,1115.1,801.1] $F.

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

clauses generated   14883
Kbytes malloced       766
user CPU time           3.63  seconds