tuning

fixed conjecture resolution bug for Vampire 1.0's TSTP output

ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded

Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it

drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines

use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.

further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up

reenabled equality proxy in Metis for higher-order reasoning

added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file

reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions