Treating a saturation-based automatic theorem prover (ATP) as a Las Vegas randomized algorithm
is a way to illuminate the chaotic nature of proof search and make it amenable to study by probabilistic tools. On a series of experiments with the ATP Vampire, we showcase some implications of this perspective for prover evaluation.