Certification Problem

Input (COPS 1156)

We consider the TRS containing the following rules:

a(b(x)) b(c(x)) (1)
a(c(x)) c(a(x)) (2)
b(b(x)) a(c(x)) (3)
c(b(x)) b(c(x)) (4)
c(b(x)) c(c(x)) (5)
c(c(x)) c(b(x)) (6)
0(1(2(x))) 2(0(1(x))) (7)
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))) (8)

The underlying signature is as follows:

{a/1, b/1, c/1, 0/1, 1/1, 2/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2022)

1 Persistent Decomposition (Many-Sorted)

Non-confluence is proven, because a system induced by the sorts in the following many-sorted sort attachment is not confluent.
a : 1 → 1
b : 1 → 1
c : 1 → 1
0 : 0 → 0
1 : 0 → 0
2 : 0 → 0
The subsystem is

(1.1)

0(1(2(x))) 2(0(1(x))) (7)
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))) (8)

1.1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.

t0 = 0(1(2(2(2(2(2(2(2(2(1(1(1(1(2(x581)))))))))))))))
0(1(2(2(1(2(2(0(1(2(1(1(0(1(0(x581)))))))))))))))
0(1(2(2(1(2(2(2(0(1(1(1(0(1(0(x581)))))))))))))))
2(0(1(2(1(2(2(2(0(1(1(1(0(1(0(x581)))))))))))))))
2(2(0(1(1(2(2(2(0(1(1(1(0(1(0(x581)))))))))))))))
= t4

t0 = 0(1(2(2(2(2(2(2(2(2(1(1(1(1(2(x581)))))))))))))))
2(0(1(2(2(2(2(2(2(2(1(1(1(1(2(x581)))))))))))))))
2(2(0(1(2(2(2(2(2(2(1(1(1(1(2(x581)))))))))))))))
2(2(2(0(1(2(2(2(2(2(1(1(1(1(2(x581)))))))))))))))
2(2(2(2(0(1(2(2(2(2(1(1(1(1(2(x581)))))))))))))))
2(2(2(2(2(0(1(2(2(2(1(1(1(1(2(x581)))))))))))))))
2(2(2(2(2(2(0(1(2(2(1(1(1(1(2(x581)))))))))))))))
2(2(2(2(2(2(2(0(1(2(1(1(1(1(2(x581)))))))))))))))
2(2(2(2(2(2(2(2(0(1(1(1(1(1(2(x581)))))))))))))))
= t8

The two resulting terms cannot be joined for the following reason: