merged

don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

fix Mirabelle timeout

make Mirabelle happy

fix bug in the newly introduced "bound concealing" code

handle division by zero gracefully (used to raise Unordered later on)

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses

fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)

handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

revert exception throwing in FOL_SOLVE, since they're not caught anyway