Certification Problem

Input (COPS 950)

We consider the TRS containing the following rules:

0(0(1(0(x)))) 0(2(0(0(3(1(x)))))) (1)
0(0(1(0(x)))) 0(2(0(4(1(0(x)))))) (2)
0(0(1(0(x)))) 2(0(0(0(2(1(x)))))) (3)
3(0(1(0(x)))) 0(2(3(1(0(x))))) (4)
3(0(1(0(x)))) 3(1(0(0(2(x))))) (5)
3(0(1(0(x)))) 3(1(1(0(0(x))))) (6)
3(0(1(0(x)))) 3(1(2(0(0(x))))) (7)
3(0(1(0(x)))) 3(1(5(0(0(x))))) (8)
3(0(1(0(x)))) 3(5(1(0(0(x))))) (9)
3(0(1(0(x)))) 5(0(3(1(0(x))))) (10)
3(0(1(0(x)))) 2(0(2(3(1(0(x)))))) (11)
3(0(1(0(x)))) 2(2(0(3(1(0(x)))))) (12)
3(0(1(0(x)))) 3(1(5(0(0(0(x)))))) (13)
3(0(1(0(x)))) 3(1(5(0(2(0(x)))))) (14)
3(0(1(0(x)))) 3(1(5(1(0(0(x)))))) (15)
3(0(1(0(x)))) 3(1(5(2(0(0(x)))))) (16)
3(0(1(0(x)))) 3(1(5(5(0(0(x)))))) (17)
3(0(1(0(x)))) 3(2(2(1(0(0(x)))))) (18)
3(0(1(0(x)))) 3(5(1(0(0(2(x)))))) (19)
3(0(1(0(x)))) 3(5(1(5(0(0(x)))))) (20)
3(0(1(0(x)))) 5(1(1(3(0(0(x)))))) (21)
3(4(1(0(x)))) 3(1(2(4(0(x))))) (22)
3(4(1(0(x)))) 3(1(4(0(2(x))))) (23)
3(4(1(0(x)))) 3(1(5(4(0(x))))) (24)
3(4(1(0(x)))) 3(4(2(1(0(x))))) (25)
3(4(1(0(x)))) 3(1(1(5(4(0(x)))))) (26)
3(4(1(0(x)))) 3(1(2(1(4(0(x)))))) (27)
3(4(1(0(x)))) 3(1(2(5(4(0(x)))))) (28)
3(4(1(0(x)))) 3(1(4(2(0(2(x)))))) (29)
3(4(1(0(x)))) 3(1(5(4(0(2(x)))))) (30)
3(4(1(0(x)))) 3(1(5(5(4(0(x)))))) (31)
3(4(1(0(x)))) 3(4(2(1(1(0(x)))))) (32)
3(4(1(0(x)))) 3(4(5(1(2(0(x)))))) (33)
0(1(4(1(0(x))))) 0(1(1(4(0(2(x)))))) (34)
0(2(0(1(0(x))))) 0(2(0(0(3(1(x)))))) (35)
0(2(0(1(0(x))))) 2(0(0(0(3(1(x)))))) (36)
0(3(0(1(0(x))))) 0(0(3(1(3(0(x)))))) (37)
0(3(0(1(0(x))))) 0(0(3(3(1(0(x)))))) (38)
0(3(0(1(0(x))))) 0(0(3(5(1(0(x)))))) (39)
0(3(0(1(0(x))))) 2(0(0(3(1(0(x)))))) (40)
0(3(4(1(0(x))))) 0(2(0(4(3(1(x)))))) (41)
0(5(0(1(0(x))))) 0(0(0(1(5(2(x)))))) (42)
0(5(0(1(0(x))))) 0(0(1(5(1(0(x)))))) (43)
0(5(0(1(0(x))))) 0(2(0(0(1(5(x)))))) (44)
3(0(1(0(0(x))))) 3(1(3(0(0(0(x)))))) (45)
3(0(1(1(0(x))))) 3(1(0(1(2(0(x)))))) (46)
3(0(2(1(0(x))))) 2(0(3(1(1(0(x)))))) (47)
3(0(2(1(0(x))))) 2(3(1(5(0(0(x)))))) (48)
3(0(2(1(0(x))))) 3(1(2(0(1(0(x)))))) (49)
3(0(2(1(0(x))))) 3(1(2(0(5(0(x)))))) (50)
3(0(5(1(0(x))))) 3(1(5(2(0(0(x)))))) (51)
3(1(0(1(0(x))))) 2(0(3(1(1(0(x)))))) (52)
3(1(0(1(0(x))))) 3(1(1(1(0(0(x)))))) (53)
3(1(0(1(0(x))))) 3(1(2(1(0(0(x)))))) (54)
3(1(4(1(0(x))))) 3(1(2(1(4(0(x)))))) (55)
3(1(4(1(0(x))))) 3(1(5(1(4(0(x)))))) (56)
3(2(0(1(0(x))))) 0(2(3(1(5(0(x)))))) (57)
3(2(0(1(0(x))))) 2(0(3(1(1(0(x)))))) (58)
3(3(0(1(0(x))))) 3(1(2(0(3(0(x)))))) (59)
3(3(0(1(0(x))))) 3(1(2(3(0(0(x)))))) (60)
3(3(4(1(0(x))))) 3(1(2(4(3(0(x)))))) (61)
3(3(4(1(0(x))))) 3(1(3(4(0(2(x)))))) (62)
3(3(4(1(0(x))))) 3(1(4(3(1(0(x)))))) (63)
3(4(0(1(0(x))))) 0(2(4(1(3(0(x)))))) (64)
3(4(0(1(0(x))))) 3(1(4(0(0(2(x)))))) (65)
3(4(0(1(0(x))))) 3(2(0(4(1(0(x)))))) (66)
3(4(4(1(0(x))))) 3(1(1(4(4(0(x)))))) (67)

The underlying signature is as follows:

{0/1, 1/1, 2/1, 3/1, 4/1, 5/1}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2021)

1 Non-Joinable Fork

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

t0 = 0(0(1(0(x))))
0(2(0(0(3(1(x))))))
= t1

t0 = 0(0(1(0(x))))
0(2(0(4(1(0(x))))))
= t1

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