The TRS category deals with confluence of first-order term rewrite systems.
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.
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.
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.
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.