Система предлагает вектор булевой функции, пользователь вводит её КНФ