CTRS Category

The CTRS category deals with confluence of conditional term rewrite systems (CTRSs).

Input

The input is an oriented CTRS of type 3, specified in the CTRS format.

Problem

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.

Problem Selection

100 problems are selected from problems with tags 'oriented', '3_ctrs', 'ctrs' and 'literature' in our problem database (Cops). Our advisory board performs the selection using a random number.

Output Format

The output format should follow the same rules as for the TRS category.

Scoring

The scoring is the same as for the TRS category.