<|instruction|>
Solve the below problem. The solution should start with an abridged problem statement. Then key observations. Then full solution based on the observations. Then C++ and Python implementations with comments.

161. Intuitionistic Logic
time limit per test: 2.75 sec.
memory limit per test: 65536 KB
input: standard input
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.

Input
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.

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

Sample test(s)

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)

Output
Sample output #1
invalid
valid
valid
valid
valid
valid

Sample output #2
invalid
invalid
valid
invalid
valid
invalid
valid
valid
invalid
valid
valid

Note
Author:	Andrew Lopatin, Nikolay Durov
Resource:	ACM ICPC 2002-2003 NEERC, Northern Subregion
Date:	November, 2002

<|response|>
## 1. Abridged problem statement

Given a DAG with `N ≤ 100`, define a partial order on vertices:

```text
x ≤ y  iff  there is a directed path from x to y
```

The model elements are all antichains of this poset. Several intuitionistic logic operations are defined on these antichains: constants `0`, `1`, negation `~`, conjunction `&`, disjunction `|`, implication `=>`, and equivalence `=`.

For each given logical formula, determine whether it is **valid**, meaning that for every assignment of model elements to its variables, the formula evaluates to `1`.

The statement guarantees that the number of model elements `D = |H|` is at most `100`, and the total number of assignments that must be checked is small enough.

---

## 2. Key observations needed to solve the problem

### Observation 1: Use ideals instead of antichains

Directly working with antichains is possible but inconvenient.

For an antichain `a`, define its downward closure:

```text
Down(a) = { x : exists y in a such that x ≤ y }
```

This is an **order ideal**, i.e. a downward-closed set.

Conversely, every order ideal is uniquely represented by its maximal elements, which form an antichain.

Therefore:

```text
antichains  <=>  ideals
```

So we store each algebra element as a bitset representing an ideal.

---

### Observation 2: Constants become reversed-looking

In the statement:

```text
1 = empty antichain
0 = Max(X)
```

In ideal representation:

```text
1 = empty ideal
0 = full ideal
```

This may look opposite to classical Boolean logic, but it is exactly what the statement defines.

---

### Observation 3: Operations become simple set operations

Let `A` and `B` be ideals corresponding to algebra elements `a` and `b`.

#### Conjunction

The statement defines:

```text
a & b = Max(a ∪ b)
```

In ideal form:

```text
A & B = A ∪ B
```

#### Disjunction

The statement defines disjunction using common lower bounds.

In ideal form:

```text
A | B = A ∩ B
```

#### Implication

The statement defines:

```text
a => b = { x in b : no y in a satisfies x ≤ y }
```

In ideal form, `b` corresponds to the maximal elements of ideal `B`.

So `A => B` is:

```text
downward closure of all maximal elements of B that are not inside A
```

A vertex `x` is maximal inside ideal `B` if no strictly greater vertex of `B` exists.

Using reachability bitsets:

```text
x is maximal in B iff (up[x] & B) contains only x
```

---

### Observation 4: Precompute all operation tables

Since `D ≤ 100`, we can precompute:

```text
and_tbl[D][D]
or_tbl[D][D]
imp_tbl[D][D]
eq_tbl[D][D]
not_tbl[D]
```

Then formula evaluation is fast: every operation is a table lookup.

---

### Observation 5: Brute force all variable assignments

For each formula:

1. Parse it into an expression tree.
2. Collect variables used in the formula.
3. Try every assignment of these variables to one of the `D` algebra elements.
4. If all assignments evaluate to logical `1`, the formula is `valid`.
5. Otherwise, it is `invalid`.

The input guarantee makes this brute force feasible.

---

## 3. Full solution approach

### Step 1: Compute transitive closure

We need to know whether `x ≤ y`, i.e. whether `x` reaches `y`.

Use bitsets:

```text
up[x] = all vertices reachable from x
```

Initialize:

```text
up[x][x] = true
```

For every edge `s -> t`:

```text
up[s][t] = true
```

Then compute transitive closure:

```cpp
for k in vertices:
    for i in vertices:
        if up[i][k]:
            up[i] |= up[k]
```

Also compute:

```text
down[x] = all vertices z such that z ≤ x
```

---

### Step 2: Enumerate all ideals

Start with the empty ideal.

An ideal can be extended by adding vertex `x` if all elements below `x`, except `x` itself, are already present.

In bitset form:

```text
need = down[x] \ current_ideal
```

We can add `x` iff:

```text
need contains only x
```

Because `D ≤ 100`, this enumeration is small.

---

### Step 3: Precompute operations

Let `H[i]` be the bitset of the `i`-th ideal.

```text
1 = empty ideal
0 = full ideal
```

For every pair `(i, j)`:

```text
H[i] & H[j] as logic conjunction = set union
H[i] | H[j] as logic disjunction = set intersection
```

So:

```cpp
and_tbl[i][j] = index[H[i] | H[j]]
or_tbl[i][j]  = index[H[i] & H[j]]
```

For implication:

```cpp
res = empty ideal

for every vertex x:
    if x is in H[j]
       and x is not in H[i]
       and x is maximal inside H[j]:
           res |= down[x]

imp_tbl[i][j] = index[res]
```

Then:

```cpp
not_tbl[i] = imp_tbl[i][zero_idx]
eq_tbl[i][j] = and_tbl[imp_tbl[i][j]][imp_tbl[j][i]]
```

---

### Step 4: Parse formulae

Operator priority, from highest to lowest:

```text
~
&
|
=>
=
```

Associativity:

```text
& and | are left-associative
=> is right-associative
= is expanded as pairwise equivalence
```

For example:

```text
A = B = C
```

means:

```text
(A = B) & (B = C)
```

A recursive descent parser is natural.

---

### Step 5: Evaluate validity

For each formula, enumerate all assignments of its used variables:

```text
variable -> algebra element index
```

Evaluate the expression tree using precomputed tables.

If any assignment gives a value other than `one_idx`, the formula is invalid.

---

## 4. C++ implementation

```cpp
#include <bits/stdc++.h>

using namespace std;

template<typename T1, typename T2>
ostream& operator<<(ostream& out, const pair<T1, T2>& x) {
    return out << x.first << ' ' << x.second;
}

template<typename T1, typename T2>
istream& operator>>(istream& in, pair<T1, T2>& x) {
    return in >> x.first >> x.second;
}

template<typename T>
istream& operator>>(istream& in, vector<T>& a) {
    for(auto& x: a) {
        in >> x;
    }
    return in;
};

template<typename T>
ostream& operator<<(ostream& out, const vector<T>& a) {
    for(auto x: a) {
        out << x << ' ';
    }
    return out;
};

const int MAXN = 100;
using BS = bitset<MAXN>;

int n, m, K;
vector<string> formulas;
vector<BS> up, down;

void read() {
    cin >> n >> m;
    up.assign(n, BS());
    for(int i = 0; i < n; i++) {
        up[i][i] = 1;
    }

    for(int i = 0; i < m; i++) {
        int s, t;
        cin >> s >> t;
        up[s - 1][t - 1] = 1;
    }

    for(int k = 0; k < n; k++) {
        for(int i = 0; i < n; i++) {
            if(up[i][k]) {
                up[i] |= up[k];
            }
        }
    }

    down.assign(n, BS());
    for(int x = 0; x < n; x++) {
        for(int z = 0; z < n; z++) {
            if(up[z][x]) {
                down[x][z] = 1;
            }
        }
    }

    cin >> K;
    string line;
    getline(cin, line);
    while((int)formulas.size() < K && getline(cin, line)) {
        if(line.find_first_not_of(" \t\r") != string::npos) {
            formulas.push_back(line);
        }
    }
}

vector<BS> H;
map<string, int> h_index;
vector<vector<int>> and_tbl, or_tbl, imp_tbl, eq_tbl;
vector<int> not_tbl;
int zero_idx, one_idx;

enum { T_ZERO, T_ONE, T_VAR, T_LPAR, T_RPAR, T_NOT, T_AND, T_OR, T_IMP, T_EQ };
enum { OP_CONST, OP_VAR, OP_NOT, OP_AND, OP_OR, OP_IMP, OP_EQ };

struct Token {
    int type, var;
};

struct Node {
    int op, a, b;
};

vector<Token> toks;
int pos;
vector<Node> nodes;
bool used[26];

int make_node(int op, int a, int b) {
    nodes.push_back({op, a, b});
    return (int)nodes.size() - 1;
}

int parse_equiv();

int parse_atom() {
    Token t = toks[pos];
    if(t.type == T_LPAR) {
        pos++;
        int e = parse_equiv();
        pos++;
        return e;
    }
    if(t.type == T_ZERO) {
        pos++;
        return make_node(OP_CONST, zero_idx, 0);
    }
    if(t.type == T_ONE) {
        pos++;
        return make_node(OP_CONST, one_idx, 0);
    }
    pos++;
    used[t.var] = true;
    return make_node(OP_VAR, t.var, 0);
}

int parse_neg() {
    if(toks[pos].type == T_NOT) {
        pos++;
        return make_node(OP_NOT, parse_neg(), 0);
    }
    return parse_atom();
}

int parse_conj() {
    int left = parse_neg();
    while(toks[pos].type == T_AND) {
        pos++;
        left = make_node(OP_AND, left, parse_neg());
    }
    return left;
}

int parse_disj() {
    int left = parse_conj();
    while(toks[pos].type == T_OR) {
        pos++;
        left = make_node(OP_OR, left, parse_conj());
    }
    return left;
}

int parse_impl() {
    int left = parse_disj();
    if(toks[pos].type == T_IMP) {
        pos++;
        return make_node(OP_IMP, left, parse_impl());
    }
    return left;
}

int parse_equiv() {
    vector<int> terms = {parse_impl()};
    while(toks[pos].type == T_EQ) {
        pos++;
        terms.push_back(parse_impl());
    }
    if(terms.size() == 1) {
        return terms[0];
    }

    int node = make_node(OP_EQ, terms[0], terms[1]);
    for(int i = 2; i < (int)terms.size(); i++) {
        node =
            make_node(OP_AND, node, make_node(OP_EQ, terms[i - 1], terms[i]));
    }
    return node;
}

int cur_assign[26];

int eval(int u) {
    Node nd = nodes[u];
    switch(nd.op) {
        case OP_CONST:
            return nd.a;
        case OP_VAR:
            return cur_assign[nd.a];
        case OP_NOT:
            return not_tbl[eval(nd.a)];
        case OP_AND:
            return and_tbl[eval(nd.a)][eval(nd.b)];
        case OP_OR:
            return or_tbl[eval(nd.a)][eval(nd.b)];
        case OP_IMP:
            return imp_tbl[eval(nd.a)][eval(nd.b)];
        default:
            return eq_tbl[eval(nd.a)][eval(nd.b)];
    }
}

void solve() {
    // The graph's reachability gives a partial order on the vertices, and the
    // model H is exactly the Heyting algebra of that poset. The bridge is a
    // bijection between antichains and down-closed sets (order ideals): an
    // antichain a corresponds to its downward closure, and conversely an ideal
    // corresponds to its set of maximal elements. We store every H element by
    // its ideal as a bitset, which makes the operations clean.
    //
    // Under this encoding the problem's "0" (false) is the full poset (the
    // largest ideal) and "1" (true) is the empty ideal. Because truth is
    // measured by reverse inclusion of ideals, the connectives come out dual to
    // naive set logic:
    //
    // - conjunction a/\b is the union of the two ideals;
    // - disjunction a\/b is their intersection;
    // - implication a=>b is the smallest ideal C with ideal(a) | C covering
    //   ideal(b), which equals the downward closure of the maximal elements of
    //   ideal(b) that do not already lie in ideal(a);
    // - negation is a=>0 (the pseudocomplement), and == is (a=>b)/\(b=>a).
    //
    // These are precisely the Heyting operations, so a formula is "valid" iff
    // it evaluates to the top element 1 for every assignment of ideals to its
    // variables; classical-only laws such as X\/~X or ~~X=>X fail whenever the
    // poset is non-trivial, while genuine intuitionistic theorems survive.
    //
    // Implementation: enumerate all ideals by growing from the empty set one
    // maximal element at a time (the guarantee |H|<=100 keeps this small),
    // precompute the full operation tables over H, parse each formula by
    // precedence (~ then & then | then => then ==, with => right-associative
    // and == expanding to a conjunction of consecutive pairwise equivalences)
    // into an expression tree, and brute force every variable assignment using
    // table lookups.
    //
    // The cost is dominated by those assignments: a formula with v distinct
    // variables ranges each variable independently over all of H, so it needs
    // D^v evaluations, and one evaluation is just a linear walk over the tree
    // with O(1) table lookups. There is a single graph, hence a single D, so
    // the statement's "Sum(Di)<=10^6" cannot mean Sum(D)=K*D (that is at most
    // 20*100 and would be a vacuous bound). It only bites if Di is the per
    // formula work D^v, and indeed 10^6 = 100^3 is exactly the worst single
    // formula (D=100 with three variables). So this reads as a promise that the
    // overall number of assignments Sum(D^v) is bounded, which is precisely
    // what makes plain full enumeration pass.

    H.clear();
    h_index.clear();

    BS empty;
    H.push_back(empty);
    h_index[empty.to_string()] = 0;

    for(size_t front = 0; front < H.size(); front++) {
        BS cur = H[front];
        for(int x = 0; x < n; x++) {
            if(cur[x]) {
                continue;
            }

            BS need = down[x] & ~cur;
            if(need.count() != 1) {
                continue;
            }

            BS nxt = cur;
            nxt[x] = 1;
            string key = nxt.to_string();
            if(h_index.find(key) == h_index.end()) {
                h_index[key] = (int)H.size();
                H.push_back(nxt);
            }
        }
    }

    int d = (int)H.size();
    BS full;
    for(int i = 0; i < n; i++) {
        full[i] = 1;
    }

    one_idx = h_index[empty.to_string()];
    zero_idx = h_index[full.to_string()];

    and_tbl.assign(d, vector<int>(d));
    or_tbl.assign(d, vector<int>(d));
    imp_tbl.assign(d, vector<int>(d));
    eq_tbl.assign(d, vector<int>(d));
    not_tbl.assign(d, 0);

    for(int i = 0; i < d; i++) {
        for(int j = 0; j < d; j++) {
            and_tbl[i][j] = h_index[(H[i] | H[j]).to_string()];
            or_tbl[i][j] = h_index[(H[i] & H[j]).to_string()];

            BS res;
            for(int x = 0; x < n; x++) {
                if(H[j][x] && !H[i][x] && (up[x] & H[j]).count() == 1) {
                    res |= down[x];
                }
            }
            imp_tbl[i][j] = h_index[res.to_string()];
        }
    }

    for(int i = 0; i < d; i++) {
        not_tbl[i] = imp_tbl[i][zero_idx];
    }

    for(int i = 0; i < d; i++) {
        for(int j = 0; j < d; j++) {
            eq_tbl[i][j] = and_tbl[imp_tbl[i][j]][imp_tbl[j][i]];
        }
    }

    for(const string& formula: formulas) {
        toks.clear();
        for(size_t i = 0; i < formula.size(); i++) {
            char c = formula[i];
            if(c == ' ' || c == '\t' || c == '\r') {
                continue;
            }

            if(c == '0') {
                toks.push_back({T_ZERO, 0});
            } else if(c == '1') {
                toks.push_back({T_ONE, 0});
            } else if(c >= 'A' && c <= 'Z') {
                toks.push_back({T_VAR, c - 'A'});
            } else if(c == '(') {
                toks.push_back({T_LPAR, 0});
            } else if(c == ')') {
                toks.push_back({T_RPAR, 0});
            } else if(c == '~') {
                toks.push_back({T_NOT, 0});
            } else if(c == '&') {
                toks.push_back({T_AND, 0});
            } else if(c == '|') {
                toks.push_back({T_OR, 0});
            } else if(c == '=') {
                if(i + 1 < formula.size() && formula[i + 1] == '>') {
                    toks.push_back({T_IMP, 0});
                    i++;
                } else {
                    toks.push_back({T_EQ, 0});
                }
            }
        }
        toks.push_back({-1, 0});

        nodes.clear();
        memset(used, 0, sizeof(used));
        pos = 0;
        int root = parse_equiv();

        vector<int> vars;
        for(int v = 0; v < 26; v++) {
            if(used[v]) {
                vars.push_back(v);
            }
        }

        memset(cur_assign, 0, sizeof(cur_assign));
        vector<int> digit(vars.size(), 0);
        bool valid = true;
        while(true) {
            for(size_t p = 0; p < vars.size(); p++) {
                cur_assign[vars[p]] = digit[p];
            }

            if(eval(root) != one_idx) {
                valid = false;
                break;
            }

            size_t i = 0;
            for(; i < vars.size(); i++) {
                if(++digit[i] < d) {
                    break;
                }
                digit[i] = 0;
            }
            if(i == vars.size()) {
                break;
            }
        }

        cout << (valid ? "valid" : "invalid") << '\n';
    }
}

int main() {
    ios_base::sync_with_stdio(false);
    cin.tie(nullptr);

    int T = 1;
    // cin >> T;
    for(int test = 1; test <= T; test++) {
        read();
        solve();
    }

    return 0;
}
```

---

## 5. Python implementation with detailed comments

```python
import sys
from itertools import product


# Token types.
T_ZERO = 0
T_ONE = 1
T_VAR = 2
T_LPAR = 3
T_RPAR = 4
T_NOT = 5
T_AND = 6
T_OR = 7
T_IMP = 8
T_EQ = 9
T_END = 10

# Expression node operation types.
OP_CONST = 0
OP_VAR = 1
OP_NOT = 2
OP_AND = 3
OP_OR = 4
OP_IMP = 5
OP_EQ = 6


def tokenize(s):
    """
    Converts a formula string into tokens.

    The implication token is represented by '=>'.
    The equivalence token is represented by '='.
    """

    tokens = []
    i = 0

    while i < len(s):
        c = s[i]

        if c in " \t\r\n":
            i += 1
            continue

        if c == "0":
            tokens.append((T_ZERO, 0))
        elif c == "1":
            tokens.append((T_ONE, 0))
        elif "A" <= c <= "Z":
            tokens.append((T_VAR, ord(c) - ord("A")))
        elif c == "(":
            tokens.append((T_LPAR, 0))
        elif c == ")":
            tokens.append((T_RPAR, 0))
        elif c == "~":
            tokens.append((T_NOT, 0))
        elif c == "&":
            tokens.append((T_AND, 0))
        elif c == "|":
            tokens.append((T_OR, 0))
        elif c == "=":
            if i + 1 < len(s) and s[i + 1] == ">":
                tokens.append((T_IMP, 0))
                i += 1
            else:
                tokens.append((T_EQ, 0))

        i += 1

    tokens.append((T_END, 0))
    return tokens


class Parser:
    def __init__(self, tokens, zero_idx, one_idx):
        self.tokens = tokens
        self.pos = 0

        # Expression tree nodes.
        # Each node is a tuple (op, a, b).
        self.nodes = []

        self.zero_idx = zero_idx
        self.one_idx = one_idx

        # Variables used by the formula.
        self.used = [False] * 26

    def make_node(self, op, a, b=0):
        self.nodes.append((op, a, b))
        return len(self.nodes) - 1

    def parse_atom(self):
        """
        atom:
            0
            1
            variable
            '(' expression ')'
        """

        typ, val = self.tokens[self.pos]

        if typ == T_LPAR:
            self.pos += 1
            inside = self.parse_equiv()
            self.pos += 1  # skip ')'
            return inside

        if typ == T_ZERO:
            self.pos += 1
            return self.make_node(OP_CONST, self.zero_idx)

        if typ == T_ONE:
            self.pos += 1
            return self.make_node(OP_CONST, self.one_idx)

        # Variable.
        self.pos += 1
        self.used[val] = True
        return self.make_node(OP_VAR, val)

    def parse_neg(self):
        """
        neg:
            '~' neg
            atom
        """

        if self.tokens[self.pos][0] == T_NOT:
            self.pos += 1
            return self.make_node(OP_NOT, self.parse_neg())

        return self.parse_atom()

    def parse_conj(self):
        """
        conjunction:
            neg '&' neg '&' ...

        Left-associative.
        """

        left = self.parse_neg()

        while self.tokens[self.pos][0] == T_AND:
            self.pos += 1
            right = self.parse_neg()
            left = self.make_node(OP_AND, left, right)

        return left

    def parse_disj(self):
        """
        disjunction:
            conj '|' conj '|' ...

        Left-associative.
        """

        left = self.parse_conj()

        while self.tokens[self.pos][0] == T_OR:
            self.pos += 1
            right = self.parse_conj()
            left = self.make_node(OP_OR, left, right)

        return left

    def parse_impl(self):
        """
        implication:
            disj
            disj '=>' implication

        Right-associative.
        """

        left = self.parse_disj()

        if self.tokens[self.pos][0] == T_IMP:
            self.pos += 1
            right = self.parse_impl()
            return self.make_node(OP_IMP, left, right)

        return left

    def parse_equiv(self):
        """
        equivalence:
            impl '=' impl '=' impl ...

        A = B = C is interpreted as:
            (A = B) & (B = C)
        """

        terms = [self.parse_impl()]

        while self.tokens[self.pos][0] == T_EQ:
            self.pos += 1
            terms.append(self.parse_impl())

        if len(terms) == 1:
            return terms[0]

        result = self.make_node(OP_EQ, terms[0], terms[1])

        for i in range(2, len(terms)):
            pair_eq = self.make_node(OP_EQ, terms[i - 1], terms[i])
            result = self.make_node(OP_AND, result, pair_eq)

        return result


def evaluate(node_id, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl):
    """
    Evaluates the expression tree under the current variable assignment.
    All algebra operations are table lookups.
    """

    op, a, b = nodes[node_id]

    if op == OP_CONST:
        return a

    if op == OP_VAR:
        return assignment[a]

    if op == OP_NOT:
        x = evaluate(a, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        return not_tbl[x]

    if op == OP_AND:
        x = evaluate(a, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        y = evaluate(b, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        return and_tbl[x][y]

    if op == OP_OR:
        x = evaluate(a, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        y = evaluate(b, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        return or_tbl[x][y]

    if op == OP_IMP:
        x = evaluate(a, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        y = evaluate(b, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
        return imp_tbl[x][y]

    # OP_EQ
    x = evaluate(a, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
    y = evaluate(b, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)
    return eq_tbl[x][y]


def main():
    lines = sys.stdin.read().splitlines()
    ptr = 0

    n, m = map(int, lines[ptr].split())
    ptr += 1

    # up[x] is a bitmask of vertices reachable from x.
    up = [0] * n

    for i in range(n):
        up[i] |= 1 << i

    for _ in range(m):
        s, t = map(int, lines[ptr].split())
        ptr += 1

        s -= 1
        t -= 1

        up[s] |= 1 << t

    # Transitive closure.
    for k in range(n):
        bit_k = 1 << k

        for i in range(n):
            if up[i] & bit_k:
                up[i] |= up[k]

    # down[x] = all z such that z <= x.
    down = [0] * n

    for x in range(n):
        mask = 0

        for z in range(n):
            if up[z] & (1 << x):
                mask |= 1 << z

        down[x] = mask

    K = int(lines[ptr].strip())
    ptr += 1

    formulas = []

    while len(formulas) < K and ptr < len(lines):
        line = lines[ptr]
        ptr += 1

        # Formula lines are non-empty in valid input.
        # This also tolerates accidental blank lines.
        if line.strip():
            formulas.append(line)

    full = (1 << n) - 1

    # Enumerate all ideals.
    H = [0]
    index = {0: 0}

    front = 0

    while front < len(H):
        current = H[front]
        front += 1

        for x in range(n):
            bit_x = 1 << x

            if current & bit_x:
                continue

            # Missing vertices below x.
            need = down[x] & (full ^ current)

            # Can add x iff x is the only missing lower vertex.
            if need.bit_count() != 1:
                continue

            nxt = current | bit_x

            if nxt not in index:
                index[nxt] = len(H)
                H.append(nxt)

    d = len(H)

    # Logical constants in ideal representation.
    one_idx = index[0]
    zero_idx = index[full]

    # Operation tables.
    and_tbl = [[0] * d for _ in range(d)]
    or_tbl = [[0] * d for _ in range(d)]
    imp_tbl = [[0] * d for _ in range(d)]
    eq_tbl = [[0] * d for _ in range(d)]
    not_tbl = [0] * d

    for i in range(d):
        A = H[i]

        for j in range(d):
            B = H[j]

            # Logical conjunction is union of ideals.
            and_tbl[i][j] = index[A | B]

            # Logical disjunction is intersection of ideals.
            or_tbl[i][j] = index[A & B]

            # Implication:
            # downward closure of maximal elements of B that are not in A.
            result = 0

            for x in range(n):
                bit_x = 1 << x

                if not (B & bit_x):
                    continue

                if A & bit_x:
                    continue

                # x is maximal in B iff only x itself in B is reachable from x.
                if (up[x] & B).bit_count() == 1:
                    result |= down[x]

            imp_tbl[i][j] = index[result]

    # Negation is implication to 0.
    for i in range(d):
        not_tbl[i] = imp_tbl[i][zero_idx]

    # Equivalence is mutual implication plus conjunction.
    for i in range(d):
        for j in range(d):
            left = imp_tbl[i][j]
            right = imp_tbl[j][i]
            eq_tbl[i][j] = and_tbl[left][right]

    answer = []

    for formula in formulas:
        tokens = tokenize(formula)

        parser = Parser(tokens, zero_idx, one_idx)
        root = parser.parse_equiv()

        vars_used = [v for v in range(26) if parser.used[v]]

        assignment = [0] * 26
        valid = True

        # Try all assignments of used variables to algebra elements.
        for values in product(range(d), repeat=len(vars_used)):
            for var, value in zip(vars_used, values):
                assignment[var] = value

            value = evaluate(
                root,
                parser.nodes,
                assignment,
                not_tbl,
                and_tbl,
                or_tbl,
                imp_tbl,
                eq_tbl,
            )

            if value != one_idx:
                valid = False
                break

        answer.append("valid" if valid else "invalid")

    print("\n".join(answer))


if __name__ == "__main__":
    main()
```

Both implementations follow the same idea:

1. Convert antichains to ideals.
2. Enumerate all ideals.
3. Precompute the finite algebra operations.
4. Parse each formula.
5. Brute force all assignments and check whether the result is always logical `1`.