The CPF-TRS category deals with certified (non-)confluence proofs of first-order term rewrite systems.
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
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.
The same problems as in the TRS category are selected.