// Independent array-based backtracking checker. C++17, standard library only.
#include <array>
#include <vector>
#include <iostream>
#include <fstream>
#include <algorithm>
#include <numeric>
#include <chrono>
#include <stdexcept>
using namespace std;
using Quad=array<int,6>;
struct Search {
 vector<Quad> blocks;
 array<int,136> need{};
 unsigned long long nodes=0;
 vector<int> solution;
 bool dfs(const vector<int>& active,int remaining) {
  ++nodes;
  if(remaining==0)return true;
  array<int,136> counts{};
  for(int q:active)for(int p:blocks[q])++counts[p];
  int edge=-1,best=100000;
  for(int p=135;p>=0;--p)if(need[p]){
   if(counts[p]<need[p])return false;
   if(counts[p]<best){edge=p;best=counts[p];}
  }
  if(edge<0)throw runtime_error("inconsistent remaining");
  for(auto it=active.rbegin();it!=active.rend();++it){
   int q=*it;
   if(find(blocks[q].begin(),blocks[q].end(),edge)==blocks[q].end())continue;
   for(int p:blocks[q])--need[p];
   vector<int> next;
   for(int r:active){
    if(r==q)continue;
    bool ok=true;
    for(int p:blocks[r])if(need[p]==0){ok=false;break;}
    if(ok)next.push_back(r);
   }
   solution.push_back(q);
   if(dfs(next,remaining-6))return true;
   solution.pop_back();
   for(int p:blocks[q])++need[p];
  }
  return false;
 }
};
int main(int argc,char**argv){
 if(argc<2){cerr<<"usage: check_links graphs.txt [first last]\n";return 2;}
 ifstream in(argv[1]);int total;in>>total;int lo=argc>2?stoi(argv[2]):0,hi=argc>3?stoi(argv[3]):total;
 unsigned long long allnodes=0;int cases=0,sat=0;
 int pairid[17][17];int pcount=0;
 for(int i=0;i<17;i++)for(int j=i+1;j<17;j++)pairid[i][j]=pairid[j][i]=pcount++;
 for(int g=0;g<total;g++){
  array<unsigned,10> adj{};for(auto &a:adj)in>>a;
  if(g<lo||g>=hi)continue;
  vector<vector<int>> F(10);int index=0;
  for(int i=0;i<10;i++)for(int j=i+1;j<10;j++)if(adj[i]&(1u<<j)){F[i].push_back(index);F[j].push_back(index++);}
  if(index!=13)throw runtime_error("edge count");
  for(int i=0;i<10;i++)while(F[i].size()<3)F[i].push_back(index++);
  if(index!=17)throw runtime_error("stub count");
  int mats[3][4]={{13,14,15,16},{13,15,14,16},{13,16,14,15}};
  for(int m=0;m<3;m++){
   Search S;S.need.fill(1);
   for(auto T:F)for(int i=0;i<3;i++)for(int j=i+1;j<3;j++)--S.need[pairid[T[i]][T[j]]];
   for(int j=0;j<4;j+=2)++S.need[pairid[mats[m][j]][mats[m][j+1]]];
   int remaining=accumulate(S.need.begin(),S.need.end(),0);
   if(remaining!=108)throw runtime_error("demand sum");
   for(int a=0;a<17;a++)for(int b=a+1;b<17;b++)for(int c=b+1;c<17;c++)for(int d=c+1;d<17;d++){
    Quad Q={pairid[a][b],pairid[a][c],pairid[a][d],pairid[b][c],pairid[b][d],pairid[c][d]};
    if(all_of(Q.begin(),Q.end(),[&](int p){return S.need[p]>0;}))S.blocks.push_back(Q);
   }
   vector<int> active(S.blocks.size());iota(active.begin(),active.end(),0);
   bool yes=S.dfs(active,remaining);++cases;sat+=yes;allnodes+=S.nodes;
   cout<<g<<" "<<m<<" "<<(yes?"SAT":"UNSAT")<<" "<<S.nodes<<"\n";
   if(yes){cerr<<"Found SAT at "<<g<<" "<<m<<"\n";return 1;}
  }
 }
 cerr<<"COMPLETE cases="<<cases<<" sat="<<sat<<" nodes="<<allnodes<<"\n";
}