Categories
In all categories the input consists of a suitable problem from the
ARI database. The first line of the output
must be YES or NO, and
the output must be followed either by a
certificate that can be passed on to a certifier for verification, or
a justification that is understandable by a human expert.
Any other first output line (e.g. MAYBE) indicates that the
tool could not determine the status of the input problem.
Two different certifiers can be used: