Certification Problem

Input (COPS 765)

We consider the TRS containing the following rules:

xor(x,0) x (1)
xor(0,x) x (2)
xor(x,x) 0 (3)
and(x,0) 0 (4)
and(0,x) 0 (5)
and(x,1) x (6)
and(1,x) x (7)
and(x,x) x (8)
xor(xor(x,y),z) xor(x,xor(y,z)) (9)
xor(x,xor(y,z)) xor(y,xor(x,z)) (10)
xor(x,y) xor(y,x) (11)
xor(x,xor(x,y)) y (12)
and(and(x,y),z) and(x,and(y,z)) (13)
and(x,and(y,z)) and(y,and(x,z)) (14)
and(x,y) and(y,x) (15)
and(x,and(x,y)) and(x,y) (16)
and(x,xor(y,z)) xor(and(x,y),xor(x,z)) (17)
and(xor(x,y),z) xor(and(x,z),and(y,z)) (18)

The underlying signature is as follows:

{xor/2, 0/0, and/2, 1/0}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ACP @ CoCo 2022)

1 Non-Joinable Fork

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

t0 = and(0,xor(c_1,c_2))
xor(and(0,c_1),xor(0,c_2))
xor(0,xor(0,c_2))
c_2
= t3

t0 = and(0,xor(c_1,c_2))
0
= t1

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