SKOLEMS1 : WFFOPSKOLEMS1 is a wff operation.
Skolemize a wff using method S1. See page 127 of Andrews' book.
If equivalences are present, you must eliminate them first by REW-EQUIV.
The calling scheme for SKOLEMS1 is:
(SKOLEMS1 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