All about Eve

Eve (Eve Verifies Equality) is a tool to check the validity of a conjecture s ≈ t against a set of axioms E. In case the conjecture can be shown valid, a proof of s ≈ t using the axioms E is provided.
Internally, Eve attempts to derive a complete system R equivalent to E using MKBtt. If such a system can be computed and the R-normal forms of s and t are equal, the obtained rewrite proof is transformed to an equational proof applying only axioms in E.