Important Wires

A computer motherboard has several important wires, each in one of two binary states: live (true) or dead (false). The wires are named by the lowercase letters a through k, so there are at most 11 of them.

The wires cannot be observed directly. Instead, a maintenance socket exposes a number of output pins, each named by an uppercase letter. Every pin is driven by an integrated circuit, so its state is a fixed Boolean function of the wire states, given as a Boolean formula over the wires.

A formula is built from the constructs below, listed from the highest precedence to the lowest:

• Atom — a wire name (a lowercase letter a..k); its value is that wire's state.
• Parentheses — if E is a formula, then (E) is a formula.
• Negation — ~E (the highest-precedence operator).
• Conjunction — E1 & E2 & ... & En.
• Disjunction — E1 | E2 | ... | En.
• Implication — E1 => E2 => ... => En, evaluated from right to left, so E1 => E2 => E3 means E1 => (E2 => E3).
• Equivalence — E1 <=> E2 <=> ... <=> En, defined as (E1 <=> E2) & (E2 <=> E3) & ... & (E(n-1) <=> En).

As the wires range over all of their possible binary states, the pins take on various combinations of states. Your task is to count how many distinct combinations of pin states can occur.

Formally, list the pins as P1, ..., Pn in the order they are given in the input. Each assignment of live/dead states to the wires makes every pin evaluate to a definite state, yielding one tuple (P1, ..., Pn). Let w be the number of wires that appear in the formulas; report the number of distinct tuples obtained as the wire assignment ranges over all 2^w possibilities.

The first line contains a single integer n — the number of output pins (1 <= n <= 10).

Each of the next n lines describes one pin as an uppercase pin name, the token :=, and the pin's formula. A formula is a string over the tokens a..k, (, ), ~, &, |, =>, <=>, and spaces, where ~, &, |, =>, and <=> denote negation, conjunction, disjunction, implication, and equivalence respectively. Tokens may be separated by any number of spaces, and each line contains at most 1000 characters. Pin names are distinct.

Print a single integer: the number of distinct combinations of pin states that can occur as the wires range over all of their possible binary states.