Problem D. Important Wires ≡

Statement

Nick bought a new motherboard for his computer and it seems that it does not work properly. The motherboard is pretty complicated but it has only few important wires that have binary states: live or dead. Nick wants to know the states of these wires.

Unfortunately, important wires are not directly accessible. But Nick found a maintenance socket. Each output pin of this socket is connected to some of important wires via an integrated circuit. Fortunately, Nick found the circuit layout in the Internet. To specify it, he marked important wires by lowercase letters and socket's output pins by uppercase letters. After that he wrote down Boolean formula for each output pin. In these formulae live wires and pins are represented by true and dead wires — by false.

Nick used following notation for formulae (operations are listed from the highest priority to the lowest):

• Pin names — letters from 'a' to 'k';
• Parentheses — if E is a formula, then (E) is another;
• Negation — ¬ E is a formula for any formula E;
• Conjunction — E₁ ∧ E₂ ∧ ⋯ ∧ E_n;
• Disjunction — E₁ ∨ E₂ ∨ ⋯ ∨ E_n;
• Implication — E₁⇒ E₂⇒ ⋯ ⇒ E_n. Implication is evaluated from right to left: E₁⇒ E₂⇒ E₃ means E₁⇒ (E₂⇒ E₃);
• Equivalence — E₁ ≡ E₂ ≡ ⋯ ≡ E_n. This expression is by definition computed as follows: (E₁ ≡ E₂) ∧ (E₂ ≡ E₃) ∧ ⋯ ∧ (E_n − 1 ≡ E_n).

Nick has lots of various gates at hand, so he can build a new circuit that implements any formula. The variables of this formula are states of maintenance socket's pins. First of all, Nick wants to construct a circuit that takes all maintenance socket's pins as inputs and has a single output wire that is always live. Write a program to help him.

Input file format

The first line of the input file contains a single integer number n — the number of pins in the maintenance socket. The following n lines contain description of one pin each.

Each pin description consists of a pin name and corresponding formula delimited by ':=' token. Pin name is a uppercase English letter. Formula is represented by a string consisting of tokens 'a'..'k', '(', ')', '~', '&', '|', '=>', and '<=>'. The last five tokens stand for ¬, ∧, ∨, ⇒ and ≡ respectively. Tokens can be separated by an arbitrary number of spaces.

Output file format

The first line of the output file must contain "Yes" if there exists a circuit which output wire is always live and "No" otherwise.

In the former case the following line must contain the formula for the constructed circuit in the same format as in the input file. Remember that the formula must contain each of pin names at least once and it must not contain the wire names. The line must not exceed 1000 characters.

Constraints

1 ≤ n ≤ 10.

Each pin description contains 1000 characters at most.

Sample tests

3
A := (a=>c )& (b<=>d)
C:= a | b
B := c | d

Yes
C&A => B | ~A