Interpolation and Symbol Elimination in Vampire?

Abstract. It has recently been shown that proofs in which some symbols are colored (e.g. local or split proofs and symbol-eliminating proofs) can be used for a number of applications, such as invariant generation and computing interpolants. This tool paper describes how such proofs and interpolant generation are imple-mented in the first-order theorem prover Vampire.