A first order logic prover via resolution.