Генератор доказательств
Логическая формула имеет синтаксис, представленный на рисунке 1(a), где переменная обозначает истинностное значение, формула (+ F_1 ... F_n) представляет логическую дизъюнкцию формул F_i, (* F_1 ... F_n) — логическую конъюнкцию формул F_i, а F обозначает отрицание F. Если формула соответствует синтаксису, показанному на рисунке 1(b), мы говорим, что она находится в нормальной форме ACM (ACMNF).
Формула преобразуется в ACMNF с помощью следующих правил переписывания, где F обозначает формулу, S — непустую последовательность формул, а s и s' — возможно, пустые последовательности формул. Применение правила переписывания q→r к формуле F означает замену части F, соответствующей шаблону q, на r, как показано на рисунке 2. Преобразование завершается, когда ни одно правило переписывания больше не может быть применено. Преобразование завершится для любой формулы, и результат будет уникальным, независимо от того, какие правила применяются к каким частям формулы и в каком порядке.
Набор аксиом представлен в виде списка (V_1 V_2 ... V_n) ложных. Доказательство формулы F в соответствии с набором аксиом A — это термин из ACMNF формулы F, который является истинным в соответствии с A. Например, термины (* a a) являются доказательствами формулы (+(*(+ (*ab))(+ a))c) в соответствии с аксиомами (bc).
Ваша задача — написать генератор доказательств, который для данной формулы F, набора аксиом A и числа k выводит следующие k доказательств формулы F в порядке их появления в ACMNF формулы F. Если доказательства исчерпаны, генератор продолжает с первого доказательства формулы F. Например, генерация первого доказательства формулы (+(*(+ (*ab))(+ a))c) в соответствии с аксиомами (bc) дает (* a a). Генерация еще трех доказательств дает c, (* a a) и c. Если ACMNF формулы содержит похожие термины, как в последнем примере на рисунке 3, эти термины считаются различными.
Входные данные
Напишите генератор доказательств, который считывает наборы данных из стандартного ввода. Содержимое набора данных — это F A k_1 ... k_n 0, где n > 0, F — формула, A — набор аксиом, а k_1 ... k_n — длинные целые числа, отличные от 0. Для каждого k_i, i = 1, n, программа генерирует следующие |k_i| доказательств формулы F и, если k_i > 0, выводит эти доказательства на стандартный вывод.
Выходные данные
Каждое напечатанное доказательство начинается с новой строки, и между символами доказательства нет пробелов. Сгенерированные доказательства не печатаются, если k_i < 0. Пробелы свободно используются во входных данных. Формула имеет не более 500 символов, а термин ACMNF — не более 80 символов, не считая пробелов. Входные данные завершаются концом файла и корректны.