Induction with Generalization in Superposition Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2020)

Inductive Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2021)

Making Theory Reasoning Simpler. - Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (2), 2021)

Automating Induction by Reflection. - Johannes Schoisswohl; Laura Kovács (LFMTP, 2021)

Algorithm selection and instance space analysis for curriculum-based course timetabling. - Arnaud De Coster; Nysret Musliu; Andrea Schaerf; Johannes Schoisswohl; Kate Smith-Miles (J. Sched., 2022)

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

Refining Unification with Abstraction. - Ahmed Bhayat; Konstantin Korovin; Laura Kovács; Johannes Schoisswohl (LPAR, 2023)

ALASCA: Reasoning in Quantified Linear Arithmetic. - Konstantin Korovin; Laura Kovács; Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (1), 2023)

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. - Johannes Schoisswohl; Laura Kovács; Konstantin Korovin (LPAR, 2024)

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)