Получение нижних оценок на размер резолюционных доказательств для задачи поиска противоречия в паросочетании на двудольном графе с разным числом вершин.