The CPF-TRS category deals with certified (non-)confluence proofs of first-order term rewrite systems. It is a component category of the CPF category.
The competition uses the same collection of problems as those for the TRS category.
The problem is to answer a formalized (non-)confluence proof of the question whether the input TRS is confluent or not.
The same collection of problems as TRS category is used.
Tools should output certifiable proofs as well as the result of certification: YES followed by a certifiable proof (e.g. a proof in cpf format) if the confluence proof is certified, and NO followed by a certifiable proof if the non-confluence proof is certified.
The scoring is same as for the TRS category.