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

#define MAXN 60

/* Precomputed binomial numbers \binom{n}{k}.  */
static unsigned long long nnadk[MAXN][MAXN + 1];
static void
precompute_nnadk (void)
{
  int n, k;

  for (n = 0; n < MAXN; n++)
    {
      nnadk[n][0] = 1;
      for (k = 1; k <= n; k++)
	{
	  nnadk[n][k] = nnadk[n - 1][k - 1] + nnadk[n - 1][k];

	  if (nnadk[n][k] >> 62)
	    abort ();
	}
    }
}

/* The description of a face.  */
struct face
{
  /* The range for the size of the set of colors not forbidden by the precoloring
     of the vertices of the face outside of the configuration.  */
  int remco_f, remco_t;

  /* The list and the number of non-internal vertices incident with the face.  */
  int adjsing[100];
  int nadj;

  /* In case the face is external (remco_f = 0), the id of the set of colors
     not forbidden by the outside vertices of the face.  */
  int setno;
};

/* The faces of the reducent graph.  */
#define MAXF 10
static struct face faces[MAXF];
static int nf;

/* singletons[i] is true if the non-internal vertex 'a' + i appears in the
   configuration and the reducent; ...  */
static int singletons[26];

/* ... in that case, ssetno[i] is the id of the set consisting of the color
   of this vertex.  */
static int ssetno[26];

/* A set of colors referred to from either an external face or a non-internal vertex,
   as described above.  */
struct set
{
  /* If origin >= 0, then the set is referred from the vertex 'a' + origin, otherwise
     from the face (-1 - origin).  */
  int origin;

  /* The lower and the upper bound in the size of the set.  */
  int size_f, size_u;
};

/* An inequality: The sum of the variables listed in the LHS list of length NL is at least
   RHS_MIN and at most RHS_MAX.  */
struct eq
{
  int nl;
  int *lhs;
  int rhs_min, rhs_max;

  /* The next inequality in a linked list.  */
  struct eq *next;
};

/* The sets of colors, see above for details.  */
#define MAXS (MAXF + 26)
static struct set sets[MAXS];
static int nsets;

/* Relationships between the sets arising from the incidences of
   the non-internal vertices with common faces and with external
   faces.  */
enum rel {ANY, SUBSET, SUPERSET, DISJOINT};

static enum rel setrel[MAXS][MAXS];

/* Possible options for the relationships of a color to each of the sets;
   NALL is the number of these options, for i=0,...,nall-1, allowed[i] describes
   it is possible that some color belongs exactly to those sets s for which
   allowed[i][s] is true  .*/
#define MAXALL 10000
static int allowed[MAXALL][MAXS];
static int nall;

#define MAXV 20

/* The graph describing the adjacencies of the vertices with and through the faces.  */
struct graph
{
  /* gph[u][v] is true if u and v are incident with a common face.  */
  int gph[MAXV][MAXV];
  /* gadjset[u][s] is true if u and the vertices responsible for the set
     are incident with a common face.  */
  int gadjset[MAXV][MAXS];
  /* Number of vertices of the graph.  */
  int nv;
};

/* The graph as described above, for the reducent and the configuration.  */
static struct graph reducent, conf;

/* ACTALL describes a possible relation between a color and the sets, with
   some relationships still undecided (marked with -1).  Fix this relationship
   for the set i, setting ACTALL[I] to V, and propagate the consequences of this
   decision to the other sets.  If this results in a contradiction (so setting
   ACTALL[I] to V is not possible), return false, otherwise return true.  */
static int
set_and_prune (int actall[], int i, int v)
{
  int r;

  if (actall[i] != -1)
    return actall[i] == v;

  actall[i] = v;
  for (r = 0; r < nsets; r++)
    switch (setrel[i][r])
      {
      case ANY:
	break;

      case SUBSET:
	if (v == 1 && !set_and_prune (actall, r, 1))
	  return 0;
	break;

      case SUPERSET:
	if (v == 0 && !set_and_prune (actall, r, 0))
	  return 0;
	break;

      case DISJOINT:
	if (v == 1 && !set_and_prune (actall, r, 0))
	  return 0;
	break;

      default:
	abort ();
      }

  return 1;
}

/* ACTALL describes a possible relation between a color and the sets, with
   some relationships still undecided (marked with -1).  Generate all possible
   relations extending ACTALL, storing them in the list ALLOWED.  */
static void
gen_all_mem (int actall[])
{
  int newall[MAXS];
  int i, a, v;

  for (a = 0; a < nsets; a++)
    if (actall[a] == -1)
      break;

  if (a == nsets)
    {
      if (nall == MAXALL)
	abort ();

      for (i = 0; i < nsets; i++)
	if (actall[i])
	  break;

      /* We exclude the possibility of a color not belonging to any of the sets.
	 This possibility is not relevant for us, as in all the configurations,
	 every internal vertex is incident to an external face (see also the
	 verification of this condition in dump_graph), and thus the color
	 used to color such a vertex must appear in the set of colors not forbidden
	 by the precoloring of the non-configuration vertices of this face.  */
      if (i == nsets)
	return;

      for (i = 0; i < nsets; i++)
	allowed[nall][i] = actall[i];

      nall++;
      return;
    }

  for (v = 0; v <= 1; v++)
    {
      for (i = 0; i < nsets; i++)
	newall[i] = actall[i];
      if (set_and_prune (newall, a, v))
	gen_all_mem (newall);
    }
}

/* Generate all possible relationships between a color and the sets,
   storing them in the list ALLOWED.  */
static void
gen_allowed_memberships (void)
{
  int actall[MAXS];
  int i;

  for (i = 0; i < nsets; i++)
    actall[i] = -1;

  gen_all_mem (actall);
}

/* Write out a human-readable description of the relationship ACTALL
   between a color and the sets.  */
static void
dump_allowed_membership (int actall[])
{
  int i, j;

  for (i = 0; i < 26; i++)
    if (singletons[i] && actall[ssetno[i]])
      break;

  if (i == 26)
    printf ("A non-singleton");
  else
    {
      printf ("A singleton %c equal to ", i + 'a');
      for (j = i + 1; j < 26; j++)
	if (singletons[j] && actall[ssetno[j]])
	  printf ("%c", j + 'a');
    }
  printf (" excluded at");
  for (i = 0; i < nf; i++)
    if (faces[i].remco_f > 0 && actall[faces[i].setno])
      printf (" F%d", i + 1);
  printf ("\n");
}

/* Write out human-readable descriptions of all relationships stored
   in ALLOWED.  */
static void
dump_allowed_memberships (void)
{
  int i;

  for (i = 0; i < nall; i++)
    {
      printf ("A%d: ", i + 1);
      dump_allowed_membership (allowed[i]);
    }
}

/* Generate the inequality for the numbers of appearances of
   color-sets relationship types arising from the constraints
   on the size of the set S.  */
static struct eq *
gen_equation (int s)
{
  int i;
  int nc = 0;
  struct eq *e = malloc (sizeof (struct eq));

  for (i = 0; i < nall; i++)
    if (allowed[i][s])
      nc++;

  e->nl = nc;
  e->lhs = malloc (nc * sizeof (int));

  nc = 0;
  for (i = 0; i < nall; i++)
    if (allowed[i][s])
      {
	e->lhs[nc] = i;
	nc++;
      }
  e->rhs_min = sets[s].size_f;
  e->rhs_max = sets[s].size_u;
  e->next = NULL;

  return e;
}

/* Write out the inequality E in a human-readable format.  */
static void
dump_equation (struct eq *e)
{
  int i;
  const char *sep = "";

  for (i = 0; i < e->nl; i++)
    {
      printf ("%sA%d", sep, e->lhs[i] + 1);
      sep = " + ";
    }
  if (e->rhs_min == e->rhs_max)
    printf (" = %d\n", e->rhs_min);
  else
    printf (" in [%d,%d]\n", e->rhs_min, e->rhs_max);
}

/* Generate the inequalities for the numbers of appearances of
   color-sets relationship types arising from the set sizes.  */
static struct eq *
gen_equations (void)
{
  struct eq *ret = NULL, *e;
  int i;

  for (i = 0; i < nsets; i++)
    {
      e = gen_equation (i);
      e->next = ret;
      ret = e;
    }

  return ret;
}

/* Write out all the inequalities in a human-readable format.  */
static void
dump_equations (struct eq *e)
{
  for (; e; e = e->next)
    dump_equation (e);
}

/* A solution to the set of inequalities, giving an integer value to each variable.  */
struct sol
{
  int *cfs;
};

/* Returns false if the inequality E cannot be satisfied by non-negative
   variables (the upper bound is negative).  Returns true otherwise.  */
static int
valid (struct eq *e)
{
  for (; e; e = e->next)
    {
      if (e->rhs_max < 0)
	return 0;

      if (e->nl == 0)
	{
	  if (e->rhs_min <= 0)
	    abort ();

	  return 0;
	}
    }

  return 1;
}

/* Substitute the value X for the variable V in the inequalities in the list E,
   returning the new list of inequalities.  We omit the inequalities that
   are trivially true.  */
static struct eq *
substitute (struct eq *e, int v, int x)
{
  struct eq *nx, *nw;
  int i;

  if (!e)
    return NULL;

  nx = substitute (e->next, v, x);
  if (e->nl == 1 && e->lhs[0] == v && e->rhs_min <= x && x <= e->rhs_max)
    return nx;

  nw = malloc (sizeof (struct eq));
  nw->lhs = malloc (e->nl * sizeof (int));
  nw->nl = 0;
  nw->rhs_min = e->rhs_min;
  nw->rhs_max = e->rhs_max;
  for (i = 0; i < e->nl; i++)
    {
      if (e->lhs[i] == v)
	{
	  nw->rhs_min -= x;
	  nw->rhs_max -= x;
	  continue;
	}

      nw->lhs[nw->nl++] = e->lhs[i];
    }

  nw->next = nx;
  return nw;
}

/* Returns the number of non-negative integer solutions
   to the system x_1 + ... + x_VS = SUM, which is
   \binom{SUM+VS-1}{VS-1}.  */
static unsigned long long
choices (int vs, int sum)
{
  /* HACK! Actually, we use the value returned by this function
     only heuristically; so, to avoid overflows, it is ok to
     return "a very large value" instead, in the case we are passed too
     large arguments.  */
  if (sum + vs - 1 > MAXN)
    return nnadk[MAXN - 1][(MAXN - 1) / 2];
  return nnadk[sum + vs - 1][vs - 1];
}

/* Delete the list E of inequalities.  */
static void
free_eqs (struct eq *e)
{
  struct eq *nx;

  for (; e; e = nx)
    {
      nx = e->next;

      free (e->lhs);
      free (e);
    }
}

/* Generate all non-negative integer solutions to the system E of inequalities.
   A partial solution with the values of already eliminated variables is given in PSOL.
   The callback PROCESS is called for each solution.  */
static void
gen_eq_solutions (struct eq *e, int psol[], void (*process)(struct sol *))
{
  struct eq *ae, *be = NULL;
  unsigned long long ach, bestch = nnadk[MAXN - 1][(MAXN - 1) / 2] + 1;
  int i, v, m;

  if (!e)
    {
      struct sol as;
      as.cfs = malloc (nall * sizeof (int));
      for (i = 0; i < nall; i++)
	as.cfs[i] = psol[i];
      process (&as);
      free (as.cfs);
      return;
    }

  /* Heuristically guess the most restrictive inequality, to bound
     the amount of branching.  */
  for (ae = e; ae; ae = ae->next)
    {
      ach = choices (ae->nl, ae->rhs_max);
      if (ach < bestch)
	{
	  bestch = ach;
	  be = ae;
	}
    }

  if (ach == 0)
    return;

  v = be->lhs[0];
  m = be->rhs_max;

  /* Substitute all the possible values for one of the variables in the selected
     inequality and generate the solutions of the resulting systems.  */
  for (i = 0; i <= m; i++)
    {
      struct eq *ne = substitute (e, v, i);

      if (valid (ne))
	{
	  psol[v] = i;
	  gen_eq_solutions (ne, psol, process);
	}
      free_eqs (ne);
    }
}

/* Write out the solution S to the system of inequalities
   in a human-readable format.  */

static void
dump_eq_solution (struct sol *s)
{
  int i;

  for (i = 0; i < nall; i++)
    if (s->cfs[i])
      {
	if (s->cfs[i] > 1)
	  printf ("%d*", s->cfs[i]);
	printf("A%d ", i + 1);
      }
  printf ("\n");
}

/* Parse the internal vertices from IVS, storing in the graph G the incidences
   between them and to the non-internal vertices specified in INAMED.
   If FNO >= 0, we also store in G the incidence with the set with id FNO.  */
static void
parse_face_vs (struct graph *g, int fno, char *ivs, char *inamed)
{
  int fvs[MAXV], v;
  int nfv = 0, last = 0;
  int i, j;
  char *q;

  if (*ivs == '-')
    return;

  while (1)
    {
      for (q = ivs; *q && *q != ','; q++)
	continue;

      if (!*q)
	last = 1;
      else
	*q++ = 0;

      sscanf (ivs, "%d", &v);
      fvs[nfv++] = v - 1;
      if (last)
	break;

      ivs = q;
    }

  for (i = 0; i < nfv; i++)
    {
      v = fvs[i];

      for (j = i + 1; j < nfv; j++)
	{
	  int u = fvs[j];

	  g->gph[u][v] = g->gph[v][u] = 1;
	}

      for (q = inamed; *q && *q != '-'; q++)
	g->gadjset[v][ssetno[*q - 'a']] = 1;

      if (fno >= 0)
	g->gadjset[v][faces[fno].setno] = 1;
    }
}

/* Writes out a human-readable description of the information stored
   in the graph G.  */

static void
dump_graph (struct graph *g)
{
  int u, v, s, any_fc;

  for (u = 0; u < g->nv; u++)
    {
      printf (" vertex %d neighbors", u + 1);

      for (v = 0; v < g->nv; v++)
	if (g->gph[u][v])
	  printf (" %d", v + 1);

      printf (" forbidden colors");
      any_fc = 0;
      for (s = 0; s < nsets; s++)
	if (g->gadjset[u][s])
	  {
	    if (sets[s].origin >= 0)
	      printf (" %c", 'a' + sets[s].origin);
	    else
	      {
		printf (" f%d", -sets[s].origin);
		any_fc = 1;
	      }
	  }
      printf ("\n");
      if (!any_fc)
	{
	  printf ("Vertex %d is not incident with an unbounded face!\n", u + 1);
	  abort ();
	}
    }
}

#define MAXLC 100

/* The lists of colors available at each of the vertices of the current graph.  */
static int llen[MAXV];
static int list[MAXV][MAXLC];

/* The total number of colors appearing in the lists.  */
static int nlc;

/* The partial coloring of the current graph, used in FIND_COLORING_REC.  */
static int color[MAXV];

/* An operation to undo a change made via the SET_WITH_UNDO function:
   "Set *WHERE to the value VAL.  */
struct undo
{
  int *where;
  int val;
};

/* A stack of operations to be made in order to undo the changes made
   via the SET_WITH_UNDO function.  */
#define MAXU 10000
static struct undo ustack[MAXU];
static int ustop;

/* Set *WH to X, recording the information necessary to undo this change.  */
static void
set_with_undo (int *wh, int x)
{
  if (ustop == MAXU)
    abort ();

  ustack[ustop].where = wh;
  ustack[ustop].val = *wh;
  *wh = x;
  ustop++;
}

/* Undo all the changes to the lists made from the timestamp TOP.  */
static void
undo_till (int top)
{
  while (ustop > top)
    {
      ustop--;
      *ustack[ustop].where = ustack[ustop].val;
    }
}

/* Remove the color C from the list of V, recording the information
   necessary to undo this change.  */
static void
rem_with_undo (int v, int c)
{
  int i, x;

  for (i = 0; i < llen[v]; i++)
    if (list[v][i] == c)
      break;

  if (i == llen[v])
    return;

  x = llen[v] - 1;
  set_with_undo (&llen[v], x);
  set_with_undo (&list[v][i], list[v][x]);
}

/* Remove the color C from the lists of the neighbors of the vertex V
   in the graph G.  */
static void
prune_colors (struct graph *g, int v, int c)
{
  int u;

  for (u = 0; u < g->nv; u++)
    if (g->gph[u][v])
      rem_with_undo (u, c);
}

/* Returns true if the partial coloring stored in the global variable
   COLOR extends to a coloring of the graph G from the lists.  */
static int
find_coloring_rec (struct graph *g)
{
  int v, bv = -1, mlen = 1000, i;
  int till = ustop;

  /* Choose a vertex with the smallest number of available colors,
     to limit the branching.  */
  for (v = 0; v < g->nv; v++)
    if (color[v] == -1 && llen[v] < mlen)
      {
	mlen = llen[v];
	bv = v;
      }

  if (bv == -1)
    return 1;

  /* Try coloring the chosen vertex by each color in its list,
     removing the color from the lists of adjacent vertices.  */
  for (i = 0; i < llen[bv]; i++)
    {
      color[bv] = list[bv][i];
      prune_colors (g, bv, list[bv][i]);
      if (find_coloring_rec (g))
	{
	  undo_till (till);
	  return 1;
	}

      undo_till (till);
    }
  color[bv] = -1;

  return 0;
}

/* Returns true if the graph G is colorable from the lists.  */
static int
find_coloring (struct graph *g)
{
  int v;

  ustop = 0;
  for (v = 0; v < g->nv; v++)
    color[v] = -1;

  return find_coloring_rec (g);
}

/* Translate the solution S to the inequalities to the assignment of lists
   of colors to the vertices of the graph G according to the corresponding
   precoloring of the non-configuration and non-internal vertices.  */
static void
gen_lists (struct sol *s, struct graph *g)
{
  int i, j, ak, v, as;
  int forb;

  nlc = 0;
  for (i = 0; i < nall; i++)
    nlc += s->cfs[i];

  for (v = 0; v < g->nv; v++)
    llen[v] = 0;

  ak = 0;
  for (i = 0; i < nall; i++)
    for (j = 0; j < s->cfs[i]; j++)
      {
	for (v = 0; v < g->nv; v++)
	  {
	    forb = 0;
	    for (as = 0; as < nsets; as++)
	      if (g->gadjset[v][as])
		{
		  /* We cannot use the color c (whose relationship to the sets
		     is described by allowed[i]) at v if
		     -- v and some non-internal vertex w are incident with the
		        same face, and the vertex w is colored by c, or
		     -- for an incident external face f, the color c is used at one
		        of the incident non-configuration vertices (and thus
			c does not appear in the corresponding set of allowed colors).  */
		  if ((sets[as].origin >= 0 && allowed[i][as])
		      || (sets[as].origin < 0 && !allowed[i][as]))
		    {
		      forb = 1;
		      break;
		    }
		}
	    if (!forb)
	      list[v][llen[v]++] = ak;
	  }

	ak++;
      }
}

/* Writes out a human-readable interpretation of the solution S,
   in terms of a precoloring of the non-configuration vertices
   incident with the external faces of the configuration, and
   of the non-internal vertices of the configuration.  */

static void
dump_eq_interpretation (struct sol *s)
{
  int i, j, ak, as;

  for (as = 0; as < nsets; as++)
    {
      if (sets[as].origin >= 0)
	printf (" %c=", 'a' + sets[as].origin);
      else
	printf (" f%d=!", -sets[as].origin);

      ak = 0;
      for (i = 0; i < nall; i++)
	for (j = 0; j < s->cfs[i]; j++)
	  {
	    if (allowed[i][as])
      	      printf ("%c", 'A' + ak);

	    ak++;
	  }
    }
  printf ("\n");
}

/* Write out the lists of available colors at the vertices of the graph G.  */

static void
dump_lists (struct graph *g)
{
  int v, i;

  for (v = 0; v < g->nv; v++)
    {
      printf ("  vertex %d: ", v + 1);
      for (i = 0; i < llen[v]; i++)
	printf ("%c", 'A' + list[v][i]);
      printf ("\n");
    }
}

/* The minimum number of colors needed to show that the configuration
   is not reducible.  */
#define INFT 10000
static int nonrc = INFT;

/* The number of solution to process, the id of the actually processed solution,
   the number of precolorings that extent to the reducent.  */
static int nsol, asol, ext_to_reducent;

/* Increase the counter of the number of solutions.  */

static void
count_solutions (struct sol *as)
{
  nsol++;

  if (nsol % 1000000 == 0)
    {
      fprintf (stderr, "#");
      fflush (stderr);
    }
}

/* For the solution AS (describing a precoloring of the non-configuration
   vertices, determine whether it extends to the reducent.  If so and
   it does not extend to the configuration, the configuration is not
   reducible.  We also keep track of how many colors in total are used
   in this case, for debugging purposes.  */

static void
process_solution (struct sol *as)
{
  int step = (nsol + 99) / 100;

  asol++;
  if (asol % step == 0)
    {
      fprintf (stderr, "%d%%\n", asol / step);
      fflush (stderr);
    }
  gen_lists (as, &reducent);
  if (!find_coloring (&reducent))
    return;
  ext_to_reducent++;
  gen_lists (as, &conf);

  if (!find_coloring (&conf))
    {
      printf ("Solution:\n");
      dump_eq_interpretation (as);

      printf (" Configuration lists:\n");
      dump_lists (&conf);
      printf ("Does not extend to the configuration, %d distinct colors.\n", nlc);
      if (nlc < nonrc)
	nonrc = nlc;
    }
}

/* The starting point.  */

int main(void)
{
  int i, j, k, a, cf, fno;
  char remco[1000], buf1[1000], buf2[1000], *p;
  int cfs[MAXALL];
  struct eq *e;

  /* Read the reducent and initialze the sets of colors for its
     external faces and non-internal vertices.  */
  scanf ("%d%d", &nf, &reducent.nv);

  for (i = 0; i < nf; i++)
    {
      scanf ("%s %s %s", remco, buf1, buf2);

      p = strchr (remco, '-');
      if (!p)
	faces[i].remco_f = faces[i].remco_t = atoi (remco);
      else
	{
	  *p = 0;
	  faces[i].remco_f = atoi (remco);
	  faces[i].remco_t = atoi (p + 1);
	}
      for (p = buf1, j = 0; *p && *p != '-' ; p++, j++)
	{
	  a = *p - 'a';
	  if (!singletons[a])
	    {
	      singletons[a] = 1;
	      sets[nsets].origin = a;
	      sets[nsets].size_f = 1;
	      sets[nsets].size_u = 1;
	      ssetno[a] = nsets;
	      nsets++;
	    }
	  faces[i].adjsing[j] = a;
	}
      faces[i].nadj = j;

      if (faces[i].remco_f > 0)
	{
	  sets[nsets].origin = -1 - i;
	  sets[nsets].size_f = faces[i].remco_f;
	  sets[nsets].size_u = faces[i].remco_t;
	  faces[i].setno = nsets;
	  nsets++;
	}

      parse_face_vs (&reducent, faces[i].remco_f > 0 ? i : -1, buf2, buf1);
    }

  /* Read the configuration.  */
  scanf ("%d%d", &cf, &conf.nv);
  for (i = 0; i < cf; i++)
    {
      scanf ("%d %s %s", &fno, buf1, buf2);
      parse_face_vs (&conf, fno - 1, buf2, buf1);
    }

  /* Determines the relationships between the sets.  Non-internal
     vertices incident with the same face must receive distinct colors,
     and their colors must be among those not forbidden by the
     outside vertices of incident external faces.  */
  for (i = 0; i < nf; i++)
    {
      for (j = 0; j < faces[i].nadj; j++)
	{
	  a = ssetno[faces[i].adjsing[j]];
	  if (faces[i].remco_f > 0)
	    {
	      setrel[faces[i].setno][a] = SUPERSET;
	      setrel[a][faces[i].setno] = SUBSET;
	    }

	  for (k = j + 1; k < faces[i].nadj; k++)
	    {
	      int b = ssetno[faces[i].adjsing[k]];
	      setrel[a][b] = setrel[b][a] = DISJOINT;
	    }
	}
    }

  precompute_nnadk ();

  /* Generate the list of all possible relationships between a color and the set,
     and store them in the ALLOWED list.  */
  gen_allowed_memberships ();
  printf ("Membership options:\n");
  dump_allowed_memberships ();

  /* We introduce an integer variable for each of these relationships, expressing
     how many colors with the prescribed relationship are there.  The constraints
     on the sizes of the sets then correspond to a system of linear inequalities for these
     variables.  Let us compute this system.  */
  printf ("Equations:\n");
  e = gen_equations ();
  dump_equations (e);

  printf ("Reduced configuration:\n");
  dump_graph (&reducent);
  printf ("Original configuration:\n");
  dump_graph (&conf);

  /* Enumerate all solutions to the system.  Each solution describes the effect of
     a precoloring of the non-configuration vertices on the lists of available colors
     in the configuration.  We first just count the number of solutions, as this is
     relatively fast and makes it possible to inform about the progress of processing
     them (which is much slower). */
  gen_eq_solutions (e, cfs, count_solutions);
  gen_eq_solutions (e, cfs, process_solution);

  printf ("%d outer colorings, out of which %d do not extend to the reduced configuration.\n", nsol, nsol-ext_to_reducent);
  if (nonrc == INFT)
    printf ("All %d remaining colorings extend to the original configuration.\nThe configuration is reducible.\n",ext_to_reducent);
  else
    printf ("Non-reducible with %d colors.\n", nonrc);

  return 0;
}