Prover9.org
Prover9
Mace4
Prover9+Mace4
E Prover
Vampire
-- Examples --
2 + 2 = 4 (paramodulation demo)
Sqrt(2) is irrational
Group theory: right identity and inverse
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)
-- TPTP Domain --
-- Problem --
Load File
Save Output
Clear
Stop
Verify
Visualize
Run
Manual
Ready
Input
Output
Input
Output
Prover9
Mace4