Prover9.org
Prover9
Mace4
Prover9+Mace4
-- Examples --
Sqrt(2) is irrational
Group theory (x*e=x)
Idempotent rings are commutative
x*x=e implies abelian
PUZ001-1 (Pelletier puzzle)
COL060-1 (combinatory logic)
LAT005-1 (lattice theory)
Group of order 4
Non-commutative group
Lattice of order 6
Non-abelian group (TPTP/FOF)
Load File
Save Output
Clear
Stop
Verify
Run
Manual
Ready
Input
Output
Input
Output
Prover9
Mace4