revived Refute in Mutabelle

tuned;

more scalable zero_var_indexes, depending on canonical order within table;

more benchmarks;

try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways

replace higher-order matching against schematic theorem with dedicated reconstruction method

merged

tuned signature -- avoid spurious Thm.mixed_attribute;

discontinued numbered structure indexes (legacy feature);

tuned proofs;

return outcome code, so that it can be picked up by Mutabelle

align columns in output and keep error log around

offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;

clarified attribute "mono_set": pure declaration, proper export in ML;

misc tuning;

made SML/NJ happy;

more millisecond cleanup

updated documentation

try "smt" as a fallback for ATPs if "metis" fails/times out

more detailed preplay output

tuning

tuning

more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;

tuned;

merged

cascading timeouts in minimizer, part 2

tuning

use "Time.time" rather than milliseconds internally

tune: no need for option

cascading timeouts in minimizer

shortcut binary minimization algorithm

speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half