PAAR-2020 Seventh Workshop on Practical Aspects of Automated Reasoning June 29-30, 2020 http://www.eprover.org/EVENTS/PAAR-2020.html SC2 -2020 Fifth Workshop on Symbolic Computation and Satisfiability Checking July 5, 2020 http://www.sc-square.org/CSA/workshop5.html Affiliated with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020) Virtual (originally Paris, France) Preface This volume contains the papers presented at the Seventh Workshop on Practical Aspects of Automated Reason- ing (PAAR-2020) and at the Fifth Workshop on Satisfiability Checking and Symbolic Computation (SC2 -2020). The workshops were held respectively on June 29–30, 2020, and on July 5, 2020, virtually, in association with the Tenth International Joint Conference on Automated Reasoning (IJCAR-2020). PAAR provides a forum for developers of automated reasoning tools to discuss and compare different im- plementation 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 appli- cation of automated reasoning tools. It allows researchers to present work in progress, and to discuss current trends, new implementation techniques and new 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 received nineteen submissions. Each submission was reviewed by at least three program committee members. Sixteen papers were accepted for presentation, and the workshop was extended from one day to two days to accommodate for the unexpectedly high number of presentations. Thirteen papers were invited for the proceedings; in the end, twelve papers could be included in the proceedings. The aim of the SC2 workshop is to provide an opportunity to discuss, 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. Satisfiabil- ity Checking has recently started to tackle similar problems but with different algorithmic and technological solutions. SC2 received three papers, each of which received three reviews by the members of the programme committee. We attribute low submission rate to disruptions caused by COVID-19. Nevertheless, all submitted papers were of high quality and were accepted for presentation at the workshop and publication in this volume. The PAAR and SC2 workshop organizers would like to thank the authors and participants of both workshops for making two very successful events possible, particularly in these special COVID-19 times. 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. The SC2 workshop organizers would like to thank the SMT-2020 workshop for accommodating a joint SC2 /SMT session. Last but not least, the IJCAR organizers were extremely helpful in finding good solutions to still have the workshops in spite of the 2020 sanitary crisis. The PAAR and SC2 workshop chairs are very grateful to them for their support and for virtually hosting the workshops. November 2020 Konstantin Korovin and Ilias S. Kotsireas (SC2 Chairs) Pascal Fontaine, Philipp Rümmer, Sophie Tourret (PAAR Chairs) II Program Committee (PAAR) Simon Cruanes Aesthetic Integration, Texas, USA Hans de Nivelle Nazarbayev University, Kazakhstan Bruno Dutertre SRI international, California, USA Gabriel Ebner VU Amsterdam, Netherlands Pascal Fontaine (co-chair) Liège University, Belgium Antti Hyvärinen University of Lugano, Switzerland Ahmed Irfan Stanford University, California, USA Cezary Kaliszyk University of Innsbruck, Austria Daniel Le Berre CNRS - University of Artois, France Ondrej Lengal Brno University of Technology, Czech Republic Tomer Libal American University of Paris, France Cláudia Nalon University of Brası́lia, Brasil Jens Otten University of Oslo, Norway Philipp Rümmer (co-chair) Uppsala University, Sweden Renate A. Schmidt The University of Manchester, UK Stephan Schulz DHBW Stuttgart, Germany Martina Seidl Johannes Kepler University Linz, Austria Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France Alexander Steen University of Luxembourg, Luxembourg Martin Suda Czech Technical University, Czech Republic Geoff Sutcliffe University of Miami, Florida, USA Sophie Tourret (co-chair) Max-Planck Institute for Informatics, Germany Sarah Winkler University of Verona, Italy Aleksandar Zeljić Stanford University, California, USA Program Committee (SC2 ) John Abbott Università degli Studi di Genova, Italy Erika Abraham RWTH Aachen University, Germany Anna M. Bigatti Universita di Genova, Italy Curtis Bright University of Waterloo James H. Davenport University of Bath, U.K. Matthew England Coventry University, UK Pascal Fontaine Liège University, Belgium Vijay Ganesh University of Waterloo, Canada Alberto Griggio Fondazione Bruno Kessler, Trento, Italy Marijn J.H. Heule Carnegie Mellon University, USA Ahmed Irfan Stanford, USA Dejan Jovanovic SRI, USA Manuel Kauers Johannes Kepler University, Linz, Austria Konstantin Korovin (co-chair) The University of Manchester, UK Ilias S. Kotsireas (co-chair) Wilfrid Laurier University, Canada Laura Kovacs TU Wien, Austria David Monniaux University of Grenoble, France Norbert Mueller University of Trier, Germany Stefan Ratschan Academy of Sciences of the Czech Republic, Prague, Czech Republic Martina Seidl Johannes Kepler University, Linz, Austria Thomas Sturm CNRS, Nancy, France and MPI Informatik, Germany III Table of Contents Workshop on Practical Aspects of Automated Reasoning 2020 Animated Logic: Correct Functional Conversion to Conjunctive Normal Form . . . . . . . . . . . . . . . . 1 Pedro Barroso, Mario Pereira and António Ravara Learning Precedences from Simple Symbol Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Filip Bártek and Martin Suda Layered Clause Selection for Saturation-Based Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . 34 Bernhard Gleiss and Martin Suda Simplifying Casts and Coercions (Extended Abstract) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 Robert Y. Lewis and Paul-Nicolas Madelaine Evaluation of Axiom Selection Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 Qinghua Liu, Zishi Wu, Zihao Wang and Geoff Sutcliffe Equality Preprocessing in Connection Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 Benjamin E. Oliver and Jens Otten Give Reasoning a Trie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 Thomas Prokosch and François Bry Directed Graph Networks for Logical Reasoning (Extended Abstract) . . . . . . . . . . . . . . . . . . . . 109 Michael Rawson and Giles Reger Efficient Implementation of Large-Scale Watchlists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 Constantin Ruhdorfer and Stephan Schulz Cutting Down the TPTP Language (And Others) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 Nahku Saidy, Hanna Siegfried, Stephan Schulz and Geoff Sutcliffe Boolean Reasoning in a Higher-Order Superposition Prover . . . . . . . . . . . . . . . . . . . . . . . . . . 148 Petar Vukmirović and Visa Nummelin Querying the Guarded Fragment via Resolution (Extended Abstract) . . . . . . . . . . . . . . . . . . . . 167 Sen Zheng and Renate A. Schmidt Satisfiability Checking and Symbolic Computation Workshop 2020 New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract) . . . . . 178 Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer and Zak Tonks Computing Tropical Prevarieties With Satisfiability Modulo Theories (SMT) Solvers . . . . . . . . . . . . 189 Christoph Lüders GeoGebra and the realgeom Reasoning Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204 Róbert Vajda and Zoltán Kovács IV