#!/usr/bin/env python3
import re
import sys

# Maximum number of elements
n = 8

matrix = []

for line in sys.stdin:
    line = line.strip()
    if line == "unsat":
        sys.exit('unsat!')
    if line == "sat":
        continue
    m = re.match(r'a(\d+)_(\d+) -> (\d+)', line)
    var_number, step, value = map(int, m.groups())

    # auto-detect size, extending matrix size if necessary.
    while len(matrix) <= step:
        matrix.append([None] * n)

    matrix[step][var_number - 1] = value

# List of cells that have changed since the previous iteration. Note that the
# first row has no changed cell and therefore stores "None"
changedCells = [None]
for i, cells in enumerate(matrix):
    if i == 0:
        continue # skip first row
    previousRow = matrix[i - 1]
    for col, prevValue in enumerate(previousRow):
        if cells[col] != prevValue:
            # Found changed cell!
            changedCells.append(col)
            break
    else:
        # Should not happen! Something got stuck?
        changedCells.append(None)

line = "  "
for col in range(len(matrix[0])):
    line += " & $a_%d$" % (col + 1)
line += r" \\"
print(line)
print(r"\hline")

for step, cells in enumerate(matrix):
    line = "%2d" % step
    for col, value in enumerate(cells):
        if changedCells[step] == col:
            line += r" & \bf%2d" % value
        else:
            line += " & %5d" % value
    line += r" \\"
    if step > 0 and changedCells[step] is None:
        line += " % unchanged!"
    print(line)