TRS Category

The TRS category deals with confluence of first-order term rewrite systems.

Input

The input is a TRS, specified in the basic TRS format. Each function symbol in the input TRS has a fixed arity and the input TRS satisfies the usual variable conditions.

Problem

A TRS is confluent if any two convertible terms are joinable. The problem is to answer the question whether the input TRS is confluent or not.

Problem Selection

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

Output Format

The first line of the output should be YES (indicating that the input system is confluent), NO (indicating that the input system is non-confluent); any other answer (e.g., MAYBE) indicates that the tool could not determine the status of the input problem. In the first two cases, the output must be followed by an expert-readable justification for the answer. An example of acceptable output is as follows:

YES

Input problem:
  +(x,0()) -> x
  +(x,s(y)) -> s(+(x,y))

The input problem is orthogonal.

Scoring

The score is computed in percent of solved problems (i.e. number of YES/NO answers). In case of a draw there might be more winners. The tool with the maximal score wins.