The CTRS category deals with confluence of conditional term rewrite systems (CTRSs).
The input is an oriented CTRS of type 3, specified in the CTRS format.
A CTRS is confluent if any two convertible terms are joinable. The problem is to answer the question whether the input CTRS is confluent or not.
The output format should follow the same rules as for the TRS category.
The scoring is the same as for the TRS category.