Settings

The idea to include settings into the problem file format is to enable people to reproduce specific proofs that depend on particular input settings of the respective prover.

settings	::=	list_of_general_settings {setting_entry}+ end_of_list. |
		list_of_settings(setting_label).  {* text  *} end_of_list.
setting_entry	::=	hypothesis[label {,label}$^\ast$].
setting_label	::=	KIV | LEM | OTTER | PROTEIN | SATURATE | 3TAP | SETHEO | SPASS

The labels name the following systems: KIV [8], LEM [4], OTTER [6], PROTEIN [1], SATURATE [3], $_{3}\!T^{\!\!\textstyle A}\!\!P$