## HRS Category

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

- R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, 1998.

### Input

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

### Problem

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.

### Scoring

The scoring is same as the TRS category.