BliStr: The Blind Strategymaker
  BliStr is a system that automatically develops strategies for E prover on a
large set of problems. The main idea is to interleave (i) iterated
low-timelimit local search for new strategies on small sets of similar easy
problems with (ii) higher-timelimit evaluation of the new strategies on all
problems. The accumulated results of the global higher-timelimit runs are used
to define and evolve the notion of "similar easy problems", and to control the
selection of the next strategy to be improved. The technique was used to
significantly strengthen the set of E strategies used by the MaLARea, PS-E,
E-MaLeS, and E systems in the CASC@Turing 2012 competition, particularly in the
Mizar division. Similar improvement was obtained on the problems created from
the Flyspeck corpus.
