further worked around LEO-II parser limitation, with eta-expansion

use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)

no need for existential witnesses for sorts in TFF and THF formats

mangle "undefined"

tuning -- remove useless function (at this point combinators are already in)

remove spurious message

give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts

merged