Beth Tableaux

문제

Your program has to check the validity of a given logical formula. If the formula $EE$ is invalid (i.e. evaluates to $\mathbf{0}\backslash mathbf\{0\}$ for some assignment of boolean values to the variables), you’ll also have to find such an assignment of values.

Usually such tasks are solved just by processing all possible assignments of values to the variables occurring in $EE$; if there are $kk$ such variables, this requires considering $2^{k}2^k$ such assignments. Of course, this is almost impossible for large values of $kk$. Besides, this process is much different from the way people usually check (i.e. prove) logical formulae.

In this task you are to implement a natural way of checking validity of logical formulae based on the so-called Beth tableaux. This way of checking validity of formulae models to a certain extent the process of finding proofs or contrary instances used by humans, at least, a short rigorous proof can be usually obtained quite immediately from constructed Beth tableaux.

Let us fix the syntax of logical formulae considered:

• Constants $\mathbf{1}\backslash mathbf\{1\}$ and $\mathbf{0}\backslash mathbf\{0\}$;
• Variables — letters from A to Z and from a to z;
• Parentheses — if $EE$ is a formula, then $(E)(E)$ is another;
• Negation — $\mathrm{\neg }E\backslash neg\; E$ is a formula for any formula $EE$;
• Conjunction — $E_1\wedge E_2\wedge \cdots \wedge E_{n}E\_1\; \backslash wedge\; E\_2\; \backslash wedge\; \backslash cdots\; \backslash wedge\; E\_n$. Note that the conjunction is evaluated from left to right: $E_1\wedge E_2\wedge E_3=(E_1\wedge E_2)\wedge E_{3}E\_1\; \backslash wedge\; E\_2\; \backslash wedge\; E\_3\; =\; (E\_1\; \backslash wedge\; E\_2)\; \backslash wedge\; E\_3$.
• Disjunction — $E_1\vee E_2\vee \cdots \vee E_{n}E\_1\; \backslash vee\; E\_2\; \backslash vee\; \backslash cdots\; \backslash vee\; E\_n$. The same remark applies.
• Implication — $E_1\Rightarrow E_{2}E\_1\; \backslash Rightarrow\; E\_2$. Unlike the previous two operations it is evaluated from right to left: $E_1\Rightarrow E_2\Rightarrow E_{3}E\_1\; \backslash Rightarrow\; E\_2\; \backslash Rightarrow\; E\_3$ means $E_1\Rightarrow (E_2\Rightarrow E_3)E\_1\; \backslash Rightarrow\; (E\_2\; \backslash Rightarrow\; E\_3)$.
• Equivalence — $E_1\equiv E_2\equiv \cdots \equiv E_{n}E\_1\; \backslash equiv\; E\_2\; \backslash equiv\; \backslash cdots\; \backslash equiv\; E\_n$. This expression is by definition computed as follows: $(E_1\equiv E_2)\wedge (E_2\equiv E_3)\wedge \cdots \wedge (E_{n-1}\equiv E_n)(E\_1\; \backslash equiv\; E\_2)\; \backslash wedge\; (E\_2\; \backslash equiv\; E\_3)\; \backslash wedge\; \backslash cdots\; \backslash wedge\; (E\_\{n-1\}\; \backslash equiv\; E\_n)$.

The operations are listed from the highest priority to the lowest.

Let us define the principal operation of a compound formula $EE$ as the operation in $EE$ which is performed last (of course, formulae consisting just of one constant or variable have no principal operation). Also let us suppose that our formula does not contain equivalence operations since we can always replace $E_1\equiv E_{2}E\_1\; \backslash equiv\; E\_2$with $(E_1\Rightarrow E_2)\wedge (E_2\Rightarrow E_1)(E\_1\; \backslash Rightarrow\; E\_2)\; \backslash wedge\; (E\_2\; \backslash Rightarrow\; E\_1)$.

Now we define a Beth tableau to be a table with two columns with some formulae written in them. The order formulae are written in the columns and the number of times a formula appears in a column is irrelevant: we can assume for example that all formulae in a column are different and that they are ordered lexicographically.

Informally the left column corresponds to formulae which we want to be true and the right column to those which we want to be false; the whole process can be considered then as an attempt to produce a contrary instance to given formula $EE$. A Beth tableau is said to be contradictory if some formula $E_{\ast }E\_*$ occurs in both columns of this tableau, or if $\mathbf{0}\backslash mathbf\{0\}$ occurs in the left column, or if $\mathbf{1}\backslash mathbf\{1\}$ occurs in the right column.

At every step of the process we have a collection of Beth tableaux. We start with a single Beth tableau with empty left column and the right column containing just the given formula $EE$. A step of the process consists in choosing a compound formula $CC$ from a non-contradictory Beth tableau from the collection and applying a rule chosen by the principal operation of $CC$ and by the column (left or right) in which $CC$ is situated. As a result some formulae are added to the left or right columns of this Beth tableau (or both); of course, if these formulae that we want to add are already there the Beth tableau won’t change, so in this case we say that the corresponding rule is inapplicable. There are also some rules that make two copies of the original Beth tableau and add some formulae into one of these copies and some other into the second one. In this case we say that the rule is inapplicable if both Beth tableaux thus obtained were already in the collection before applying the rule.

The process stops when no rule is applicable. Note that all formulae occurring in all Beth tableaux constructed will be sub-formulae of the original formula, so there are only finitely many Beth tableaux that can be obtained and thus only finitely many collections of Beth tableaux can be obtained. Therefore the process will have to stop at some point. If at this point all Beth tableaux in the collection are contradictory, the original formula $EE$ has been proved to be valid. Otherwise if $\tau \backslash tau$ is a non-contradictory Beth tableau from the collection, any variable $xx$ occurring in $EE$ must occur in exactly one column of $\tau \backslash tau$ (it cannot occur in both columns since $\tau \backslash tau$ is not contradictory; it must occur in at least one column since otherwise a rule would be applicable to the shortest formula in $\tau \backslash tau$ containing $xx$). Then let us assign $\mathbf{1}\backslash mathbf\{1\}$ to all the variables from the left column and $\mathbf{0}\backslash mathbf\{0\}$ to the variables from the right column of $\tau \backslash tau$. This would give us a contrary instance to $EE$, i.e. an assignment of values to variables for which our original formula $EE$ evaluates to $\mathbf{0}\backslash mathbf\{0\}$.

Now let us list all possible rules. It has been already explained that a rule is defined by the principal operation $\ast *$ of a formula $CC$ and the column (left or right) in which $CC$ was found. We shall label these rules by ${\ast }_l*\_l$ and ${\ast }_r*\_r$ where $\ast *$ is the operation (one of $\wedge \backslash wedge$, $\vee \backslash vee$, $\Rightarrow \backslash Rightarrow$ or $\mathrm{\neg }\backslash neg$). If $\ast *$ is binary, we shall assume that $C=A\ast BC\; =\; A\; *\; B$; otherwise we assume $C=\mathrm{\neg }AC\; =\; \backslash neg\; A$.

Let us list the rules that do not increase the number of tableaux (i.e. they just add some formulae to the columns of selected Beth tableau):

This means the following: for example, if we apply the rule ${\Rightarrow }_r\backslash Rightarrow\_r$ to the formula $A\Rightarrow BA\; \backslash Rightarrow\; B$ in the right column of a Beth tableau, then we have to add formula $AA$ to the left column and $BB$ to the right column of this tableau.

The next rules produce two Beth tableaux from one. A similar notation is used, but two Beth tableaux are shown for each rule:

These three rules are interpreted as follows: if we apply for example ${\vee }_l\backslash vee\_l$ to the formula $A\vee BA\; \backslash vee\; B$ in the left column of a Beth tableau $\tau \backslash tau$, we have to replace $\tau \backslash tau$ with two copies of itself ${\tau }^{\mathrm{\prime }}\backslash tau\; \text{'}$ and \tau ' ', and then add $AA$ to the left column of ${\tau }^{\mathrm{\prime }}\backslash tau\; \text{'}$ and $BB$ to the left column of \tau ' '.

입력

The only line of input contains the formula represented as a string consisting of tokens ‘0’, ‘1’, ‘A’. . . ‘Z’, ‘a’. . . ‘z’, ‘(’, ‘)’, ‘~’, ‘&’, ‘|’, ‘=>’, ‘=’. The last five tokens stand for $\mathrm{\neg }\backslash neg$, $\wedge \backslash wedge$, $\vee \backslash vee$ , $\Rightarrow \backslash Rightarrow$ and $\equiv \backslash equiv$ respectively. Tokens can be separated by an arbitrary number of spaces. The line will contain at most 1 000 characters. The formula in the file will be syntactically correct.

출력

The output file must contain exactly one line. Output just “true” if the formula is valid or “false” followed by an assignment of variables that invalidates the formula. List the variables in lexicographical order. Adhere to the sample output as strictly as possible.

0

false

(A=>B)=>(~A=>~B)

false: A=0, B=1

(A=a)&(B=b)=>(A&B=a&b)

true

K|~i|t|t|~e|~n

false: K=0, e=1, i=1, n=1, t=0

1

true

A

false: A=0

A|B => A&B

false: A=1, B=0

A&B => A|B

true

r=>Y

false: Y=0, r=1

R=r

false: R=0, r=1

(A=>B)&(B=>C)=>(A=>C)

true

(A=>B)=>(~B=>~A)

true