Prover9 is a program that searches for proofs of statements in first-order logic with equality.
Mace4 is a program that searches for small (finite) models or counterexamples of the same kind of statement.
The problems you construct with Son of BirdBrain II are given to Prover9, which tries for a few seconds to find a proof. If Prover9 fails, the problem is given to Mace4, which searches for small counterexamples.
You can't do much serious work with Son of BirdBrain II, because you can't modify the search parameters, and we can't give you more than a few seconds of search time. But, once you're hooked, it's easy to install your own copy of Prover9 and Mace4 for your Unix, Macintosh, or Microsoft computer.
Comments and questions can be sent to William McCune. Also, it's easy to add new areas to Son of BirdBrain II's repertoire.
(We know that the proofs and counterexamples aren't pretty---maybe someday ...)