The SAT Competition series, which started in 2002, is arguably one of the central driving forces of SAT solver development and its benchmark suites have been used in evaluations of hundreds of research papers. This article provides an overview of the

The time evolution of a quantum wave packet in the linear gravity potential is known as Quantum Bouncing Ball. The qBounce collaboration recently observed such a system by dropping wave packets of ultracold neutrons by a height of roughly 30 microns. In this article, space and momentum spectra as well as Wigner functions of the neutron wave functions in the gravitational field of the Earth are analyzed. We investigate the quantum states in the “preparation region”, into which they transition after exiting a narrow double-mirror system and where we would expect to observe free fall and bounces in classical physics. For this, we start from the stationary solutions and eigenvalues of the Schrödinger equation in terms of Airy functions and their zeros. Subsequently, we examine space and momentum distributions as well as Wigner functions in phase space for pure and mixed quantum states. The possible influence of Yukawa-like forces for small distances of several micrometers from the mirror is included through first order perturbation calculations. Those allow us to study the resulting modifications of space and momentum distributions, and phase space functions.

The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are still under development, so we discuss them at a high level in this paper. We also describe the implementation of the calculus in the Vampire theorem prover, the strategy schedule construction and several empirical performance statistics.

We re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.