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 ...)