ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

Karel Chvalovský, Jan Jakubův, Martin Suda +1

We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation wh…