Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. - Lukas Bartl; Jasmin Blanchette; Tobias Nipkow (CADE, 2025)