work Krympa Proof minimization tool for equational reasoning Taelja Translates refutations produced by resolution and superposition provers into direct, structured, and readable proofs