archsat

A first-order theorem prover with formal proof output