// Enumeration of zero-sum incidence matrices. NUM_COLS and REMAINDER_H
// specify the number of columns and the remainder size, respectively.
// Row multiplicities (kappa,r) are supplied by the accompanying exhaustive generator.
// All pruning uses necessary conditions, enumerated explicitly in the paper.
#include <algorithm>
#include <array>
#include <bitset>
#include <chrono>
#include <fstream>
#include <functional>
#include <iostream>
#include <stdexcept>
#include <string>
#include <utility>
#include <vector>
#include <boost/rational.hpp>
#include <boost/multiprecision/cpp_int.hpp>
using namespace std;
using Rat=boost::rational<boost::multiprecision::cpp_int>;
#ifndef NUM_COLS
#define NUM_COLS 10
#endif
#ifndef REMAINDER_H
#define REMAINDER_H 6
#endif
constexpr int N=NUM_COLS,H=REMAINDER_H,MAXT=21;
using Mask=bitset<512>;
using OMask=bitset<128>;
using Big=boost::multiprecision::cpp_int;
ofstream certificates;
Big gcdBig(Big a,Big b){
    if(a<0)a=-a;
    if(b<0)b=-b;
    while(b!=0){
        Big c=a%b;
        a=b;
        b=c;
    }
    return a;
}
pair<vector<Big>,Big> integralize(vector<Rat> const& v){
    Big den=1;
    for(auto &x:v)den=den/gcdBig(den,x.denominator())*x.denominator();
    vector<Big>w;
    for(auto &x:v)w.push_back(x.numerator()*(den/x.denominator()));
    return {
        w,den
    };
}
void writeInts(ostream& os,vector<Big> const& v){
    os<<"[";
    for(size_t j=0;j<v.size();j++){
        if(j)os<<",";
        os<<"\""<<v[j]<<"\"";
    }
    os<<"]";
}
int pairidx[N][N];
struct Candidate {
    array<unsigned char,N> v{};
    Mask cover{};
    OMask overlap{};
    bool pure=false;
};
struct RowTask {
    int K,R;
    vector<Candidate> choices;
    int maxcover=0;
};
long long nodes=0,leaves=0,coef=0,rankbad=0,eqbad=0,found=0,endpoint_pass=0,inconsistent=0,boundsbad=0;
int cases=0;
int rr(vector<vector<Rat>>&a,int n,vector<int>&piv){
    int i=0;
    piv.clear();
    for(int j=0;j<n&&i<(int)a.size();j++){
        int q=i;
        while(q<(int)a.size()&&a[q][j]==0)q++;
        if(q==(int)a.size())continue;
        swap(a[i],a[q]);
        Rat z=a[i][j];
        for(int l=j;l<(int)a[i].size();l++)a[i][l]/=z;
        for(int k=0;k<(int)a.size();k++)if(k!=i&&a[k][j]!=0){
            Rat z=a[k][j];
            for(int l=j;l<(int)a[k].size();l++)a[k][l]-=z*a[i][l];
        }
        piv.push_back(j);
        i++;
    }
    return i;
}
struct Solver {
    int t,d,p1,p2,c,case_id=-1;
    vector<pair<int,int>> row_data;
    vector<RowTask> tasks;
    vector<array<unsigned char,N>> P;
    vector<int>K;
    array<int,N>cap{};
    vector<int> chosen;
    Mask target{};
    vector<vector<int>> subsets;
    int pureUsed=0;
    long long ns=0,ls=0,cs=0,es=0;
    array<int,MAXT> successor{},predecessor{};
    int zeroRow=-1;
    bool endpoint_ok(){
        vector<int>head(t,-1);
        int pureRow=-1;
        for(int u=0;u<t;u++)for(int j=0;j<N;j++)if(P[u][j]==3)pureRow=u;
        vector<int>next(t,-1);
        for(int j=0;j<N;j++){
            int a=-1,b=-1;
            for(int u=0;u<t;u++){
                if(P[u][j]==2)a=u;
                else if(P[u][j]==1)b=u;
            }
            if(a>=0){
                if(b<0||head[b]>=0||a==pureRow||b==pureRow)return false;
                head[b]=a;
                next[a]=b;
            }
        }
        for(int u=0;u<t;u++){
            int x=u;
            for(int q=0;q<t;q++){
                x=next[x];
                if(x<0)break;
                if(x==u)return false;
            }
        }
        return true;
    }
    void baseCertificate(string const& type){
        if(!certificates)return;
        certificates<<"{\"case_id\":"<<case_id<<",\"k\":"<<N<<",\"h\":"<<H<<",\"type\":\""<<type<<"\",\"P\":[";
        for(int u=0;u<t;u++){
            if(u)certificates<<",";
            certificates<<"[";
            for(int j=0;j<N;j++){
                if(j)certificates<<",";
                certificates<<(int)P[u][j];
            }
            certificates<<"]";
        }
        certificates<<"],\"kappa\":[";
        for(int u=0;u<t;u++){
            if(u)certificates<<",";
            certificates<<K[u];
        }
        certificates<<"]";
    }
    void finishCertificate(){
        if(certificates)certificates<<"}\n";
    }
    void check(){
        leaves++;
        ls++;
        if(!endpoint_ok())return;
        endpoint_pass++;
        // The identity block records exact elementary row operations.
        vector<vector<Rat>>a(t,vector<Rat>(N+1+t));
        for(int u=0;u<t;u++){
            for(int j=0;j<N;j++)a[u][j]=P[u][j];
            a[u][N]=K[u];
            a[u][N+1+u]=1;
        }
        vector<int>pv;
        int rk=rr(a,N,pv);
        if(rk<N){
            rankbad++;
            vector<bool>used(N,false);
            for(int j:pv)used[j]=true;
            int f=0;
            while(used[f])f++;
            vector<Rat>z(N);
            z[f]=1;
            for(int u=0;u<rk;u++)z[pv[u]]=-a[u][f];
            auto [w,den]=integralize(z);
            baseCertificate("rank_deficient");
            if(certificates){
                certificates<<",\"z\":";
                writeInts(certificates,w);
            }
            finishCertificate();
            return;
        }
        for(int u=N;u<t;u++)if(a[u][N]!=0){
            inconsistent++;
            vector<Rat>y(t);
            for(int v=0;v<t;v++)y[v]=a[u][N+1+v];
            auto[w,den]=integralize(y);
            baseCertificate("inconsistent");
            if(certificates){
                certificates<<",\"y\":";
                writeInts(certificates,w);
            }
            finishCertificate();
            return;
        }
        vector<Rat>mu(N);
        for(int j=0;j<N;j++)mu[j]=a[j][N];
        for(int j=0;j<N;j++)if(!(mu[j]>0&&mu[j]<1)){
            boundsbad++;
            baseCertificate("coefficient_bounds");
            if(certificates){
                certificates<<",\"mu\":[";
                for(int l=0;l<N;l++){
                    if(l)certificates<<",";
                    certificates<<"\""<<mu[l].numerator()<<"/"<<mu[l].denominator()<<"\"";
                }
                certificates<<"],\"left_rows\":[";
                vector<Big>ds;
                for(int u=0;u<N;u++){
                    vector<Rat>r(t);
                    for(int v=0;v<t;v++)r[v]=a[u][N+1+v];
                    auto[w,den]=integralize(r);
                    if(u)certificates<<",";
                    writeInts(certificates,w);
                    ds.push_back(den);
                }
                certificates<<"],\"diagonal\":";
                writeInts(certificates,ds);
            }
            finishCertificate();
            return;
        }
        coef++;
        cs++;
        vector<vector<Rat>>b(N,vector<Rat>(t));
        for(int j=0;j<N;j++)for(int u=0;u<t;u++)b[j][u]=P[u][j];
        vector<int>qv;
        int br=rr(b,t,qv);
        if(br!=N)abort();
        vector<bool>isp(t,false);
        for(int u:qv)isp[u]=true;
        vector<int>free;
        for(int u=0;u<t;u++)if(!isp[u])free.push_back(u);
        vector<vector<Rat>>sig(t,vector<Rat>(free.size()));
        for(int q=0;q<(int)free.size();q++){
            sig[free[q]][q]=1;
            for(int j=0;j<N;j++)sig[qv[j]][q]=-b[j][free[q]];
        }
        for(int u=0;u<t;u++)for(int v=u+1;v<t;v++)if(sig[u]==sig[v]){
            eqbad++;
            es++;
            vector<Rat>z(N);
            for(int j=0;j<N;j++)z[j]=a[j][N+1+u]-a[j][N+1+v];
            auto[w,den]=integralize(z);
            baseCertificate("forced_equality");
            if(certificates){
                certificates<<",\"pair\":["<<u<<","<<v<<"],\"z\":";
                writeInts(certificates,w);
                certificates<<",\"scale\":\""<<den<<"\"";
            }
            finishCertificate();
            return;
        }
        found++;
        baseCertificate("accepted");
        finishCertificate();
        if(certificates)certificates.flush();
        cerr<<"FOUND k="<<N<<" h="<<H<<" t="<<t<<" d="<<d<<" p1="<<p1<<" p2="<<p2<<"\n";
        for(int u=0;u<t;u++){
            cerr<<K[u]<<" : ";
            for(int j=0;j<N;j++)cerr<<(int)P[u][j]<<",";
            cerr<<"\n";
        }
        exit(2);
    }
    vector<Candidate> make(int K,int R){
        vector<Candidate> out;
        array<unsigned char,N>v{};
        function<void(int,int,int,int,int)>rec=[&](int j,int rem,int twos,int threes,int ends){
            if(j==N){
                if(rem)return;
                int supp=0;
                for(auto x:v)supp+=x>0;
                if(supp<=1)return;
                Candidate q;
                q.v=v;
                q.pure=threes;
                for(int i=0;i<N;i++)for(int l=i+1;l<N;l++){
                    if(v[i]&&v[l])q.overlap.set(pairidx[i][l]);
                }
                for(int a=0;a<(int)subsets.size();a++){
                    int z=0;
                    for(int j:subsets[a])z+=v[j];
                    if(z>R)q.cover.set(a);
                }
                out.push_back(q);
                return;
            }
            int mx=min(rem,j<d?1:(j<c?0:3));
            for(int x=0;x<=mx;x++){
                int nt=twos+(x==2),np=threes+(x==3),ne=ends+(j<d&&x>0);
                if(nt>1||np+pureUsed>1||ne>1||(nt&&np))continue;
                v[j]=x;
                rec(j+1,rem-x,nt,np,ne);
            }
            v[j]=0;
        };
        rec(0,K+R,0,0,0);
        sort(out.begin(),out.end(),[](auto&a,auto&b){
            int x=a.cover.count(),y=b.cover.count();if(x!=y)return x>y;return a.v<b.v;
        });
        return out;
    }  // A completed repeated column gives a directed relation beta_head=-2 beta_tail.
    // Checking already completed columns cannot discard an admissible completion.
    bool stage_edges(Candidate const&q,vector<pair<int,int>>&added,int proposedZero){
        int current=P.size();
        for(int j=0;j<N;j++)if(q.v[j]>0&&q.v[j]==cap[j]){
            int a=-1,b=-1;
            if(q.v[j]==2){
                a=current;
                for(int u=0;u<current;u++)if(P[u][j]==1)b=u;
            }
            else if(q.v[j]==1){
                b=current;
                for(int u=0;u<current;u++)if(P[u][j]==2)a=u;
            }
            if(a<0)continue;
            if(b<0||a==proposedZero||b==proposedZero||successor[a]>=0||predecessor[b]>=0)return false;
            int x=b;
            while(x>=0){
                if(x==a)return false;
                x=successor[x];
            }
            successor[a]=b;
            predecessor[b]=a;
            added.emplace_back(a,b);
        }
        return true;
    }
    void unstage(vector<pair<int,int>> const& added){
        for(auto[a,b]:added){
            successor[a]=-1;
            predecessor[b]=-1;
        }
    }
    void dfs(int at,Mask covered,OMask overlap,int pure){
        nodes++;
        ns++;
        if(at==(int)tasks.size()){
            for(int x:cap)if(x)return;
            if((covered&target)==target)check();
            return;
        }
        Mask missing=target&~covered;
        int need=missing.count(),upper=0;
        for(int a=at;a<(int)tasks.size();a++)upper+=tasks[a].maxcover;
        if(need>upper)return;
        auto&T=tasks[at];
        int start=0;
        if(at&&T.K==tasks[at-1].K&&T.R==tasks[at-1].R)start=chosen[at-1];
        for(int ci=start;ci<(int)T.choices.size();ci++){
            auto&q=T.choices[ci];
            if((q.overlap&overlap).any())continue;
            if(q.pure&&pure)continue;
            bool ok=true;
            for(int j=0;j<N;j++)if(q.v[j]>cap[j]){
                ok=false;
                break;
            }
            if(!ok)continue;
            // Prefix lexicographic order among otherwise interchangeable normal columns.
            for(int j=c;j+1<N;j++){
                bool same=true;
                for(auto &r:P)if(r[j]!=r[j+1]){
                    same=false;
                    break;
                }
                if(same&&q.v[j]>q.v[j+1]){
                    ok=false;
                    break;
                }
            }
            if(!ok)continue;
            vector<pair<int,int>>added;
            int previousZero=zeroRow;
            int proposedZero=q.pure?(int)P.size():zeroRow;
            if(!stage_edges(q,added,proposedZero)){
                unstage(added);
                continue;
            }
            zeroRow=proposedZero;
            for(int j=0;j<N;j++)cap[j]-=q.v[j];
            P.push_back(q.v);
            K.push_back(T.K);
            chosen[at]=ci;
            dfs(at+1,covered|q.cover,overlap|q.overlap,pure||q.pure);
            K.pop_back();
            P.pop_back();
            for(int j=0;j<N;j++)cap[j]+=q.v[j];
            unstage(added);
            zeroRow=previousZero;
        }
    }
    void run(){
        c=d+p1+p2;
        // For unit complementary rows, a pair selected from each nonprivate row
        // gives a graph of independence number at most H-4. Turan's theorem applies.
        bool unit=(p2==0);
        for(auto [a,b]:row_data)if(a!=1)unit=false;
        if(unit){
            int n=N-c,q=H-4,edges=0;
            for(int j=0;j<q;j++){
                int z=n/q+(j<n%q);
                edges+=z*(z-1)/2;
            }
            if(c+d+edges>t)return;
        }
        successor.fill(-1);
        predecessor.fill(-1);
        zeroRow=(p1+p2)?d:-1;
        cap.fill(3);
        pureUsed=p1+p2;
        P.clear();
        K.clear();
        for(int j=0;j<d;j++){
            array<unsigned char,N>v{};
            v[j]=2;
            P.push_back(v);
            K.push_back(1);
            cap[j]=1;
        }
        if(pureUsed){
            array<unsigned char,N>v{};
            v[d]=3;
            P.push_back(v);
            K.push_back(p1?1:2);
            cap[d]=0;
        }
        vector<int> cur;
        function<void(int)> comb=[&](int j){
            if((int)cur.size()==H-3){
                subsets.push_back(cur);
                return;
            }
            for(int l=j;l<N;l++){
                cur.push_back(l);
                comb(l+1);
                cur.pop_back();
            }
        };
        comb(c);
        if(subsets.size()>512)throw runtime_error("mask too short");
        for(int i=0;i<(int)subsets.size();i++)target.set(i);
        for(auto[K,R]:row_data){
            RowTask a;
            a.K=K;
            a.R=R;
            a.choices=make(K,R);
            for(auto&q:a.choices)a.maxcover=max(a.maxcover,(int)q.cover.count());
            tasks.push_back(move(a));
        }
        sort(tasks.begin(),tasks.end(),[](auto&a,auto&b){
            if(a.maxcover!=b.maxcover)return a.maxcover>b.maxcover;if(a.K!=b.K)return a.K>b.K;return a.R<b.R;
        });
        chosen.resize(tasks.size());
        dfs(0,0,0,pureUsed);
    }
};
int main(int argc,char**argv){
    if(argc<2){
        cerr<<"usage: executable CASES [SHARD SHARDS [CERTIFICATES.jsonl]]\n";
        return 3;
    }
    if(N*(N-1)/2>128)throw runtime_error("overlap mask too short");
    if(argc>4){
        certificates.open(argv[4]);
        if(!certificates)throw runtime_error("cannot open certificate output");
    }
    int q=0;
    for(int i=0;i<N;i++)for(int j=i+1;j<N;j++)pairidx[i][j]=q++;
    string file=argv[1];
    int part=argc>2?stoi(argv[2]):0,parts=argc>3?stoi(argv[3]):1;
    ifstream in(file);
    int id,t,d,p1,p2;
    while(in>>id>>t>>d>>p1>>p2){
        vector<pair<int,int>>row_data;
        for(int j=0;j<t-d-p1-p2;j++){
            int a,b;
            in>>a>>b;
            row_data.emplace_back(a,b);
        }
        if(id%parts!=part)continue;
        Solver s;
        s.case_id=id;
        s.t=t;
        s.d=d;
        s.p1=p1;
        s.p2=p2;
        s.row_data=row_data;
        auto tm=chrono::steady_clock::now();
        s.run();
        cases++;
        cout<<"case="<<id<<" t="<<t<<" d="<<d<<" p1="<<p1<<" p2="<<p2<<" nodes="<<s.ns<<" leaves="<<s.ls<<" coeff="<<s.cs<<" equal="<<s.es<<" seconds="<<chrono::duration<double>(chrono::steady_clock::now()-tm).count()<<"\n";
        cout.flush();
    }
    if(!in.eof())throw runtime_error("malformed case file");
    if(certificates.is_open()){
        certificates.flush();
        if(!certificates)throw runtime_error("certificate write failed");
    }
    cout<<"COMPLETE cases="<<cases<<" nodes="<<nodes<<" leaves="<<leaves<<" coeff="<<coef<<" endpoint_pass="<<endpoint_pass<<" inconsistent="<<inconsistent<<" boundsbad="<<boundsbad<<" rankbad="<<rankbad<<" equal="<<eqbad<<" found="<<found<<"\n";
}