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

speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"

work around atomization failures

fiddle with the fudge factors, to get similar results as before

perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs

fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)

generate correct names for "$true" and "$false"; this was lost somewhere in the non-clausification

don't assume canonical rule format

avoid "clause" and "cnf" terminology where it no longer makes sense

"axiom_clauses" -> "axioms" (these are no longer clauses)

remove the "extra_clauses" business introduced in 19a5f1c8a844; it isn't working reliably because of: * relevance_override * it is ignored anyway by TPTP generator A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable

adapting output for first solution

removing pointless type information in internal prolog terms

cleaning example file; more natural ordering of variable names

improving translation to prolog; restoring terms from prolog output; adding tracing support

working on parser for prolog reponse

querying for multiple solutions in values command for prolog execution

correcting scanning

adding values command and parsing prolog output

adding example file for prolog code generation; adding prolog code generation example to IsaMakefile

adding a mockup version for prolog code generation

exporting retrieval function for graph of introduction rules in the predicate compiler core

merged

rebinding ref is illegal

tuned example

intermediate operation avoids invariance problem in Scala