UN Category

The UN category is the combined category of UNR, UNC and NFP categories. The category runs its component categories and the optimal answer is rewarded by the weighted scoring.

Input

The input is a TRS, specified in basic TRS format or in extended TRS format.

Problem

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.)

Problem Selection

Problems are selected from those with tags 'trs' and 'literature' in our problem database (Cops). The same collection of TRSs is used for UNR category, UNC category and NFP category.

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.

Output Format

See the corresponding sections of UNR category, UNC category and NFP category.

Scoring

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: -NFP, column: UNR). The missing table entries correspond to inconsistent outputs.