The next Equality Parade $P = NP$ is approaching. This year, the informal leader of the $P = NP$ movement, Bajtazar, has decided to finally silence his numerous opponents by announcing a proof of the famous equality at the Parade.
Bajtazar's proof consists of showing an algorithm that solves the well-known NP-hard problem CNF-SAT in polynomial time. In this problem, we are given $n$ logical variables $x_1, \dots, x_n$ and a logical formula in so-called conjunctive normal form. Such a formula is of the form:
$$(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}),$$
where each expression $(l_{i,1} \vee \dots \vee l_{i,q_i})$ is called a clause, and each expression $l_{i,j}$ is a literal, i.e., a certain variable or the negation of a variable from the given $x_1, \dots, x_n$. We assume that no valid clause contains two identical literals. For $n = m = 3$, an example formula in conjunctive normal form could be $(x_1 \vee \neg x_3) \wedge (x_2) \wedge (\neg x_3 \vee \neg x_1 \vee x_2)$.
The CNF-SAT problem consists of determining whether there exists an assignment of variables $x_1, \dots, x_n$ for which the given formula is satisfied (that is, its logical value is true).
Unfortunately, Bajtazar is missing one step to complete his proof. He claims that he has managed to reduce* the general CNF-SAT problem to its special case, where every clause $C$ of the given formula is consistent, meaning it has the following properties:
- For any $i$, $x_i$ and $\neg x_i$ cannot both be literals in $C$.
- If $i, j, k$ are such that $i < j < k$ and both the variable $x_i$ (or its negation) and $x_k$ (or $\neg x_k$) appear in clause $C$, then $x_j$ or $\neg x_j$ also appears in $C$.
For example, for $n = 3$, the clauses $(x_2)$ and $(\neg x_3 \vee \neg x_1 \vee x_2)$ are consistent, while the clauses $(x_2 \vee \neg x_2)$ and $(x_1 \vee \neg x_3)$ are not.
Help Bajtazar find an efficient algorithm to solve this special case of the CNF-SAT problem. To surprise him even more, write a program that finds the number of assignments of variables $x_1, \dots, x_n$ satisfying the given CNF-SAT formula consisting only of consistent clauses.
Input
The first line of input contains an integer $n$ ($1 \le n \le 1\,000\,000$) representing the number of variables. The second line of input contains the given CNF-SAT formula on variables $x_1, \dots, x_n$, consisting only of consistent clauses. The formula is given in the following format (see also the example below):
- Each clause begins with an opening parenthesis
(and ends with a closing parenthesis). - A literal $x_i$ (for $1 \le i \le n$) is represented as
xi, and a literal $\neg x_i$ as~xi, e.g.,x2or~x15. - Adjacent literals within one clause are separated by the character
v(denoting logical OR) surrounded on both sides by single spaces. - Adjacent clauses are separated by the character
^(denoting logical AND) surrounded on both sides by single spaces.
The total number of literals in all clauses of the given formula will not exceed $1\,000\,000$.
Output
Output the number of assignments of variables $x_1, \dots, x_n$ that satisfy the given formula, modulo $10^9 + 7$.
Examples
Input 1
3 (x2) ^ (x3 v ~x2) ^ (x2 v x1 v ~x3)
Output 1
2
Note 1
The given formula is satisfied only for two assignments: $(0, 1, 1)$ and $(1, 1, 1)$.
*Bajtazar forgot to mention whether his reduction worked in polynomial time...