  Vampire has been for a long time the strongest first-order automated theorem
prover, widely used for hammer-style proof automation in ITPs such as Mizar,
Isabelle, HOL and Coq. In this work, we considerably improve the performance of
Vampire in hammering over the full Mizar library by enhancing its saturation
procedure with efficient neural guidance. In particular, we employ a recursive
neural network classifying the generated clauses based only on their derivation
history. Compared to previous neural methods based on considering the logical
content of the clauses, this leads to large real-time speedup of the neural
guidance. The resulting system shows good learning capability and achieves
state-of-the-art performance on the Mizar library, while proving many theorems
that the related ENIGMA system could not prove in a similar hammering
evaluation.
