Генератор Доказів
Логічна формула має синтаксис, показаний на рисунку 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 символів, не враховуючи пробілів. Вхідні дані завершуються кінцем файлу і є коректними.