Наталья Романова собирается протестировать новое оружие, которое ей выдали в S.H.I.E.L.D. Чтобы определить результат эксперимента, ей требуется найти количество решений следующего уравнения:
Здесь 
означает логическое ИЛИ (OR), а 
означает логическое исключающее ИЛИ (то есть XOR), а vi, j — булевы переменные и их отрицания. Наталья называет левую часть уравнения XNF формулой. Каждое условие в скобках называется клаузой, а переменные vi, j — литералами.
На самом деле в уравнении Натальи левая часть является 2-XNF-2 формулой от переменных x1, x2, ..., xm и их отрицаний. XNF формула называется 2-XNF-2 формулой, если:
- ki ≤ 2 для всех 1 ≤ i ≤ n, то есть размер каждой клаузы не превосходит двух.
- Каждая переменная встречается в формуле суммарно (как с отрицанием, так и без него) не более чем дважды. Обратите внимание, что переменная может дважды встретиться с отрицанием и ни разу без него (или наоборот).
У Натальи есть формула от m переменных, состоящая из n клауз. Обязательно посмотрите на примеры, чтобы убедиться, что вы правильно понимаете, как задаётся формула.
Наталья больше любит практику, чем теорию, поэтому просит вас найти количество решений уравнения, чтобы уже начать стрелять. Формально, требуется найти количество способов установить значения булевых переменных x1, ..., xm в true или false (всего существует 2m способов), так что равенство будет выполнено. Поскольку это число может быть очень большим, выведите остаток от его деления на 109 + 7.
Обратите внимание, что какая-то переменная может дважды появиться в одной и той же клаузе, а может не появиться вообще ни разу (однако присвоение ей true или false всё равно даёт разные способы).
Примечание
В первом примере уравнение имеет следующий вид:
Во втором примере уравнение выглядит так:
В третьем примере уравнение принимает вид:
