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

avoid "ATP Error: Error: blah" style messages

avoid "_def_raw" theorems

better error and minimizer output

deal with chained facts more gracefully