// g++ program-dvorak.cc -o program-dvorak -lgmp -lgmpxx -lppl -lgurobi90 -lgurobi_c++ -O2
// ./program-dvorak
// Expected running time: 20-30 minutes

#include <cstdio>
#include <cstdlib>
#include <list>
#include <vector>
#include <algorithm>
#include <map>
#include <unordered_set>
#include <gmpxx.h>
#include <ppl.hh>
#include "gurobi_c++.h"
using namespace std;
using namespace Parma_Polyhedra_Library;
using namespace IO_Operators;

#define DO_GEN true
#define DO_TEST true
#define DO_EXACT true

#define EPS 0.001
#define GAP 1e-5

static GRBEnv env;

/* Type of a vertex; consists of the color VT of the vertex,
   and of the census of the colors of its neighbors: for a color c,
   NT[c] is the number of neighbors of color c.  */
struct color_type
{
  int vt;
  map<int,int> nt;

  /* Initialize the type by the color _VT of the vertex.  */
  color_type(int _vt) : vt(_vt)
    {
    }

  /* Add the color T of a neighbor to the census.  */
  void add_neighbor (int t)
    {
      if (nt.count (t) > 0)
	nt[t]++;
      else
	nt[t] = 1;
    }

  /* Equality and comparison of types.  */
  bool operator==(const color_type &w) const
    {
      return vt == w.vt && nt == w.nt;
    }
  bool operator<(const color_type &w) const
    {
      if (vt < w.vt)
	return true;
      if (vt > w.vt)
	return false;
      return nt < w.nt;
    }
};

/* A set of vertices. */
typedef vector<bool> vecset;

/* Create a subset of [N] from the bitmask S.  */
static vecset
mk_vecset (unsigned n, unsigned s)
{
  vecset ret(n);
  for (unsigned i = 0; i < n; i++)
    ret[i] = (s >> i) & 1;
  return ret;
}

/* Returns the size of the set S.  */
static int
vecset_size (const vecset &s)
{
  int sz = 0;
  for (bool e : s)
    if (e)
      sz++;
  return sz;
}

/* Applies function VMAP to the set S, obtaining a subset of [N].  */
static vecset
recode (const vecset &s, const vector<int> &vmap, int n)
{
  vecset ret (n, false);
  int ns = s.size ();
  for (int v = 0; v < ns; v++)
    if (s[v])
      ret[vmap[v]] = true;

  return ret;
}

/* Returns true if a path of L vertices of degree two with a given
   sum SUMR of their requirements is reducible when its ends
   are vertices of (extended) degree 3.  */
static bool
reducible_path (int l, int sumr)
{
  int delta = (l & 1) ? 5 : 8;
  return 2 * sumr <= 11 * l - delta;
}

/* Returns true if a cycle of N vertices of degree two with a given
   sum SUMR of their requirements is reducible.  */
static bool
reducible_cycle (int n, int sumr)
{
  if (n % 2 == 0)
    return true;

  return 2 * sumr <= 11 * n - 11;
}

/* List of neighbors in a graph.  */
typedef list<int> nbrlist;

/* A precoloring of some vertices of a graph.  */
typedef map<vecset, mpq_class> precol;

static void
dump_vecset (int n, const vecset &ss)
{
  for (int i = 0; i < n; i++)
    printf ("%c", ss[i] ? '1' : '0');
}

/* Writes out the values of the precoloring.  */
static void
dump_precoloring (int n, const precol &p)
{
  for (int s = 0; s < (1 << n); s++)
    {
      vecset ss = mk_vecset (n, s);
      if (p.count (ss) == 0 || p.at (ss) == 0)
	continue;
      dump_vecset (n, ss);
      printf (" -> ");
      cout << p.at (ss);
      printf ("; ");
    }
  printf ("\n");
}

/* Additional constraint.  */
struct addit
{
  bool leq;
  int rhs;
  virtual bool relevant (const vecset &s) const = 0;
  virtual string code (void) = 0;
  virtual ~addit (void)
    {
    }
};

typedef list<const addit *> addits;

/* Intersection at most ... */
struct aci_le : addit
{
  int u, v;

  aci_le (int _u, int _v, int _val) : u(_u), v(_v)
    {
      rhs = _val;
      leq = true;
    }

  virtual bool relevant (const vecset &s) const
    {
      return s[u] && s[v];
    }

  virtual string code (void)
    {
      return to_string (u) + " cap " + to_string (v) + " <= " + to_string (rhs);
    }
};

/* Prepares singleton objects of aci_le type.  */
static const addit *
paci_le (int u, int v, int val)
{
  if (u > 3 || v > 3 || val > 3)
    abort ();

  static const addit *aci_les[4][4][4];

  const addit *&ret = aci_les[u][v][val];
  if (!ret)
    ret = new aci_le (u, v, val);

  return ret;
}

/* Union at most ... */

struct acu_le : addit
{
  vector<int> uof;

  acu_le (const vector<int> _uof, int _val) : uof (_uof)
    {
      rhs = _val;
      leq = true;
    }

  virtual bool relevant (const vecset &s) const
    {
      for (int v : uof)
	if (s[v])
	  return true;
      return false;
    }

  virtual string code (void)
    {
      string uos;
      for (int v : uof)
	uos += " " + to_string (v);
      return "Union of" + uos + " <= " + to_string (rhs);
    }
};

/* Prepares singleton objects of acu_le type.  */
static const addit *
pacu_le (const vector<int> &s, int val)
{
  if (val > 10)
    abort ();

  static map<vector<int>, const addit *> acu_les[11];

  const addit *&ret = acu_les[val][s];
  if (!ret)
    ret = new acu_le (s, val);

  return ret;
}


/* Union of 1 and 2 intersects 0 in at most 2. */

struct ac_i0u12_2 : addit
{
  ac_i0u12_2 (void)
    {
      rhs = 2;
      leq = true;
    }

  virtual bool relevant (const vecset &s) const
    {
      return s[0] && (s[1] || s[2]);
    }

  virtual string code (void)
    {
      return "Union of 1 and 2 intersects 0 in at most 2.";
    }
};

/* Prepares the singleton object of ac_i0u12_2 type.  */
static const addit *
pac_i0u12_2 (void)
{
  static ac_i0u12_2 ac;

  return &ac;
}


/* Round X to a nearby rational value using continued fractions.  */
#define TOL 1e-8

static mpq_class
to_rational (double orig_x, double x, mpz_class h2, mpz_class k2, mpz_class h1, mpz_class k1)
{
  int ipart = (int) x;
  mpz_class h0 (ipart * h1 + h2);
  mpz_class k0 (ipart * k1 + k2);
  x -= ipart;
  mpq_class act (h0, k0);
  act.canonicalize ();
  double by = fabs (mpq_get_d (act.get_mpq_t ()) - orig_x);
  if (by < TOL)
    return act;

  if (x < TOL)
    abort ();
      
  return to_rational (orig_x, 1 / x, h1, k1, h0, k0);
}

static mpq_class
to_rational (double x)
{
  return to_rational (x, x, 0, 1, 1, 0);
}

/* Solver for systems of linear equations.  */
typedef vector<mpq_class> qvec;

/* Returns first non-zero coordinate of the vector V.  */
static int
first_nonzero (qvec v)
{
  int i = 0;

  for (qvec::iterator a = v.begin (); a != v.end (); ++a, ++i)
    if (*a != 0)
      return i;

  return -1;
}

/* FROM -= BY * WHAT.  */

static void
subtract (qvec &from, mpq_class by, qvec &what)
{
  qvec::iterator w = what.begin ();
  for (qvec::iterator f = from.begin (); f != from.end (); ++f, ++w)
    *f -= by * *w;
}

/* Finds COEFfficients such that WHAT = sum_i COEF[i] * SYST[i].
   Returns false if this is not possible.  */

static bool
express_as_lc (list<qvec> &syst, qvec &what, qvec &coef)
{
  if (syst.empty ())
    return (first_nonzero (what) < 0);

  qvec lst = syst.back ();
  syst.pop_back ();
  int nz = first_nonzero (lst);
  if (nz < 0)
    {
      if (!express_as_lc (syst, what, coef))
	return false;
      coef.push_back (0);
      return true;
    }
  mpq_class piv = lst[nz];

  list<qvec> nsyst (syst);
  list<qvec>::iterator sp = nsyst.begin ();
  for (list<qvec>::iterator s = syst.begin (); s != syst.end (); ++s, ++sp)
    subtract (*sp, (*s)[nz] / piv, lst);
  qvec wp (what);
  subtract (wp, what[nz] / piv, lst);
  if (!express_as_lc (nsyst, wp, coef))
    return false;

  mpq_class cf (what[nz]);
  qvec::iterator c = coef.begin ();
  for (list<qvec>::iterator s = syst.begin (); s != syst.end (); ++s, ++c)
    cf -= *c * (*s)[nz];

  coef.push_back (cf / piv);
  return true;
}

/* Verifies whether WHAT = sum_i COEF[i] * SYST[i].  */

static bool
is_solution (const list<qvec> &syst, const qvec &what, const qvec &coef)
{
  for (int p = 0; p < (int) what.size (); p++)
    {
      auto si = syst.begin ();
      mpq_class a (0);
      for (int i = 0; i < (int) coef.size (); ++i, ++si)
	a += coef[i] * (*si)[p];

      if (a != what[p])
	return false;
    }

  return true;
}

/* A graph with total degrees assigned to vertices.  */
struct graph
{
  vector<nbrlist> vs;
  vector<int> total_degree;

  /* Number of vertices. */
  int nvs () const
    {
      return vs.size ();
    }

  /* Expand the number of vertices to make V the last one;
     added vertices are isolated of total degree 0.  */
  void expand_till (int v)
    {
      if (v < nvs ())
	return;

      vs.resize (v + 1);
      total_degree.resize (v + 1, 0);
    }

  /* Adds edge between U and V, not changing their total degree. */
  void add_edge (int u, int v)
    {
      vs[u].push_back (v);
      vs[v].push_back (u);
    }

  /* Adds a vertices and edges of another graph G.  */
  void add (const graph &g)
    {
      int delta = nvs ();
      expand_till (delta + g.nvs () - 1);
      for (int v = 0; v < g.nvs (); v++)
	{
	  total_degree[v + delta] = g.total_degree[v];
	  for (int u : g.vs[v])
	    if (u < v)
	      add_edge (u + delta, v + delta);
	}
    }

  /* Deletes V from the list of neighbors of U.  */
  void delete_half_edge (int u, int v)
    {
      nbrlist &uns = vs[u];
      uns.erase (find (uns.begin (), uns.end (), v));
    }

  /* Deletes edge between U and V, not changing their total degree. */
  void delete_edge (int u, int v)
    {
      delete_half_edge (u, v);
      delete_half_edge (v, u);
    }

  /* Adds a path with L internal vertices of total degree two
     between U and V; the total degree of U and V is not changed.  */
  void add_path (int u, int v, int l)
    {
      int n = nvs ();
      expand_till (n + l - 1);
      int b = u, a = n;
      for (int i = 0; i < l; i++)
	{
	  add_edge (b, a);
	  total_degree[a] = 2;
	  b = a;
	  a++;
	}
      add_edge (b, v);
    }

  /* Adds a path with OP.size () internal vertices between U and V.
     The total degree of U and V is not changed.  The vertices of
     the path marked in OP have total degree 3, the other 2.  */
  void add_path (int u, int v, const vecset &op)
    {
      int l = op.size ();
      int n = nvs ();
      add_path (u, v, l);
      for (int i = 0; i < l; i++)
	total_degree[n + i] = op[i] ? 3 : 2;
    }

  /* Adds a vertex of total degree TD adjacent to NBRS
     (whose total degree is not changed.  */
  int add_vertex (const vector<int> &nbrs, int td)
    {
      int n = nvs ();
      expand_till (n);
      for (int x : nbrs)
	add_edge (n, x);
      total_degree[n] = td;
      return n;
    }

  /* Adds a subdivided K_4 linking U with V.  */
  void add_diamond (int u, int v)
    {
      int x = nvs ();
      add_path (u, u, vecset{true, false, false, true});
      add_path (x, x + 3, vecset{true});
      add_edge (x + 4, v);
    }

  /* Adds a 5-cycle with two adjacent vertices of degree two
     plus its neighbors in a 6-cycle passing through A, B, and C.  */
  void add_two2_6cycle (int a, int b, int c)
    {
      int d = nvs ();
      int e = d + 1;
      int f = e + 1;
      int g = f + 1;
      int h = g + 1;
      int i = h + 1;
      add_path (a, c, vecset{true});
      add_path (a, b, vecset{true});
      add_path (b, c, vecset{true});
      add_path (d, f, vecset{true, true, true});
      add_edge (e, h);
      add_path (g, i, 2);
    }

  /* Adds a 5-cycle with two adjacent vertices of degree two,
     with A, B, and C being the neighbors of this 5-cycle.  */
  void add_two2 (int a, int b, int c)
    {
      int d = nvs ();
      int e = d + 1;
      int f = e + 1;
      add_path (a, c, vecset{true,true,true});
      add_edge (b, e);
      add_path (d, f, 2);
    }

  /* Initializes the graph as a cycle of N vertices of
     total degree 2.  */
  graph (int n)
    {
      expand_till (n - 1);

      for (int a = 0; a < n; a++)
	{
	  add_edge (a, (a + 1) % n);
	  total_degree[a] = 2;
	}
    }

  /* Initializes the graph as a cycle of OP.size () vertices,
     those marked in OP have total degree 3, others 2.  */
  graph (const vecset &op)
    {
      int n = op.size ();
      expand_till (n - 1);

      for (int a = 0; a < n; a++)
	{
	  add_edge (a, (a + 1) % n);
	  total_degree[a] = op[a] ? 3 : 2;
	}
    }

  /* Returns true if U is adjacent to V.  */
  bool adjacent (int u, int v) const
    {
      for (int x : vs[u])
	if (x == v)
	  return true;

      return false;
    }

  /* Returns the degree of V.  */
  int degree (int v) const
    {
      return vs[v].size ();
    }

  /* Returns true if all vertices have degree two.  */
  bool is_cycle (void) const
    {
      for (int v = 0; v < nvs (); v++)
	if (degree (v) != 2)
	  return false;
      return true;
    }


  /* Sum of differences between total and actual degrees.  */
  int nails (void) const
    {
      int ret = 0;
      for (int v = 0; v < nvs (); v++)
	ret += total_degree[v] - degree (v);

      return ret;
    }

  /* Returns in NS the vertices whose total degree is larger than actual.  */
  void nails (vector<int> &ns) const
    {
      for (int v = 0; v < nvs (); v++)
	if (total_degree[v] > degree (v))
	  ns.push_back (v);
    }

  /* Returns in VOT the vertices of degree D and total degree TD.  */
  void vertices_of_type (int d, int td, vector<int> &vot) const
    {
      for (int v = 0; v < nvs (); v++)
	if (total_degree[v] == td && degree (v) == d)
	  vot.push_back (v);
    }

  /* Returns true if the set S of vertices is independent. */
  bool independent (const vecset &s) const
    {
      int n = s.size ();
      for (int u = 0; u < n; u++)
	{
	  if (!s[u])
	    continue;
	  for (int v = u + 1; v < n; v++)
	    if (s[v] && adjacent (u, v))
	      return false;
	}

      return true;
    }

  /* Returns true if V has no neighbors in S.  */
  bool can_add (const vecset &s, int v) const
    {
      for (int u : vs[v])
	if (s[u])
	  return false;

      return true;
    }

  /* Returns true if the independent set S is maximal in the subgraph induced
     on SG.  */
  bool is_maximal (const vecset &s, const vecset &sg) const
    {
      for (int v = 0; v < nvs (); v++)
	if (sg[v] && !s[v] && can_add (s, v))
	  return false;
      return true;
    }

  /* Determines the type of the vertex V in the coloring given by COLORS.  */
  color_type colored_type (int v, const vector<int> &colors) const
    {
      color_type ret(colors[v]);

      for (int u : vs[v])
	ret.add_neighbor (colors[u]);
      return ret;
    }

  /* Colors each vertex by its type with respect to the coloring given by COLORS,
     and returns the new coloring in the COLORS array.  The types are mapped to colors
     1, 2, ... according to the type ordering.  */
  void refine_colors (vector<int> &colors) const
    {
      map<color_type, int> color_types;
      for (int v = 0; v < nvs (); v++)
	color_types[colored_type (v, colors)] = 0;

      int id = 0;
      for (map<color_type, int>::iterator a = color_types.begin (); a != color_types.end (); ++a)
	a->second = id++;

      vector<int> old_colors(colors);
      for (int v = 0; v < nvs (); v++)
	colors[v] = color_types[colored_type (v, old_colors)];
    }

  /* Iterate REFINE_COLORS until the coloring stabilizes.  */
  void stabilize_colors (vector<int> &colors) const
    {
      vector<int> old_colors;
      do
	{
	  old_colors = colors;
	  refine_colors (colors);
	} while (colors != old_colors);
    }

  /* Returns the number of vertices colored by color C in the coloring COLORS.  */
  int class_size (const vector<int> &colors, int c) const
    {
      int sz = 0;
      for (int v = 0; v < nvs (); v++)
	if (colors[v] == c)
	  sz++;
      return sz;
    }

  /* Returns false if in the coloring COLORS, each color is used on exactly one
     vertex (all color classes are trivial).  Otherwise, finds the smallest
     non-trivial color class (and among those the one with the smallest color number),
     fills its vertices into CL, and returns true.  */
  bool find_class_to_split (const vector<int> &colors, vector<int> &cl) const
    {
      int snt = nvs () + 1;
      int snt_c = -1;
      int c = 0;
      while (true)
	{
	  int cs = class_size (colors, c);
	  if (cs == 0)
	    break;

	  if (cs > 1 && cs < snt)
	    {
	      snt = cs;
	      snt_c = c;
	    }

	  c++;
	}

      if (snt > nvs ())
	return false;

      cl.clear ();
      for (int v = 0; v < nvs (); v++)
	if (colors[v] == snt_c)
	  cl.push_back (v);

      return true;
    }

  /* A string encoding the graph after permuting its vertices according
     to the permutation PERM.  */
  string code_according_to_order (const vector<int> &perm) const
    {
      vector<int> vord (nvs ());
      for (int v = 0; v < nvs (); v++)
	vord[perm[v]] = v;

      string ret;
      for (int i = 0; i < nvs (); i++)
	{
	  int v = vord[i];

	  vector<int> vns;
	  for (int x : vs[v])
	    if (perm[x] > i)
	      vns.push_back (perm[x]);

	  if (vns.empty ())
	    continue;
	  sort (vns.begin (), vns.end ());
	  ret.push_back ('a' + i);
	  ret.push_back (':');
	  for (int x : vns)
	    ret.push_back ('a' + x);
	  ret.push_back (';');
	}
      for (int i = 0; i < nvs (); i++)
	{
	  int v = vord[i];
	  if (total_degree[v] > degree (v))
	    {
	      ret.push_back ('a' + i);
	      ret.push_back ('0' + total_degree[v] - degree (v));
	    }
	}

      return ret;
    }

  string code (void) const
    {
      vector<int> perm (nvs (), 0);
      for (int i = 0; i < nvs (); i++)
	perm[i] = i;
      return code_according_to_order (perm);
    }

  /* Returns the canonical code for the graph with vertices colored by COLORS;
     total degree is ignored.  */
  string canonical_code (vector<int> &colors) const
    {
      stabilize_colors (colors);
      vector<int> class_to_split;
      if (!find_class_to_split (colors, class_to_split))
	return code_according_to_order (colors);
      int next_color = *(max_element (colors.begin (), colors.end ())) + 1;
      string ret("");
      for (int v : class_to_split)
	{
	  vector<int> scolors (colors);
	  scolors[v] = next_color;
	  string act = canonical_code (scolors);
	  if (act > ret)
	    ret = act;
	}

      return ret;
    }

  /* Returns the canonical code for the graph and the total degree assignment.  */
  string canonical_code (void) const
    {
      vector<int> colors (nvs ());
      /* Initialize the colors according to the actual and total degree.  */
      for (int v = 0; v < nvs (); v++)
	colors[v] = 4 * degree (v) + total_degree[v];

      return canonical_code (colors);
    }

  /* Returns the degree of V in the subgraph induced by SG.  */
  int degree_in_sg (int v, const vecset &sg)
    {
      int d = 0;
      for (int x : vs[v])
	if (sg[x])
	  d++;
      return d;
    }

  /* Returns a neighbor of V in the subgraph induced by SG (assumes V is not isolated in SG.  */
  int neighbor_in_sg (int v, const vecset &sg)
    {
      for (int x : vs[v])
	if (sg[x])
	  return x;

      abort ();
    }

  /* Deletes the neighbors of V from the set SG.  */
  void clear_neighborhood (int v, vecset &sg)
    {
      for (int x : vs[v])
	sg[x] = false;
      sg[v] = false;
    }

  /* Fills into MAX_INDEP_SETS maximal independent sets of the subgraph induced by FULL_SG that
     consist of the set START and a subset of SG (vertices of SG are non-adjacent to vertices of START).
     Before recording, VMAP is applied to the sets to map them to subsets of [N].  */
  void maximal_independent_sets (const vecset &start, const vecset &sg, const vecset &full_sg, const vector<int> &vmap, int n, list<vecset> &max_indep_sets)
    {
      int bestv = -1;
      int bestd = 0;

      /* Let BESTV be a vertex with 0 or 1 neighbors in SG if possible,
	 a vertex with the maximum number of neighbors in SG otherwise.  */
      for (int v = 0; v < nvs (); v++)
	if (sg[v])
	  {
	    int d = degree_in_sg (v, sg);
	    if (d == 0)
	      {
		bestv = v;
		bestd = 0;
		break;
	      }

	    if (d == 1)
	      {
		bestv = v;
		bestd = 1;
		continue;
	      }
	    if (bestd == 1)
	      continue;

	    if (d > bestd)
	      {
		bestv = v;
		bestd = d;
	      }
	  }

      /* If SG is empty, test whether the set is maximal and if so, record it.  */
      if (bestv < 0)
	{
	  if (is_maximal (start, full_sg))
	    max_indep_sets.push_back (recode (start, vmap, n));
	  return;
	}

      /* Try including BESTV in the set.  */
      vecset nsg(sg);
      vecset nst(start);
      nst[bestv] = true;
      clear_neighborhood (bestv, nsg);
      maximal_independent_sets (nst, nsg, full_sg, vmap, n, max_indep_sets);

      /* If a vertex with one neighbor is not in a maximal independent set,
	 its neighbor must be.  */
      if (bestd == 1)
	{
	  int u = neighbor_in_sg (bestv, sg);
      
	  vecset nsga(sg);
	  vecset nsta(start);
	  nsta[u] = true;
	  clear_neighborhood (u, nsga);
	  maximal_independent_sets (nsta, nsga, full_sg, vmap, n, max_indep_sets);
	}
      /* Enumerate sets not containing BESTV.  */
      else if (bestd > 1)
	{
	  vecset nsga(sg);
	  nsga[bestv] = false;
	  maximal_independent_sets (start, nsga, full_sg, vmap, n, max_indep_sets);
	}
    }

  /* For a vertex U of degree 2 in the subgraph induced by SG, fill in PATH
     the path of vertices of degree two from U to a vertex of degree other than
     two that does not contain the neighbor V of U.  */
  void trace_till_deg3 (int v, int u, const vecset &sg, vector<int> &path)
    {
      if (degree_in_sg (u, sg) != 2)
	return;

      for (int y : vs[u])
	if (y != v && sg[y])
	  {
	    path.push_back (u);
	    trace_till_deg3 (u, y, sg, path);
	    return;
	  }

      abort ();
    }

  /* For a vertex U of degree 2 in the subgraph induced by SG, fill in PATH
     the vertices of the maximal subpath of vertices of degree two containing V.  */
  void trace_till_deg3 (int v, const vecset &sg, vector<int> &path)
    {
      path.push_back (v);
      for (int u : vs[v])
	if (sg[u])
	  trace_till_deg3 (v, u, sg, path);
    }

  /* Returns true of the subgraph induced by SG contains a reducible
     path or cycle.  Assumes the subgraph is connected.  */
  bool any_reducible_subgraph (const vecset &sg)
    {
      int n = 0, s = 0;
      bool any_deg3 = false;
      for (int v = 0; v < nvs (); v++)
	if (sg[v])
	  {
	    n++;

	    int d = degree_in_sg (v, sg);
	    /* Vertices of degree at most one are always reducible
	       (we assume the graph is not a single edge with both
	       ends of total degree 1). */
	    if (d < 2)
	      return true;

	    if (d == 3)
	      any_deg3 = true;
	    else
	      s += 7 - total_degree[v];
	  }

      if (!any_deg3)
	return reducible_cycle (n, s);

      vecset seen (nvs (), false);

      for (int v = 0; v < nvs (); v++)
	if (sg[v] && !seen[v])
	  {
	     if (degree_in_sg (v, sg) != 2)
	       continue;
	  
	     vector<int> path;
	     trace_till_deg3 (v, sg, path);

	     int sumr = 0;
	     for (int y : path)
	       {
		 seen[y] = true;
		 sumr += 7 - total_degree[y];
	       }
	     if (reducible_path (path.size (), sumr))
	       return true;
	  }

      return false;
    }

  /* Returns true if the subgraph induced by SG is fractionally colorable.  */
  bool colorable (const vecset &sg)
    {
      /* Create a map from vertices of SG to ids 0, 1, ..., |SG|-1 (VID) and back (VMAP).  */
      vector<int> vmap;
      for (int v = 0; v < nvs (); v++)
       	if (sg[v])
	  vmap.push_back (v);
      if (vmap.empty ())
	return true;
      int n = vmap.size ();
      vector<int> vid(nvs ());
      for (int i = 0; i < n; i++)
	vid[vmap[i]] = i;

      list<vecset> max_indep_sets;
      maximal_independent_sets (vecset (nvs (), false), sg, sg, vid, n, max_indep_sets);

      /* A heuristic: setting x_v = 1/|maximum independent set containing v| gives a valid
	 fractional clique.  If it is too heavy, the subgraph is not colorable.  */
      vector<int> lis_cont (n, 0);
      for (const vecset &rvs : max_indep_sets)
	{
	  int sz = vecset_size (rvs);
	      
	  for (int i = 0; i < n; i++)
    	    if (rvs[i] && sz > lis_cont[i])
	      lis_cont[i] = sz;
	}

      mpq_class lis_val (0);
      for (int i = 0; i < n; i++)
	{
	  mpq_class toa(7 - total_degree[vmap[i]], lis_cont[i]);
	  toa.canonicalize ();
	  lis_val += toa;
	}
      if (lis_val > 11)
	return false;

      /* We use the LP for the fractional clique.  */
      GRBModel lp (env);
      vector<GRBVar> vars;
      lp.set (GRB_IntAttr_ModelSense, GRB_MAXIMIZE);
      for (int i = 0; i < n; i++)
	vars.push_back (lp.addVar (0, GRB_INFINITY, 7 - total_degree[vmap[i]], GRB_CONTINUOUS));
      lp.update ();

      vector<GRBConstr> cons;
      for (const vecset &rvs : max_indep_sets)
	{
	  GRBLinExpr lhs;
	  for (int i = 0; i < n; i++)
	    if (rvs[i])
	      lhs += vars[i];

	  cons.push_back (lp.addConstr (lhs, GRB_LESS_EQUAL, 1));
	}

      lp.optimize ();
      if (lp.get(GRB_IntAttr_Status) != GRB_OPTIMAL)
	abort ();
      double val = lp.get (GRB_DoubleAttr_ObjVal);
      if (val < 11 + EPS)
	{
	  if (DO_EXACT)
	    {
	      vector<mpq_class> cons_val;
	      /* Round the dual solution and verify it is a coloring.  */
	      int nc = cons.size ();
	      mpq_class totcol (0);
	      for (int i = 0; i < nc; i++)
		{
		  cons_val.push_back (to_rational (cons[i].get (GRB_DoubleAttr_Pi)));
		  if (cons_val[i] < 0)
		    abort ();

		  totcol += cons_val[i];
		}

	      mpq_class gap (1);
	      for (int v = 0; v < n; v++)
		{
		  mpq_class vcol (0);
		  int i = 0;
      
		  for (const vecset &rvs : max_indep_sets)
		    {
		      if (rvs[v])
			vcol += cons_val[i];

		      i++;
		    }

		  if (vcol < 7 - total_degree[vmap[v]])
		    {
		      mpq_class agap = (7 - total_degree[vmap[v]]) / vcol;
		      if (agap > gap)
			gap = agap;
		    }
		}
	      if (totcol * gap > 11)
		abort ();

	    }
	  return true;
	}
      else
	{
	  if (DO_EXACT)
	    {
	      /* Round the solution and verify it is indeed a too large fractional clique.  */

	      vector<mpq_class> var_val;
	      mpq_class obj (0);
	      for (int i = 0; i < n; i++)
		{
		  var_val.push_back (to_rational (vars[i].get (GRB_DoubleAttr_X)));
		  if (var_val[i] < 0)
		    abort ();

		  obj += (7 - total_degree[vmap[i]]) * var_val[i];
		}

	      if (obj <= 11)
		abort ();

	      for (const vecset &rvs : max_indep_sets)
		{
		  mpq_class lhs (0);
		  for (int i = 0; i < n; i++)
		    if (rvs[i])
		      lhs += var_val[i];

		  if (lhs > 1)
		    abort ();
		}
	    }

	  return false;
	}
    }

  /* Returns true if the graph is fractionally colorable.  */
  bool colorable (void)
    {
      return colorable (vecset (nvs (), true));
    }

  /* Returns true if the graph is not colorable, but every
     proper induced subgraph is colorable.  */
  bool critical (void)
    {
      vecset all (nvs (), true);
      if (any_reducible_subgraph (all) || colorable (all))
	return false;
      for (int v = 0; v < nvs (); v++)
	{
	  all[v] = false;
	  if (!colorable (all))
	    return false;
	  all[v] = true;
	}

      return true;
    }

  /* Returns the distance between U and V.  */
  int distance (int u, int v) const
    {
      vector<int> dist(nvs (), nvs ());
      dist[u] = 0;
      list<int> tp{u};
      while (true)
	{
	  int a = tp.front ();
	  tp.pop_front ();
	  int d = dist[a] + 1;

	  for (int x : vs[a])
	    {
	      if (x == v)
		return d;

	      if (dist[x] > d)
		{
		  dist[x] = d;
		  tp.push_back (x);
		}
	    }
	}
    }

  /* Returns true if the precoloring of BOUNDARY given by PRECOLORING (giving the amount of color
     that appear exactly on each subset of the boundary vertices) extends to a coloring of the subgraph induced by SG.  */
  bool coloring_extends (const vecset &sg, const vector<int> &boundary, const precol &precoloring)
    {
      /* Create a map from vertices of SG to ids 0, 1, ..., |SG|-1 (VID) and back (VMAP).  */
      vector<int> vmap;
      for (int v = 0; v < nvs (); v++)
       	if (sg[v])
	  vmap.push_back (v);
      if (vmap.empty ())
	return true;
      int n = vmap.size ();
      vector<int> vid(nvs ());
      for (int i = 0; i < n; i++)
	vid[vmap[i]] = i;

      unsigned bn = boundary.size ();
      list<vecset> max_indep_sets;

      for (unsigned s = 0; s < (1u << bn); s++)
	{
	  vecset ss = mk_vecset (bn, s);
	  vecset ss_in_g (nvs (), false);
	  vecset pruned (sg);
	  for (unsigned i = 0; i < bn; i++)
	    if (ss[i])
	      {
		ss_in_g[boundary[i]] = true;
		clear_neighborhood (boundary[i], pruned);
	      }
	    else
	      pruned[boundary[i]] = false;

	  if (!independent (ss_in_g))
	    {
	      if (precoloring.at (ss) != 0)
		abort ();
	      continue;
	    }
	  maximal_independent_sets (ss_in_g, pruned, pruned, vid, n, max_indep_sets);
	}

      /* We use the LP for the fractional clique.  */
      GRBModel lp (env);
      vector<GRBVar> vars;
      map<vecset, GRBVar> ss_vars;
      lp.set (GRB_IntAttr_ModelSense, GRB_MAXIMIZE);
      for (int i = 0; i < n; i++)
	vars.push_back (lp.addVar (0, GRB_INFINITY, 7 - total_degree[vmap[i]], GRB_CONTINUOUS));
      for (unsigned s = 0; s < (1u << bn); s++)
	{
	  vecset ss = mk_vecset (bn, s);
	  ss_vars[ss] = lp.addVar (-GRB_INFINITY, GRB_INFINITY, precoloring.at (ss).get_d (), GRB_CONTINUOUS);
	}
      lp.update ();

      vector<GRBConstr> cons;
      lp.addConstr (ss_vars[vecset (bn, false)], GRB_EQUAL, 0);

      for (const vecset &rvs : max_indep_sets)
	{
	  GRBLinExpr lhs;
	  for (int i = 0; i < n; i++)
	    if (rvs[i])
	      lhs += vars[i];

	  vecset rest(bn, false);
	  for (unsigned i = 0; i < bn; i++)
	    if (rvs[vid[boundary[i]]])
	      rest[i] = true;
	  lhs += ss_vars[rest];

	  cons.push_back (lp.addConstr (lhs, GRB_LESS_EQUAL, 1));
	}

      lp.optimize ();
      if (lp.get(GRB_IntAttr_Status) != GRB_OPTIMAL)
	abort ();
      double val = lp.get (GRB_DoubleAttr_ObjVal);
      if (val < 11 + EPS)
	{
	  if (DO_EXACT)
	    {
	      vector<mpq_class> cons_val;
	      /* Round the dual solution and verify it is a coloring.  */
	      int nc = cons.size ();
	      vector<int> isids;
	      vector<vecset> isvecs;
	      qvec sol;
	      auto isi = max_indep_sets.begin ();
	      for (int i = 0; i < nc; ++i, ++isi)
		{
		  cons_val.push_back (to_rational (cons[i].get (GRB_DoubleAttr_Pi)));
		  if (cons_val[i] < 0)
		    abort ();

		  if (cons_val[i] != 0)
		    {
		      isids.push_back (i);
		      isvecs.push_back (*isi);
		      sol.push_back (cons_val[i]);
		    }
		}

	      /* List the expected tight inequalities (and equalities).  */
	      list<qvec> tight_lhs (isids.size ());
	      qvec rhs;
	      for (int v = 0; v < n; v++)
		{
		  mpq_class vcol (0);
		  int i = 0;
      
		  for (const vecset &rvs : max_indep_sets)
		    {
		      if (rvs[v])
			vcol += cons_val[i];

		      i++;
		    }

		  if (vcol > (7 - total_degree[vmap[v]]) + GAP)
		    continue;

		  auto eq = tight_lhs.begin ();
		  for (int j = 0; j < (int) isids.size (); ++j, ++eq)
		    eq->emplace_back (isvecs[j][v] ? 1 : 0);
		  rhs.emplace_back (7 - total_degree[vmap[v]]);
		}

	      vector<vecset> isvecs_proj;
	      for (int j = 0; j < (int) isids.size (); ++j)
		{
		  vecset rest(bn, false);
		  for (unsigned i = 0; i < bn; i++)
		    if (isvecs[j][vid[boundary[i]]])
		      rest[i] = true;
		  isvecs_proj.push_back (rest);
		}

	      for (auto s = ss_vars.begin (); s != ss_vars.end (); ++s)
		{
		  vecset ss = s->first;
		  if (vecset_size (ss) == 0)
		    continue;

		  auto eq = tight_lhs.begin ();
		  for (int j = 0; j < (int) isids.size (); ++j, ++eq)
		    eq->emplace_back (isvecs_proj[j] == ss ? 1 : 0);
		  rhs.emplace_back (precoloring.at (ss));
		}

	      /* Sometimes, the rounding does not result in exact equality in the
		 tight inequalities.  In this case, solve the system given by the
		 tight inequalities exactly and use this solution instead of the
		 one obtained by rounding.  */
	      if (!is_solution (tight_lhs, rhs, sol))
		{
		  sol.clear ();
		  if (!express_as_lc (tight_lhs, rhs, sol))
		    abort ();

		  for (int j = 0; j < (int) isids.size (); ++j)
		    {
		      if (sol[j] < 0)
			abort ();
		      cons_val[isids[j]] = sol[j];
		    }
		}

	      for (int v = 0; v < n; v++)
		{
		  mpq_class vcol (0);
		  int i = 0;
      
		  for (const vecset &rvs : max_indep_sets)
		    {
		      if (rvs[v])
			vcol += cons_val[i];

		      i++;
		    }

		  if (vcol < 7 - total_degree[vmap[v]])
	      	    abort ();
		}

	      map<vecset, mpq_class> pcvals;
	      int ci = 0;
      
	      for (const vecset &rvs : max_indep_sets)
		{
	     	  vecset rest(bn, false);
    		  for (unsigned j = 0; j < bn; j++)
		    if (rvs[vid[boundary[j]]])
		      rest[j] = true;

		  if (vecset_size (rest) == 0)
		    {
		      ci++;
		      continue;
		    }

		  if (pcvals.count (rest) == 0)
		    pcvals[rest] = cons_val[ci];
		  else
		    pcvals[rest] += cons_val[ci];

		  ci++;
		}

	      for (auto si = pcvals.begin (); si != pcvals.end (); ++si)
	       	if (si->second != precoloring.at (si->first))
		  abort ();

	      mpq_class totcol (0);
	      for (int i = 0; i < nc; i++)
		totcol += cons_val[i];
	      if (totcol > 11)
		abort ();
	    }
	  return true;
	}
      else
	{
	  /* We should actually never get here, so let's not bother with the verification.  */
	  if (DO_EXACT)
	    abort ();
	  return false;
	}
    }

  /* Generates all extremal precolorings of the BOUNDARY, subject to additional constraints in ACON.  */
  void extremal_precolorings (const vector<int> &boundary, const addits &acon, list<precol> &precolorings)
    {
      int n = boundary.size ();
      vector<vecset> vars;
      precol base;

      int id = 0;
      Constraint_System cs;
      Linear_Expression total;
      for (unsigned s = 0; s < (1u << n); s++)
	{
	  vecset ss = mk_vecset (n, s);
	  vecset gss(nvs (), false);
	  for (int i = 0; i < n; i++)
	    if (ss[i])
	      gss[boundary[i]] = true;

	  if (!independent (gss))
	    {
	      base[ss] = 0;
	      continue;
	    }

	  vars.push_back (ss);
	  cs.insert (Variable (id) >= 0);
	  total += Variable (id);
	  id++;
	}
      cs.insert (total == 11);

      for (int i = 0; i < n; i++)
	{
	  Linear_Expression ci;
	  for (int v = 0; v < (int) vars.size (); v++)
	    if (vars[v][i])
	      ci += Variable (v);
	  cs.insert (ci == 7 - total_degree[boundary[i]]);
	}

      for (const addit *a : acon)
	{
  	  Linear_Expression intij;
	  for (int v = 0; v < (int) vars.size (); v++)
	    if (a->relevant (vars[v]))
	      intij += Variable (v);
	  if (a->leq)
	    cs.insert (intij <= a->rhs);
	  else
	    cs.insert (intij >= a->rhs);
	}

      C_Polyhedron poly (cs);
      const Generator_System &res = poly.minimized_generators ();
      for (Generator_System::const_iterator v = res.begin(), gs_end = res.end(); v != gs_end; ++v)
	{
	  if (!v->is_point ())
	    abort ();

	  precol act (base);
	  for (int i = 0; i < (int) vars.size (); i++)
	    {
	      act[vars[i]] = mpq_class (v->coefficient (Variable (i)),  v->divisor ());
	      act[vars[i]].canonicalize ();
	    }
	  precolorings.push_back (act);
	}
    }

  /* Tests whether all valid precolorings of the BOUNDARY (subject to additional constraints given
     by ACON) extend.  If not, a non-extending coloring of the boundary is returned in NONEXT.  */
  bool all_precolorings_extend (const vector<int> &boundary, precol &nonext, const addits &acon)
    {
      list<precol> precolorings;
      extremal_precolorings (boundary, acon, precolorings);
      int npc = precolorings.size ();
      vecset all (nvs (), true);
      int id = 0;
      for (precol &p : precolorings)
	{
	  id++;
	  if (id % 1000 == 0)
	    printf ("%d/%d\n", id, npc);
	  if (!coloring_extends (all, boundary, p))
	    {
	      nonext = p;
	      return false;
	    }
	}

      return true;
    }

  /* Initializes the graph from an encoding S (following the format used by code).  */
  graph (const string &s)
    {
      int n = s.size ();

      for (int a = 0; a < n; a++)
	{
	  if (!islower (s[a]))
	    continue;

	  int u = s[a] - 'a';
	  expand_till (u);
	  a++;
	  for (; a < n && s[a] != ';'; a++)
	    {
	      if (isdigit (s[a]))
		{
		  total_degree[u] += (s[a] - '0');
		  break;
		}

	      if (!islower (s[a]))
		continue;

	      int v = s[a] - 'a';
	      expand_till (v);
	      add_edge (u, v);
	    }
	}

      for (int v = 0; v < nvs (); v++)
	{
  	  total_degree[v] += degree(v);
	  if (total_degree[v] > 3)
	    abort ();
	}
    }

  /* Tests whether degree <= total degree for every vertex.  */
  void verify (void)
    {
      for (int v = 0; v < nvs (); v++)
	if (total_degree[v] < 2 || total_degree[v] > 3 || total_degree[v] < degree (v))
	  abort ();
    }
};

/* List of canonical codes of graphs we have already processed.  */
static unordered_set<string> seen;

/* Returns true if G was already processed, false otherwise.  Records
   G in the list of processed graphs.  */
static bool
register_graph (graph *g)
{
  string c = g->canonical_code ();
  if (seen.count (c) > 0)
    return true;

  seen.insert (c);
  return false;
}

/* Tests whether G is an obstacle, and if so, generates further obstacles from it.  */
static void generate_from (graph *g);

/* Tries subdividing twice edges of an obstacle G.  */
static void
subdivision_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    for (int v : g->vs[u])
      {
	if (v < u)
	  continue;

  	graph *ng = new graph (*g);
    	ng->delete_edge (u, v);
      	ng->add_path (u, v, 2);
	generate_from (ng);
      }
}

/* Tries nailing vertices of an obstacle G.  */
static void
nailed_obstacles (const graph *g)
{
  for (int v = 0; v < g->nvs (); v++)
    if (g->total_degree[v] == 2)
      {
	graph *ng = new graph (*g);
	ng->total_degree[v]++;
	generate_from (ng);
      }
}

/* Replaces nailed 2-vertices by subdivided K_4 in G.  */
static void
two_cut_obstacles (const graph *g)
{
  for (int v = 0; v < g->nvs (); v++)
    if (g->degree (v) == 2 && g->total_degree[v] == 3)
      {
	int u = g->vs[v].front ();

	graph *ng = new graph (*g);
	ng->delete_edge (u, v);
	ng->add_diamond (v, u);
	generate_from (ng);
      }
}

/* Replaces 2-vertices adjacent to 3-vertices in G by a vertex with three neighbors of degree
   two, the third of them attaches to a nailed vertex of G.  */
static void
tripod_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 2 && g->total_degree[u] == 2)
      {
	int v = g->vs[u].front ();
	int w = g->vs[u].back ();
	if (g->degree (v) != 3 || g->degree (w) != 3)
	  continue;

	for (int z = 0; z < g->nvs (); z++)
	  if (g->degree (z) == 2 && g->total_degree[z] == 3)
	    {
	      graph *ng = new graph (*g);
    	      ng->delete_edge (u, w);
	      int a = ng->nvs ();
	      ng->add_path (z, w, vecset{false,true,false});
	      ng->add_edge (u, a+1);
	      generate_from (ng);
	    }
      }
}

/* Splits 2-vertices adjacent to 3-vertices in G.  */
static void
split_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 2 && g->total_degree[u] == 2)
      for (int v : g->vs[u])
	if (g->degree (v) == 3)
	  {
	    for (int w : g->vs[v])
	      if (w != u)
		{
		  graph *ng = new graph (*g);
		  ng->delete_edge (v, w);
		  ng->total_degree[u] = 3;
		  ng->total_degree[v] = 2;
		  ng->add_path (u, w, vecset{false});
		  generate_from (ng);
		  break;
		}
	  }
}

/* Attaching subdivided K_4 on two edges of G.  */
static void
sdk4_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 2 && g->total_degree[u] == 2)
      for (int v : g->vs[u])
	if (g->degree (v) == 2 && g->total_degree[v] == 2 && u < v)
	  for (int x = 0; x < g->nvs (); x++)
	    if (g->degree (x) == 2 && g->total_degree[x] == 3)
	      for (int y : g->vs[x])
		if (g->degree (y) == 2 && g->total_degree[y] == 3 && x < y)
		  {
		    graph *ng = new graph (*g);
		    ng->total_degree[u] = 3;
		    ng->total_degree[v] = 3;
		    int a = ng->nvs ();
		    ng->add_path (u, x, vecset{true, true});
		    ng->add_path (v, y, vecset{true, true});
		    ng->add_edge (a, a + 2);
		    ng->add_edge (a + 1, a + 3);
		    generate_from (ng);
		  }
}

/* Attaching 5-cycle with two adjacent vertices of degree two
   plus its neighbors in a 6-cycle on a twice subdivided T in G.  */
static void
two2_6cycle_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 2 && g->total_degree[u] == 3)
      for (int v : g->vs[u])
	if (g->degree (v) == 2 && g->total_degree[v] == 2)
	  for (int w : g->vs[u])
	    if (g->degree (w) == 3)
	      {
		int x = -1;
		for (int t : g->vs[w])
		  if (t != u)
		    {
		      x = t;
		      break;
		    }
		graph *ng = new graph (*g);
		ng->total_degree[v] = 3;
		ng->delete_edge (u, v);
		ng->delete_edge (u, w);
		ng->delete_edge (x, w);
		ng->add_edge (x, u);
		int bnd[] = {u, v, w};
		for (int i = 0; i < 3; i++)
		  {
		    graph *ngm = new graph (*ng);
		    ngm->add_two2_6cycle (bnd[i], bnd[(i+1)%3], bnd[(i+2)%3]);
		    generate_from (ngm);
		  }
		delete ng;
	      }
}

/* Replacing edge + vertex by attaching a 5-cycle with two adjacent vertices of degree two in G.  */
static void
two2_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->total_degree[u] == 3)
      for (int v : g->vs[u])
	if (g->total_degree[v] == 3 && u < v)
	  for (int x = 0; x < g->nvs (); x++)
	    if (g->total_degree[x] == 2)
	      {
		graph *ng = new graph (*g);
		ng->delete_edge (u, v);
		ng->total_degree[x] = 3;

		int bnd[2][3] = {{u, v, x},{v,u,x}};
		for (int j = 0; j < 2; j++)
		  for (int i = 0; i < 3; i++)
		    {
		      graph *ngm = new graph (*ng);
		      ngm->add_two2 (bnd[j][i], bnd[j][(i+1)%3], bnd[j][(i+2)%3]);

		      if (g->nails () < 2)
			{
			  generate_from (ngm);
			  continue;
			}

		      if (ngm->critical ())
			abort ();

		      vector<int> ns;
		      ngm->nails (ns);
		      if (!ngm->adjacent (ns[0], ns[1]))
			{
			  graph *ngm1 = new graph (*ngm);
			  ngm1->add_path (ns[0], ns[1], 1);
			  generate_from (ngm1);
			}
		      ngm->add_path (ns[0], ns[1], 2);
		      generate_from (ngm);
		    }
		delete ng;
	      }
}

/* Adding an edge between non-adjacent vertices of total degree two in G
   that do not have a common neighbor.  */
static void
add_edge_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->total_degree[u] == 2)
      for (int v = u + 1; v < g->nvs (); v++)
	if (g->total_degree[v] == 2)
	  {
	    if (g->distance (u,v) <= 2)
	      continue;

	    graph *ng = new graph (*g);
	    ng->total_degree[u] = 3;
	    ng->total_degree[v] = 3;
	    ng->add_edge (u, v);
	    generate_from (ng);
	  }
}

/* Adding a path with one unnailed vertex of degree two between non-adjacent
   vertices of total degree two in G.  */
static void
add_2path_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->total_degree[u] == 2)
      for (int v = u + 1; v < g->nvs (); v++)
	if (g->total_degree[v] == 2)
	  {
	    if (g->adjacent (u,v))
	      continue;

	    graph *ng = new graph (*g);
	    ng->total_degree[u] = 3;
	    ng->total_degree[v] = 3;
	    ng->add_path (u, v, 1);
	    generate_from (ng);
	  }
}

/* Expanding an edge to a 4-cycle in G.  */
static void
add_flattened_c4_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 3)
      for (int v : g->vs[u])
	if (u < v && g->degree (v) == 3)
	  for (int x : g->vs[u])
	    {
	      if (x == v)
		continue;
	      for (int w : g->vs[u])
		{
		  if (w == v || w == x)
		    continue;
		  for (int y : g->vs[v])
		    {
		      if (y == u)
			continue;
		      for (int z : g->vs[v])
			{
			  if (z == u || z == y)
			    continue;

			  graph *ng = new graph (*g);
			  int a = g->nvs ();
			  ng->delete_edge (u, w);
			  ng->delete_edge (v, z);
			  ng->add_path (u, v, vecset{true,true});
			  ng->add_edge (a, z);
			  ng->add_edge (a + 1, w);
			  generate_from (ng);
			}
		    }
		}
	    }
}

/* Adds a vertex of degree two and its neighbors of degree three to G.  */
static void
add_deg2_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->total_degree[u] == 2)
      for (int v = u + 1; v < g->nvs (); v++)
	if (g->total_degree[v] == 2 && !g->adjacent (u, v))
	  for (int w = u + 1; w < g->nvs (); w++)
	    if (v != w && g->total_degree[w] == 2)
	      for (int z = w + 1; z < g->nvs (); z++)
		if (v != z && g->total_degree[z] == 2 && !g->adjacent (w, z))
		  {
		    graph *ng = new graph (*g);
		    int a = g->nvs ();
		    ng->total_degree[u] = 3;
		    ng->total_degree[v] = 3;
		    ng->total_degree[w] = 3;
		    ng->total_degree[z] = 3;
		    ng->add_path (u, v, vecset{true});
		    ng->add_path (w, z, vecset{true});
		    ng->add_path (a, a + 1, 1);
		    generate_from (ng);
		  }
}

/* Replaces a vertex of degree two and its neighbors of degree three in G
   by symmetric joined 5-cycles with two vertices of degree two.  */
static void
add_deg2_sym5c_obstacles (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 2 && g->total_degree[u] == 3)
      {
	int z1 = g->vs[u].front ();
	int z2 = g->vs[u].back ();
	if (g->degree (z1) != 3 || g->degree (z2) != 3)
	  continue;

	vector<int> roots;
	for (int v : g->vs[z1])
	  if (v != u)
	    roots.push_back (v);
	for (int v : g->vs[z2])
	  if (v != u)
	    roots.push_back (v);
	if (roots.size () != 4)
	  abort ();

	for (int i = 0; i < 3; i++)
	  for (int j = 0; j < 3; j++)
	    {
	      if (i == j)
		continue;

	      int a = roots[i];
	      int b = roots[j];
	      int c = roots[3 - i - j];
	      int d = roots[3];
		    
	      graph *ng = new graph (*g);
	      ng->delete_edge (z1, roots[0]);
	      ng->delete_edge (z1, roots[1]);
	      ng->delete_edge (z2, roots[2]);
	      ng->delete_edge (z2, roots[3]);
	      int x = g->nvs ();
	      ng->add_path (z1, z2, vecset{false, true, true, true, false});
	      ng->add_edge (u, x + 2);
	      ng->add_edge (z1, a);
	      ng->add_edge (x + 1, b);
	      ng->add_edge (x + 3, c);
	      ng->add_edge (z2, d);
	      generate_from (ng);
	    }
      }
}

/* Adds a C_4 on neighbors of degree two vertices in G.  */
static void
add_c4_obstacles (const graph *g)
{
  if (g->nails () != 0)
    return;

  vector<int> d2s;
  g->vertices_of_type (2, 2, d2s);
  if (d2s.size () != 4)
    return;

  for (int i = 0; i < 3; i++)
    {
      int u = d2s[3];
      int v = d2s[i];
      int x = d2s[(i + 1) % 3];
      int y = d2s[(i + 2) % 3];
		    
      graph *ng = new graph (*g);
      int a = g->nvs ();
      for (int j = 0; j < 4; j++)
	ng->total_degree[d2s[j]] = 3;
      ng->add_path (u,x,vecset{true,true,true,true});
      ng->add_edge (a+1,y);
      ng->add_edge (a+2,v);
      ng->add_edge (a,a+3);
      generate_from (ng);
    }
}

/* Adds a neighborhood of a vertex on degree two vertices in G.  */
static void
add_nbhd_obstacles (const graph *g)
{
  vector<int> d2s;
  g->nails (d2s);
  g->vertices_of_type (2, 2, d2s);
  if (d2s.size () != 6)
    return;
  vector<bool> match (6, false);

  int a = 0;
  for (int i = 1; i < 6; i++)
    {
      if (g->distance (d2s[a], d2s[i]) <= 2)
	continue;

      match[a] = match[i] = true;

      int b = a + 1;
      while (match[b])
	b++;

      for (int j = b + 1; j < 6; j++)
	{
	  if (match[j] || g->distance (d2s[b], d2s[j]) <= 2)
	    continue;
	  match[b] = match[j] = true;

	  int c = b + 1;
	  while (match[c])
	    c++;
	  int k = c + 1;
	  while (match[k])
	    k++;

	  if (g->distance (d2s[c], d2s[k]) > 2)
	    {
	      graph *ng = new graph (*g);
	      int t = ng->nvs ();
	      for (int r = 0; r < 6; r++)
		ng->total_degree[d2s[r]] = 3;

	      ng->add_path (d2s[a], d2s[i], vecset{true});
	      ng->add_path (d2s[b], d2s[j], vecset{true});
	      ng->add_path (d2s[c], d2s[k], vecset{true});
	      ng->add_vertex (vector<int>{t, t+1, t+2}, 3);
	      generate_from (ng);
	    }

	  match[b] = match[j] = false;
	}

      match[a] = match[i] = false;
    }
}

/* Tests reducibility of G + subdivided k4 + one or two pending edges.  */

static void
test_reducibility_add_k4 (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->degree (u) == 2 && g->total_degree[u] == 2)
      for (int v : g->vs[u])
	if (g->degree (v) == 2 && g->total_degree[v] == 2 && u < v)
	  for (int x = 0; x < g->nvs (); x++)
	    if (g->degree (x) == 2 && g->total_degree[x] == 3)
	      {
		precol bad;
		graph *ng = new graph (*g);
		ng->total_degree[u] = 3;
	    	ng->total_degree[v] = 3;
		int a = ng->nvs ();
		ng->add_path (u, v, vecset{true, true, true, true, true, true});
		ng->add_edge (a, a + 4);
		ng->add_edge (a + 1, a + 5);
		int b1 = a+2;
		int b2 = a+3;

		graph *nge = new graph (*ng);
		int c = nge->add_vertex (vector<int>{x}, 2);
		if (!nge->all_precolorings_extend (vector<int>{b1,b2,c}, bad, addits{}))
		  {
		    printf ("Irreducible (add_k4_1, %d, %d, %d) %s ", u, v, x, g->code ().c_str ());
		    dump_precoloring (3, bad);
		    abort ();
		  }

      		for (int y = x + 1; y < g->nvs (); y++)
      		  if (g->degree (y) == 2 && g->total_degree[y] == 3)
		    {
		      if (g->adjacent (x, y))
			{
			  if (!ng->all_precolorings_extend (vector<int>{b1,b2,x,y}, bad, addits{}))
			    {
			      printf ("Irreducible (add_k4_2a, %d, %d, %d, %d) %s ", u, v, x, y, g->code ().c_str ());
			      dump_precoloring (4, bad);
			      abort ();
			    }
			}
		      else
			{
			  graph *ngee = new graph (*nge);
			  /* G is necessarily C_5, so x & y cannot have neighbors of degree 2 by previous
			     reductions.  Furthermore, we replace by a reducent consisting of a nailed 2-vertex.
			     If c and d are adjacent, we instead extend the configuration by one more rung, with
			     just one vertex nailed in the reducent.  In either case, if that creates an obstruction,
			     the combined configuration is reducible.  */
			  int d = ngee->add_vertex (vector<int>{y}, 3);
			  ngee->total_degree[c] = 3;
			  if (!ngee->all_precolorings_extend (vector<int>{b1,b2, c, d}, bad, addits{pacu_le (vector<int>{2, 3}, 7)}))
			    {
			      printf ("Irreducible (add_k4_2b, %d, %d, %d, %d) %s ", u, v, x, y, g->code ().c_str ());
			      dump_precoloring (4, bad);
			      abort ();
			    }

			  graph ngee_k4 (*ngee);
			  ngee_k4.add_diamond (c, d);
			  int e = ngee_k4.add_vertex (vector<int>{d}, 2);
			  if (!ngee_k4.all_precolorings_extend (vector<int>{b1,b2, e}, bad, addits{}))
			    {
			      printf ("Irreducible (add_k4_2b_k4, %d, %d, %d, %d) %s ", u, v, x, y, g->code ().c_str ());
			      dump_precoloring (3, bad);
			      abort ();
			    }

			  ngee->add_edge (c, d);
			  int c1 = ngee->add_vertex (vector<int>{c}, 2);
			  int d1 = ngee->add_vertex (vector<int>{d}, 2);
			  if (!ngee->all_precolorings_extend (vector<int>{b1,b2, c1, d1}, bad, addits{paci_le (2, 3, 2)}))
			    {
			      printf ("Irreducible (add_k4_2b+, %d, %d, %d, %d) %s ", u, v, x, y, g->code ().c_str ());
			      dump_precoloring (4, bad);
			      abort ();
			    }
			  ngee->add_path (c1, d1, vecset{false});
			  ngee->total_degree[c1] = 3;
			  if (!ngee->all_precolorings_extend (vector<int>{b1,b2, c1}, bad, addits{}))
			    {
			      printf ("Irreducible (add_k4_2b++, %d, %d, %d, %d) %s ", u, v, x, y, g->code ().c_str ());
			      dump_precoloring (4, bad);
			      abort ();
			    }
			  delete ngee;
			}
		    }

		delete ng;
		delete nge;
	      }
}

/* Tests whether all possible ways of adding neighbors of degree 2 or 3
   to BOUNDARY in G result in a reducible subgraph.  DEG2NBR is the
   number of neighbors that must have degree two.
   REDU_UNION gives a total amount of color that can appear on the boundary
   (due to a reducent).  */
static bool
all_ns_extend (const graph *g, const vector<int> &boundary, int deg2nbr, int redu_union = 11)
{
  int n = boundary.size ();
  for (int i = 0; i < n; i++)
    if (g->degree (boundary[i]) != 2 || g->total_degree[boundary[i]] != 3)
      abort ();

  graph ng (*g);
  vector<int> bn[2];
  for (int i = 0; i < n; i++)
    {
      bn[0].push_back (ng.add_vertex (vector<int>{boundary[i]}, 3));
      bn[1].push_back (ng.add_vertex (vector<int>{bn[0].back ()}, 3));
    }
  vector<int> all;
  for (int i = 0; i < n; i++)
    all.push_back (i);

  for (int s = 0; s < (1 << n); s++)
    {
      vecset ss = mk_vecset (n, s);
      int nd2 = 0;
      for (int i = 0; i < n; i++)
	if (ss[i])
	  nd2++;
      if (nd2 < deg2nbr)
	continue;
      vector<int> abou;
      for (int i = 0; i < n; i++)
	{
	  if (ss[i])
	    {
	      abou.push_back (bn[1][i]);
	      ng.total_degree[bn[0][i]] = 2;
	    }
	  else
	    {
	      abou.push_back (bn[0][i]);
	      ng.total_degree[bn[0][i]] = 3;
	    }
	}
      addits acs;
      for (int i = 0; i < n; i++)
	for (int j = i + 1; j < n; j++)
	  if (!ss[i] && !ss[j] && ng.adjacent (boundary[0], boundary[1]))
	    acs.push_back (new aci_le (i, j, 3));

      if (s == 0 && acs.empty ())
	acs.push_back (new acu_le (all, redu_union));

      precol none;
      if (!ng.all_precolorings_extend (abou, none, acs))
	{
	  printf ("%d\n", s);
	  dump_precoloring (n, none);
	  return false;
	}

      for (const addit *a : acs)
	delete a;
    }

  return true;
}


/* Tests reducibility of G + deg 2 vertex and its deg 3 neighbors.  */

static void
test_reducibility_add_deg2 (const graph *g)
{
  for (int u = 0; u < g->nvs (); u++)
    if (g->total_degree[u] == 2)
      for (int v = 0; v < g->nvs (); v++)
	if (u != v && g->total_degree[v] == 2)
	  for (int x = 0; x < g->nvs (); x++)
	    if (g->degree (x) == 2 && g->total_degree[x] == 3)
	      {
		precol bad;
		graph ng (*g);
		ng.total_degree[u] = 3;
	    	ng.total_degree[v] = 3;
		int a = ng.nvs ();
		ng.add_path (u, v, vecset{true, false, true});
		int b1 = ng.add_vertex (vector<int>{a}, 3);
		int b2 = ng.add_vertex (vector<int>{a+2}, 3);

		graph nge (ng);
		int c = nge.add_vertex (vector<int>{x}, 3);
		if (!nge.all_precolorings_extend (vector<int>{b1,b2,c}, bad, addits{pacu_le (vector<int>{0, 1}, 6)}))
		  {
		    printf ("Irreducible (add_deg2 + redu, %d, %d, %d) %s ", u, v, x, g->code ().c_str ());
		    dump_precoloring (3, bad);
		    abort ();
		  }

		nge.total_degree[c] = 2;
		int cp = nge.add_vertex (vector<int>{c}, 3);
		if (!nge.all_precolorings_extend (vector<int>{b1,b2,cp}, bad, addits{}))
		  {
		    printf ("Irreducible (add_deg2 + neighbor of x has deg 2, %d, %d, %d) %s ", u, v, x, g->code ().c_str ());
		    dump_precoloring (3, bad);
		    abort ();
		  }

		graph ngek4 (ng);
		int l = ngek4.nvs ();
		ngek4.add_path (b1, b2, vecset{true, true, false, true, true});
		ngek4.add_edge (l, l+4);
		ngek4.add_edge (l+1, b2);
		if (!all_ns_extend (&ngek4, vector<int>{b1,l+3,x}, 0))
		  {
		    printf ("Irreducible (add_deg2 + k4 obstacle to redu, %d, %d, %d) %s ", u, v, x, g->code ().c_str ());
		    abort ();
		  }

		ng.add_edge (b1, b2);
		if (!all_ns_extend (&ng, vector<int>{b1,b2,x}, 1))
		  {
		    printf ("Irreducible (add_deg2 adj deg2, %d, %d, %d) %s ", u, v, x, g->code ().c_str ());
		    abort ();
		  }

		int b1p = ng.add_vertex (vector<int>{b1}, 3);
		int b2p = ng.add_vertex (vector<int>{b2}, 3);
		int cx = ng.add_vertex (vector<int>{x}, 3);
		if (!ng.all_precolorings_extend (vector<int>{b1p,b2p,cx}, bad, addits{paci_le (0, 1, 2)}))
		  {
		    printf ("Irreducible (add_deg2 adj + redu, %d, %d, %d) %s ", u, v, x, g->code ().c_str ());
		    dump_precoloring (3, bad);
		    abort ();
		  }
	      }
}

/* Tests reducibility of configurations created by combining G (with four vertices
   of degree two and one nailed vertex) with a neighborhood of a vertex.  */
static void
test_reducibility_add_nbhd4 (const graph *g)
{
  if (g->nails () != 1)
    return;

  vector<int> d2s;
  g->vertices_of_type (2, 2, d2s);
  if (d2s.size () != 4)
    return;

  for (int i = 0; i < 4; i++)
    for (int j = i + 1; j < 4; j++)
      {
	int u = d2s[i];
	int v = d2s[j];
	/* Do not create 4-cycles.  */
	if (g->distance (u, v) <= 2)
	  continue;
	vector<int> r;
	for (int k = 0; k < 4; k++)
	  if (k != i && k != j)
	    r.push_back (d2s[k]);

	vector<int> ns;
	g->nails (ns);

	graph ng(*g);
	for (int k = 0; k < 4; k++)
	  ng.total_degree[d2s[k]] = 3;
	int a = g->nvs ();
	ng.add_path (u, v, vecset{true});
	ng.add_path (a, r[0], vecset{true,true});
	ng.add_path (a+1, r[1], vecset{true});

	int x = ng.add_vertex (vector<int>{a+2},3);
	int y = ng.add_vertex (vector<int>{a+3},3);
	int z = ng.add_vertex (vector<int>{ns[0]},3);
	precol bad;
	if (!ng.all_precolorings_extend (vector<int>{x,y,z}, bad, addits{}))
	  {
	    printf ("Irreducible (add_nbhd4, %d, %d, %d, %d) %s ", u, v, r[0], r[1], g->code ().c_str ());
	    dump_precoloring (3, bad);
	    abort ();
	  }
      }
}

/* Tests reducibility of configurations created by adding a neighborhood of a vertex
   on three vertices of degree two in G plus one nailed vertex.  */
static void
test_reducibility_add_nbhd31 (const graph *g)
{
  if (g->nails () != 1)
    return;

  vector<int> d2s;
  g->vertices_of_type (2, 2, d2s);
  if (d2s.size () != 3)
    return;

  /* We already excluded subdivided K_4 as a subgraph.  */
  if (g->canonical_code () == "a:dh;b:cf;c:g;d:fg;e:fgh;c1")
    return;

  precol bad;

  vector<int> ns;
  g->nails (ns);
  int t = g->nvs ();

  graph nga (*g);
  for (int i = 0; i < 3; i++)
    nga.total_degree[d2s[i]] = 3;
  nga.add_path (d2s[0], d2s[1], vecset{true,true,true});
  nga.add_path (t+1, d2s[2], vecset{true});

  int x = nga.add_vertex(vector<int>{t},3);
  int y = nga.add_vertex(vector<int>{t+2},3);
  int z = nga.add_vertex(vector<int>{t+3},3);
  int u = nga.add_vertex(vector<int>{ns[0]},3);
	
  if (!nga.all_precolorings_extend (vector<int>{x,y,z,u}, bad, addits{}))
    {
      printf ("Irreducible (add_nbhd31 sym, %d, %d, %d, %d) %s ", d2s[0], d2s[1], d2s[2], ns[0], g->code ().c_str ());
      dump_precoloring (4, bad);
      abort ();
    }

  for (int r = 0; r < 3; r++)
    {
      if (g->distance (d2s[(r+1) % 3], d2s[(r+2) % 3]) <= 2)
	continue;

      graph ngb (*g);
      for (int i = 0; i < 3; i++)
	ngb.total_degree[d2s[i]] = 3;

      ngb.add_path (d2s[r], d2s[(r+1) % 3], vecset{true,true,true});
      ngb.add_edge (d2s[(r+2) % 3], t+2);

      x = ngb.add_vertex(vector<int>{t},3);
      y = ngb.add_vertex(vector<int>{t+1},3);
      u = ngb.add_vertex(vector<int>{ns[0]},3);
	
      if (!ngb.all_precolorings_extend (vector<int>{x,y,u}, bad, addits{paci_le (0,1,3)}))
	{
	  printf ("Irreducible (add_nbhd31 asym, %d, %d, %d, %d) %s ", d2s[r], d2s[(r+1)%3], d2s[(r+2)%3], ns[0], g->code ().c_str ());
	  dump_precoloring (3, bad);
	  abort ();
	}
    }
}

/* Tests reducibility of various configurations derived from G.  */

static void
test_reducibility_of_superconfigurations (const graph *g)
{
  /* Verify the conditions (b0) and (c0).  */
  int ns = g->nails ();
  vector<int> d2s;
  g->vertices_of_type (2, 2, d2s);

  if (ns == 1 && d2s.size () < 3)
    abort ();
  if (ns + d2s.size () == 3)
    abort ();

  /* Lemma 5.3.  */
  test_reducibility_add_k4 (g);

  /* Lemma 8.2.  */
  if (g->nails () == 1
      && !g->is_cycle ())
    test_reducibility_add_deg2 (g);

  /* Lemma 10.1, case F intersects N in four vertices.  */
  test_reducibility_add_nbhd4 (g);

  /* Lemma 10.1, case F intersects N in three vertices.  */
  test_reducibility_add_nbhd31 (g);
}

/* List of all found obstacles.  */
static list<graph *> obstacles;

/* Tests whether G is an obstacle, and if so, generates further obstacles from it.  */
static void
generate_from (graph *g)
{
  if (register_graph (g) || !g->critical ())
    {
      delete g;
      return;
    }

  obstacles.push_back (new graph (*g));

  if (g->nails () > 1)
    cout << "DANGEROUS! ";
  if (find (g->total_degree.begin (), g->total_degree.end (), 2) == g->total_degree.end ())
    cout << "FULL! ";
  cout << g->nvs () << " vertices " << g->nails () << " nails ";
  cout << g->canonical_code () << endl;

  if (DO_TEST)
    test_reducibility_of_superconfigurations (g);

  if (!DO_GEN)
    {
      delete g;
      return;
    }

  /* Lemma 3.3:  */
  two_cut_obstacles (g);

  /* Lemma 3.4:  */
  nailed_obstacles (g);

  /* Lemma 3.5:  */
  subdivision_obstacles (g);

  /* Lemma 4.2:  */
  tripod_obstacles (g);
  split_obstacles (g);

  /* Lemma 5.3:  */
  sdk4_obstacles (g);

  /* Lemma 6.2:  */
  two2_6cycle_obstacles (g);

  /* Lemma 6.3:  */
  two2_obstacles (g);

  /* Lemma 7.2:  */
  add_flattened_c4_obstacles (g);

  /* Lemma 7.3:  */
  add_edge_obstacles (g);

  /* Lemma 8.2:  */
  add_2path_obstacles (g);
  add_deg2_obstacles (g);

  /* Lemma 8.3: */
  add_deg2_sym5c_obstacles (g);

  /* Lemma 9.1: */
  add_c4_obstacles (g);

  /* Lemma 10.1: */
  add_nbhd_obstacles (g);

  delete g;
}

/* Tests graphs created by combining G1 and G2.  */

static void
test_obstacle_combinations (const graph *g1, const graph *g2)
{
  for (int u = 0; u < g1->nvs (); u++)
    if (g1->total_degree[u] == 2)
      for (int v = u + 1; v < g1->nvs (); v++)
	if (g1->total_degree[v] == 2)
	  for (int x = 0; x < g1->nvs (); x++)
	    if (g1->degree (x) == 2 && g1->total_degree[x] == 3)
	      for (int z = 0; z < g2->nvs (); z++)
		if (g2->total_degree[z] == 2)
		  for (int y = 0; y < g2->nvs (); y++)
		    if (g2->degree (y) == 2 && g2->total_degree[y] == 3)
		      {
			int zns[2][2] = {{g2->vs[z].front (), g2->vs[z].back ()},
			      {g2->vs[z].back (), g2->vs[z].front ()}};
			for (int i = 0; i < 2; i++)
			  {
			    int z1 = zns[i][0];
			    int z2 = zns[i][1];

			    graph ng (*g1);
			    int delta = g1->nvs ();
			    ng.add (*g2);
			    ng.total_degree[u] = 3;
			    ng.total_degree[v] = 3;
			    ng.delete_edge (z + delta, z1 + delta);
			    ng.delete_edge (z + delta, z2 + delta);
			    ng.add_edge (x, y + delta);
			    ng.add_vertex (vector<int>{u,z1+delta,z+delta}, 3);
			    ng.add_vertex (vector<int>{v,z2+delta,z+delta}, 3);
			    vecset all (ng.nvs (), true);
			    if (!register_graph (&ng) && !ng.colorable (all))
			      {
				cout << "EXTRA! ";
				cout << ng.nvs () << " vertices " << ng.nails () << " nails ";
				cout << ng.canonical_code () << endl;
				abort ();
			      }
			  }
		      }
}

int main (int argc, char *argv[])
{
  env.set (GRB_IntParam_OutputFlag, 0);
  precol none;

  /* The basic obstructions: C_5 and K_4^+  */
  generate_from (new graph (string ("a:be;b:c;c:d;d:e;")));
  generate_from (new graph (string ("a:bde;b:ch;c:df;d:g;e:f;g:h;")));

  /* Lemma 4.1: 5-cycle with three nailed vertices, one of them adjacent
     to a path of two vertices of degree two outside.  */
  graph five3two2 (string ("a:eh;b:ce;c:d;d:f;e:f;f:g;g:h;a1"));
  for (int v = 1; v <= 3; v++)
    for (int l = 0; l <= 2; l++)
      {
	if (v == 1 && l == 0)
	  continue;

	graph *ng = new graph (five3two2);
	ng->total_degree[v] = 3;
	ng->add_path (0, v, l);
	generate_from (ng);
      }

  /* Lemma 4.1: Reducibility of 5-cycles with non-adjacent vertices of degree two,
     and at least one of the adjacent vertices of degree three has a neighbor of
     degree two outside.  */
  graph five3nonadj (string ("a:be;b:c;c:d;d:e;a1b1d1"));
  if (!all_ns_extend (&five3nonadj, vector<int>{0,1,3}, 2))
    abort ();
  graph five3nonadja (string ("a:d;b:f;c:h;d:e;e:fi;f:g;g:h;h:i;a2b2c2"));
  if (!five3nonadja.all_precolorings_extend (vector<int>{0, 1, 2}, none, addits{}))
    abort ();

  /* Lemma 4.1: 5-cycles with non-adjacent vertices of degree two, the adjacent vertices
     of degree three do not have a neighbor of degree two outside, reducibility with a reducent,
     and the graphs arising from the condition (iv).  */
  graph five3nonadjb (string ("a:d;b:e;c:g;d:eh;e:f;f:g;g:h;a2b2c1"));
  if (!five3nonadjb.all_precolorings_extend (vector<int>{0, 1, 2}, none, addits{paci_le (0, 1, 2)}))
    abort ();

  if (!graph (string ("a:be;b:c;c:df;d:eh;f:gi;g:hj;h:i;i:k;j:k;k:a")).colorable ()
      || !graph (string ("a:be;b:c;c:df;d:eh;f:gi;g:hj;h:i;i:k;j:k;k:l;l:a")).colorable ())
    abort ();

  /* Lemma 4.1: 5-cycles with adjacent vertices of degree two, the paths leaving them join
     at the same vertex.  */
  graph five3adj (string ("a:be;b:c;c:d;d:e;a1b1c1"));
  for (int s1 = 0; s1 < 2; s1++)
    for (int s2 = 0; s2 < 2; s2++)
      for (int s3 = s1; s3 < 2; s3++)
	{
	  if (s1 == 0 && s2 == 0)
	    continue;

	  graph *ng = new graph (five3adj);
	  int m = 5 + s1;
	  ng->add_path (0, 2, s1 + s3 + 1);
	  ng->add_path (m, 1, s2);
	  ng->total_degree[m] = 3;
	  generate_from (ng);
	}

  /* Lemma 4.1: 5-cycles with adjacent vertices of degree two, at least one neighbor of
     degree two outside, reducibility with a reducent.  */
  for (int s1 = 0; s1 < 2; s1++)
    for (int s2 = 0; s2 < 2; s2++)
      for (int s3 = s1; s3 < 2; s3++)
	{
	  if (s2 == 0 && s3 == 0)
	    continue;

	  graph five3adja (five3adj);
	  int a = five3adja.nvs ();
	  five3adja.expand_till (a + 2);
	  five3adja.total_degree[a] = 3;
	  five3adja.total_degree[a+1] = 3;
	  five3adja.total_degree[a+2] = 3;
	  five3adja.add_path (0, a, s1);
	  five3adja.add_path (1, a + 1, s2);
	  five3adja.add_path (2, a + 2, s3);
	  if (!five3adja.all_precolorings_extend (vector<int>{a, a + 1, a + 2}, none, addits{paci_le (0, 1 + s2, 2)}))
	    {
	      cout << s1 << " " << s2 << " " << s3 << endl;
	      dump_precoloring (3, none);
	      abort ();
	    }
	}

  /* Lemma 4.1: The graphs corresponding graphs arising from the condition (iv).  */
  for (int s1 = 0; s1 < 2; s1++)
    for (int s2 = 0; s2 < 2; s2++)
      for (int s3 = s1; s3 < 2; s3++)
	{
	  if (s2 == 0 && s3 == 0)
	    continue;

	  graph five3adjb (five3adj);
	  int a = five3adjb.nvs ();
	  five3adjb.expand_till (a + 2);
	  five3adjb.total_degree[a] = 3;
	  five3adjb.total_degree[a+1] = 3;
	  five3adjb.total_degree[a+2] = 3;
	  five3adjb.add_path (0, a, s1);
	  five3adjb.add_path (1, a + 1, s2);
	  five3adjb.add_path (2, a + 2, s3);

	  int w, r;
	  if (s2)
	    {
	      w = a + 2;
	      r = a + 1;
	    }
	  else
	    {
	      w = a + 1;
	      r = a + 2;
	    }
	  int m1 = five3adjb.nvs ();
	  five3adjb.add_path (a, r, vecset{true, false});
	  int m2 = five3adjb.nvs ();
	  five3adjb.add_path (a, r, vecset{true});
	  five3adjb.add_edge (m1, w);
	  five3adjb.add_edge (m2, w);
	  if (!five3adjb.colorable ())
	    abort ();
	}

  /* Lemma 4.2: A vertex with three neighbors of degree two, reducibility with a reducent.  See also
     tripod_obstacles for graphs arising from the condition (iv).  */
  graph threedeg2 (string ("a:d;b:e;c:f;g:def;a2b2c2"));
  if (!threedeg2.all_precolorings_extend (vector<int>{0, 1, 2}, none, addits{pacu_le (vector<int>{0,1}, 6)}))
    abort ();

  /* Lemma 4.2: Contracting two neighbors of degree two as a reducent.  See also split_obstacles for
     graphs arising from the condition (iv).  */
  graph twodeg2ns (string ("a:d;b:e;c:f;d:ef;a2b2c2"));
  if (!twodeg2ns.all_precolorings_extend (vector<int>{0, 1, 2}, none, addits{pacu_le (vector<int>{1,2}, 7), pac_i0u12_2 ()}))
    abort ();

  /* Lemma 4.2: The last graph discussed in the proof.  */
  if (!graph (string ("a:beh;b:ci;c:d;d:ej;e:f;f:g;g:hi;h:j")).colorable ())
    abort ();

  /* Lemma 5.1: Reducibility of a 4-cycle with a vertex of degree two.  */
  graph fourdeg2 (string ("a:d;b:e;c:f;d:eg;e:f;f:g;a2b1c2"));
  if (!fourdeg2.all_precolorings_extend (vector<int>{0, 1, 2}, none, addits{paci_le (0, 1, 3), paci_le (1, 2, 3)}))
    abort ();

  /* Lemma 5.2: Reducibility of a subdivided K_4 with three nailed vertices.  */
  graph k4three (string ("a:d;b:ci;c:g;d:eh;e:f;f:gi;g:h;h:i;a2b1c1"));
  if (!k4three.all_precolorings_extend (vector<int>{0, 1, 2}, none, addits{}))
    abort ();

  /* Lemma 5.3: Reducibility of a subdivided K_4 with four nailed vertices, with reducent.  
     See also sdk4_obstacles for graphs arising from the condition (iv), and
     test_reducibility_add_k4 for the case F is an obstruction with one or two nailed vertices.  */
  graph k4four (string ("a:e;b:f;c:k;d:l;e:fi;f:g;g:hj;h:ik;i:j;j:l;k:l;a1b1c1d1"));
  if (!k4four.all_precolorings_extend (vector<int>{0, 1, 2, 3}, none, addits{paci_le (0, 1, 3), paci_le (2, 3, 1)}))
    abort ();

  /* Lemma 5.3: Obstruction with two nailed vertices that results in a new obstruction.  */
  generate_from (new graph (string ("a:bfe;b:ci;c:dk;d:ef;e:h;f:g;g:ih;h:k;i:j;j:k")));

  /* Lemma 5.3: Colorability of graphs from the case {w_1,w_2} intersects {v_3,v_4}.  */
  if (!graph (string ("a:bdg;b:ce;c:dk;d:m;e:fh;f:gj;g:h;h:i;i:jm;j:k;k:l;l:m")).colorable ()
      || !graph (string ("a:bng;b:ce;c:dk;d:mn;e:fh;f:gj;g:h;h:i;i:jm;j:k;k:l;l:m")).colorable ())
    abort ();

  /* Lemma 6.1: 5-cycle with three vertices of degree three, whose neighbors have a common neighbor.  */
  graph g1 (string ("a:de;b:df;c:dg;e:fi;f:g;g:h;h:i;a1b1c1"));
  if (!all_ns_extend (&g1, vector<int>{0,1,2}, 0))
    abort ();

  /* Lemma 6.2: 5-cycle with three vertices of degree three, z_1 or z_2 has degree two.  */
  generate_from (new graph (string ("a:bfi;b:ch;c:dj;d:eg;e:fk;g:h;i:jm;j:k;k:l;l:m")));
  generate_from (new graph (string ("a:bfi;b:ch;c:dj;d:eg;e:fk;f:m;g:h;i:j;j:k;k:l;l:m")));

  /* Lemma 6.2: 5-cycle with three vertices of degree three, w_1=w_2 or w_1=w_3.  */
  if (!graph (string ("a:bik;b:ch;c:dk;d:el;e:f;f:g;g:hl;h:i;i:j;j:lk")).colorable ()
      || !graph (string ("a:bim;b:ch;c:dk;d:el;e:f;f:g;g:hl;h:i;i:j;j:lk;k:m")).colorable ()
      || !graph (string ("a:mik;b:chm;c:dk;d:el;e:f;f:g;g:hl;h:i;i:j;j:lk")).colorable ())
    abort ();

  /* Lemma 6.2: 5-cycle with three vertices of degree three, at least one of w_1,w_2,w_3
     has degree two.  */
  graph g2 (string ("a:de;b:ef;c:df;d:g;e:h;f:i;g:hk;h:i;i:j;j:k;a1b1c1"));
  if (!all_ns_extend (&g2, vector<int>{0,1,2}, 1))
    abort ();

  /* Lemma 6.2: The same configuration, w_1, w_2, w_3 have degree three; reducibility with
     a reducent.  See also two2_6cycle_obstacles for graphs arising from the condition (iv).  */
  int a1 = g2.add_vertex (vector<int>{0}, 3);
  int b1 = g2.add_vertex (vector<int>{1}, 3);
  int c1 = g2.add_vertex (vector<int>{2}, 3);
  graph g2a (g2);
  if (!g2a.all_precolorings_extend (vector<int>{a1,b1,c1}, none, addits{pacu_le (vector<int>{0,1,2},9)}))
    abort ();

  /* Lemma 6.3: 5-cycle with two vertices of degree three, replacing an edge in a subdivided K_4.
     We use twice subdivided T with two nails as a reducent if both ends of the edge have degree
     three.  */
  graph sk4 (string("a:bde;b:ch;c:df;d:g;e:f;g:h;"));
  int es[2][2] = {{0,1},{0,4}};
  for (int i = 0; i < 2; i++)
    {
      graph sk4m (sk4);
      int l = es[i][0];
      int b = es[i][1];
      sk4m.delete_edge (l, b);

      for (int x = 0; x < sk4m.nvs (); x++)
	if (sk4m.total_degree[x] == 2)
	  for (int y = x + 1; y < sk4m.nvs (); y++)
	    if (sk4m.total_degree[y] == 2)
	      {
		graph ga (sk4m);
		ga.total_degree[x] = 3;
		ga.total_degree[y] = 3;
		int k = ga.nvs ();

		graph gaa (ga);
		gaa.add_path (l, b, vecset{true, true});
		gaa.add_path (k, k+1, 3);
		int z = k + 2;
		gaa.total_degree[z] = 3;
		if (!all_ns_extend (&gaa, vector<int>{x,y,z}, 0, 10 + i))
		  {
		    printf ("%c %c %c %s\n", 'a' + x, 'a' + y, 'a' + z, gaa.code ().c_str ());
		    abort ();
		  }
		gaa.total_degree[z] = 2;

		z = k + 4;
		gaa.total_degree[z] = 3;
		if (!all_ns_extend (&gaa, vector<int>{x,y,z}, 0, 10 + i))
		  {
		    printf ("%c %c %c %s\n", 'a' + x, 'a' + y, 'a' + z, gaa.code ().c_str ());
		    abort ();
		  }

		ga.add_path (l, b, vecset{true,true,true});
		ga.add_path (k, k+2, 2);
		z = k + 1;
		if (!all_ns_extend (&ga, vector<int>{x,y,z}, 0, 10 + i))
		  {
		    printf ("%c %c %c %s\n", 'a' + x, 'a' + y, 'a' + z, ga.code ().c_str ());
		    abort ();
		  }
	      }
    }

  /* Lemma 6.3: The condition (iv) for the previous case; G'' is necessarily necessarily K_4^+.  */
  graph two2k4 (string ("a:dj;b:ck;c:m;d:e;e:i;f:gj;g:h;h:ik;i:j;k:l;l:m;a1b1c1"));
  for (int t = 0; t < 2; t++)
    for (int x = 3; x < 7; x++)
      for (int y = x + 1; y < 7; y++)
	for (int i = 0; i < 3; i++)
	  {
	    graph *ng = new graph (two2k4);
	    ng->total_degree[x] = 3;
	    ng->total_degree[y] = 3;
	    ng->add_edge (0, t + 1);
	    int out[3] = {2 - t, x, y};
	    ng->add_two2 (out[i], out[(i + 1) % 3], out[(i + 2) % 3]);
	    generate_from (ng);
	  }

  /* Lemma 6.6, the graph from the case j=3.  */
  if (!graph (string ("a:bek;b:cg;c:dl;d:e;f:gjk;g:h;h:il;i:j;k:l")).colorable ())
    abort ();

  /* Lemma 6.6, reducibility of C + F, with a reducent.  */
  graph c5wf (string ("a:e;b:d;c:dg;d:e;e:f;f:g;a2b2c1"));
  for (int i = 0; i < 3; i++)
    {
      graph c5wfa (c5wf);
      int w1 = c5wf.nvs ();
      int w2 = w1 + 1;
      c5wfa.expand_till (w2);
      c5wfa.total_degree[w1] = c5wfa.total_degree[w2] = 3;
      int out[] = {2,w1,w2};
      c5wfa.add_two2 (out[i], out[(i+1) % 3], out[(i+2) % 3]);
      if (!c5wfa.all_precolorings_extend (vector<int>{0, 1, w1, w2}, none, addits{paci_le (0, 1, 0), paci_le (2, 3, 3)}))
	abort ();
    }

  /* Lemma 6.6, case F_1=G'': three C_5's with three nailed vertices, plus one vertex linking them.  */
  graph threec5 (string ("a:d;b:cf;c:d;d:e;e:f;g:hk;h:i;i:j;j:k;l:mp;m:n;n:o;o:p;a2b1c1g1h1i1l1m1n1"));
  for (int atl = 6; atl <= 8; atl++)
    for (int bt = 6; bt <= 8; bt++)
      {
	if (atl == bt)
	  continue;
	int lj = 21 - atl - bt;

	for (int atr = 11; atr <= 13; atr++)
	  for (int ct = 11; ct <= 13; ct++)
	    {
	      if (atr == ct)
		continue;
	      int rj = 36 - atr - ct;

	      graph ng (threec5);
	      ng.add_edge (0, atl);
	      ng.add_edge (0, atr);
	      ng.add_edge (1, bt);
	      ng.add_edge (2, ct);
	      ng.add_edge (lj, rj);

	      if (!ng.colorable ())
		abort ();
	    }
      }

  /* Lemma 7.1: 4-cycle adjacent to at least three vertices of degree two.  */
  graph c4 (vecset{true,true,true,true});
  if (!all_ns_extend (&c4, vector<int>{0,1,2,3}, 3))
    abort ();

  /* Lemma 7.1: 4-cycle adjacent to opposite vertices of degree two.  */
  int u1p = c4.add_vertex (vector<int>{0}, 2);
  int u1 = c4.add_vertex (vector<int>{u1p}, 3);
  int u2 = c4.add_vertex (vector<int>{1}, 3);
  int u3p = c4.add_vertex (vector<int>{2}, 2);
  int u3 = c4.add_vertex (vector<int>{u3p}, 3);
  int u4 = c4.add_vertex (vector<int>{3}, 3);
  if (!c4.all_precolorings_extend (vector<int>{u1,u2,u3,u4}, none, addits{}))
    abort ();

  /* Lemma 7.2: Graph arising from the identification of both pairs of antipodal vertices.  */
  generate_from (new graph (string ("a:bde;b:ch;c:dg;d:f;e:fg;f:h")));

  /* Lemma 7.2: Reducibility in the case u'_1=u_3.  */
  if (!graph (string ("a:d;b:i;c:j;d:eg;e:fh;f:gi;g:j;j:h;a2b2c2")).all_precolorings_extend (vector<int>{0,1,2}, none, addits{paci_le (0, 1, 3)}))
    abort ();

  /* Lemma 7.2: The case the general reduction results in K_4^+.  */
  graph c4r2 (string("a:h;b:i;c:j;d:ehm;e:fj;f:hk;g:ilm;i:o;k:l;l:n;m:n;n:o;a2b2c2"));
  if (!c4r2.all_precolorings_extend (vector<int>{0,1,2}, none, addits{}))
    abort ();

  /* Lemma 7.3: 4-cycle adjacent to a vertex of degree two, replaced by a reducent.  See
     also add_edge_obstacles for the graphs arising from the condition (iv).  */
  graph c4a2 (string("a:e;b:f;c:g;d:i;e:fh;f:g;g:h;h:i;a2b2c2d2"));
  if (!c4a2.all_precolorings_extend (vector<int>{0,1,2,3}, none, addits{paci_le (0,1,2),paci_le(1,2,3),pacu_le (vector<int>{0,2,3},10)}))
    abort ();

  /* Lemma 8.3: Reducibility with a reducent.  See also add_deg2_sym5c_obstacles
     for the graphs arising from the condition (iv).  */
  graph deg2sym1 (string ("a:e;b:g;c:l;d:j;e:fi;f:g;g:h;h:il;i:j;j:k;k:l;a2b2c2d2"));
  if (!deg2sym1.all_precolorings_extend (vector<int>{0,1,2,3}, none, addits{pacu_le (vector<int>{0,1,2,3}, 10)}))
    abort ();

  /* Lemma 8.4: Colorability if the subgraph is not induced.  */
  if (!graph (string ("a:bef;b:c;c:dh;d:ej;e:i;f:gj;g:h;h:i;i:j")).colorable ()
      || !graph (string ("a:bef;b:c;c:dh;d:ek;e:i;f:gj;g:h;h:i;i:j;j:k")).colorable ())
    abort ();

  /* Lemma 8.4: Colorability if a vertex of degree two has both neighbors in the configuration.  */
  if (!graph (string ("a:bef;b:c;c:dh;d:ek;e:l;f:gj;g:h;h:i;i:jk;j:l")).colorable ()
      || !graph (string ("a:bef;b:c;c:dh;d:ek;e:l;f:gj;g:h;h:i;i:jl;j:k")).colorable ())
    abort ();

  /* Lemma 8.4: Reducibility if a neighbor has degree two.  */
  graph deg2sym2_hex (string ("a:be;b:g;c:dh;d:j;e:fj;f:g;g:h;h:i;i:j;a1b1c1d1"));
  if (!all_ns_extend (&deg2sym2_hex, vector<int>{0,1,2,3}, 1))
    abort ();

  /* Lemma 8.4: Reducibility with a reducent.  */
  graph deg2sym2_hexe (string ("a:k;b:l;c:m;d:n;e:fjk;f:g;g:hl;h:im;i:j;j:n;k:l;m:n;a2b2c2d2"));
  if (!deg2sym2_hexe.all_precolorings_extend (vector<int>{0,1,2,3}, none, addits{paci_le (0,1,2), paci_le (2,3,3)}))
    abort ();

  /* Lemma 8.5: Reducibility in the case u_{1,1}u_{2,1} is in C_2, u_{1,2} and w_5
     have a common neighbor of degree two.  */
  graph deg2ns1 (string ("a:di;b:gj;c:eh;d:e;e:f;f:gi;g:h;i:j;a1b1c1"));
  if (!all_ns_extend (&deg2ns1, vector<int>{0,1,2}, 0))
    abort ();

  /* Lemma 8.5: The graph from the case u_{1,1}u_{2,1} is in C_2.  */
  if (!graph (string ("a:bek;b:cj;c:d;d:eh;e:f;f:gj;g:h;h:i;i:jk")).colorable ())
    abort ();

  /* Lemma 8.5: The graph from the case the neighbors of v_1 and v_2 in C_2
     are non-adjacent.  */
  if (!graph (string ("a:bek;b:cj;c:dh;d:e;e:f;f:gj;g:hk;h:i;i:j")).colorable ())
    abort ();

  /* Lemma 9.1: Configurations arising from a 4-cycle with three neighbors in a 5-cycle.  */
  graph c4s (string("a:i;c:l;d:el;f:ek;g:hi;h:j;i:j;j:k;k:l;a2b3c2d1e1f1g1h1"));
  int c4sin[3] = {1, 6, 7};
  for (int i = 0; i < 3; i++)
    for (int j = 0; j < 3; j++)
      {
	if (i == j)
	  continue;

	graph c4m (c4s);
	c4m.add_edge (3, c4sin[i]);
	c4m.add_edge (4, c4sin[j]);
	c4m.add_edge (5, c4sin[3 - i - j]);
	addits acs;
	aci_le bc(1,2,3);
	if (c4sin[i] == 1)
	  acs.push_back (&bc);
	if (!c4m.all_precolorings_extend (vector<int>{0,1,2}, none, acs))
	  abort ();
      }

  /* Lemma 10.2, the first case, subcase v'=z_2, z_3=u'_2.  */
  if (!graph (string ("a:bej;b:cl;c:dh;d:ge;e:f;f:il;g:ik;h:ij;j:k;k:l")).colorable ())
    abort ();

  /* Lemma 10.2, the first case, subcase v'=z_2, reducibility and the situation where the reducent
     would create a triangle.  */
  graph c5con (string("a:o;b:j;c:l;d:p;e:fio;f:gp;g:hl;h:ik;i:j;j:m;k:mn;l:m;n:op;a2b2c2d2"));
  if (!c5con.all_precolorings_extend (vector<int>{0, 1, 2, 3}, none, addits{paci_le (0,1,3)}))
    abort ();
  generate_from (new graph (string("a:djc;c:lb;e:fid;f:gb;g:hl;h:ik;i:j;j:m;k:mn;l:m;n:db;")));

  /* Lemma 10.2, the first case, subcase v'=u_3, reducibility.  */
  graph c5cn (string("a:e;b:j;c:l;d:n;e:fi;f:gn;g:hl;h:ik;i:j;j:m;k:mn;l:m;a2b2c2d2"));
  if (!c5cn.all_precolorings_extend (vector<int>{0, 1, 2, 3}, none, addits{}))
    abort ();

  /* Lemma 10.2, the second case, subcase v'=z_2, {v_1,v_3,w_1,w_4} induces a perfect matching.  */
  graph c52noi (string ("a:ej;b:ek;c:gn;d:gm;e:f;f:gh;h:il;i:jn;j:k;k:l;l:m;m:n;a1b1c1d1"));
  for (int i = 0; i < 2; i++)
    {
      graph *ng = new graph (c52noi);
      ng->add_edge (0, 2 + i);
      ng->add_edge (1, 3 - i);
      generate_from (ng);
    }

  /* Lemma 10.2, the second case, subcase v'=z_2, reducibility.  */
  vector<int> c52noib;
  for (int i = 0; i < 4; i++)
    c52noib.push_back (c52noi.add_vertex (vector<int>{i}, 3));
  if (!c52noi.all_precolorings_extend (c52noib, none, addits {}))
    abort ();

  /* Lemma 10.2, the second case, subcase v'=u'_4, {v_1,v_3,y_1,y_2} induces a perfect matching.  */
  graph c52noz (string ("a:ln;b:mn;c:ej;d:ei;e:f;f:gm;g:hk;h:in;i:j;j:k;k:l;l:m;a1b1c1d1"));
  for (int i = 0; i < 2; i++)
    {
      graph *ng = new graph (c52noz);
      ng->add_edge (0, 2 + i);
      ng->add_edge (1, 3 - i);
      generate_from (ng);
    }

  /* Lemma 10.2, the second case, subcase v'=z_2, reducibility.  */
  vector<int> c52nozb;
  for (int i = 0; i < 4; i++)
    c52nozb.push_back (c52noz.add_vertex (vector<int>{i}, 3));
  if (!c52noz.all_precolorings_extend (c52nozb, none, addits {}))
    abort ();

  int stat[3][30];
  int n1 = 0;
  for (int n = 0; n <= 2; n++)
    for (int d2 = 0; d2 < 30; d2++)
      stat[n][d2] = 0;
  int md2 = 0;
  for (graph *g1 : obstacles)
    {
      int n = g1->nails ();
      if (n == 1 && !g1->is_cycle ())
	n1++;

      int d2 = -n;
      for (int v = 0; v < g1->nvs (); v++)
	if (g1->degree (v) == 2)
	  d2++;

      stat[n][d2]++;
      if (d2 > md2)
	md2 = d2;
    }
  fprintf (stderr, "%d obstacles in total, %d non-cycle with 1 nail.\n", (int) obstacles.size (), n1);
  for (int n = 0; n <= 2; n++)
    {
      for (int d2 = 0; d2 <= md2; d2++)
	fprintf (stderr, "\t%d", stat[n][d2]);
      fprintf (stderr, "\n");
    }

  /* Lemma 8.2, the case adding a adjacent to u_{1,2} and u_{2,2} results in an obstruction.  */
  int id = 0;
  for (graph *g1 : obstacles)
    {
      if (g1->nails () != 1 || g1->is_cycle ())
	continue;
      id++;
      fprintf (stderr, "Combining eligible obstacle %d/%d\n", id, n1);
      
      for (graph *g2 : obstacles)
	if (g2->nails () == 1 && !g2->is_cycle ())
	  test_obstacle_combinations (g1, g2);
    }

  fprintf (stderr, "Proof verified!\n");

  return 0;
}