1

¬x

¬xy

¬x¬y

¬x¬yz

┴ Rx (x + y + z)

┴ Rx (¬x + z + ¬t)

┴ Rx (x + ¬y + t)

┴ Rx (x + ¬y + ¬t)

┴ Rx (y + z + t)

┴ Ry (y + z)

┴ Ry (¬y + t)

┴ Ry (¬y + ¬t)

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

(¬t) Rt (t)

(t) Rt (¬t)

┴ Rz z

┴ Rz (z + t)