move "nice names" from Metis to TPTP format

move functions not needed by Metis out of "Metis_Clauses"

no setup is necessary anymore

adapt call

remove obsolete component of CNF clause tuple (and reorder it)

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

merged