{
  "audit": {
    "certificate_verified": true,
    "classes": 6,
    "max_witness_length": 2,
    "refinement_rounds": 2,
    "shared_classes": 0,
    "shared_ids": [],
    "source_pins": {
      "A": "dfc27584ce2be2211cdfd831b4838b6670f6bb60ec5d503f4301430cd73acde9",
      "B": "e44f80809b810ead218db729f771c4a382d7acd4c587dc70b711520757d24ae7"
    },
    "source_states": 12,
    "witness_count": 15
  },
  "cycle_obstruction": {
    "certificate_verified": true,
    "classes": 2,
    "max_witness_length": 0,
    "refinement_rounds": 0,
    "shared_classes": 2,
    "shared_ids": [
      "C000",
      "C001"
    ],
    "source_pins": {
      "A": "ec47a9d05342517ef76f988050ababec9038fefc4c11d4cfec11ac4e71ee1fbf",
      "B": "3c48fa39c8d20488f5f76f5586636fc724b2dffab50bd6f6f74ab299cc59ee52"
    },
    "source_states": 6,
    "witness_count": 1
  },
  "exact_audit": {
    "certificate_verified": true,
    "classes": 12,
    "max_witness_length": 2,
    "refinement_rounds": 2,
    "shared_classes": 0,
    "shared_ids": [],
    "source_pins": {
      "A": "b2aa9648e6b9f18bfeae88d05484f206923a9602a7ba5dec858a479a6863b80c",
      "B": "278ffd1851d52ed606a3a23f27eefde85e698f1b1c0f585d87179b4ca6a5104a"
    },
    "source_states": 12,
    "witness_count": 66
  },
  "exact_value": {
    "certificate_verified": true,
    "classes": 4,
    "max_witness_length": 0,
    "refinement_rounds": 0,
    "shared_classes": 4,
    "shared_ids": [
      "C000",
      "C001",
      "C002",
      "C003"
    ],
    "source_pins": {
      "A": "1d395e8679446a0e2369ee7c0b076c8f5b40c40874e0634eacf8e227008e222e",
      "B": "814fa4d81335de527c5426212a7f13efab2542555f549aa4f0e8b5c228b3c39b"
    },
    "source_states": 12,
    "witness_count": 6
  },
  "parity": {
    "certificate_verified": true,
    "classes": 2,
    "max_witness_length": 0,
    "refinement_rounds": 0,
    "shared_classes": 2,
    "shared_ids": [
      "C000",
      "C001"
    ],
    "source_pins": {
      "A": "46f71cda2bdb36b9f6711acd88ba4636c1670f2be46b894bd991ed64bda89b07",
      "B": "8607270b075430718ed2350c9126b7eb8955aa6551a907a87bca5e9d39187c6b"
    },
    "source_states": 12,
    "witness_count": 1
  },
  "partial_overlap": {
    "certificate_verified": true,
    "classes": 4,
    "max_witness_length": 0,
    "refinement_rounds": 0,
    "shared_classes": 2,
    "shared_ids": [
      "C000",
      "C001"
    ],
    "source_pins": {
      "A": "545421221c6adcf844806dd5b557e3f7687029d70a92200abf323d7648d50f29",
      "B": "567c08f8462838b557eaa50c7391d9206970bfb38dbf3c3bbbdb05a34c594f36"
    },
    "source_states": 6,
    "witness_count": 6
  },
  "randomized": {
    "cross_system_pairs_checked": 2838,
    "disagreements": 0,
    "model_pairs": 180,
    "seed": 20261105,
    "state_pairs_checked": 5719,
    "total_states": 1437
  },
  "scope": "Finite typed partial deterministic systems, exact tagged observations only",
  "split_base": {
    "certificate_verified": true,
    "classes": 1,
    "max_witness_length": 0,
    "refinement_rounds": 0,
    "shared_classes": 1,
    "shared_ids": [
      "C000"
    ],
    "source_pins": {
      "A": "892021ffdaf125daafa222a0da6b38cb7700ad6b139612f75484b15d64b67a24",
      "B": "77992e7fe5bcc46d9cf0bcce14b7cd58966e54526e32d566a99efafb17795a04"
    },
    "source_states": 4,
    "witness_count": 0
  },
  "split_extended": {
    "certificate_verified": true,
    "classes": 2,
    "max_witness_length": 1,
    "refinement_rounds": 1,
    "shared_classes": 2,
    "shared_ids": [
      "C000",
      "C001"
    ],
    "source_pins": {
      "A": "ace303a28cdcf1787188e3de8cfb7c5c28e12d8ac9496ae810d4ba352778cf39",
      "B": "9af11cda9b7c85009d75605f90b997530b52342a08f3a421ee04ffa0dfe8d4ea"
    },
    "source_states": 4,
    "witness_count": 1
  },
  "undefined": {
    "certificate_verified": true,
    "classes": 2,
    "max_witness_length": 1,
    "refinement_rounds": 1,
    "shared_classes": 0,
    "shared_ids": [],
    "source_pins": {
      "A": "f3e84bb686958a662c6cb4ce4a3972844c10c3aea3733f6c6db3c6c1c22e0285",
      "B": "0ed003ab99009ef6b7a2899c7b6987f7fcf76964bd1aafc510f88b15485b7945"
    },
    "source_states": 2,
    "witness_count": 1
  }
}
