Confluence Competition

## Commutation Category

CoCo 2019 will feature a new competition category on commutation problems.

### Format

Commutation problems are incorporated into COPS as follows:

```(PROBLEM COMMUTATION)
(COPS number1 number2)
(COMMENT string)
```
where `number1` and `number2` refer to existing problems in TRS format. To ensure that the union of the two TRSs is a proper TRS, function symbols in TRS `number2` that appear as variable or as function symbol with a different arity in TRS `number1` are renamed (by adding a ′). The same holds for variables in TRS `number2` that occur as function symbol in TRS `number1`. The renaming program is available.

For the competition, the `(COPS number1 number2)` declaration will be inlined (after renaming), before the problem is passed to participating tools. The inlining program is available.

The question to be answered is whether the two TRSs commute: `YES` if they do, `NO` if they do not.

### Examples

1. ```(PROBLEM COMMUTATION)
(COPS 532 68)
(COMMENT this comment will be removed)
```
which expands to
```(PROBLEM COMMUTATION)
(COMMENT COPS 532 68)
(VAR w x y z)
(RULES
+(x,0()) -> x
-(0()) -> 0()
-(-(x)) -> x
-(+(x,y)) -> +(-(x),-(y))
+(x,-(x)) -> 0()
+(+(x,-(x)),y) -> y
*(x,0()) -> 0()
*(x,1()) -> x
*(x,-(y)) -> -(*(x,y))
*(*(x,-(y)),z) -> *(-(*(x,y)),z)
*(x,+(y,z)) -> +(*(x,y),*(x,z))
*(*(x,+(y,z)),w) -> +(*(*(x,y),w),*(*(x,z),w))
+(+(x,y),z) -> +(x,+(y,z))
+(x,+(y,z)) -> +(+(x,y),z)
+(x,y) -> +(y,x)
*(*(x,y),z) -> *(x,*(y,z))
*(x,*(y,z)) -> *(*(x,y),z)
*(x,y) -> *(y,x)
)
(VAR x)
(RULES
b(w'(x)) -> w'(w'(w'(b(x))))
w'(b(x)) -> b(x)
b(b(x)) -> w'(w'(w'(w'(x))))
w'(w'(x)) -> w'(x)
)
```
The correct answer is `YES`.
2. ```(PROBLEM COMMUTATION)
(COPS 82 80)
(COMMENT this comment will be removed)
```
which expands to
```(PROBLEM COMMUTATION)
(COMMENT COPS 82 80)
(VAR x)
(RULES
f(a) -> f(f(a))
f(x) -> f(a)
)
(VAR )
(RULES
a -> f'(a,b)
f'(a,b) -> f'(b,a)
)
```
The correct answer is `YES`.

### Problem Selection

Problems are selected among those in COPS with the 'commutation' tag.