The description part should help to understand what the problem is about. In particular, the logic part is mandatory, if non-standard quantifiers or operators are used.
| description | ::= | list_of_descriptions. |
| name( {* text *} ). | ||
| author( {* text *} ). | ||
| {version( {* text *} ).} | ||
| {logic( {* text *} ).} | ||
| status(log_state). | ||
| description( {* text *} ). | ||
| {date( {* text *} ).} | ||
| end_of_list. | ||
| log_state | ::= | satisfiable | unsatisfiable | unknown |