killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem

get rid of Skolem cache by performing CNF-conversion after fact selection

always perform "inline" skolemization, polymorphism or not, Skolem cache or not

always perform relevance filtering on original formulas