TRS Category
This is the oldest CoCo category. It is concerned with confluence of firstorder rewrite systems.
Format
The input is a firstorder rewrite system without conditions, specified in the basic TRS format.
The question to be answered is whether the rewrite system is confluent on
the terms that can be built from the function symbols appearing in
(RULES rulelist)
and variables. The first line of
the output must be

YES
, indicating that the input system is confluent, 
NO
, indicating that the input system is nonconfluent, 
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 justification that is understandable by a human expert.
Examples

(VAR x) (RULES f(a) > b f(f(x)) > a )
The correct answer isNO
and possible outputs includeNO The peak a *< f(f(a)) >* f(b) is not joinable.
andMAYBE

(VAR x y z) (RULES Ap(Ap(Ap(S,x),y),z) > Ap(Ap(x,z),Ap(y,z)) Ap(Ap(K,x),y) > x Ap(I,x) > x )
The correct answer isYES
and a possible output isYES The TRS is orthogonal.
Problem Selection
Problems are selected among those in COPS with the 'trs' tag.