e has been integrated into several other theorem provers. it is, with vampire, spass, cvc4, and z3, at the core of isabelle's "sledgehammer" strategy. e also is the reasoning engine in sine and leo-ii and used as the clausification system for iprover.