This package provides a graphical user interface for easily running the Prover9 theorem prover and the Mace4 countermodel generator along with a number of sample input files.