Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples. Both can be run simultaneously from the same input, with Prover9 attempting to find a proof, while Mace4 attempts to find a (disproving) counter-example. Prover9, Mace4, and many other tools are built on an underlying library named LADR to simplify implementation. Resulting proofs can be double-checked by Ivy, a proof-checking tool that has been separately verified using ACL2.
In July 2006 the LADR/Prover9/Mace4 input language made a major change (which also differentiates it from Otter). The key distinction between "clauses" and "formulas" completely disappeared; "formulas" can now have free variables; and "clauses" are now a subset of "formulas". Prover9/Mace4 also supports a "goal" type of formula, which is automatically negated for proof. Prover9 attempts to automatically generate a proof by default; in contrast, Otter's automatic mode must be explicitly set.
The traditional "all men are mortal", "Socrates is a man", prove "Socrates is mortal" can be expressed this way in Prover9:
man(x) -> mortal(x). % open formula with free variable x
This will be automatically converted into clausal form (which Prover9 also accepts):
-man(x) | mortal(x).
A proof that the square root of 2 is irrational can be expressed this way:
1*x = x. % identity
x*1 = x.
x*(y*z) = (x*y)*z. % associativity
x*y = y*x. % commutativity
(x*y = x*z ) -> y = z. % cancellation (0 is not allowed, so x!=0).
% Now let's define divides(x,y): x divides y. divides(2,6) is true b/c 2*3=6.
divides(x,y) <-> (exists z x*z = y).
(divides(2,x) | divides(2,y)). % If 2 divides x*y, it divides x or y.
a*a = (2*(b*b)). % a/b = sqrt(2), so a^2 = 2 * b^2.
(x != 1) -> -(divides(x,a) &
divides(x,b)). % a/b is in lowest terms
2 != 1. % Original author almost forgot this.