SKOLEM-TERM : FLAVORSKOLEM-TERM is a flavor.
A skolem-term label contains both a skolem term, which is a
skolem function applied to some free variables (if any), and a parameter,
which is a new constant. Skolem-terms may be printed in either of the
two ways: the flag SHOW-SKOLEM controls how they are printed.
TPS documentation homepage