No tags yet

No tag edit access

The problem statement has recently been changed. View the changes.

×
time limit per test: 2.75 sec.

memory limit per test: 65536 KB

memory limit per test: 65536 KB

input: standard input

output: standard output

output: standard output

Recently Vasya became acquainted with an interesting movement in mathematics and logic called "intuitionism". The main idea of this movement consists in the rejection of the law of excluded middle (the logical law stating that any assertion is either true or false). Vasya liked this idea; he says: "Classical mathematics says that Fermat Last Theorem is either true or false; but this statement is completely useless for me until I see the proof or a contrary instance". So Vasya became a born-again intuitionist. He tries to use the intuitionistic logic in all his activities and especially in his scientific work. But this logic is much more di+cult than the classical one. Vasya often tries to use logical formulae that are valid in classical logic but aren't so in the intuitionistic one.

Now he wants to write a program that will help him to check the validity of his formulae automatically. He has found a book describing how to do that but unfortunately he isn't good at programming, so you'll have to help him.

The construction starts from an arbitrary acyclic oriented graph**X** = <X, G>. Then a partial order is constructed on X, the set of vertices of **X**: for any x, y in X we define x <= y iff there exists a path (possibly of zero length) in **X** from x to y. Next, consider the set B of all subsets of X and the set H in B consisting of all a in X such that any two different x and y from R are incomparable (i.e. neither x <= y nor y <= x). Note that H always contains the empty set and all one-element subsets of X. Now it is possible to define a map Max : B -> H in B. For any M in X we put Max(M) = {x in M : not exists y in M : x <> y, x <= y} - the set of all maximal elements of M.

Next we define several operations on H. For any a,b in H put a => b = {x in b : not exists y in a : x <= y}, a /\ b = Max(a or b), a \/ b = Max({x in X: exists y in a, z in b: x <= y, x <= z}),**0** = Max(X), **1** = empty set, not a = (a => **0**), a == b = ((a => b) /\ (b => a)).

Now consider logical formulae consisting of the following symbols:

* Constants**1** and **0**;

* Variables - capital letters from A to Z;

* Parentheses - if E is a formula, then (E) is another;

* Negation - not E is a formula for any formula E;

* Conjunction - E1 /\ E2 /\ ... /\ En. Note that the conjunction is evaluated from left to right: E1 /\ E2 /\ E3 = (E1 /\ E2) /\ E3.

* Disjunction - E1 \/ E2 \/ ... \/ En. The same remark applies.

* Implication - E1 => E2. Unlike the previous two operations it is evaluated from right to left: E1 => E2 => E3 means E1 => (E2 => E3).

* Equivalence - E1 == E2 == ... == En. This expression is equal to (E1 == E2) /\ (E2 == E3) /\ ... /\ (En-1 => En).

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

A formula E is called valid (in the model defined by**X**) if after substitution of arbitrary elements of H for the variables involved in E it evaluates to **1**; otherwise it is called invalid.

Your task is to determine for a given graph**X**, which formulae from a given set are valid and which invalid.

Now he wants to write a program that will help him to check the validity of his formulae automatically. He has found a book describing how to do that but unfortunately he isn't good at programming, so you'll have to help him.

The construction starts from an arbitrary acyclic oriented graph

Next we define several operations on H. For any a,b in H put a => b = {x in b : not exists y in a : x <= y}, a /\ b = Max(a or b), a \/ b = Max({x in X: exists y in a, z in b: x <= y, x <= z}),

Now consider logical formulae consisting of the following symbols:

* Constants

* Variables - capital letters from A to Z;

* Parentheses - if E is a formula, then (E) is another;

* Negation - not E is a formula for any formula E;

* Conjunction - E1 /\ E2 /\ ... /\ En. Note that the conjunction is evaluated from left to right: E1 /\ E2 /\ E3 = (E1 /\ E2) /\ E3.

* Disjunction - E1 \/ E2 \/ ... \/ En. The same remark applies.

* Implication - E1 => E2. Unlike the previous two operations it is evaluated from right to left: E1 => E2 => E3 means E1 => (E2 => E3).

* Equivalence - E1 == E2 == ... == En. This expression is equal to (E1 == E2) /\ (E2 == E3) /\ ... /\ (En-1 => En).

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

A formula E is called valid (in the model defined by

Your task is to determine for a given graph

The first line contains two integers N and M separated by a single space - the number of vertices (1 <= N <= 100) and edges (0 <= M <= 5000) of **X**. The next M lines contain two integers si and ti each - the beginning and the end of i-th edge respectively. The next line contains K (1 <= K <= 20) - the number of formulae to be processed. The following K lines contain one formula each. A formula is represented by a string consisting of tokens 0, 1, A, ..., Z, (, ), ~, &, |, =>, =. The last five tokens stand for not, /\, \/, => and == respectively. Tokens can be separated by an arbitrary number of spaces. No line will be longer than 254 characters. All formulae in the file will be syntactically correct. Also you may assume that the number D = |H| of elements of H doesn't exceed 100 and that Sum(Di) <= 10^6.

The output file must contain K lines - one line for each formula. Write to the j-th line of output either valid or invalid.

Input

Sample input #1

1 0

6

1=0

X|~X

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

~~X => X

X => ~~X

(X => Y) = (Y | ~X)

Sample input #2

6 6

1 2

2 3

2 4

3 5

4 5

5 6

11

1=0

X|~X

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

~~X => X

X => ~~X

(X => Y) = (Y | ~X)

A&(B|C) = A&B|A&C

(X=>A)&(Y=>A) => X|Y=>A

X = ~~X

~X=~~~X

~X = (X => 0)

1 0

6

1=0

X|~X

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

~~X => X

X => ~~X

(X => Y) = (Y | ~X)

Sample input #2

6 6

1 2

2 3

2 4

3 5

4 5

5 6

11

1=0

X|~X

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

~~X => X

X => ~~X

(X => Y) = (Y | ~X)

A&(B|C) = A&B|A&C

(X=>A)&(Y=>A) => X|Y=>A

X = ~~X

~X=~~~X

~X = (X => 0)

Output

Sample output #1

invalid

valid

valid

valid

valid

valid

Sample output #2

invalid

invalid

valid

invalid

valid

invalid

valid

valid

invalid

valid

valid

invalid

valid

valid

valid

valid

valid

Sample output #2

invalid

invalid

valid

invalid

valid

invalid

valid

valid

invalid

valid

valid

Author: | Andrew Lopatin, Nikolay Durov |

Resource: | ACM ICPC 2002-2003 NEERC, Northern Subregion |

Date: | November, 2002 |

Codeforces (c) Copyright 2010-2021 Mike Mirzayanov

The only programming contests Web 2.0 platform

Server time: Jul/25/2021 00:44:41 (j3).

Desktop version, switch to mobile version.

Supported by

User lists

Name |
---|