/*
 * vim:tw=76:ts=4:sts=4:sw=4:cindent:expandtab
 */

#include <stdio.h>
#include <ctype.h>
#include <string.h>
#include <stdlib.h>
#include <stdint.h>
#include <inttypes.h>

#define max_level 100
#define max_degree 6000
#define max_cols 6000
#define max_nodes 1000000

#define root col_array[0]

#define buf_size ((8*max_cols)+3)

#define panic(m) {fprintf(stderr,"%s!\n%s",m,buf) ;exit(1) ;} \

#include <stdio.h>
#include <ctype.h>
#include <string.h>
#include <stdlib.h>

typedef struct node_struct {
    struct node_struct *left, *right;
    struct node_struct *up, *down;
    struct col_struct *col;
    int color;
} node;

typedef struct col_struct {
    node head;
    int len;
    char name[8];
    struct col_struct *prev, *next;
} column;

int verbose;
int count = 0;
uint64_t updates;
uint64_t purifs;
int spacing = 1;
int profile[max_level][max_degree];
unsigned int upd_prof[max_level];
unsigned int pur_prof[max_level];
int maxb = 0;
int maxl = 0;

column col_array[max_cols + 2];
node node_array[max_nodes];
node *cutoff = &node_array[max_nodes];
char buf[buf_size];
column *first_nonprim_col;
column *last_nonprim_col;

int level;
node *choice[max_level];

void print_row(p)
node *p;
{
    node *q = p;
    int k;

    do {
        printf(" %s", q->col->name);
        if (q->color)
            printf(":%c", q->color > 0 ? q->color : q->col->head.color);
        q = q->right;
    } while (q != p);

    for (q = p->col->head.down, k = 1; q != p; k++) {
        if (q == &(p->col->head)) {
            printf("\n");
            return;
        } else {
            q = q->down;
        }
    }
    printf(" (%d of %d)\n", k, p->col->len);
}

void cover(column *c)
{
    column *l, *r;
    node *rr, *nn, *uu, *dd;
    int k = 1;

    l = c->prev;
    r = c->next;
    l->next = r;
    r->prev = l;
    for (rr = c->head.down; rr != &(c->head); rr = rr->down) {
        for (nn = rr->right; nn != rr; nn = nn->right) {
            uu = nn->up;
            dd = nn->down;
            uu->down = dd;
            dd->up = uu;
            k++;
            nn->col->len--;
        }
    }
    updates += k;
    upd_prof[level] += k;
}

void uncover(column *c)
{
    column *l, *r;
    node *rr, *nn, *uu, *dd;

    for (rr = c->head.up; rr >= cutoff; rr = rr->up) {
        if (rr == &(c->head))
            break;
        c->len--;
    }

    c->head.up = rr, rr->down = &(c->head);
    for (; rr != &(c->head); rr = rr->up) {
        for (nn = rr->left; nn != rr; nn = nn->left) {
            uu = nn->up;
            dd = nn->down;
            if (dd >= cutoff)
                nn->down = dd = &(nn->col->head);
            uu->down = dd->up = nn;
            nn->col->len++;
        }
    }
    l = c->prev;
    r = c->next;
    l->next = r->prev = c;
}

void purify(node *p)
{
    column *c = p->col;
    int x = p->color;
    node *rr, *nn, *uu, *dd;
    int k = 0, kk = 1;

    c->head.color = x;
    for (rr = c->head.down; rr != &(c->head); rr = rr->down) {
        if (rr->color != x) {
            for (nn = rr->right; nn != rr; nn = nn->right) {
                uu = nn->up;
                dd = nn->down;
                uu->down = dd;
                dd->up = uu;
                k++;
                nn->col->len--;
            }
        } else if (rr != p)
            kk++, rr->color = -1;
    }

    updates += k;
    purifs += kk;
    upd_prof[level] += k, pur_prof[level] += kk;
}

void unpurify(node *p)
{
    column *c = p->col;
    int x = p->color;
    node *rr, *nn, *uu, *dd;

    for (rr = c->head.up; rr >= cutoff; rr = rr->up) {
        if (rr == &(c->head))
            break;
    }

    c->head.up = rr, rr->down = &(c->head);
    for (; rr != &(c->head); rr = rr->up) {
        if (rr->color < 0) {
            rr->color = x;
        } else if (rr != p) {
            for (nn = rr->left; nn != rr; nn = nn->left) {
                uu = nn->up;
                dd = nn->down;
                if (dd >= cutoff)
                    nn->down = dd = &(nn->col->head);
                uu->down = dd->up = nn;
                nn->col->len++;
            }
        }
    }
    c->head.color = 0;
}

void show_state()
{
    int k;

    printf("Current state (level %d):\n", level);
    for (k = 0; k < level; k++)
        print_row(choice[k]);
    printf("Max level so far: %d\n", maxl);
    printf("Max branching so far: %d\n", maxb);
    printf("Solutions so far: %d\n", count);
}

int main(int argc, char *argv[])
{
    column *cur_col;
    char *p, *q;
    node *cur_node;
    int primary;
    column *best_col = NULL;
    node *pp;
    int minlen;
    int j, k, x;

    verbose = argc - 1;
    if (verbose)
        sscanf(argv[1], "%d", &spacing);

    cur_col = col_array + 1;
    fgets(buf, buf_size, stdin);
    if (buf[strlen(buf) - 1] != '\n')
        panic("Input line too long");
    for (p = buf, primary = 1; *p; p++) {
        while (isspace(*p))
            p++;
        if (!*p)
            break;
        if (*p == '|') {
            primary = 0;
            if (cur_col == col_array + 1)
                panic("No primary columns");
            (cur_col - 1)->next = &root, root.prev = cur_col - 1;
            first_nonprim_col = cur_col;
            continue;
        }
        for (q = p + 1; !isspace(*q); q++);
        if (q > p + 7)
            panic("Column name too long");
        if (cur_col >= &col_array[max_cols])
            panic("Too many columns");
        for (q = cur_col->name; !isspace(*p); q++, p++)
            *q = *p;
        cur_col->head.up = cur_col->head.down = &cur_col->head;
        cur_col->len = 0;
        if (primary)
            cur_col->prev = cur_col - 1, (cur_col - 1)->next = cur_col;
        else
            cur_col->prev = cur_col->next = cur_col;
        cur_col++;
    }
    if (primary) {
        if (cur_col == col_array + 1)
            panic("No primary columns");
        (cur_col - 1)->next = &root, root.prev = cur_col - 1;
        first_nonprim_col = cur_col;
    }
    last_nonprim_col = cur_col;

    cur_node = node_array;
    while (fgets(buf, buf_size, stdin)) {
        column *ccol;
        node *row_start, *x;

        if (buf[strlen(buf) - 1] != '\n')
            panic("Input line too long");
        row_start = NULL;
        for (p = buf; *p; p++) {
            while (isspace(*p))
                p++;
            if (!*p)
                break;
            for (q = p + 1; !isspace(*q) && *q != ':'; q++);
            if (q > p + 7)
                panic("Column name too long");
            for (q = cur_col->name; !isspace(*p) && *p != ':'; q++, p++)
                *q = *p;
            *q = '\0';
            for (ccol = col_array; strcmp(ccol->name, cur_col->name);
                 ccol++);
            if (ccol == cur_col)
                panic("Unknown column name");
            if (cur_node == &node_array[max_nodes])
                panic("Too many nodes");
            if (!row_start)
                row_start = cur_node;
            else
                cur_node->left = cur_node - 1, (cur_node - 1)->right =
                    cur_node;
            for (x = row_start; x != cur_node; x++)
                if (x->col == ccol)
                    panic("A row can't use a column twice");
            cur_node->col = ccol;
            cur_node->up = ccol->head.up, ccol->head.up->down = cur_node;
            ccol->head.up = cur_node, cur_node->down = &ccol->head;
            ccol->len++;
            if (*p == ':') {
                if (ccol < first_nonprim_col)
                    panic("Color isn't allowed in a primary column");
                if (isspace(*(p + 1)) || !isspace(*(p + 2)))
                    panic("Color should be a single character");
                cur_node->color = *(p + 1);
                p += 2;
            }
            cur_node++;
        }
        if (!row_start)
            panic("Empty row");
        row_start->left = cur_node - 1, (cur_node - 1)->right = row_start;
    }

    level = 0;
  forward:
    minlen = max_nodes;
    if (verbose > 2)
        printf("Level %d:", level);
    for (cur_col = root.next; cur_col != &root; cur_col = cur_col->next) {
        if (verbose > 2)
            printf(" %s(%d)", cur_col->name, cur_col->len);
        if (cur_col->len < minlen)
            best_col = cur_col, minlen = cur_col->len;
    }
    if (verbose) {
        if (level > maxl) {
            if (level >= max_level)
                panic("Too many levels");
            maxl = level;
        }
        if (minlen > maxb) {
            if (minlen >= max_degree)
                panic("Too many branches");
            maxb = minlen;
        }
        profile[level][minlen]++;
        if (verbose > 2)
            printf(" branching on %s(%d)\n", best_col->name, minlen);
    }

    cover(best_col);
    cur_node = choice[level] = best_col->head.down;
  advance:
    if (cur_node == &(best_col->head))
        goto backup;
    if (verbose > 1) {
        printf("L%d:", level);
        print_row(cur_node);
    }

    for (pp = cur_node->right; pp != cur_node; pp = pp->right) {
        if (!pp->color)
            cover(pp->col);
        else if (pp->color > 0)
            purify(pp);
    }

    if (root.next == &root) {
        count++;
        for (k = 0, cutoff = NULL; k <= level; k++) {
            if (choice[k] >= cutoff) {
                for (pp = choice[k]; pp->right > pp; pp = pp->right);
                cutoff = pp + 1;
            }
        }

        for (k = 0; k <= level; k++) {
            cur_col = choice[k]->col;
            for (pp = cur_col->head.up, j = 0; pp >= cutoff; pp = pp->up)
                j++;
            if (j) {
                pp->down = &(cur_col->head);
                cur_col->head.up = pp;
                cur_col->len -= j;
            }
        }

        if (verbose) {
            profile[level + 1][0]++;
            if (count % spacing == 0) {
                printf("%d:\n", count);
                for (k = 0; k <= level; k++)
                    print_row(choice[k]);
            }
        }
        goto recover;
    }

    level++;
    goto forward;
  backup:
    uncover(best_col);
    if (level == 0)
        goto done;
    level--;
    cur_node = choice[level];
    best_col = cur_node->col;
  recover:
    for (pp = cur_node->left; pp != cur_node; pp = pp->left)
        if (!pp->color)
            uncover(pp->col);
        else if (pp->color > 0)
            unpurify(pp);

    cur_node = choice[level] = cur_node->down;
    goto advance;
  done:
    if (verbose > 3) {
        printf("Final column lengths");
        for (cur_col = root.next; cur_col != &root;
             cur_col = cur_col->next)
            printf(" %s(%d)", cur_col->name, cur_col->len);
        printf("\n");
    }

    printf("Altogether %d solutions,", count);
    printf(" after %" PRIu64 " updates", updates);
    printf(" and %" PRIu64 " cleansings.\n", purifs);

    if (verbose) {
        x = 1;
        for (level = 1; level <= maxl + 1; level++) {
            j = 0;
            for (k = 0; k <= maxb; k++) {
                printf("%6d", profile[level][k]);
                j += profile[level][k];
            }
            printf("%8d nodes, %u updates, %u cleansings\n",
                   j, upd_prof[level - 1], pur_prof[level - 1]);
            x += j;
        }
        printf("Total %d nodes.\n", x);
    }

    exit(0);
}