Das Ergebnis beider Varianten ist praktisch dasselbe - in der Version mit Vorbedingung hat man nur einen Haufen zusätzlicher Axiome, die aufgrund der unerfüllten Prämisse überflüssig sind. Um eines der Axiome anzuwenden, muss man aber so oder so diese Vorbedingung prüfen - entweder um zu sehen, dass das Axiom existiert oder um eben die Prämisse als erfüllt zu erkennen.