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