sat: Starting Saturation

$$\mbox{{\tt sat, sat($N$)}}$$

This starts the saturation of the set of clauses/rules in the database according to the chosen strategy. In case a number $N$ is provided, saturation stops after $N$ non-redundant clauses have been generated.

Strategies are defined by calling the sa ${<}\mbox{{\tt xx}}{>}$ commands for setting the various parameters. If no settings are provided explicitly, the directory-specific default settings as contained in the local defaults file are assumed.

Imprint | Data Protection