considero la negazione della formula e la converto in CNF
considero l’unione di clausole corrispondente
se esce fuori il $\square$, allora la formula negata è insoddisfacibile e quindi la formula iniziale è una tautologia
1
2
3
4
5
6