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.