Upload folder using huggingface_hub (part 11)

.gitattributes

@@ -35,3 +35,5 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
 attempts/labelonly20_100_train.jsonl filter=lfs diff=lfs merge=lfs -text
 catalog.sqlite3 filter=lfs diff=lfs merge=lfs -text
+manifests/labelonly20_100_train.jsonl filter=lfs diff=lfs merge=lfs -text
+manifests/pilot20_train.jsonl filter=lfs diff=lfs merge=lfs -text

cores/pilot20_train/f2427631e5814ceec51423766becabf9dd0628a08ade46e95469dcadac9fa364.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f2427631e5814ceec51423766becabf9dd0628a08ade46e95469dcadac9fa364",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "bf99ee3d0468d9d68755cc61352e46c9fd4113374adb9812ce6196715e87c844",
+  "clause_indices_zero_based": [
+    0,
+    2,
+    3,
+    10,
+    16,
+    17,
+    19,
+    21,
+    22,
+    23,
+    27,
+    29,
+    33,
+    34,
+    35,
+    36,
+    40,
+    42,
+    45,
+    49,
+    50,
+    51,
+    52,
+    55,
+    56,
+    59,
+    63,
+    67,
+    68,
+    70,
+    71,
+    72,
+    75,
+    78,
+    79,
+    80,
+    82,
+    91
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f2465062b5e97c619dd13ef5776a25daa554ba89dd0c90e630cf146a40fa2660.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f2465062b5e97c619dd13ef5776a25daa554ba89dd0c90e630cf146a40fa2660",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "1fa156152613b4562d8503b6ce4cd843bf0586f0f009d3278f3771fe2db54718",
+  "clause_indices_zero_based": [
+    1,
+    7,
+    10,
+    14,
+    16,
+    20,
+    21,
+    22,
+    24,
+    30,
+    31,
+    39,
+    41,
+    42,
+    45,
+    46,
+    47,
+    48,
+    54,
+    57,
+    62,
+    64,
+    65,
+    66,
+    67,
+    69,
+    72,
+    73,
+    74,
+    75,
+    77,
+    78,
+    81,
+    82,
+    83,
+    84,
+    88,
+    89
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f246d0847b98573199dd5d726b7c87eeb731c258bbd05d29b8bcf3b5e5b4c80f.json

@@ -0,0 +1,46 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f246d0847b98573199dd5d726b7c87eeb731c258bbd05d29b8bcf3b5e5b4c80f",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "474cc0c253b1ed45ff976fdc590a7d470b79dd39ce8baf3db2a33a74a31947c0",
+  "clause_indices_zero_based": [
+    12,
+    14,
+    16,
+    19,
+    21,
+    24,
+    25,
+    29,
+    31,
+    32,
+    37,
+    38,
+    40,
+    47,
+    48,
+    49,
+    50,
+    52,
+    54,
+    56,
+    57,
+    59,
+    61,
+    62,
+    66,
+    68,
+    73,
+    74,
+    75,
+    77,
+    83,
+    84,
+    86,
+    88
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f2576822f01230112b83dfcb730052285ccfee40366881b1d9081e260919fcf2.json

@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f2576822f01230112b83dfcb730052285ccfee40366881b1d9081e260919fcf2",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "4c7fba7a3ec716b79096d894653cb12b6c8dd92a00c589cfe2b6243aa6a01cf8",
+  "clause_indices_zero_based": [
+    0,
+    2,
+    6,
+    10,
+    13,
+    20,
+    22,
+    24,
+    29,
+    36,
+    37,
+    41,
+    43,
+    45,
+    46,
+    47,
+    52,
+    55,
+    56,
+    60,
+    62,
+    64,
+    65,
+    69,
+    71,
+    73,
+    76,
+    79,
+    81,
+    87,
+    88
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f25a5b655a0334ebfad9810dc3f871976ff0477ca67f75b51b4554790da26e90.json

@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f25a5b655a0334ebfad9810dc3f871976ff0477ca67f75b51b4554790da26e90",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "cc7484402d81ffef00d98f4c03c2c618266399edcc06a26e8f5c0930e6ac4ce5",
+  "clause_indices_zero_based": [
+    0,
+    1,
+    2,
+    3,
+    9,
+    14,
+    22,
+    24,
+    26,
+    29,
+    34,
+    39,
+    40,
+    41,
+    44,
+    45,
+    49,
+    50,
+    53,
+    64,
+    69,
+    70,
+    71,
+    72,
+    74,
+    75,
+    76,
+    77,
+    79,
+    80,
+    82,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f2660a8e271753c7cf67abc6296596d89375f42172448d20fe0d3aa22e8bf7e0.json

@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f2660a8e271753c7cf67abc6296596d89375f42172448d20fe0d3aa22e8bf7e0",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "5b35a64d67d66494210b3ed43ab12c8d107ade8a7c82c4fad7a3dd1b8d7f0359",
+  "clause_indices_zero_based": [
+    1,
+    6,
+    8,
+    9,
+    10,
+    13,
+    20,
+    21,
+    22,
+    26,
+    27,
+    28,
+    32,
+    33,
+    40,
+    43,
+    51,
+    54,
+    57,
+    61,
+    62,
+    63,
+    66,
+    67,
+    68,
+    70,
+    71,
+    74,
+    84
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f279615271aee5ca92dee89fb2abe41169d90b466ce1ace9241e2a5d6b2b3ca2.json

@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f279615271aee5ca92dee89fb2abe41169d90b466ce1ace9241e2a5d6b2b3ca2",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "c1c42c80209e9285b21c28da3ca18d6b5c7a4ba18cbf2f9a8f8029ae40b2ea5e",
+  "clause_indices_zero_based": [
+    1,
+    3,
+    6,
+    8,
+    9,
+    14,
+    18,
+    20,
+    22,
+    23,
+    25,
+    32,
+    33,
+    38,
+    39,
+    43,
+    44,
+    50,
+    53,
+    57,
+    64,
+    66,
+    70,
+    71,
+    74,
+    75,
+    80,
+    81,
+    83,
+    87,
+    91
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f287e27369c334d3ca34aee35c97a3aa4c2ba4286f49d8a2112d20ad71089d67.json

@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f287e27369c334d3ca34aee35c97a3aa4c2ba4286f49d8a2112d20ad71089d67",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "86cd78cdd2cb2cc0d4e9ba2a6170bc07f620df732db338c1139e7b9e16df8822",
+  "clause_indices_zero_based": [
+    4,
+    6,
+    8,
+    9,
+    12,
+    15,
+    16,
+    17,
+    28,
+    31,
+    34,
+    36,
+    40,
+    45,
+    48,
+    51,
+    54,
+    55,
+    56,
+    57,
+    61,
+    63,
+    64,
+    66,
+    69,
+    71,
+    74,
+    78,
+    79,
+    80,
+    81,
+    86
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f28b9c8eb46ab6d7b0cf0a4ac95ce6ccba455c5de3eebb720b1207bf29da7df0.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f28b9c8eb46ab6d7b0cf0a4ac95ce6ccba455c5de3eebb720b1207bf29da7df0",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "5bd998cd62aaad13b6454690b1cbc9cb342b98cd4b44ded23cf13717bc1177e4",
+  "clause_indices_zero_based": [
+    0,
+    3,
+    6,
+    7,
+    9,
+    11,
+    14,
+    16,
+    18,
+    22,
+    24,
+    26,
+    28,
+    30,
+    33,
+    34,
+    37,
+    38,
+    41,
+    43,
+    48,
+    49,
+    51,
+    53,
+    54,
+    56,
+    57,
+    62,
+    63,
+    64,
+    66,
+    67,
+    68,
+    70,
+    71,
+    79,
+    81,
+    83
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f28c9caa2c601eec09172871d87cae8a73bdb800dd08674bb9ee512b562c066a.json

@@ -0,0 +1,49 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f28c9caa2c601eec09172871d87cae8a73bdb800dd08674bb9ee512b562c066a",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "d585c1ea2baa17a548a24955d93c31134b507d86f1a0b1bc07a4400db4a77326",
+  "clause_indices_zero_based": [
+    7,
+    11,
+    15,
+    17,
+    18,
+    20,
+    23,
+    25,
+    28,
+    32,
+    34,
+    36,
+    37,
+    38,
+    46,
+    48,
+    49,
+    51,
+    52,
+    53,
+    54,
+    55,
+    56,
+    60,
+    61,
+    65,
+    66,
+    68,
+    70,
+    71,
+    74,
+    77,
+    78,
+    79,
+    80,
+    82,
+    85
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f2ce62a9d5791bb44a62ae1fd766820e73746522e04211d1c63c33d7138cbbf1.json

@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f2ce62a9d5791bb44a62ae1fd766820e73746522e04211d1c63c33d7138cbbf1",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "62868d8bde726aba16519e7685e1d7b5c4b99022294ab09cde25835e96d2fe6e",
+  "clause_indices_zero_based": [
+    0,
+    11,
+    13,
+    14,
+    20,
+    22,
+    24,
+    27,
+    32,
+    33,
+    41,
+    42,
+    44,
+    47,
+    49,
+    51,
+    53,
+    59,
+    62,
+    63,
+    74,
+    75,
+    77,
+    79,
+    81,
+    88,
+    90
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f2d43f75f380fdd1cb9b178f38583f7c761e83738264416f6e713ad75b602f13.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f2d43f75f380fdd1cb9b178f38583f7c761e83738264416f6e713ad75b602f13",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "c79730c38cff867ac351a394b7e07334af1a13b6a8be31dd12fc8d9e009d3c33",
+  "clause_indices_zero_based": [
+    1,
+    2,
+    3,
+    4,
+    5,
+    7,
+    8,
+    13,
+    14,
+    16,
+    19,
+    20,
+    25,
+    27,
+    32,
+    34,
+    36,
+    39,
+    40,
+    41,
+    43,
+    46,
+    47,
+    49,
+    51,
+    56,
+    57,
+    59,
+    62,
+    64,
+    67,
+    70,
+    71,
+    77,
+    79,
+    83,
+    84,
+    88
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f30cbb82f6e88ba38823466519157ab3471e39e964b076af4bed4f1578a9202d.json

@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f30cbb82f6e88ba38823466519157ab3471e39e964b076af4bed4f1578a9202d",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "03d7e7fe08308b0dcb3963cca5b46ec7e70fbea5767074652be159cfe91ae21e",
+  "clause_indices_zero_based": [
+    5,
+    6,
+    9,
+    10,
+    11,
+    12,
+    14,
+    19,
+    21,
+    23,
+    24,
+    25,
+    29,
+    32,
+    36,
+    38,
+    39,
+    40,
+    42,
+    44,
+    46,
+    47,
+    53,
+    57,
+    69,
+    71,
+    74,
+    75,
+    81,
+    85,
+    86
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f30e56a786a76e87f933be3864e4e3d50b8fb7f6c9090442b0f83e3379aecbe1.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f30e56a786a76e87f933be3864e4e3d50b8fb7f6c9090442b0f83e3379aecbe1",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "c5f1b4d220735c4a7ce037382c31019c367225ce9f86e405ca9e871c86e419b5",
+  "clause_indices_zero_based": [
+    2,
+    3,
+    5,
+    6,
+    7,
+    8,
+    9,
+    11,
+    13,
+    14,
+    17,
+    18,
+    24,
+    25,
+    29,
+    30,
+    31,
+    34,
+    36,
+    37,
+    38,
+    39,
+    45,
+    49,
+    55,
+    57,
+    59,
+    64,
+    66,
+    70,
+    72,
+    75,
+    76,
+    78,
+    81,
+    86
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f323dbf2d40ce33465215a2ec99c93925de9b15d2988539d33af6fa6aeb6cb48.json

@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f323dbf2d40ce33465215a2ec99c93925de9b15d2988539d33af6fa6aeb6cb48",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "cbdbf60e2d26b7bff1814ba1aeec34da8b83aa4fcd2312efec35105a9ae62e18",
+  "clause_indices_zero_based": [
+    2,
+    5,
+    7,
+    12,
+    15,
+    23,
+    24,
+    25,
+    26,
+    30,
+    32,
+    33,
+    34,
+    36,
+    37,
+    39,
+    42,
+    43,
+    44,
+    45,
+    46,
+    49,
+    52,
+    53,
+    54,
+    62,
+    64,
+    70,
+    73,
+    77,
+    82,
+    83,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f344f61dbcb6b1c9df7f658789eefed37afdba818f602977e076d4181ce2fe17.json

@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f344f61dbcb6b1c9df7f658789eefed37afdba818f602977e076d4181ce2fe17",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "5cbd26679c1453cfe810c6a1197beb4f67404a4ce8b77c2ff329ae0a6e9d3a50",
+  "clause_indices_zero_based": [
+    2,
+    8,
+    16,
+    18,
+    19,
+    22,
+    24,
+    25,
+    26,
+    27,
+    28,
+    34,
+    36,
+    38,
+    40,
+    41,
+    42,
+    47,
+    49,
+    53,
+    58,
+    61,
+    63,
+    66,
+    67,
+    68,
+    72,
+    75,
+    79,
+    80,
+    81,
+    82,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f363c984c79afc187bbe91b556c7e6cba36da8b42c19c4635c8431684c738c1c.json

@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f363c984c79afc187bbe91b556c7e6cba36da8b42c19c4635c8431684c738c1c",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "6f88e2bbfe30551ce27412b35088e8606ac3fb2e21e41567c45a6a576c3be792",
+  "clause_indices_zero_based": [
+    0,
+    3,
+    5,
+    8,
+    12,
+    16,
+    22,
+    23,
+    28,
+    31,
+    35,
+    40,
+    45,
+    53,
+    55,
+    57,
+    63,
+    64,
+    65,
+    67,
+    69,
+    71,
+    73,
+    75,
+    76,
+    81,
+    82,
+    83,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f36cb8a43c1807f69610d387994a916a1579f4a0e07f7556656049ba1c8a0717.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f36cb8a43c1807f69610d387994a916a1579f4a0e07f7556656049ba1c8a0717",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "a193c2de236da2a5df7c81b9221648e47a022bacad2fe5ebbfc910831aff8a02",
+  "clause_indices_zero_based": [
+    0,
+    2,
+    10,
+    14,
+    15,
+    16,
+    17,
+    20,
+    24,
+    32,
+    33,
+    39,
+    42,
+    44,
+    47,
+    50,
+    52,
+    53,
+    54,
+    55,
+    57,
+    59,
+    60,
+    63,
+    64,
+    65,
+    66,
+    67,
+    69,
+    70,
+    74,
+    77,
+    78,
+    80,
+    82,
+    86,
+    89,
+    90
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f36f5f5f50729a7500f1d693d67ccb33ace55cb4dbab09861de39b18a437c3f4.json

@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f36f5f5f50729a7500f1d693d67ccb33ace55cb4dbab09861de39b18a437c3f4",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "50547a0039a0449a8881de5c9d6d412878d11d9085e4a1b0272b22066a1ec461",
+  "clause_indices_zero_based": [
+    2,
+    9,
+    12,
+    14,
+    15,
+    21,
+    29,
+    36,
+    40,
+    42,
+    44,
+    45,
+    47,
+    51,
+    52,
+    54,
+    57,
+    58,
+    60,
+    62,
+    64,
+    66,
+    69,
+    72,
+    73,
+    74,
+    75,
+    76,
+    81,
+    82,
+    83,
+    85
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f371b3b9f889c848ef687e5fc40f9b3e9952b8db837a426dd5a240775feabfd0.json

@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f371b3b9f889c848ef687e5fc40f9b3e9952b8db837a426dd5a240775feabfd0",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "05cb0bd595708c943a721f903917f22f009258ec988419223b43863c1cdec99d",
+  "clause_indices_zero_based": [
+    3,
+    5,
+    6,
+    12,
+    16,
+    18,
+    21,
+    23,
+    25,
+    27,
+    28,
+    29,
+    35,
+    36,
+    38,
+    39,
+    43,
+    44,
+    46,
+    50,
+    53,
+    55,
+    57,
+    58,
+    66,
+    67,
+    69,
+    72,
+    73,
+    80,
+    81,
+    83,
+    86
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f381d4a042689d1d9746a5fc744f9407b10d33de802d4e88674c8d46fbfd122a.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f381d4a042689d1d9746a5fc744f9407b10d33de802d4e88674c8d46fbfd122a",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "50ccc4cb20486f3eacfb9adc565f1241a0a4d37a073df9f85735eb5125f44712",
+  "clause_indices_zero_based": [
+    0,
+    5,
+    7,
+    11,
+    13,
+    17,
+    24,
+    27,
+    28,
+    30,
+    34,
+    37,
+    40,
+    41,
+    42,
+    45,
+    46,
+    47,
+    50,
+    51,
+    54,
+    55,
+    60,
+    61,
+    64,
+    65,
+    66,
+    68,
+    71,
+    73,
+    75,
+    76,
+    79,
+    80,
+    81,
+    82,
+    83,
+    84
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f38cdcb5f761d178c6c67b7f5c35bc6c3f486f7efbc5fccf8faa7ff982727211.json

@@ -0,0 +1,49 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f38cdcb5f761d178c6c67b7f5c35bc6c3f486f7efbc5fccf8faa7ff982727211",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "e5e935ea75f00308db01a820b36ef3397a12f9cea6edb1ceddf72262c2a54a3a",
+  "clause_indices_zero_based": [
+    1,
+    4,
+    5,
+    6,
+    8,
+    10,
+    13,
+    14,
+    16,
+    18,
+    19,
+    24,
+    25,
+    28,
+    33,
+    37,
+    39,
+    40,
+    42,
+    43,
+    46,
+    51,
+    56,
+    59,
+    60,
+    61,
+    64,
+    66,
+    67,
+    70,
+    71,
+    72,
+    77,
+    78,
+    80,
+    87,
+    88
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f391d99416807173910955868dc179a32c2d8e19472c95c283828c882c3a9072.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f391d99416807173910955868dc179a32c2d8e19472c95c283828c882c3a9072",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "5b7f11cffc7d7c884614b0e9909f17adc68cc184be052c1324226fd328023cfc",
+  "clause_indices_zero_based": [
+    4,
+    7,
+    8,
+    9,
+    15,
+    24,
+    28,
+    29,
+    30,
+    31,
+    33,
+    36,
+    39,
+    44,
+    45,
+    46,
+    49,
+    54,
+    71,
+    72,
+    82
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f39fa41dbc81aac36d3970161b37c9651733ec330fe01648f41f121aae4e57bb.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f39fa41dbc81aac36d3970161b37c9651733ec330fe01648f41f121aae4e57bb",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "f3a771d811337983701a61acadfecb3b949d56829281f9d491d06016f1048c16",
+  "clause_indices_zero_based": [
+    1,
+    7,
+    16,
+    17,
+    20,
+    22,
+    23,
+    24,
+    28,
+    29,
+    31,
+    33,
+    42,
+    43,
+    46,
+    48,
+    51,
+    52,
+    55,
+    56,
+    59,
+    61,
+    62,
+    66,
+    75,
+    76,
+    77,
+    78,
+    80,
+    83
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3a0c6f529d46b90854c7cd48e969dd4863ee5cb2741d93322b39f5cd9be57ca.json

@@ -0,0 +1,46 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3a0c6f529d46b90854c7cd48e969dd4863ee5cb2741d93322b39f5cd9be57ca",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "f66aca67c1b6a012a6febe4e91c485a8720b223525ec892d2b4c19484bdf607d",
+  "clause_indices_zero_based": [
+    2,
+    4,
+    5,
+    8,
+    19,
+    20,
+    23,
+    25,
+    32,
+    34,
+    36,
+    37,
+    46,
+    48,
+    49,
+    52,
+    62,
+    63,
+    67,
+    68,
+    69,
+    70,
+    72,
+    73,
+    75,
+    77,
+    78,
+    81,
+    83,
+    85,
+    86,
+    88,
+    90,
+    91
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3b0853130cc5164dc8f9e070e2f6dde0164dc636a1c281317dbd2a9c4eec0d2.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3b0853130cc5164dc8f9e070e2f6dde0164dc636a1c281317dbd2a9c4eec0d2",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "0f3d0025f03ff0bc0ee71156ae941e9bdace261317551921664634942ef340fc",
+  "clause_indices_zero_based": [
+    1,
+    2,
+    3,
+    4,
+    6,
+    7,
+    9,
+    12,
+    13,
+    15,
+    16,
+    23,
+    28,
+    32,
+    37,
+    41,
+    43,
+    44,
+    45,
+    47,
+    49,
+    51,
+    60,
+    61,
+    63,
+    64,
+    66,
+    71,
+    72,
+    73,
+    76,
+    78,
+    81,
+    85,
+    86,
+    89
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3b8ee47d49831261af2f09fc172f8075df3903fa5d575cacf36dc20b23272b4.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3b8ee47d49831261af2f09fc172f8075df3903fa5d575cacf36dc20b23272b4",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "33f607f02f6cc37e3c12ae071bd2162eaede05f48512256b6f9750f435fe95e1",
+  "clause_indices_zero_based": [
+    4,
+    13,
+    16,
+    17,
+    20,
+    21,
+    22,
+    25,
+    27,
+    29,
+    31,
+    39,
+    42,
+    45,
+    47,
+    49,
+    50,
+    51,
+    52,
+    54,
+    55,
+    58,
+    59,
+    61,
+    64,
+    68,
+    71,
+    72,
+    73,
+    74,
+    77,
+    80,
+    81,
+    84,
+    86,
+    88
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3bdb2a6179ddca27dd03e5ee389ee6ea5d647a52d6f91d862f037c398074a0c.json

@@ -0,0 +1,47 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3bdb2a6179ddca27dd03e5ee389ee6ea5d647a52d6f91d862f037c398074a0c",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "dd6e2224464b0afd7c872d8562e318eba81f0e8320b821ba5c0538f9e1a91513",
+  "clause_indices_zero_based": [
+    6,
+    9,
+    10,
+    11,
+    17,
+    18,
+    19,
+    27,
+    29,
+    30,
+    31,
+    32,
+    33,
+    34,
+    35,
+    37,
+    39,
+    41,
+    42,
+    47,
+    49,
+    56,
+    57,
+    58,
+    59,
+    62,
+    64,
+    65,
+    66,
+    67,
+    75,
+    79,
+    84,
+    85,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3c1bca2759b1fdb34bb802f99745a02bbf11daf6a0a18ef668a15d9826135a9.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3c1bca2759b1fdb34bb802f99745a02bbf11daf6a0a18ef668a15d9826135a9",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "0bd5d307052f79d913fcd607d0b9f72eb8d2b80d1196ee366db25767ea9a70d9",
+  "clause_indices_zero_based": [
+    1,
+    2,
+    8,
+    10,
+    12,
+    13,
+    16,
+    18,
+    19,
+    20,
+    22,
+    27,
+    28,
+    29,
+    31,
+    32,
+    33,
+    34,
+    36,
+    41,
+    44,
+    46,
+    47,
+    48,
+    51,
+    58,
+    59,
+    63,
+    64,
+    67,
+    68,
+    69,
+    71,
+    72,
+    73,
+    77,
+    78,
+    81,
+    82,
+    83,
+    84,
+    89
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3d73de2278a539f826a2d19e1ffc9511190959259cf94acf6b8a72a810d5ec5.json

@@ -0,0 +1,49 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3d73de2278a539f826a2d19e1ffc9511190959259cf94acf6b8a72a810d5ec5",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "9af5232dd3ecd06a6239978fc20c993ed3e127093d5b451b02202e3e16cc2e71",
+  "clause_indices_zero_based": [
+    1,
+    3,
+    4,
+    10,
+    12,
+    13,
+    16,
+    19,
+    21,
+    22,
+    23,
+    24,
+    25,
+    30,
+    31,
+    33,
+    38,
+    40,
+    41,
+    42,
+    47,
+    50,
+    57,
+    59,
+    60,
+    61,
+    62,
+    64,
+    65,
+    67,
+    72,
+    75,
+    77,
+    79,
+    80,
+    82,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3dd377b03352f5bfc08af7f5c44cd65dfcff0c4036cc09c8b5f56261c41ee52.json

@@ -0,0 +1,51 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3dd377b03352f5bfc08af7f5c44cd65dfcff0c4036cc09c8b5f56261c41ee52",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "4d605bac81990e4be0a15ed8a060303b5984dbd72608a4f9ca3b1a550130fc31",
+  "clause_indices_zero_based": [
+    0,
+    2,
+    4,
+    5,
+    7,
+    14,
+    15,
+    17,
+    19,
+    21,
+    24,
+    31,
+    32,
+    34,
+    39,
+    41,
+    43,
+    45,
+    46,
+    48,
+    50,
+    51,
+    52,
+    54,
+    56,
+    59,
+    61,
+    64,
+    67,
+    69,
+    70,
+    71,
+    75,
+    79,
+    80,
+    82,
+    83,
+    88,
+    89
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3e753db02751e111c7b5ff96e8ceb926c56d015b4d1b4fe52165a66dfbf7a4d.json

@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3e753db02751e111c7b5ff96e8ceb926c56d015b4d1b4fe52165a66dfbf7a4d",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "6f4e6c1d7f63ffedfd885d95b08d89d61c57bab6f9a7b9ce2b152deb18776983",
+  "clause_indices_zero_based": [
+    0,
+    3,
+    4,
+    5,
+    8,
+    10,
+    14,
+    16,
+    18,
+    19,
+    23,
+    26,
+    28,
+    31,
+    33,
+    34,
+    45,
+    47,
+    49,
+    53,
+    59,
+    62,
+    69,
+    71,
+    72,
+    84,
+    86,
+    87,
+    89
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3e9a78ece1b26bdf3153b93f1cad0a24a83869aa6ba58480ed791eb3ddcb114.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3e9a78ece1b26bdf3153b93f1cad0a24a83869aa6ba58480ed791eb3ddcb114",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "6db168661beb6b3751da790e5bc26ff7d81481e2f078fd2057fa4fe9f48af0d3",
+  "clause_indices_zero_based": [
+    1,
+    4,
+    5,
+    8,
+    9,
+    22,
+    24,
+    32,
+    34,
+    45,
+    46,
+    54,
+    56,
+    61,
+    62,
+    64,
+    70,
+    76,
+    78,
+    79,
+    80,
+    88,
+    90
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3f965d61281c9b3e1ad32cbe6a2e1c6d5276c59768af07f69071a9f6a39e1b5.json

@@ -0,0 +1,47 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3f965d61281c9b3e1ad32cbe6a2e1c6d5276c59768af07f69071a9f6a39e1b5",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "1cdc901be5d6607f14bb9de62a1304f2d3ff8658ad122cec38a0d62a643f2ecd",
+  "clause_indices_zero_based": [
+    15,
+    19,
+    22,
+    26,
+    27,
+    32,
+    34,
+    36,
+    37,
+    38,
+    40,
+    42,
+    44,
+    48,
+    51,
+    54,
+    56,
+    57,
+    58,
+    59,
+    60,
+    62,
+    66,
+    71,
+    76,
+    77,
+    78,
+    80,
+    82,
+    83,
+    84,
+    85,
+    87,
+    90,
+    91
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f3fe7ee9a62b1723bdd9be88400251f79f9987a89a581db1e7da27512e23ee55.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f3fe7ee9a62b1723bdd9be88400251f79f9987a89a581db1e7da27512e23ee55",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "8826b7e8f71a946cf8f2956b624f43346b95bc9dd61e6d99381b05af2e364925",
+  "clause_indices_zero_based": [
+    1,
+    3,
+    8,
+    11,
+    15,
+    25,
+    28,
+    32,
+    40,
+    41,
+    42,
+    43,
+    45,
+    46,
+    48,
+    49,
+    50,
+    54,
+    57,
+    58,
+    59,
+    60,
+    63,
+    68,
+    70,
+    71,
+    72,
+    76,
+    78,
+    84
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f40dcae7bc7a69a0fcb6fc3a0ee53a61c53b6d8f72484911c71d9765f8632001.json

@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f40dcae7bc7a69a0fcb6fc3a0ee53a61c53b6d8f72484911c71d9765f8632001",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "78fddbaa2e9b1a2471148c9d5766b6a23bc980bb498a1c77f1babe3c93a7ce14",
+  "clause_indices_zero_based": [
+    1,
+    4,
+    6,
+    8,
+    12,
+    13,
+    14,
+    15,
+    17,
+    18,
+    20,
+    21,
+    23,
+    33,
+    34,
+    35,
+    41,
+    42,
+    46,
+    52,
+    55,
+    57,
+    60,
+    65,
+    66,
+    67,
+    70,
+    73,
+    75,
+    80,
+    81
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f4198de62d591b226c8fabe2388dba0feb2ea60a7f5c46a05c2f99d43abb68c2.json

@@ -0,0 +1,49 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f4198de62d591b226c8fabe2388dba0feb2ea60a7f5c46a05c2f99d43abb68c2",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "2adff5d4808cec5c1ff8b0fb8516df39a5793f49694c409a8d1eacfdf8fbb5b4",
+  "clause_indices_zero_based": [
+    1,
+    3,
+    6,
+    7,
+    9,
+    12,
+    14,
+    15,
+    17,
+    18,
+    19,
+    20,
+    21,
+    22,
+    24,
+    29,
+    30,
+    31,
+    33,
+    34,
+    38,
+    39,
+    42,
+    43,
+    46,
+    50,
+    53,
+    54,
+    55,
+    56,
+    61,
+    62,
+    67,
+    68,
+    72,
+    73,
+    74
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f4249968d673aa3455c2b39d2234ab96896532b61c7b7250c8ef56b8f9e07dbb.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f4249968d673aa3455c2b39d2234ab96896532b61c7b7250c8ef56b8f9e07dbb",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "a39c273b2df20aff81d7d25cfed9ea68a669a741870921c013bdbdd7e8db8f34",
+  "clause_indices_zero_based": [
+    9,
+    13,
+    14,
+    16,
+    17,
+    18,
+    19,
+    20,
+    21,
+    25,
+    26,
+    28,
+    30,
+    32,
+    33,
+    36,
+    39,
+    42,
+    46,
+    48,
+    50,
+    53,
+    54,
+    57,
+    60,
+    61,
+    62,
+    64,
+    65,
+    66,
+    67,
+    68,
+    71,
+    72,
+    74,
+    77,
+    79,
+    82
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f440bfddb1390cef6ec5af248c47b9010960cc993611a48e7acfe62b058ac367.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f440bfddb1390cef6ec5af248c47b9010960cc993611a48e7acfe62b058ac367",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "8ee60a0e85d1985882ec608c318ac5ea2e0a05a8e978d02d28ddca09ec45bfec",
+  "clause_indices_zero_based": [
+    4,
+    5,
+    6,
+    7,
+    8,
+    10,
+    11,
+    17,
+    18,
+    24,
+    28,
+    31,
+    33,
+    35,
+    37,
+    41,
+    46,
+    47,
+    48,
+    53,
+    58,
+    61,
+    62,
+    63,
+    64,
+    65,
+    69,
+    70,
+    74,
+    78,
+    80,
+    81,
+    82,
+    83,
+    85,
+    88
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f442ba9cb3ecf46f7287bfe5207495c322a4706cbf5bf923c9146ce17b045ad6.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f442ba9cb3ecf46f7287bfe5207495c322a4706cbf5bf923c9146ce17b045ad6",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "42e8581e1f5df9be4404a64c7186d99af0da0e92429a0abfdeb65144b554937f",
+  "clause_indices_zero_based": [
+    0,
+    2,
+    3,
+    15,
+    17,
+    18,
+    19,
+    20,
+    22,
+    23,
+    25,
+    27,
+    28,
+    29,
+    32,
+    34,
+    35,
+    36,
+    37,
+    40,
+    46,
+    48,
+    49,
+    51,
+    56,
+    57,
+    59,
+    60,
+    65,
+    74,
+    75,
+    76,
+    77,
+    79,
+    81,
+    82,
+    84,
+    86
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f4521057c72948b551a6cb88a1cca97230668da3757f0ee2d72f8327fe5bff5b.json

@@ -0,0 +1,47 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f4521057c72948b551a6cb88a1cca97230668da3757f0ee2d72f8327fe5bff5b",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "3916ddc1bc7fbf6886af0b646649e5dda43c8349b3dc84779c4a6405b2c492a7",
+  "clause_indices_zero_based": [
+    2,
+    6,
+    9,
+    11,
+    12,
+    19,
+    21,
+    27,
+    29,
+    31,
+    32,
+    35,
+    36,
+    42,
+    43,
+    45,
+    48,
+    49,
+    53,
+    54,
+    57,
+    60,
+    61,
+    63,
+    64,
+    68,
+    69,
+    70,
+    71,
+    72,
+    73,
+    76,
+    86,
+    88,
+    89
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f45fcde3bc9411d4f70ffa98c5d8b15bfd5f17eac9e012cb8e576f08a6a2e103.json

@@ -0,0 +1,47 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f45fcde3bc9411d4f70ffa98c5d8b15bfd5f17eac9e012cb8e576f08a6a2e103",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "cde810c65e5e573e29563690d154fd9c836b78fbecde9b5fdf79479de83b16f6",
+  "clause_indices_zero_based": [
+    0,
+    7,
+    9,
+    11,
+    12,
+    14,
+    15,
+    17,
+    22,
+    23,
+    27,
+    29,
+    30,
+    34,
+    39,
+    40,
+    41,
+    43,
+    45,
+    47,
+    48,
+    50,
+    53,
+    55,
+    57,
+    59,
+    61,
+    62,
+    67,
+    68,
+    69,
+    70,
+    76,
+    82,
+    85
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f4652c1c28fb4a146e7f46d97dcec9ec2bef8be577b003ecbeb0d9904fdf0d9d.json

@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f4652c1c28fb4a146e7f46d97dcec9ec2bef8be577b003ecbeb0d9904fdf0d9d",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "b8883ef7667de91d939dd950fa0febee783f69bb25c845ec5983d46b7bde925b",
+  "clause_indices_zero_based": [
+    4,
+    12,
+    13,
+    16,
+    20,
+    21,
+    32,
+    33,
+    34,
+    35,
+    38,
+    42,
+    45,
+    48,
+    49,
+    52,
+    56,
+    57,
+    59,
+    61,
+    62,
+    64,
+    67,
+    68,
+    70,
+    74,
+    77,
+    87
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f4658e09eabcbe490a3de9e0fbb30caea25e9249a7aa811c7acc126eb2091cd9.json

@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f4658e09eabcbe490a3de9e0fbb30caea25e9249a7aa811c7acc126eb2091cd9",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "ec38088a4f5ca369cc1b7c81cd3d169cf52a33b6a0b0c5256088120799a7a6da",
+  "clause_indices_zero_based": [
+    1,
+    2,
+    5,
+    11,
+    14,
+    19,
+    21,
+    22,
+    25,
+    29,
+    30,
+    33,
+    37,
+    38,
+    49,
+    50,
+    55,
+    56,
+    58,
+    59,
+    61,
+    62,
+    65,
+    66,
+    68,
+    71,
+    73,
+    76,
+    78,
+    80,
+    82,
+    86,
+    91
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f466f3d689cad08e1b566df3d5d75d5dbfb0ab66914e7f98601899bc58adb133.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f466f3d689cad08e1b566df3d5d75d5dbfb0ab66914e7f98601899bc58adb133",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "49702a78244d25e729f8040cb97ea80e1da801aeca4b2b07ab693298efd9daa8",
+  "clause_indices_zero_based": [
+    0,
+    1,
+    3,
+    8,
+    15,
+    17,
+    18,
+    19,
+    20,
+    22,
+    23,
+    24,
+    33,
+    34,
+    42,
+    45,
+    46,
+    47,
+    48,
+    51,
+    53,
+    54,
+    56,
+    59,
+    62,
+    63,
+    65,
+    66,
+    69,
+    75,
+    79,
+    82,
+    83,
+    85,
+    86,
+    87,
+    89,
+    91
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f474e2cb6bd642fcd6acba0f5f11057b9c0a3ea4a775b29b928dd6346ed25b87.json

@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f474e2cb6bd642fcd6acba0f5f11057b9c0a3ea4a775b29b928dd6346ed25b87",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "9ae5e6e2c24ac3a75c5bd094a2357c8b6fd9e2bc14df6b9c6b3e331f8c1a6ec0",
+  "clause_indices_zero_based": [
+    0,
+    1,
+    4,
+    6,
+    8,
+    10,
+    11,
+    12,
+    14,
+    20,
+    23,
+    24,
+    28,
+    29,
+    33,
+    34,
+    39,
+    40,
+    42,
+    43,
+    47,
+    51,
+    55,
+    57,
+    59,
+    60,
+    62,
+    63,
+    77,
+    79,
+    82,
+    84
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f48703d7d304aee71d5ea27a33fd58a487a075418c89461e43ad579828981850.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f48703d7d304aee71d5ea27a33fd58a487a075418c89461e43ad579828981850",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "2a62c457ed7be8d56ce8eb97cbca5fb92831baa5c22a186a2225010cbcdd54b3",
+  "clause_indices_zero_based": [
+    0,
+    1,
+    10,
+    11,
+    12,
+    13,
+    17,
+    19,
+    20,
+    21,
+    22,
+    23,
+    27,
+    29,
+    30,
+    34,
+    36,
+    37,
+    38,
+    39,
+    41,
+    44,
+    45,
+    46,
+    51,
+    54,
+    57,
+    59,
+    60,
+    67,
+    69,
+    71,
+    72,
+    73,
+    77,
+    82,
+    84,
+    85
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f49c432a8035a1dd73387ce818ea2e2471c437673a24e4235bbd22697c3a8981.json

@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f49c432a8035a1dd73387ce818ea2e2471c437673a24e4235bbd22697c3a8981",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "2501da6310db2be1ee5308e2bab0f65b5b59e1ed7ab727c0d6e24726c71b4b16",
+  "clause_indices_zero_based": [
+    12,
+    13,
+    16,
+    17,
+    18,
+    19,
+    21,
+    26,
+    33,
+    34,
+    36,
+    38,
+    43,
+    44,
+    45,
+    46,
+    47,
+    48,
+    51,
+    54,
+    56,
+    57,
+    76,
+    77,
+    78,
+    80,
+    81,
+    82,
+    84
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}

cores/pilot20_train/f4a7adb8be0d764449c1dd0b008e196e70e768d5a56037ea72169a7e19e23677.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "formula_hash": "f4a7adb8be0d764449c1dd0b008e196e70e768d5a56037ea72169a7e19e23677",
+  "dataset": "pilot20_train",
+  "ordered_cnf_sha256": "ae7b446835c11e81da361dae063dfce41e1d62ea2caea53b3c57ac7a24692261",
+  "clause_indices_zero_based": [
+    3,
+    11,
+    14,
+    19,
+    21,
+    23,
+    24,
+    27,
+    30,
+    32,
+    37,
+    41,
+    44,
+    52,
+    53,
+    54,
+    56,
+    58,
+    62,
+    67,
+    71,
+    74,
+    76,
+    78,
+    82,
+    84
+  ],
+  "extractor": "pysat.MUSX/glucose4",
+  "python_sat_version": "1.9.dev17",
+  "minimality": "deletion-minimal; not minimum-cardinality",
+  "verification": "drat-and-deletion-witnesses"
+}