题目背景

译自 Potyczki Algorytmiczne 2016 R5 CNF-SAT [B] (CNF)。$\texttt{1s,256M}$。

题目描述

我们给定 SAT 问题的定义。本题中，不区分 $1$ 与 $\mathrm{True}$，$0$ 与 $\mathrm{False}$。

SAT 问题用来求出一组逻辑变量 $x_1,x_2,\cdots,x_n$ 的取值（其中 $x_i\in \{\mathrm{True},\mathrm{False}\}$），使得以下的合取范式取值为真：

其中，$(l_{i,1}\lor l_{i,2}\lor \ldots\lor l_{i,q_i})$ 称为子句（Clause），$l_{i,j}$ 是 $x_1,\ldots,x_n$ 中的变量或其否定。我们规定一个子句中，不存在 $j\lt k$，使得 $l_{i,j}$ 中的变量与 $l_{i,k}$ 中的变量相同。

某人声称解决了世界难题 $\mathrm{P}=\mathrm{NP?}$。他声称，一般的 SAT 问题都可以归约到一种特例，而这种特例中的所有子句都满足特殊性质：

• $\forall 1\le i\le n$，$x_i$ 和 $\neg x_i$ 不会同时在子句中出现。
• $\forall 1\le i\lt j\lt k\le n$，若子句中出现了 $x_i$（或 $\neg x_i$）和 $x_k$（或 $\neg x_k$），则必然有 $x_j$（或 $\neg x_j$）在这个子句中出现。

这里，所有出现的变量的下标都是 $1\sim n$。

给定满足特例的合取范式，统计有多少种不同的取值能够使其取值为真。只需要求出答案对 $(10^9+7)$ 取模后的结果。

输入格式

第一行，一个正整数 $n$，表示变量的数量。

第二行，描述一个由若干个子句组成的合取范式：

• 两个子句之间由 ^ 隔开（一个空格，和 ^，然后再是一个空格）。
• 每个子句由一对圆括号 () 包围。圆括号内部是若干变量，每个变量形如 xi 或者 ~xi（这里，x 是英文字母 $x$，i 是一个正整数），其中 xi 表示 $x_i$，~xi 表示 $\neg x_i$。两个变量之间用 v 隔开（一个空格，和英文字母 v，然后再是一个空格）。

这里，保证有 $1\le i\le n$，且子句满足题目描述中的特殊性质。

输出格式

输出答案对 $(10^9+7)$ 取模后的结果。

3
(x2) ^ (x3 v ~x2) ^ (x2 v x1 v ~x3)

2

提示

样例解释

两个合法解为 $(0,1,1)$ 和 $(1,1,1)$。

数据范围

• $1\le n\le 10^6$；
• 所有子句中变量个数的和不超过 $10^6$。