W dowodzeniu twierdzenia o rozdzielczości zwykle przyjmuje się, że zmienne w różnych klauzulach są różne. To nie dzieje się automatycznie; do wdrożenia wymaga znacznego dodatkowego kodu i obliczeń. Biorąc to pod uwagę, szukam dla niego skrzynki testowej.
Problem polega na tym, że we wszystkich testowanych dotychczas testach nie ma to znaczenia. Przypuszczalnie ma to znaczenie tylko w nietypowych przypadkach krawędzi. Jak to ujęła Wikipedia , „zmienne w różnych klauzulach są różne ... Teraz, ujednolicenie Q (X) w pierwszej klauzuli z Q (Y) w drugiej klauzuli oznacza, że X i Y i tak stają się tą samą zmienną”.
Czy są jakieś znane przypadki testowe, które faktycznie dadzą złą odpowiedź, jeśli różne klauzule będą używać tych samych zmiennych?
źródło