Streamline question answering

Many small things to improve user experience with question answering.

The new-old mode is newly invoked via -qa plain (previously, -qa answer_literal) and is mostly separate in functionality from -qa synthesis although code sharing, where available, was kept in place.

-qa plain is now compatible with AVATAR.

Disjunctive answers (with don't care variables, whose skope is clarified using a "∀") are supported.

If a skolem appears in the answer, the user is told where it came from.

Forall-exists questions are supported. Using a trick from synthesis, the forall block gets skolemized, but the skolems are recorded and replaced by the original variables back in the answer. -qa plain makes the user aware of these by starting the answer with a "λ" and binding these variables.

The original variable names from the question are kept from the parser and used to "pretty print" the answer.

Some non-trivial changes to properly track "derived from goal" (regardless of question answering), which are used to decide on "Theorem" vs "ContradictoryAxioms" and trigger some soundness checks in debug mode.

It is possible to specify what an answer should not look like, in order to get a different one. This can be used (through iterative vampire invocations) to get multiple answers. (Doing this in one run would be technically more involved and wouldn't be as reliable anyway.)

Formulas of Inference == INPUT have their unit input type shown as well (in parenthesis):

1. ? [X0] : p(X0) [input(axiom)]
3. ? [X0] : p(X0) [input(conjecture)]

So that the negated_conjecture inference which follows does not come out of the blue for the user.

Maybe there is something I forgot?

vprover / vampire

Streamline question answering #566