# reads a solution from a SAT solver, given the original yices-generated CNF.

import sys

if len(sys.argv) == 0:
    print("You've met with a terrible fate.", file=sys.stderr)
    sys.exit(1)

if len(sys.argv) != 3:
    print(f'usage: {sys.argv[0]} {{problem file}} {{solution file}}', file=sys.stderr)
    sys.exit(1)

prob, sol = sys.argv[1:]

if prob == '-':
    prob = sys.stdin
else:
    prob = open(prob, 'r')

if sol == '-':
    sol = sys.stdin
else:
    sol = open(sol, 'r')

pairs = dict()
for line in prob:
    tokens = line.split()
    if tokens[0] == 'c' and len(tokens) > 4 and tokens[2] == '-->':
        key = tokens[1]
        ids = tokens[3:]
        ids = [t.strip('[]') for t in ids]
        ids = [int(t) for t in ids]
        if -1 in ids:
            continue
        pairs[key] = ids
    if tokens[0] == 's':
        assert tokens[1] == 'SATISFIABLE', 'unsatisfiable'
        break
    assert tokens[0] != 'v', 'solution occurred too early to parse'

if prob != sol and prob != sys.stdin:
    prob.close()

bools = dict()
for line in sol:
    tokens = line.split()
    if tokens[0] == 'v':
        for i in tokens[1:]:
            i = int(i)
            bools[abs(i)] = i > 0

if sol != sys.stdin:
    sol.close()

bvs = dict((key, 0) for key in pairs.keys())
for key, ids in pairs.items():
    for i, id in enumerate(ids):
        if bools[id]:
            bvs[key] |= 1 << i

for key, value in bvs.items():
    print(key, value)