## FOL-ModelCheck

If you consult this page for the first time, read Syntax. Do not use free variables, names, identity or mathematical functions.

Enter a logical formula:

Enter a number as upperbound for the domain:

Your input in TraditionalForm (including quantifier definitions and omitted →, ≡, ⊽, ⊼, ⊻):

Enter a time constraint in seconds up to 300:

You may try other forms of presentation of models by entering "0" or "1":
Modellevel 0 provides a model that also includes tuples satisfying negated predicates that are neccessary part of the returned model.
Modellevel 1 provides even more detailed distinctions within a model by separating neccessary, optional and free features of interpretations.

In case no modellevel or modellevel 0 is chosen, "D" abbreviates "domain" and interpretations are presented as tables omitting brackets of sets. "" indicates the empty set.

$\mathrm{result}$