There are a number of well-known assumptions about automated theorem proving such as "proofs usually only use a small proportion of the given axioms to prove a goal". In this talk we present a statistical analysis of a large number of Vampire proofs and use this to investigate a number of these assumptions coming from ATP folklore.

Testing ATP folklore: a statistical analysis of Vampire proofs.