With these pages you can construct some simple abstract algebra and logic problems and run them through Prover9, which searches for proofs, and Mace4, which searches for counterexamples.
A New Feature: In addition to selecting hypotheses and conclusions from lists of formulas, you can compose your own.
This system is a successor to the original Son of BirdBrain, which uses Otter and Mace2.
Select an area from the following menu, then click "OK".