## CPF-TRS Category

The CPF-TRS category deals with certified (non-)confluence proofs of first-order term rewrite systems.

### Format

The problem is to produce a *formalized* (non-)confluence proof of
the input TRS. Tools should output
certifiable proofs as well as the result of certification:
`YES`

followed by a certifiable proof if the confluence proof is
certified, and `NO`

followed by a certifiable proof if the
non-confluence proof is certified.

As there is currently only one certifier, CeTA, certifiable proofs must be in the certifiable proof format (CPF). An example of the output can be found here.

### Problem Selection

The same problems as in the TRS category are selected.