MANSEX

MANSEX (Multiple ANSwer EXtraction) is a system the interprets a conjecture with outermost existentially quantified variables as a question, and reports bindings for the variables in proofs of the conjecture, as answers to the question. Multiple answers are extracted by iterative calls to a base system that can report the bindings for the variables in a single proof of the conjecture, as a single answer to the question. At each iteration the conjecture is augmented to deny previous answers.

MANSEX is implemented in perl, and by default uses the SNARK ATP system to prove the individual conjectures and provide single answers.