C++ Automated theorem prover
Produces new theorems from the axioms of first order logic by randomly applying deduction rules.
John Hester