Computational Sustainability: Computing for a Better World -- Machine Learning in Automated and Interactive Theorem Proving -- Circular (Yet Sound) Proofs -- Short Proofs in QBF Expansion -- Proof Complexity of QBF Symmetry Recomputation -- Satisfiability Threshold for Power Law Random 2-SAT in Configuration Model -- DRAT Proofs, Propagation Redundancy, and Extended Resolution -- Knowledge Compilation Languages as Proof Systems -- The Equivalences of Refutational QRAT -- A SAT-based System for Consistent Query Answering -- Incremental Inprocessing in SAT Solving -- Local Search for Fast Matrix Multiplication -- Speeding Up Assumption-Based SAT -- Simplifying CDCL Clause Database Reduction -- QRAT Polynomially Simulates nforall-Exp+Res -- QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties -- On Computing the Union of MUSes -- Revisiting Graph Width Measures for CNF-Encodings -- DRMaxSAT with MaxHS: First Contact -- Backing Backtracking -- Assessing Heuristic Machine Learning Explanations with Model Counting -- Syntax-Guided Rewrite Rule Enumeration for SMT Solvers -- DRAT-based Bit-Vector Proofs in CVC4 -- Combining Resolution-Path Dependencies with Dependency Learning -- Proof Complexity of Fragments of Long-Distance Q-Resolution -- Guiding High-Performance SAT Solvers with Unsat-Core Predictions -- Verifying Binarized Neural Networks by Angluin-Style Learning -- CrystalBall: Gazing in the Black Box of SAT Solving -- Clausal Abstraction for DQBF -- On Super Strong ETH. .