SKOLEMS3 : WFFOPSKOLEMS3 is a wff operation.
Skolemize a wff using method S3. At the moment it takes only
those free variables which are universally quantified somewhere before,
all other variables are considered to be constants.
See page 127 of Andrews' book.
If equivalences are present, you must eliminate them first by REW-EQUIV.
The calling scheme for SKOLEMS3 is:
(SKOLEMS3 GWFF UNIVFLAG)
The result is of type GWFF0.
The arguments have the following meaning:
GWFF : Wff to be Skolemized
UNIVFLAG : If NIL, existential quantifiers will be replaced
TPS documentation homepage