Článek popisuje plně automatickou metodu pro reformulaci problému splňování omezujících podmínek přidáním implikovaných podmínek získaných metodou jednotkové konzistence.