Confluence Competition

HRS Category

The HRS category deals with confluence of higher-order rewrite systems (HRSs) described in

available here.


The input is a pattern rewrite system, specified in the HRS format.


An HRS is confluent if any two convertible terms are joinable modulo beta-eta-equivalence. The problem is to answer the question whether the input HRS is confluent or not confluent.

Problem Selection

Problems with tags 'prs' and 'literature' in our problem database (Cops) are used. If the number of such problems exceeds 100, then 100 problems are selected from these problems; otherwise, all of them are considered. Our advisory board performs the selection using a random number.

Output Format

The output format should follow the same rule as that of the TRS category.


The scoring is same as the TRS category.