The CPF-CTRS category deals with certified (non-)confluence proofs of conditional term rewrite systems.
The problem is to produce a formalized
(non-)confluence proof of the input CTRS.
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 CTRS category are selected.