GCR Category
The GCR category is concerned with groundconfluence of manysorted term rewrite systems (MSTRSs).
Format
The input is a manysorted firstorder rewrite system without conditions, specified in the MSTRS format.
The question to be answered is whether the rewrite system is confluent
on all wellsorted ground terms that can be built from the function symbols
in the (SIG funlist)
declaration. 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) (SIG (a > 0) (b > 0) (c > 0) (f 0 0 > 1) ) (RULES a > b f(b,b) > f(a,a) f(x,a) > f(a,a) )
The correct answer isNO
and a possible output isNO The peak f(c,b) *< f(c,a) >* f(a,a) is not joinable since f(c,b) is not among the reducts { f(a,a), f(b,a), f(b,a), f(b,b) } of f(a,a).

(SIG (0 > Nat) (s Nat > Nat) (eq Nat Nat > Bool) (true > Bool) (false > Bool) ) (RULES eq(x,x) > true eq(0,s(x)) > false eq(s(x),0) > false eq(s(x),s(y)) > eq(x,y) eq(x,y) > eq(y,x) )
The correct answer isYES
and a possible output isYES Groundconfluence can be shown by rewriting induction, as explained in the FSCD 2016 paper of Takahito Aoto and Yoshihito Toyama.
Problem Selection
Problems are selected among those in COPS with the 'trs' or the 'mstrs' tag. The former are transformed into MSTRSs with a single sort, prior to passing them to competing tools.