Recall that NFP implies UNC and UNC implies UNR. The goal is to pinpoint the problem as precisely as possible inside this hierarchy. (The perfect answers are NFP; not NFP and UNC; not UNC and UNR; and not UNR.)
Only non-confluent problems are considered, where non-confluence is identified mechanically or manually. Thus, the problems are selected from those that can be proved non-confluent by some CoCo 2016 participants, Cops ♯24, ♯26, ♯47, ♯52, ♯54, ♯56, ♯57, ♯58 and ♯497. (The list may be updated by newly submitted problems.)
If the number of such problems exceeds 100, then 100 problems are selected from these problems; otherwise, all of them are considered. Our advisory board performs the selection using a random number.
In order to take logical implications into account, points will be awarded for each correct answer according to the following table:
Here, the column corresponds to the strongest property proved by the
tool, and the row corresponds to the weakest property refuted by the
tool. For example, a tool that proves UNR, disproves NFP, but doesn't
decide UNC, would score 4 points (row:
The missing table entries correspond to inconsistent outputs.