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: