Prover 9 is now working and integrated.

inferenceEngines/1 defaults to using otter and prover9. For trivial stuff,
otter is still faster

This is the Vanilla version of BB1.

That's exactly as downloaded and you should revert to it should you suspect any
bugs in my code. Please let me know if you find some.