You are given a set of logic statements. Your challenge is to remove any ones that contradict the others, but in the optimal way (i.e. removing a minimal number of statements).

###Challenge

You will write a program or a function that takes as input a list of statements, removes the minimal number of statements such that there is a solution and outputs the rest.

###Logic

Statements consist of variables A-Z and operators between them.

There are 5 operators: - (not), v (or), ^ (and), -> (if) and <-> (iff).

Truth table:

A | B | -A | AvB | A^B | A->B | A<->B
0 | 0 |  1 |  0  |  0  |   1  |   1
0 | 1 |  1 |  1  |  0  |   1  |   0
1 | 0 |  0 |  1  |  0  |   0  |   0
1 | 1 |  0 |  1  |  1  |   1  |   1

These operators can be combined together with parenthesis ():

A | B | -(AvB) | Av(-A) | A^(-A) | (AvB)->(-B)
0 | 0 |    1   |    1   |    0   |      1
0 | 1 |    0   |    1   |    0   |      0
1 | 0 |    0   |    1   |    0   |      1
1 | 1 |    0   |    1   |    0   |      0

Logic systems consist of 1 or more statements.

A solution to the logic system is a state where all of the statements are simultaneously true.

###Examples of logic systems:

AvB
-(A<->B)
(AvB)->(-B)

The only solution is A = 1, B = 0.

A^B
-(B<->A)

This one has no solution; with no combination of A and B both of the statements are true.

###Input

You will receive a set of statements as input. This can be taken via STDIN or function arguments, formatted as an array (in a convenient format) or a newline-separated or space-separated string.

The statements will be of the following form (in almost-ABNF):

statement        = variable / operation
operation        = not-operation / binary-operation
not-operation    = "-" operand
binary-operation = operand binary-operator operand
operand          = variable / "(" operation ")"
variable         = "A"-"Z"
binary-operator  = "v" / "^" / "->" / "<->"

Example statements:

A
Av(-B)
(A<->(Q^C))v((-B)vH)

###Output

You must return the (possibly) reduced set of statements, in the exact form you received them. Again, the list can be formatted as an array of strings or a newline-separated or space-separated string.

###Rules

• You should always remove the minimal number of statements. If there are multiple possible solutions, output one of them.
• You may assume that the input always contains at least 1 statement and that no statements are repeated in the input.
• You may not assume that the output always contains a statement. (see examples)
• Using standard loopholes contradicts with your answer being valid, and one of them must be removed.
• This is code-golf, so the shortest answer in bytes wins.

###Examples

Input:

A^(-A)

Output:

(nothing)

Input:

A^B A<->(-B) A<->B

Output:

A^B A<->B

Input:

["AvB","A^B"]

Output:

["AvB","A^B"]