P LNFspass	Theorem Prover SPASS
P LNFdarwin	Theorem Prover Darwin
P LNFeprover	Theorem Prover E
P LNFe-darwin	Theorem Prover E-Darwin
P LNFekrhyper	Theorem Prover and model generator E-KRHyper
P LNFleo2	Theorem Prover Leo-II
P LNFsatallax	Theorem Prover Satallax
P LNFz3	Theorem Prover Z3
P LNFhol-light	Theorem Prover HOL Light
P LNFcvc4	SMT solver Cooperating Validity Checker 4
P LNFkodkodi	Relational logic solver Kodkod
P LNFminisat	SAT solver MiniSat
P LNFyices	SMT solver Yices2
P LNFzchaff	SAT solver Zchaff
P LNFmaude	Maude 2 interpreter
P LNFtwelf	Logical framework and programming language Twelf
P LNFfactplusplus	DL reasoner FaCT++