In a754baf, some of the paramodulation logic was reportedly moved to the E prover module, whereupon param1 no longer succeeds. One possible way to fix this without apparent side effects is to uncomment the removed decide_ke clauses in paramodulation.mod. Is modularity, with the E certification code or otherwise, at risk?
In a754baf, some of the paramodulation logic was reportedly moved to the E prover module, whereupon
param1no longer succeeds. One possible way to fix this without apparent side effects is to uncomment the removeddecide_keclauses inparamodulation.mod. Is modularity, with the E certification code or otherwise, at risk?