read `BCMV.txt`:
ProveConjAx();

quit: