Intuitionistic Logic

Vasya recently ran into a movement in mathematics and logic called "intuitionism". Its central idea is the rejection of the law of the excluded middle, the logical law saying that any assertion is either true or false. Vasya liked the idea. He says: "Classical mathematics tells me that Fermat's Last Theorem is either true or false, but that statement is useless to me until I see a proof or a counterexample." So Vasya became an intuitionist. He tries to use intuitionistic logic in everything he does, above all in his scientific work. This logic is much harder than the classical one, and Vasya often writes formulas that are valid in classical logic but not in the intuitionistic one.

He now wants a program that checks his formulas automatically. He found a book that explains how to do it, but he is not good at programming, so you have to help him.

The construction starts from an arbitrary acyclic oriented graph $X = (\mathcal{X}, G)$, where $\mathcal{X}$ is the set of vertices. First a partial order on $\mathcal{X}$ is defined: $x \le y$ holds if and only if $X$ contains a path (possibly of zero length) from $x$ to $y$. Next, let $\mathcal{B}$ be the set of all subsets of $\mathcal{X}$, and let $\mathcal{H} \subset \mathcal{B}$ consist of every $\alpha \subseteq \mathcal{X}$ in which any two different elements $x$ and $y$ are incomparable, meaning that neither $x \le y$ nor $y \le x$ holds. Note that $\mathcal{H}$ always contains the empty set and every one-element subset of $\mathcal{X}$.

Now it is possible to define a map $Max : \mathcal{B} \to \mathcal{H} \subset \mathcal{B}$. For $M \subseteq \mathcal{X}$ we put $Max(M) = \{x \in M : \neg \exists y \in M,\ x \ne y,\ x \le y\}$, the set of all maximal elements of $M$.

Several operations on $\mathcal{H}$ follow. For $\alpha, \beta \in \mathcal{H}$ we put

$\alpha \wedge \beta = Max(\alpha \cup \beta)$

$\alpha \vee \beta = Max(\{x \in \mathcal{X} : \exists y \in \alpha,\ \exists z \in \beta,\ x \le y,\ x \le z\})$

$\alpha \Rightarrow \beta = \{x \in \beta : \neg \exists y \in \alpha,\ x \le y\}$

$0 = Max(\mathcal{X}), \qquad 1 = \varnothing$

$\neg \alpha = (\alpha \Rightarrow 0), \qquad \alpha \equiv \beta = ((\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \alpha))$

A logical formula consists of the following symbols.

• Constants $1$ and $0$.
• Variables, the capital letters from $A$ to $Z$.
• Parentheses. If $E$ is a formula, then $(E)$ is another one.
• Negation. If $E$ is a formula, then $\neg E$ is a formula.
• Conjunction, $E_1 \wedge E_2 \wedge \dots \wedge E_n$. The conjunction is evaluated from left to right, so $E_1 \wedge E_2 \wedge E_3 = (E_1 \wedge E_2) \wedge E_3$.
• Disjunction, $E_1 \vee E_2 \vee \dots \vee E_n$. The same remark applies.
• Implication, $E_1 \Rightarrow E_2$. Unlike the previous two operations it is evaluated from right to left, so $E_1 \Rightarrow E_2 \Rightarrow E_3$ means $E_1 \Rightarrow (E_2 \Rightarrow E_3)$.
• Equivalence, $E_1 \equiv E_2 \equiv \dots \equiv E_n$. This expression equals $(E_1 \equiv E_2) \wedge (E_2 \equiv E_3) \wedge \dots \wedge (E_{n-1} \equiv E_n)$.

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

A formula $E$ is called valid in the model defined by $X$ if it evaluates to $1$ after every substitution of elements of $\mathcal{H}$ for the variables involved in $E$. Otherwise it is called invalid.

You are given the graph $X$ and a set of formulas. Determine which of them are valid.

The input contains one or more test cases and ends at end of file.

The first line of each test case contains two integers $N$ and $M$ separated by a single space, the number of vertices ($1 \le N \le 100$) and the number of edges ($0 \le M \le 5\,000$) of $X$. Each of the next $M$ lines contains two integers $s_i$ and $t_i$, the beginning and the end of the $i$-th edge. The next line contains $K$ ($1 \le K \le 20$), the number of formulas to be processed, and each of the following $K$ lines contains one formula.

A formula is a string of the tokens 0, 1, A ... Z, (, ), ~, &, |, =>, =. The last five tokens stand for $\neg$, $\wedge$, $\vee$, $\Rightarrow$ and $\equiv$ respectively. Tokens can be separated by an arbitrary number of spaces. No line is longer than $254$ characters, and every formula in the input is syntactically correct. You may also assume that the number of elements $H = |\mathcal{H}|$ is at most $100$ and that $\sum_{1 \le j \le K} H^{v[j]} \le 10^6$, where $v[j]$ is the number of different variables used in the $j$-th formula.

For each test case print $K$ lines, one line for each formula. Write valid on the $j$-th line if the $j$-th formula is valid, and invalid otherwise.