ENIGMAWatch: ProofWatch Meets ENIGMA
  In this work we describe a new learning-based proof guidance -- ENIGMAWatch
-- for saturation-style first-order theorem provers. ENIGMAWatch combines two
guiding approaches for the given-clause selection implemented for the E ATP
system: ProofWatch and ENIGMA. ProofWatch is motivated by the watchlist (hints)
method and based on symbolic matching of multiple related proofs, while ENIGMA
is based on statistical machine learning. The two methods are combined by using
the evolving information about symbolic proof matching as an additional
information that characterizes the saturation-style proof search for the
statistical learning methods. The new system is experimentally evaluated on a
large set of problems from the Mizar Library. We show that the added
proof-matching information is considered important by the statistical machine
learners, and that it leads to improvements in E's Performance over ProofWatch
and ENIGMA.
