An Interpolating Theorem Prover