Model Generation Theorem Prover,
MGTP