This communication presents two packages, Ming and Collapse, that were created using Prover9/Mace4 as an oracle and one that manipulates Prover9's proof, sP9. Ming has the goal of finding the bases of a given set of axioms, Collapse search for a new axiom of a theory that substitutes a given set of axioms of that theory and SP9 tries to reduce the length of a Prover9 proof.