Confluence Competition

## Categories – COM

The COM category deals with commutation problems.

### Format

The input is an commutation problem specified in the ARI multiple-TRS format. The question to be answered is whether the two rewrite systems in the problem commute.

### Examples

1. ```; origin COPS 532 68
(format TRS :number 2)
(fun * 2)
(fun + 2)
(fun - 1)
(fun 0 0)
(fun 1 0)
(fun b 1)
(fun w' 1)
(rule (+ x 0) x)
(rule (- 0) 0)
(rule (- (- x)) x)
(rule (- (+ x y)) (+ (- x) (- y)))
(rule (+ x (- x)) 0)
(rule (+ (+ x (- x)) y) y)
(rule (* x 0) 0)
(rule (* x 1) x)
(rule (* x (- y)) (- (* x y)))
(rule (* (* x (- y)) z) (* (- (* x y)) z))
(rule (* x (+ y z)) (+ (* x y) (* x z)))
(rule (* (* x (+ y z)) w) (+ (* (* x y) w) (* (* x z) w)))
(rule (+ (+ x y) z) (+ x (+ y z)))
(rule (+ x (+ y z)) (+ (+ x y) z))
(rule (+ x y) (+ y x))
(rule (* (* x y) z) (* x (* y z)))
(rule (* x (* y z)) (* (* x y) z))
(rule (* x y) (* y x))
(rule (b (w' x)) (w' (w' (w' (b x)))) :index 2)
(rule (w' (b x)) (b x) :index 2)
(rule (b (b x)) (w' (w' (w' (w' x)))) :index 2)
(rule (w' (w' x)) (w' x) :index 2)
```
The correct answer is `YES`.
2. ```; origin COPS 82 80
(format TRS :number 2)
(fun a 0)
(fun f 1)
(fun b 0)
(fun f' 2)
(rule (f a) (f (f a)))
(rule (f x) (f a))
(rule a (f' a b) :index 2)
(rule (f' a b) (f' b a) :index 2)
```
The correct answer is `YES`.

### Problem Selection

Problems are selected from those in the ARI database with the '2trs' tag.