Vampire is the first order theorem proving winning the main division of the world championship in theorem proving CASC year after year since 2002.

Like all other modern theorem provers, it has a mode using a portfolio of strategies (aka strategy scheduling).

This presentation describes Spider - a previously undisclosed strategy scheduler that was key to Vampire's success at competitions and generally to its deductive power. Its first version was developed in 2003.

The current version of Spider uses the methodology RIO (Randomize, Improve, Optimize) developed in 2013.

Spider was one of the first examples of applications of machine learning in theorem proving. Unlike previous applications of machine learning focused on problems and proofs, (Jörg Denzinger, Stephan Schulz: Learning Domain Knowledge to Improve Theorem Proving. CADE 1996; Stephan Schulz: Learning Search Control Knowledge for Equational Theorem Proving. KI/ÖGAI 2001), Spider is learning search strategies.

Despite 20-year long history of Spider, this is its first ever public description.