Dynamic Strategy Priority: Empower the Strong and Abandon the Weak. - Michael Rawson 001; Giles Reger (PAAR@FLoC, 2018)

Old or Heavy? Decaying Gracefully with Age/Weight Shapes. - Michael Rawson 001; Giles Reger (CADE, 2019)

A Neurally-Guided, Parallel Theorem Prover. - Michael Rawson 001; Giles Reger (FroCos, 2019)

Directed Graph Networks for Logical Reasoning (Extended Abstract). - Michael Rawson 001; Giles Reger (PAAR+SC²@IJCAR, 2020)

On Evaluating Theorem Provers. - Michael Rawson 001; Giles Reger (ARCADE@CADE, 2021)

A Multithreaded Vampire with Shared Persistent Grounding. - Michael Rawson 001; Giles Reger (FMCAD, 2021)

lazyCoP: Lazy Paramodulation Meets Neurally Guided Search. - Michael Rawson 001; Giles Reger (TABLEAUX, 2021)

Eliminating Models During Model Elimination. - Michael Rawson 001; Giles Reger (TABLEAUX, 2021)

The Rapid Software Verification Framework. - Pamina Georgiou; Bernhard Gleiss; Ahmed Bhayat; Michael Rawson 001; Laura Kovács; Giles Reger (FMCAD, 2022)

The Vampire Approach to Induction (short paper). - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (PAAR@IJCAR, 2022)

Reuse of Introduced Symbols in Automatic Theorem Provers (short paper). - Michael Rawson 001; Martin Suda 001; Petra Hozzová; Giles Reger (PAAR@IJCAR, 2022)

Embedding the Connection Calculus in Satisfiability Modulo Theories. - Clemens Eisenhofer; Laura Kovács; Michael Rawson 001 (AReCCa@TABLEAUX, 2023)

Superposition with Delayed Unification. - Ahmed Bhayat; Johannes Schoisswohl; Michael Rawson 001 (CADE, 2023)

SAT-Based Subsumption Resolution. - Robin Coutelier; Laura Kovács; Michael Rawson 001; Jakob Rath (CADE, 2023)

CheckMate: Automated Game-Theoretic Security Reasoning. - Lea Salome Brugger; Laura Kovács; Anja Petkovic Komel; Sophie Rain; Michael Rawson 001 (CCS, 2023)

Non-Classical Logics in Satisfiability Modulo Theories. - Clemens Eisenhofer; Ruba Alassaf; Michael Rawson 001; Laura Kovács (TABLEAUX, 2023)

Lemmas: Generation, Selection, Application. - Michael Rawson 001; Christoph Wernhard; Zsolt Zombori; Wolfgang Bibel (TABLEAUX, 2023)

Reducibility Constraints in Superposition. - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (IJCAR (1), 2024)

Rewriting and Inductive Reasoning. - Márton Hajdú; Laura Kovács; Michael Rawson 001 (LPAR, 2024)

Scaling CheckMate for Game-Theoretic Security. - Sophie Rain; Lea Salome Brugger; Anja Petkovic Komel; Laura Kovács; Michael Rawson 001 (LPAR, 2024)

Spanning Matrices via Satisfiability Solving. - Clemens Eisenhofer; Michael Rawson 001; Laura Kovács (CoRR, 2024)

Scaling Game-Theoretic Security Reasoning. - Sophie Rain; Lea Salome Brugger; Anja Petkovic Komel; Laura Kovács; Michael Rawson 001 (CoRR, 2024)

SAT Solving for Variants of First-Order Subsumption. - Robin Coutelier; Jakob Rath; Michael Rawson 001; Armin Biere; Laura Kovács (CoRR, 2024)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. - Simon Jeanteur; Laura Kovács; Matteo Maffei; Michael Rawson 001 (IACR Cryptol. ePrint Arch., 2024)

Expressive Power of Temporal Message Passing. - Przemyslaw Andrzej Walega; Michael Rawson 001 (AAAI, 2025)

Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. - Michael Rawson 001; Andrei Voronkov; Johannes Schoisswohl; Anja Petkovic Komel (CADE, 2025)

The Vampire Diary. - Filip Bártek; Ahmed Bhayat; Robin Coutelier; Márton Hajdú; Matthias Hetzenberger; Petra Hozzová; Laura Kovács; Jakob Rath; Michael Rawson 001; Giles Reger; Martin Suda 001; Johannes Schoisswohl; et al. (CAV (3), 2025)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo. - Anja Petkovic Komel; Michael Rawson 001; Martin Suda 001 (CoRR, 2025)