more functions in Formula;
variant-checking, skolemization, Util_tptp and tools updated to use Formulas