  In this work in progress, we demonstrate a new use-case for the ENIGMA
system. The ENIGMA system using the XGBoost implementation of gradient boosted
decision trees has demonstrated high capability to learn to guide the E theorem
prover's inferences in real-time. Here, we strip E to the bare bones: we
replace the KBO term ordering with an identity relation as the minimal possible
ordering, disable literal selection, and replace evolved strategies with a
simple combination of the clause weight and FIFO (first in first out) clause
evaluation functions. We experimentally demonstrate that ENIGMA can learn to
guide E as well as the smart, evolved strategies even without these standard
automated theorem prover functionalities. To this end, we experiment with
XGBoost's meta-parameters over a dozen loops.
