make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive

reintroduce the higher penalty for skolems

tuning

comment tuning

get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts

fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)

make it more likely that induction rules are picked up by Sledgehammer

generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs

add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already

instantiate induction rules automatically