又是一年 $P = NP$ 平等游行。今年，$P = NP$ 运动的非正式领袖 Bajtazar 决定在游行中宣布他关于这一著名等式的证明，从而彻底平息反对者的质疑。
Bajtazar 的证明在于展示了一个能在多项式时间内解决著名的 NP-难问题 CNF-SAT 的算法。在该问题中，给定 $n$ 个逻辑变量 $x_1, \dots, x_n$ 以及一个合取范式（CNF）形式的逻辑公式。该公式的形式为：
$$(l_{1,1} \vee \dots \vee l_{1,q_1}) \wedge (l_{2,1} \vee \dots \vee l_{2,q_2}) \wedge \dots \wedge (l_{m,1} \vee \dots \vee l_{m,q_m}),$$
其中每个表达式 $(l_{i,1} \vee \dots \vee l_{i,q_i})$ 称为一个子句，每个 $l_{i,j}$ 是一个文字，即变量 $x_1, \dots, x_n$ 中的某个变量或其否定。我们假设没有任何合法的子句包含两个相同的文字。对于 $n = m = 3$，合取范式的一个示例如 $(x_1 \vee \neg x_3) \wedge (x_2) \wedge (\neg x_3 \vee \neg x_1 \vee x_2)$。
CNF-SAT 问题旨在判定是否存在一组变量 $x_1, \dots, x_n$ 的赋值，使得给定的公式为真。
遗憾的是，Bajtazar 的证明还差最后一步。他声称已经将一般的 CNF-SAT 问题归约到了一个特殊情况，即公式中的每个子句 $C$ 都是“连贯的”，即满足以下性质：
- 对于任意 $i$，$x_i$ 和 $\neg x_i$ 不能同时作为 $C$ 中的文字。
- 如果 $i < j < k$，且变量 $x_i$（或其否定）与 $x_k$（或其否定）都出现在子句 $C$ 中，则 $x_j$ 或 $\neg x_j$ 也必须出现在 $C$ 中。
例如，当 $n = 3$ 时，子句 $(x_2)$ 和 $(\neg x_3 \vee \neg x_1 \vee x_2)$ 是连贯的，而 $(x_2 \vee \neg x_2)$ 和 $(x_1 \vee \neg x_3)$ 则不是。
请帮助 Bajtazar 找到解决该特殊情况 CNF-SAT 问题的有效算法。为了让他更加惊讶，请编写一个程序，计算满足给定由连贯子句组成的 CNF-SAT 公式的变量 $x_1, \dots, x_n$ 的赋值方案数。
输入格式
第一行包含一个整数 $n$ ($1 \le n \le 1\,000\,000$)，表示变量的数量。 第二行包含一个由连贯子句组成的 CNF-SAT 公式。公式的格式如下（参见下方的样例）：
- 每个子句以左括号
(开头，以右括号)结尾。 - 文字 $x_i$ ($1 \le i \le n$) 表示为
xi，文字 $\neg x_i$ 表示为~xi，例如x2或~x15。 - 同一子句内的相邻文字由
v（表示逻辑或）分隔，两侧各有一个空格。 - 相邻子句由
^（表示逻辑与）分隔，两侧各有一个空格。
所有子句中文字的总数不超过 $1\,000\,000$。
输出格式
输出满足输入公式的变量 $x_1, \dots, x_n$ 的赋值方案数，结果对 $10^9 + 7$ 取模。
样例
输入 1
3 (x2) ^ (x3 v ~x2) ^ (x2 v x1 v ~x3)
输出 1
2
说明 1
该公式仅在以下两种赋值下为真：$(0, 1, 1)$ 和 $(1, 1, 1)$。