Im obigen Beispiel soll die Übereinstimmung der booleschen Funktionen und geprüft werden. Wie die Rechnung zeigt, kann es nicht gelingen, für a,b eine Wertebelegung zu finden, für die sich ergibt, da der Ausdruck stets 0 ist. Das kann mit einem normalen SAT-1 Löser gemacht werden.
In den entsprechenden Verifikationswerkzeugen findet der Widerspruchsbeweis auch auf andere Weise statt. Grundsätzlich geeignet sind SAT-Löser, BDD-basierte Löser und auch der D-Algorithmus, der im Abschnitt Test erläutert wird. Hier werden Signale vom Ausgang zu den Eingängen propagiert, bis sich entweder eine gültige Eingangsbelegung oder ein Widerspruch ergibt.