The CPF-CTRS category deals with certified (non-)confluence proofs of conditional term rewrite systems. It is a component category of the CPF category.
The competition uses the same collection of problems as those for the CTRS category.
The problem is to answer a certified proof of the question whether the input CTRS is confluent or not.
The same collection of problems as CTRS category is used.
The output format is the same as for the CPF-TRS category.
The scoring is the same as for the TRS category.