CPF-CTRS Category

The CPF-CTRS category deals with certified (non-)confluence proofs of conditional term rewrite systems. It is a component category of the CPF category.

Input

The competition uses the same collection of problems as those for the CTRS category.

Problem

The problem is to answer a certified proof of the question whether the input CTRS is confluent or not.

Problem Selection

The same collection of problems as CTRS category is used.

Output Format

The output format is the same as for the CPF-TRS category.

Scoring

The scoring is the same as for the TRS category.