Proof Generator#1401

Proof Generator

1 second

64 megabytes

Very hard

A logical formula has the syntax shown in figure 1(a), where a variable stands for a truth value. The formula $(\textbf{+ F_1 \ldots F_n})$ stands for the logical disjunction of the formulae $\textbf{F_i}$ , $(\textbf{* F_1 \ldots F_n})$ denotes the logical conjunction of the formulae $\textbf{F_i}$ , and $F$ is the negation of $F$ . If a formula has the particular syntax given in figure 1(b), we say that the formula is in ACM Normal Form (ACMNF).

A formula is converted to ACMNF using the rewriting rules given below, where $F$ represents a formula, $S$ stands for a non-empty sequence of formulae, and $s$ and $s’$ denote possibly empty sequences of formulae. Applying a rewriting rule $q \to r$ \textbf{q} \rightarrow \textbf{r} on a formula $F$ means to substitute by $r$ a part of $F$ that matches the pattern $q$ , as shown in figure 2. The conversion terminates when no rewriting rule can be applied. The conversion terminates for any formula, and the result is unique regardless of which rules are applied to which parts of the formula and in which order.

A set of axioms is represented as a list $(\textbf{V_1} \textbf{V_2} \ldots \textbf{V_n})$ of false values. A proof of a formula $F$ according to a set of axioms $A$ is a term from the ACMNF of $F$ such that the term is true according to $A$ . For instance, the terms $(* a a)$ and $c$ are the proofs of the formula $(+(*(+ (*ab))(+ a))c)$ according to the axioms $(bc)$ .

The problem is to write a proof generator that for a given formula $F$ , a set of axioms $A$ , and numbers $k_{1}, \dots, k_{n}$ k_1, \ldots, k_n, outputs the next $k$ proofs of $F$ in the order in which they appear in the ACMNF of $F$ . If the proofs are exhausted, the generator continues from the first proof of $F$ . For example, generating the first proof of the formula $(+(*(+ (*ab))(+ a))c)$ according to the axioms $(bc)$ yields $(* a a)$ . Generating three more proofs produces $c$ , $(* a a)$ , and $c$ . If the ACMNF of a formula contains similar terms, as in the last example in figure 3, these terms are considered distinct.

Input

Write a proof generator that reads sets of data from the standard input. The content of a data set is $\textbf{F}\ \textbf{A}\ \textbf{k_1}\ \ldots\ \textbf{k_n}\ 0$ , where $n > 0$ n > 0, $F$ is a formula, $A$ is a set of axioms, and $\textbf{k_1}, \ldots, \textbf{k_n}$ are long integers different from $0$ . For each $\textbf{k_i}$ , $i = 1, \dots, n$ i=1, \ldots, n, the program generates the next $|\textbf{k_i}|$ proofs of $F$ and, if $\textbf{k_i} > 0$ , prints these proofs to the standard output.

Output

Each printed proof starts at the beginning of a line, and there are no white spaces between the characters of the proof. The generated proofs are not printed if $\textbf{k_i} < 0$ . White spaces are freely used in the input. A formula has at most $500$ characters, and an ACMNF term is at most $80$ characters long, not counting white spaces. Input data terminate with an end of file and are correct.

Examples

Example 1