Fixing a logic system 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), -&gt; (if) and &lt;-&gt; (iff).

Truth table:

A | B | -A | AvB | A^B | A-&gt;B | A&lt;-&gt;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)-&gt;(-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&lt;-&gt;B)
(AvB)-&gt;(-B)


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

A^B
-(B&lt;-&gt;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" / "^" / "-&gt;" / "&lt;-&gt;"


Example statements:

A
Av(-B)
(A&lt;-&gt;(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&lt;-&gt;(-B) A&lt;-&gt;B


Output:

A^B A&lt;-&gt;B


Input:

["AvB","A^B"]


Output:

["AvB","A^B"]
Python 3, 431 bytes



Not very golfed right now, but I figure I'd get the ball rolling with an answer. Try it here, g() is the main function.

import re,itertools as H
def g(i):
 y=re.sub(r'\W','',''.join(set(i)).upper());l=i.split()
 def e(s):
  def f(a):
   for v,w in a:exec(v+'='+w)
   return eval(re.sub('[^A-Z()]+',lambda x:{'v':' or ','^':'*','&lt;-&gt;':'==','-&gt;':'&lt;=','-':'not '}[x.group()],s))
  return[c for c in H.product("01",repeat=len(y))if f(zip(y,c))]
 for n in range(len(l),-1,-1):
  for q in H.combinations(l,n):
   if e('('+')^('.join(q)+')'):return' '.join(q)