## 1. Abridged problem statement

Given a DAG with `N ≤ 100`, define a partial order: `x ≤ y` iff there is a path from `x` to `y`. From this poset, build a finite intuitionistic logic algebra whose elements are antichains of the poset, with operations `0`, `1`, `~`, `&`, `|`, `=>`, and `=` defined as in the statement.

You are given up to `20` logical formulae using constants `0`, `1`, variables `A..Z`, parentheses, negation `~`, conjunction `&`, disjunction `|`, implication `=>`, and equivalence `=`.

A formula is **valid** if, for every possible substitution of algebra elements for its variables, the formula evaluates to `1`.

For each formula, output `valid` or `invalid`.

---

## 2. Detailed editorial

### Key observation: antichains and ideals

The statement defines the algebra elements as antichains of the poset. Directly working with antichains is possible, but there is a much cleaner equivalent representation.

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 subset of the poset.

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

So instead of storing an algebra element as an antichain, we store it as the corresponding downward-closed set.

Since the statement guarantees `|H| ≤ 100`, there are at most `100` such ideals.

---

### Constants

In the statement:

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

Under the ideal representation:

```text
1 = empty ideal
0 = full set of all vertices
```

This may look reversed compared to Boolean logic, but it matches the ordering of this Heyting algebra.

---

### Computing reachability

We first compute the transitive closure of the DAG.

Let:

```text
up[x]   = set of vertices y such that x ≤ y
down[x] = set of vertices y such that y ≤ x
```

Both can be represented as bitsets.

The transitive closure can be computed using Floyd-Warshall style bitset propagation:

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

---

### Enumerating all ideals

Start with the empty ideal.

An element `x` can be added to an ideal `I` if all elements below `x`, except `x` itself, are already in `I`.

Equivalently:

```text
down[x] \ I = {x}
```

In bitset form:

```cpp
need = down[x] & ~I
need.count() == 1
```

Repeatedly adding such vertices enumerates all ideals.

Because the number of ideals is at most `100`, this is efficient.

---

### Operations on ideals

Suppose algebra elements `a` and `b` are represented by ideals `A` and `B`.

#### Conjunction

The statement defines:

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

In ideal representation:

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

So:

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

---

#### Disjunction

The statement defines disjunction using common lower bounds.

In ideal representation, this becomes:

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

So:

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

---

#### Implication

The statement defines:

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

In ideal representation, this means:

Take the maximal elements of `B` that are not already contained in `A`, then take their downward closure.

The implementation checks every vertex `x` such that:

1. `x ∈ B`
2. `x ∉ A`
3. `x` is maximal inside `B`

A vertex `x` is maximal inside `B` if:

```cpp
(up[x] & B).count() == 1
```

because only `x` itself among vertices reachable upward from `x` belongs to `B`.

Then:

```cpp
res |= down[x]
```

---

#### Negation

Negation is defined as:

```text
~a = a => 0
```

So after computing implication:

```cpp
not_tbl[i] = imp_tbl[i][zero_idx]
```

---

#### Equivalence

Equivalence is:

```text
a = b = (a => b) & (b => a)
```

So:

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

---

### Parsing formulae

The operators have the following precedence, from highest to lowest:

1. Parentheses, constants, variables
2. Negation `~`
3. Conjunction `&`, left-associative
4. Disjunction `|`, left-associative
5. Implication `=>`, right-associative
6. Equivalence `=`, lowest priority

Implication is right-associative:

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

Equivalence chains are expanded into conjunctions of pairwise equivalences:

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

becomes:

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

A recursive descent parser is natural here.

---

### Checking validity

For each formula:

1. Parse it into an expression tree.
2. Collect variables used in the formula.
3. Try every assignment of those variables to one of the `D = |H|` ideals.
4. Evaluate the expression using precomputed operation tables.
5. If every assignment evaluates to `1`, output `valid`; otherwise output `invalid`.

The statement guarantees the total work over all formulae is small enough.

---

## 3. C++ Solution

```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;
}
```

---

## 4. Python solution with detailed comments

```python
import sys
from itertools import product


# Token constants.
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

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


class Parser:
    def __init__(self, tokens, zero_idx, one_idx):
        # Token list of the current formula.
        self.tokens = tokens

        # Current parser position.
        self.pos = 0

        # Expression tree nodes.
        # Each node is a tuple: (operation, first_field, second_field).
        self.nodes = []

        # Algebra index of logical 0.
        self.zero_idx = zero_idx

        # Algebra index of logical 1.
        self.one_idx = one_idx

        # Variables used in this formula.
        self.used = [False] * 26

    def make_node(self, op, a, b=0):
        # Append a new expression-tree node.
        self.nodes.append((op, a, b))

        # Return index of the new node.
        return len(self.nodes) - 1

    def parse_atom(self):
        # Read current token.
        typ, val = self.tokens[self.pos]

        if typ == T_LPAR:
            # Skip '('.
            self.pos += 1

            # Parse full expression inside parentheses.
            node = self.parse_equiv()

            # Skip ')'.
            self.pos += 1

            # Return parsed subtree.
            return node

        if typ == T_ZERO:
            # Skip constant token.
            self.pos += 1

            # Store algebra element index of logical 0.
            return self.make_node(OP_CONST, self.zero_idx)

        if typ == T_ONE:
            # Skip constant token.
            self.pos += 1

            # Store algebra element index of logical 1.
            return self.make_node(OP_CONST, self.one_idx)

        # Otherwise this must be a variable.
        self.pos += 1

        # Mark variable as used.
        self.used[val] = True

        # Create variable node.
        return self.make_node(OP_VAR, val)

    def parse_neg(self):
        # Negation is unary and has high precedence.
        typ, _ = self.tokens[self.pos]

        if typ == T_NOT:
            # Skip '~'.
            self.pos += 1

            # Parse another negation-expression recursively.
            return self.make_node(OP_NOT, self.parse_neg())

        # If there is no '~', parse an atom.
        return self.parse_atom()

    def parse_conj(self):
        # Parse first operand.
        left = self.parse_neg()

        # Conjunction is left-associative.
        while self.tokens[self.pos][0] == T_AND:
            # Skip '&'.
            self.pos += 1

            # Combine current left expression with next operand.
            left = self.make_node(OP_AND, left, self.parse_neg())

        return left

    def parse_disj(self):
        # Parse first operand.
        left = self.parse_conj()

        # Disjunction is left-associative.
        while self.tokens[self.pos][0] == T_OR:
            # Skip '|'.
            self.pos += 1

            # Combine current left expression with next operand.
            left = self.make_node(OP_OR, left, self.parse_conj())

        return left

    def parse_impl(self):
        # Parse left operand.
        left = self.parse_disj()

        # Implication is right-associative.
        if self.tokens[self.pos][0] == T_IMP:
            # Skip '=>'.
            self.pos += 1

            # Recursively parse the right side.
            return self.make_node(OP_IMP, left, self.parse_impl())

        return left

    def parse_equiv(self):
        # Parse first term.
        terms = [self.parse_impl()]

        # Equivalence has lowest precedence.
        while self.tokens[self.pos][0] == T_EQ:
            # Skip '='.
            self.pos += 1

            # Parse next term.
            terms.append(self.parse_impl())

        # If there was no equivalence, return the single term.
        if len(terms) == 1:
            return terms[0]

        # Expand A=B=C into (A=B)&(B=C).
        node = 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])
            node = self.make_node(OP_AND, node, pair_eq)

        return node


def tokenize(s):
    # Result token list.
    tokens = []

    # Current character index.
    i = 0

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

        # Ignore whitespace.
        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 == "=":
            # Either implication '=>' or equivalence '='.
            if i + 1 < len(s) and s[i + 1] == ">":
                tokens.append((T_IMP, 0))
                i += 1
            else:
                tokens.append((T_EQ, 0))

        i += 1

    # Sentinel token.
    tokens.append((-1, 0))

    return tokens


def evaluate(root, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl):
    # Recursive evaluator of expression tree.
    op, a, b = nodes[root]

    if op == OP_CONST:
        # Constant stores algebra index directly.
        return a

    if op == OP_VAR:
        # Variable value comes from current assignment.
        return assignment[a]

    if op == OP_NOT:
        # Evaluate child and apply negation table.
        return not_tbl[evaluate(a, nodes, assignment, not_tbl, and_tbl, or_tbl, imp_tbl, eq_tbl)]

    if op == OP_AND:
        # Evaluate both operands and use precomputed conjunction table.
        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:
        # Evaluate both operands and use precomputed disjunction table.
        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:
        # Evaluate both operands and use precomputed implication table.
        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]

    # Remaining operation is equivalence.
    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():
    data = sys.stdin.read().splitlines()

    # Read first line.
    ptr = 0
    n, m = map(int, data[ptr].split())
    ptr += 1

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

    # Every vertex reaches itself.
    for i in range(n):
        up[i] |= 1 << i

    # Read edges.
    for _ in range(m):
        s, t = map(int, data[ptr].split())
        ptr += 1
        s -= 1
        t -= 1
        up[s] |= 1 << t

    # Compute 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] is a bitmask of vertices 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

    # Read number of formulae.
    K = int(data[ptr].strip())
    ptr += 1

    # Read formula lines.
    formulas = []
    while len(formulas) < K and ptr < len(data):
        line = data[ptr]
        ptr += 1
        if line.strip():
            formulas.append(line)

    # Full vertex set.
    full = (1 << n) - 1

    # Enumerate all ideals.
    H = [0]

    # Map ideal bitmask to its index.
    index = {0: 0}

    front = 0

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

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

            # Skip already present vertices.
            if cur & bit_x:
                continue

            # Vertices below x that are not yet in current ideal.
            need = down[x] & (full ^ cur)

            # We may add x iff the only missing predecessor is x itself.
            if need.bit_count() != 1:
                continue

            # Add x to form a new ideal.
            nxt = cur | bit_x

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

    # Number of algebra elements.
    d = len(H)

    # Logical 1 is empty ideal; logical 0 is full ideal.
    one_idx = index[0]
    zero_idx = index[full]

    # Allocate 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

    # Precompute conjunction, disjunction, and implication.
    for i in range(d):
        A = H[i]

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

            # Conjunction corresponds to union of ideals.
            and_tbl[i][j] = index[A | B]

            # Disjunction corresponds to intersection of ideals.
            or_tbl[i][j] = index[A & B]

            # Compute implication.
            res = 0

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

                # x must be in B.
                if not (B & bit_x):
                    continue

                # x must not be in A.
                if A & bit_x:
                    continue

                # x must be maximal in B.
                if (up[x] & B).bit_count() != 1:
                    continue

                # Add downward closure of x.
                res |= down[x]

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

    # Negation is implication to zero.
    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):
            eq_tbl[i][j] = and_tbl[imp_tbl[i][j]][imp_tbl[j][i]]

    output = []

    # Process formulae.
    for formula in formulas:
        # Convert string to tokens.
        tokens = tokenize(formula)

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

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

        # Current variable assignment.
        assignment = [0] * 26

        # Initially assume valid.
        valid = True

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

            # Formula must evaluate to logical 1.
            result = evaluate(
                root,
                parser.nodes,
                assignment,
                not_tbl,
                and_tbl,
                or_tbl,
                imp_tbl,
                eq_tbl,
            )

            if result != one_idx:
                valid = False
                break

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

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


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

---

## 5. Compressed editorial

Represent every antichain by its downward closure, i.e. by an order ideal. This gives a bijection because each ideal is determined by its maximal elements.

Compute reachability in the DAG to know the partial order. Enumerate all ideals starting from the empty ideal; a vertex `x` may be added to an ideal `I` iff all elements below `x` except `x` itself are already in `I`.

Under the ideal representation:

```text
1 = empty ideal
0 = full ideal
a & b = a ∪ b
a | b = a ∩ b
~a = a => 0
a = b = (a => b) & (b => a)
```

For implication `A => B`, take all maximal vertices of `B` that are not in `A`, and return their downward closure.

Precompute operation tables for all algebra elements. Then parse each formula using recursive descent according to precedence:

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

with `=>` right-associative and `=` expanded into conjunctions of pairwise equivalences.

For each formula, enumerate all assignments of its variables to algebra elements. If every assignment evaluates to `1`, print `valid`; otherwise print `invalid`.