SPASS Version 3.5. - Christoph Weidenbach; Dilyana Dimova; Arnaud Fietzke; Rohit Kumar; Martin Suda 001; Patrick Wischnewski (CADE, 2009)

External Sources of Axioms in Automated Theorem Proving. - Martin Suda 001; Geoff Sutcliffe; Patrick Wischnewski; Manuel Lamotte-Schubert; Gerard de Melo (KI, 2009)

On the Saturation of YAGO. - Martin Suda 001; Christoph Weidenbach; Patrick Wischnewski (IJCAR, 2010)

Progress Towards Effective Automated Reasoning with World Knowledge. - Geoff Sutcliffe; Martin Suda 001; Alexandra Teyssandier; Nelson Dellis; Gerard de Melo (FLAIRS, 2010)

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. - Martin Suda 001; Christoph Weidenbach (IJCAR, 2012)

Labelled Superposition for PLTL. - Martin Suda 001; Christoph Weidenbach (LPAR, 2012)

Triggered Clause Pushing for IC3. - Martin Suda 001 (CoRR, 2013)

Duality in STRIPS planning - Martin Suda 001 (CoRR, 2013)

The Challenges of Evaluating a New Feature in Vampire. - Giles Reger; Martin Suda 001; Andrei Voronkov (Vampire Workshop, 2014)

Property Directed Reachability for Automated Planning. - Martin Suda 001 (J. Artif. Intell. Res., 2014)

The Uses of SAT Solvers in Vampire. - Giles Reger; Martin Suda 001 (Vampire Workshop, 2015)

Playing with AVATAR. - Giles Reger; Martin Suda 001; Andrei Voronkov (CADE, 2015)

Variable and Clause Elimination for LTL Satisfiability Checking. - Martin Suda 001 (Math. Comput. Sci., 2015)

Resolution-based methods for linear temporal reasoning. - Martin Suda 001 (2015)

Selecting the Selection. - Krystof Hoder; Giles Reger; Martin Suda 001; Andrei Voronkov (IJCAR, 2016)

Global Subsumption Revisited (Briefly). - Giles Reger; Martin Suda 001 (Vampire@IJCAR, 2016)

A Clausal Normal Form Translation for FOOL. - Evgenii Kotelnikov; Laura Kovács; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

New Techniques in Clausal Form Generation. - Giles Reger; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

AVATAR Modulo Theories. - Giles Reger; Nikolaj S. Bjørner; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

Finding Finite Models in Multi-sorted First-Order Logic. - Giles Reger; Martin Suda 001; Andrei Voronkov (SAT, 2016)

Lifting QBF Resolution Calculi to DQBF. - Olaf Beyersdorff; Leroy Chew; Renate A. Schmidt; Martin Suda 001 (Electron. Colloquium Comput. Complex., 2016)

Splitting Proofs for Interpolation. - Bernhard Gleiss; Laura Kovács; Martin Suda 001 (CADE, 2017)

A Unifying Principle for Clause Elimination in First-Order Logic. - Benjamin Kiesl; Martin Suda 001 (CADE, 2017)

Checkable Proofs for First-Order Theorem Proving. - Giles Reger; Martin Suda 001 (ARCADE@CADE, 2017)

Automated Invention of Strategies and Term Orderings for Vampire. - Jan Jakubuv; Martin Suda 001; Josef Urban (GCAI, 2017)

Blocked Clauses in First-Order Logic. - Benjamin Kiesl; Martin Suda 001; Martina Seidl; Hans Tompits; Armin Biere (LPAR, 2017)

Set of Support for Theory Reasoning. - Giles Reger; Martin Suda 001 (IWIL@LPAR, 2017)

Instantiation and Pretending to be an SMT Solver with Vampire. - Giles Reger; Martin Suda 001; Andrei Voronkov (SMT, 2017)

Testing a Saturation-Based Theorem Prover: Experiences and Challenges. - Giles Reger; Martin Suda 001; Andrei Voronkov (TAP@STAF, 2017)

Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). - Giles Reger; Martin Suda 001; Andrei Voronkov (CoRR, 2017)

Towards Smarter MACE-style Model Finders. - Mikolas Janota; Martin Suda 001 (LPAR, 2018)

A Theory of Satisfiability-Preserving Proofs in SAT Solving. - Adrián Rebola-Pardo; Martin Suda 001 (LPAR, 2018)

Local Soundness for QBF Calculi. - Martin Suda 001; Bernhard Gleiss (SAT, 2018)

Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. - Giles Reger; Martin Suda 001; Andrei Voronkov (TACAS (1), 2018)

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. - Karel Chvalovský; Jan Jakubuv; Martin Suda 001; Josef Urban (CADE, 2019)

Symmetry Avoidance in MACE-Style Finite Model Finding. - Giles Reger; Martin Riener; Martin Suda 001 (FroCos, 2019)

Superposition Reasoning about Quantified Bitvector Formulas. - David Damestani; Laura Kovács; Martin Suda 001 (SYNASC, 2019)

TOOLympics 2019: An Overview of Competitions in Formal Methods. - Ezio Bartocci; Dirk Beyer 001; Paul E. Black; Grigory Fedyukovich; Hubert Garavel; Arnd Hartmanns; Marieke Huisman; Fabrice Kordon; Julian Nagele; Mihaela Sighireanu; Bernhard Steffen; Martin Suda 001; et al. (TACAS (3), 2019)

Aiming for the Goal with SInE. - Martin Suda 001 (Vampire, 2019)

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. - Olaf Beyersdorff; Joshua Blinkhorn; Leroy Chew; Renate A. Schmidt; Martin Suda 001 (J. Autom. Reason., 2019)

SAT Competition 2018. - Marijn J. H. Heule; Matti Järvisalo; Martin Suda 001 (J. Satisf. Boolean Model. Comput., 2019)

Learning Precedences from Simple Symbol Features. - Filip Bártek; Martin Suda 001 (PAAR+SC²@IJCAR, 2020)

Layered Clause Selection for Theory Reasoning - (Short Paper). - Bernhard Gleiss; Martin Suda 001 (IJCAR (1), 2020)

Layered Clause Selection for Saturation-Based Theorem Proving. - Bernhard Gleiss; Martin Suda 001 (PAAR+SC²@IJCAR, 2020)

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). - Jan Jakubuv; Karel Chvalovský; Miroslav Olsák; Bartosz Piotrowski; Martin Suda 001; Josef Urban (IJCAR (2), 2020)

Layered Clause Selection for Theory Reasoning. - Bernhard Gleiss; Martin Suda 001 (CoRR, 2020)

Improving ENIGMA-style Clause Selection while Learning From History. - Martin Suda 001 (CADE, 2021)

Neural Precedence Recommender. - Filip Bártek; Martin Suda 001 (CADE, 2021)

Vampire with a Brain Is a Good ITP Hammer. - Martin Suda 001 (FroCoS, 2021)

SAT Competition 2020. - Nils Froleyks; Marijn Heule; Markus Iser; Matti Järvisalo; Martin Suda 001 (Artif. Intell., 2021)

New Techniques that Improve ENIGMA-style Clause Selection Guidance. - Martin Suda 001 (CoRR, 2021)

Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). - Martin Suda 001 (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)

MizAR 60 for Mizar 50. - Jan Jakubuv; Karel Chvalovský; Zarathustra Amadeus Goertzel; Cezary Kaliszyk; Mirek Olsák; Bartosz Piotrowski; Stephan Schulz 001; Martin Suda 001; Josef Urban (ITP, 2023)

How Much Should This Symbol Weigh? A GNN-Advised Clause Selection. - Filip Bártek; Martin Suda 001 (LPAR, 2023)

Learning Guided Automated Reasoning: A Brief Survey. - Lasse Blaauwbroek; David M. Cerna; Thibault Gauthier; Jan Jakubuv; Cezary Kaliszyk; Martin Suda 001; Josef Urban (Logics and Type Systems in Theory and Practice, 2024)

Regularization in Spider-Style Strategy Discovery and Schedule Construction. - Filip Bártek; Karel Chvalovský; Martin Suda 001 (IJCAR (1), 2024)

A Higher-Order Vampire (Short Paper). - Ahmed Bhayat; Martin Suda 001 (IJCAR (1), 2024)

Lemma Discovery and Strategies for Automated Induction. - Sólrún Halla Einarsdóttir; Márton Hajdú; Moa Johansson; Nicholas Smallbone; Martin Suda 001 (IJCAR (1), 2024)

Planning Domain Model Acquisition from State Traces without Action Parameters. - Tomás Balyo; Martin Suda 001; Lukás Chrpa; Dominik Safránek; Stephan Gocht; Filip Dvorák; Roman Barták; G. Michael Youngblood (KR, 2024)

Cautious Specialization of Strategy Schedules (Extended Abstract). - Filip Bártek; Karel Chvalovský; Martin Suda 001 (PAAR+SC²@IJCAR, 2024)

Learning Planning Action Models from State Traces. - Tomás Balyo; Martin Suda 001; Lukás Chrpa; Dominik Safránek; Filip Dvorák; Roman Barták; G. Michael Youngblood (CoRR, 2024)

Efficient Neural Clause-Selection Reinforcement. - Martin Suda 001 (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)