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

% AC-BIJ.IN                 2000 June 5

formula_list(sos).
% negation of Corollary AC-BIJ
-(AxCh -> (all x (member(x,FUNS) ->
  member(composite(CHOICE,VERTSECT(inverse(x))),BIJ)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Jun 05 21:08:27 2000

Length of proof is 7. Level of proof is 3.

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

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
4 [] subclass(x,V).
1325 [] -member(x,y) | -subclass(z,x) | member(z,image(inverse(S),
          y)).
1349 [] -member(x,V) | member(inverse(x),V).
2353 [] -member(x,FUNS) | FUNCTION(x).
2651 [] -ONEONE(x) | -member(x,V) | member(x,BIJ).
2670 [] -AxCh | subclass(composite(CHOICE,VERTSECT(x)),x).
2672 [] -AxCh | -FUNCTION(x) | ONEONE(composite(CHOICE,
          VERTSECT(inverse(x)))).
2673 [] AxCh.
2674 [] member($c1,FUNS).
2675 [] -member(composite(CHOICE,VERTSECT(inverse($c1))),BIJ).
2776 [] equal(R(inverse(x)),D(x)).
2791 [] equal(image(x,V),R(x)).
2912 [] equal(D(S),V).
3565 [ur,2673,2670] subclass(composite(CHOICE,VERTSECT(x)),x).
3569 [ur,2674,2353] FUNCTION($c1).
3570 [ur,2674,1,4] member($c1,V).
3596 [ur,3569,2672,2673] 
          ONEONE(composite(CHOICE,VERTSECT(inverse($c1)))).
3608 [ur,3570,1349] member(inverse($c1),V).
3656 [ur,3596,2651,2675] 
          -member(composite(CHOICE,VERTSECT(inverse($c1))),V).
3706 [ur,3608,1325,3565,demod,2791,2776,2912] 
          member(composite(CHOICE,VERTSECT(inverse($c1))),V).
3707 [binary,3706.1,3656.1] $F.

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

clauses generated   39527
Kbytes malloced      2618
user CPU time           6.38  seconds