Problems

The unit of information we can describe are problems. A problem may not only contain formulae or clauses but also information on parameter settings for various provers or some specific proofs.

problem	::=	begin_problem(identifier).
		description
		logical_part
		{settings}$^\ast$
		end_problem.

Note that the description part as well as the logical part are mandatory.