## FOL-Skolemizer

If you consult this page for the first time, read Syntax for the Mma-syntax and fof-example for the fof-format of TPTP-syntax. If you use fof-format, don't forget to use double quotation marks at prior and subsequent to the fof-formula. The FOL-Skolemizer only works for pure FOL. Do not use free variables, names, identity or mathematical functions.

Enter a logical formula:

Enter a time constraint in seconds up to 30:

If you want more detailed out insert "1":

The result is ({time in seconds,result}):

The print output is: