9th Workshop on Practical Aspects of Automated Reasoning – and – 9th Satisfiability Checking and Symbolic Computation Workshop PAAR 2024 + SC2 2024 Preface This volume contains the papers presented at the Ninth Workshop on Practical Aspects of Automated Reasoning (PAAR-2024) and the Ninth Satisfiability Checking and Symbolic Computation Workshop (SC2 2024). The workshops were held on July 2, 2024 in association with the International Joint Conference on Automated Reasoning (IJCAR 2024) in Nancy, France. PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brings together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It allows researchers to present their work in progress, and to discuss new implementation techniques and applications. The purpose of PAAR is to help the community understand how to build useful and powerful reasoning systems in practice, and how to apply existing systems to real problems. PAAR 2024 received eleven submissions. Each submission was reviewed by at least three program committee members. Six papers were accepted for presentation, thereof four as regular papers. The PAAR 2024 organizers would like to thank the two invited speakers André Platzer (Karlsruhe Institute of Technology) and Martina Seidl (Johannes Kepler University Linz). The aim of the SC2 workshop is to share knowledge and experience across two communities: symbolic computation and satisfiability checking. Symbolic computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions. SC2 received five submissions in total. Each submission was reviewed by at least three program committee members. Four papers were accepted for presentation, thereof three as regular papers and one as short paper. SC2 hosted two invited speakers. Manuel Kauers from the Johannes Kepler University Linz, Austria talked about separating variables in polynomial ideals, while Lawrence Paulson from the University of Cambridge, UK discussed computer algebra and the formalisation of new mathematics. The PAAR and SC2 workshop organisers would like to thank the authors and participants of both workshops for making two very successful events possible. Our thanks also go to the program committee members and the external reviewers for their considerable effort to provide thorough and constructive reviews. As in all years, we are indebted to the EasyChair team for the unfailing availability of the EasyChair Conference System. We are grateful to the CEUR team for publishing our proceedings. July 2024 Cláudia Nalon, Alexander Steen, Martin Suda (PAAR 2024 Chairs) Chris Brown, Daniela Kaufmann (SC2 2024 Chairs) Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR 2024), and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square 2024), July 2, 2024, Nancy, France © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). PAAR 2024: Program Committee Gabriel Ebner Microsoft Research, US Hans de Nivelle Nazarbayev University, KZ Mathias Fleury University of Freiburg, DE Pascal Fontaine Université de Liège, BE Ulrich Furbach University of Koblenz, DE Jan Jakubuv Czech Technical University in Prague, CZ Cezary Kaliszyk University of Innsbruck, AT Daniela Kaufmann TU Wien, AT Boris Konev University of Liverpool, UK Daniel Le Berre CNRS - Université d’Artois, FR Ondrej Lengal Brno University of Technology, CZ Tomer Libal University of Luxembourg, LU Cláudia Nalon (co-chair) University of Brasília, BR Michael Rawson TU Wien, AT Philipp Rümmer University of Regensburg, DE, and Uppsala University, SE Renate A. Schmidt The University of Manchester, UK Stephan Schulz DHBW Stuttgart, DE Alexander Steen (co-chair) University of Greifswald, DE Frieder Stolzenburg Harz University of Applied Sciences, DE Martin Suda (co-chair) Czech Technical University in Prague, CZ Geoff Sutcliffe University of Miami, US Sophie Tourret Inria, FR, and MPI for Informatics, DE Zsolt Zombori HUN-REN Alfréd Rényi Institute of Mathematics, HU Additional reviewer Francis Jeffry Pelletier SC2 2024: Program Committee Erika Abraham RWTH Aachen University, DE Haniel Barbosa Universidade Federal de Minas Gerais, BR Armin Biere University of Freiburg, DE Anna Bigatti University of Genova, IT Martin Brain City University of London, UK Curtis Bright University of Waterloo, CA Chris Brown (co-chair) U.S. Naval Academy, US David Cerna Institute of Computer Science, Czech Academy of Sciences, CZ James H. Davenport University of Bath, UK Matthew England Coventry University, UK Pascal Fontaine University of Liege, BE Alberto Griggio Fondazione Bruno Kessler, IT Mikolas Janota Czech Technical University in Prague, CZ Daniela Kaufmann (co-chair) TU Wien, AT Konstantin Korovin The University of Manchester, UK Ilias Kotsireas Wilfrid Laurier University, CA & Maplesoft Gereon Kremer Certora, IL Alex Ozdemir Stanford University, US Stefan Ratschan Institute of Computer Science, Czech Academy of Sciences, CZ Christoph Scholl University of Freiburg, DE Thomas Sturm CNRS, FR & MPI Informatics, DE Bican Xia Peking University, CN Additional reviewer Simon Schwarz