Make equations recognised symmetrically when resolving nodes, gather and resolve produced subproofs with inequalities