Algoritmo Davis-Putnam

Per semplificare la domanda ho già applicato l'algoritmo di una formula proposizionale.

Sono arrivato al seguente insieme di clausole:
{ {not (b), not (d)} , {not (e)} }

Quali sono i passi successivi?

Ottengo alla fine {} o {[]} ? Ovvero soddisfacibile o non soddisfacibile ?

Grazie mille!