added lemma

added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files

comment

disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP

improve completeness of polymorphic encodings

mangle tag bound declarations properly

fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings

make sure that if slicing is disabled, a non-SOS slice is chosen

honor TFF Implicit

make polymorphic encodings more complete

make default unsound mode less unsound

make TFF output less explicit where possible

use more appropriate encoding for Z3 TPTP, as confirmed by evaluation

added one more known Z3 failure

added config options to control two aspects of the translation, for evaluation purposes

added choice operator output for Satallax

rationalized option names -- mono becomes raw_mono and mangled becomes mono

handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards

avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics

fixed bang encoding detection of which types to encode

lemma Compl_insert: "- insert x A = (-A) - {x}"

avoid variable clashes by properly incrementing indices

improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

include chained facts for minimizer, otherwise it won't work