1

¬x

¬x

¬x·z

(¬x + ¬y + z) Rx (x + y + z + t)

(¬x + ¬y + z) Rx (x + ¬y + z)

┴ Rx (x + y + z)

(x + ¬y + z) Rx (¬x + ¬y + z)

┴ Rx (¬x + z + t)

(x + y + z) Rx (¬x + y + z + u)

(¬y + z) Ry (y + z + t)

(y + z) Ry (¬y + z)

(¬y + z) Ry (y + z)

┴ Rz (y + z + t)

┴ Rz (¬y + z)

┴ Rz (y + z)