Confluence Competition


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: