#!/usr/bin/env python3
import sys
from pprint import PrettyPrinter
from os import fstat
from stat import S_ISFIFO, S_ISREG
from itertools import product

_pp = PrettyPrinter(indent=2).pprint
_is_terminal = all(not f(fstat(0).st_mode) for f in [S_ISFIFO, S_ISREG])


def _print_color(*args, **kwargs):
    print('\033[04m', *args, '\033[0m', sep='')

def readline():
    str = sys.stdin.readline().strip()
    if not _is_terminal: _print_color(str)
    return str

def to_binary(x, fill):
    return bin(x)[2:].zfill(fill)

def count_one(x):
    return x.count('1')

def try_merge(x, y):
    # Thanks @YuRen-tw for improving this function
    mer = ''.join((a if a == b else
                   ('x' if a != '-' and b != '-' else 'e'))
                  for a, b in zip(x, y))
    return mer.replace('x', '-') if (mer.count('x') <= 1 and
                                     mer.count('e') == 0) else None

def term_expr(x):
    return ''.join([
             chr(i + ord('a'))        if c == '1'
        else chr(i + ord('a')) + '\'' if c == '0'
        else ''
    for i, c in enumerate(x) ])

def input_expr(inp):
    return ' + '.join([term_expr(to_binary(k, nvar)) for k in inp])


def set_cover(instance):
    # returns a list of minimal number of terms
    len_inst = len(instance)
    len_vert = len(instance[0])
    pick_opti = len_inst
    sol_set = []

    # states are encoded as inverted bitsets
    state_acc = (1 << len_vert) - 1

    def __recur(depth, pick_cnt, pick, state):
        nonlocal pick_opti
        print('depth',  depth,
              'picked', pick_cnt,
              'state',  to_binary(state, len_vert)[::-1])
        if state == state_acc:
            print('Covered all implicants with {} terms ({})!'.format(
                pick_cnt, to_binary(pick, len_inst)[::-1]))
            win = pick_opti - pick_cnt
            if win > 0:
                sol_set.clear()
            if win >= 0:
                pick_opti = pick_cnt
                sol_set.append(to_binary(pick, len_inst))
            return
        # prune
        if depth == len_inst or pick_cnt == pick_opti: return
        # pick and cover
        state_add = sum([1 << i for i, k in enumerate(instance[depth]) if k])
        __recur(depth + 1, pick_cnt,     pick             , state            )
        __recur(depth + 1, pick_cnt + 1, pick | 1 << depth, state | state_add)

    __recur(0, 0, 0, 0)
    sol_opti = (list(k) for k in (k[::-1] for k in sol_set))
    return [[p for p, k in enumerate(x) if k == '1'] for x in sol_opti]

def solver(nvar, one_term, dc_term):
    all_term = sorted(one_term + dc_term)

    bucket = [{} for _ in range(nvar + 1)]
    for i in all_term:
        tbin = to_binary(i, nvar)
        zcube = {i}
        bucket[count_one(tbin)][tbin] = zcube

    while True:
        ok = True
        # XXX: wasting memory
        rm_term = [set() for _ in range(len(bucket))]
        # XXX: to be more functional
        for i in range(len(bucket) - 1):
            this_bucket, next_bucket = bucket[i], bucket[i + 1]
            print('Merging bucket #{}'.format(i))
            for a, b in product(this_bucket, next_bucket):
                mer = try_merge(a, b)
                if mer is None: continue
                print('  {} | {} -> {}; merge {} with {}'.format(
                    a, b, mer, this_bucket[a], next_bucket[b]
                ))
                # mark to delete
                rm_term[i].add(a)
                rm_term[i + 1].add(b)
                # add merged term
                if mer not in this_bucket:
                    this_bucket[mer] = this_bucket[a] | next_bucket[b]
                    ok = False
            for x in rm_term[i]:
                print('  remove {}'.format(x))
                del this_bucket[x]
        for x in rm_term[-1]:
            del bucket[-1][x]
        _pp(bucket)
        print()
        if ok: break
        print('NEXT ITERATION ---------------------------------')

    terms = [ kv for d in bucket for kv in d.items() ]
    print('implicants -------------------------------------')
    _pp(terms)

    sat = [[int(i in v) for i in one_term] for k, v in terms]
    print('set covering instance --------------------------')
    print(list(str(x).rjust(2) for x in one_term))
    for row in sat:
        _pp([ 'xx' if k else '  ' for k in row])

    # do set covering on `sat` and convert every possible result in `term_expr`
    if sat:
        sol_set = set_cover(sat)
        ans = [' + '.join([term_expr(terms[idx][0]) for idx in sol])
               for sol in sol_set]

        print()
        print('SOLVED -----------------------------------------')
        sat_opti = len(sol_set[0])
        print('Simplifing \033[01m\033[34m\u03a3m({}) + \u03a3d({})\033[0m'
              .format(input_expr(one_term), input_expr(dc_term)));
        print('With \033[01m{}\033[0m term(s) optimially...'.format(sat_opti));

        for rec in ans:
            print(rec or '[T]')

    else:
        print()
        print('UNSATISFABLE!! ---------------------------------')


if __name__ == '__main__':
    try:
        print('Number of variables [2-10]: ', end='', flush=True)
        nvar = int(readline())
        if nvar < 2: abort()
        npower = 2 ** nvar
    except:
        print('[END]')
        exit(0)

    print('Minterms (0..{}): '.format(npower - 1), end='', flush=True)
    one_term = [int(_) for _ in readline().split(' ') if _]

    print('Don\'t care terms (0..{}): '.format(npower - 1), end='', flush=True)
    dc_term = [int(_) for _ in readline().split(' ') if _]
    solver(nvar, one_term, dc_term)