vampire

High-performance automated theorem prover for first-order logic

brewmacoslinux
Try with needOr install directly
Source

About

High-performance theorem prover

Commands

vampire

Examples

Prove a simple first-order logic theorem from a file$ vampire input.tptp
Run with time limit of 10 seconds and verbose output$ vampire --time_limit 10 --verbosity 2 theorem.tptp
Check satisfiability of a first-order logic problem$ vampire --mode sat problem.tptp