<|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 with detailed comments

```cpp
#include <bits/stdc++.h>
using namespace std;

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

int n, m, K;

// Reachability information.
vector<BS> up_set;
vector<BS> down_set;

// All formula lines.
vector<string> formulas;

// All ideals, represented as bitsets.
vector<BS> H;

// Maps an ideal bitset to its index in H.
// bitset itself is not hashable by default, so we use to_string().
map<string, int> id;

// Operation tables.
vector<vector<int>> and_tbl;
vector<vector<int>> or_tbl;
vector<vector<int>> imp_tbl;
vector<vector<int>> eq_tbl;
vector<int> not_tbl;

int zero_idx;
int one_idx;

// Token types.
enum TokenType {
    T_ZERO,
    T_ONE,
    T_VAR,
    T_LPAR,
    T_RPAR,
    T_NOT,
    T_AND,
    T_OR,
    T_IMP,
    T_EQ,
    T_END
};

// Expression node operation types.
enum OpType {
    OP_CONST,
    OP_VAR,
    OP_NOT,
    OP_AND,
    OP_OR,
    OP_IMP,
    OP_EQ
};

struct Token {
    int type;
    int value;
};

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

vector<Token> tokens;
int pos_token;

vector<Node> nodes;
bool used_var[26];

int current_assignment[26];

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

// Forward declaration.
int parse_equiv();

/*
    atom:
        0
        1
        variable
        '(' expression ')'
*/
int parse_atom() {
    Token t = tokens[pos_token];

    if (t.type == T_LPAR) {
        pos_token++;
        int inside = parse_equiv();
        pos_token++; // skip ')'
        return inside;
    }

    if (t.type == T_ZERO) {
        pos_token++;
        return make_node(OP_CONST, zero_idx);
    }

    if (t.type == T_ONE) {
        pos_token++;
        return make_node(OP_CONST, one_idx);
    }

    // Otherwise it is a variable.
    pos_token++;
    used_var[t.value] = true;
    return make_node(OP_VAR, t.value);
}

/*
    neg:
        '~' neg
        atom
*/
int parse_neg() {
    if (tokens[pos_token].type == T_NOT) {
        pos_token++;
        return make_node(OP_NOT, parse_neg());
    }

    return parse_atom();
}

/*
    conj:
        neg
        conj '&' neg

    Left-associative.
*/
int parse_conj() {
    int left = parse_neg();

    while (tokens[pos_token].type == T_AND) {
        pos_token++;
        int right = parse_neg();
        left = make_node(OP_AND, left, right);
    }

    return left;
}

/*
    disj:
        conj
        disj '|' conj

    Left-associative.
*/
int parse_disj() {
    int left = parse_conj();

    while (tokens[pos_token].type == T_OR) {
        pos_token++;
        int right = parse_conj();
        left = make_node(OP_OR, left, right);
    }

    return left;
}

/*
    impl:
        disj
        disj '=>' impl

    Right-associative.
*/
int parse_impl() {
    int left = parse_disj();

    if (tokens[pos_token].type == T_IMP) {
        pos_token++;
        int right = parse_impl();
        return make_node(OP_IMP, left, right);
    }

    return left;
}

/*
    equiv:
        impl
        impl '=' impl '=' impl ...

    A = B = C is interpreted as:
        (A = B) & (B = C)
*/
int parse_equiv() {
    vector<int> terms;
    terms.push_back(parse_impl());

    while (tokens[pos_token].type == T_EQ) {
        pos_token++;
        terms.push_back(parse_impl());
    }

    if (terms.size() == 1) {
        return terms[0];
    }

    int result = make_node(OP_EQ, terms[0], terms[1]);

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

    return result;
}

vector<Token> tokenize(const string& s) {
    vector<Token> result;

    for (int i = 0; i < (int)s.size(); i++) {
        char c = s[i];

        if (c == ' ' || c == '\t' || c == '\r') {
            continue;
        }

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

    result.push_back({T_END, 0});
    return result;
}

int evaluate(int node_id) {
    Node node = nodes[node_id];

    if (node.op == OP_CONST) {
        return node.a;
    }

    if (node.op == OP_VAR) {
        return current_assignment[node.a];
    }

    if (node.op == OP_NOT) {
        int x = evaluate(node.a);
        return not_tbl[x];
    }

    if (node.op == OP_AND) {
        int x = evaluate(node.a);
        int y = evaluate(node.b);
        return and_tbl[x][y];
    }

    if (node.op == OP_OR) {
        int x = evaluate(node.a);
        int y = evaluate(node.b);
        return or_tbl[x][y];
    }

    if (node.op == OP_IMP) {
        int x = evaluate(node.a);
        int y = evaluate(node.b);
        return imp_tbl[x][y];
    }

    // OP_EQ
    int x = evaluate(node.a);
    int y = evaluate(node.b);
    return eq_tbl[x][y];
}

void read_input() {
    cin >> n >> m;

    up_set.assign(n, BS());

    for (int i = 0; i < n; i++) {
        up_set[i][i] = 1;
    }

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

    // Transitive closure.
    for (int k = 0; k < n; k++) {
        for (int i = 0; i < n; i++) {
            if (up_set[i][k]) {
                up_set[i] |= up_set[k];
            }
        }
    }

    // down_set[x] = all vertices z such that z <= x.
    down_set.assign(n, BS());

    for (int x = 0; x < n; x++) {
        for (int z = 0; z < n; z++) {
            if (up_set[z][x]) {
                down_set[x][z] = 1;
            }
        }
    }

    cin >> K;

    string line;
    getline(cin, line); // consume endline after K

    formulas.clear();

    while ((int)formulas.size() < K && getline(cin, line)) {
        // Formula lines are non-empty in valid input.
        // This also tolerates accidental blank lines.
        if (line.find_first_not_of(" \t\r") != string::npos) {
            formulas.push_back(line);
        }
    }
}

void enumerate_ideals() {
    H.clear();
    id.clear();

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

    // BFS-like enumeration.
    for (int ptr = 0; ptr < (int)H.size(); ptr++) {
        BS current = H[ptr];

        for (int x = 0; x < n; x++) {
            if (current[x]) {
                continue;
            }

            // Missing elements below x.
            BS need = down_set[x] & (~current);

            // Since down_set[x] contains x itself,
            // we can add x iff x is the only missing lower element.
            if (need.count() != 1) {
                continue;
            }

            BS next = current;
            next[x] = 1;

            string key = next.to_string();

            if (!id.count(key)) {
                id[key] = (int)H.size();
                H.push_back(next);
            }
        }
    }
}

void build_operation_tables() {
    int d = (int)H.size();

    BS empty;

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

    // In ideal representation:
    // logical 1 = empty ideal
    // logical 0 = full ideal
    one_idx = id[empty.to_string()];
    zero_idx = id[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++) {
            // Logical conjunction corresponds to union of ideals.
            and_tbl[i][j] = id[(H[i] | H[j]).to_string()];

            // Logical disjunction corresponds to intersection of ideals.
            or_tbl[i][j] = id[(H[i] & H[j]).to_string()];

            // Implication:
            // take maximal vertices of H[j] that are not in H[i],
            // then take their downward closure.
            BS result;

            for (int x = 0; x < n; x++) {
                if (!H[j][x]) {
                    continue;
                }

                if (H[i][x]) {
                    continue;
                }

                // x is maximal inside H[j] iff the only vertex in H[j]
                // reachable from x is x itself.
                BS above_inside = up_set[x] & H[j];

                if (above_inside.count() == 1) {
                    result |= down_set[x];
                }
            }

            imp_tbl[i][j] = id[result.to_string()];
        }
    }

    // Negation is implication to logical 0.
    for (int i = 0; i < d; i++) {
        not_tbl[i] = imp_tbl[i][zero_idx];
    }

    // Equivalence is mutual implication plus conjunction.
    for (int i = 0; i < d; i++) {
        for (int j = 0; j < d; j++) {
            int left = imp_tbl[i][j];
            int right = imp_tbl[j][i];
            eq_tbl[i][j] = and_tbl[left][right];
        }
    }
}

bool is_valid_formula(const string& formula) {
    tokens = tokenize(formula);

    nodes.clear();
    memset(used_var, 0, sizeof(used_var));

    pos_token = 0;
    int root = parse_equiv();

    vector<int> vars;

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

    int d = (int)H.size();

    memset(current_assignment, 0, sizeof(current_assignment));

    // Mixed-radix counter over all assignments.
    vector<int> digit(vars.size(), 0);

    while (true) {
        for (int i = 0; i < (int)vars.size(); i++) {
            current_assignment[vars[i]] = digit[i];
        }

        if (evaluate(root) != one_idx) {
            return false;
        }

        int p = 0;

        while (p < (int)digit.size()) {
            digit[p]++;

            if (digit[p] < d) {
                break;
            }

            digit[p] = 0;
            p++;
        }

        if (p == (int)digit.size()) {
            break;
        }
    }

    return true;
}

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

    read_input();

    enumerate_ideals();
    build_operation_tables();

    for (const string& formula : formulas) {
        cout << (is_valid_formula(formula) ? "valid" : "invalid") << '\n';
    }

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