Certification Problem

Input (COPS 592)

We consider the TRS containing the following rules:

not(true) false (1)
not(false) true (2)
or(true,y) true (3)
or(x,true) true (4)
or(false,false) false (5)
and(true,true) true (6)
and(x,true) x (7)
and(true,y) y (8)
and(false,false) false (9)
not(and(x,y)) or(not(x),not(y)) (10)
not(or(x,y)) and(not(x),not(y)) (11)

The underlying signature is as follows:

{not/1, true/0, false/0, or/2, and/2}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2023)

1 Non-Joinable Fork

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

t0 = not(or(true,y))
not(true)
false
= t2

t0 = not(or(true,y))
and(not(true),not(y))
and(false,not(y))
= t2

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