Confluence Competition

## GCR Category

The GCR category is concerned with ground-confluence of many-sorted term rewrite systems (MSTRSs).

### Format

The input is a many-sorted first-order rewrite system without conditions, specified in the MSTRS format.

The question to be answered is whether the rewrite system is confluent on all well-sorted 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 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 justification that is understandable by a human expert.

### Examples

1. ```(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 is `NO` and a possible output is
```NO

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).
```
2. ```(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 is `YES` and a possible output is
```YES

Ground-confluence 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.