Hugging Face's logo

Aleksis99
/
3sat_data

Model card Files
xet
 Community
Aleksis99 commited on
Commit
b20813b
·
verified ·
1 Parent(s): 5c70ad9

Upload folder using huggingface_hub (part 3)

Browse files
This view is limited to 50 files because it contains too many changes.   See raw diff
Files changed (50) hide show
  1. cores/pilot20_train/18bf514860b3ce81cf1f3997d86092655218d4678e9330d643e9e21c8b823a8f.json +51 -0
  2. cores/pilot20_train/18d02f8055234d8f49005198b87c47fd40a0740f8c54ddc1ce72f2e2d11a981b.json +46 -0
  3. cores/pilot20_train/18d65c49fa674db9b437aef718de0cb619a341fa11bca82b57bada3a962bbceb.json +50 -0
  4. cores/pilot20_train/18e0019b0d588bb8c30fd0b20d28aa22ddaddf56531e561db4be703bfab5d735.json +51 -0
  5. cores/pilot20_train/18ffaad91a727c4e7f3cd0bd7d13df88c015669a56a052989c685e30717d365d.json +41 -0
  6. cores/pilot20_train/190d3a1cd7d717ac3d32a8a48cf42a91ef7b1e08fd18c2e41dce35dc41a2d0c6.json +43 -0
  7. cores/pilot20_train/191a2ee22dff78c1f3273924191cdbfd1592dd8937255fee7165c7ad980537f8.json +40 -0
  8. cores/pilot20_train/19258a096f65bc338bbad929c3b89180e1459196958e80e0118e91b4c0324a3a.json +40 -0
  9. cores/pilot20_train/192a40bbb3353aa09d422cd8d2ebfebb41ecfc7242d49e47a082937160593acf.json +42 -0
  10. cores/pilot20_train/193b636156095e45662e4450430c01f5480630a8d922a4e7883d60979ab24f6a.json +39 -0
  11. cores/pilot20_train/193bc9b0e77120e764e9447351d3b8d6bc7be2bff94026b31311005812755aa0.json +48 -0
  12. cores/pilot20_train/1956c657a204e662920aac4de9a97cb399749d22435f6e9d3127c75afe1d9486.json +45 -0
  13. cores/pilot20_train/195a2621d2ba4c66ed9008780f440f08bcc9165588922da5ccf4942756b8a632.json +43 -0
  14. cores/pilot20_train/195d5449586fedda25b0d160865e7ea584f67d5dd07b4cc2955506fca2b67935.json +50 -0
  15. cores/pilot20_train/19613f45651bce4e0e768387eeade361bff87c2d42dd8f67df6a6f6c7b681e2a.json +44 -0
  16. cores/pilot20_train/197577f28207e9c48a358e9e933fb0c51760679db7750687b9cd6f587a85a657.json +41 -0
  17. cores/pilot20_train/197a6f492c28461d0e43dab913889e55e215df3f6bdc218b01ed6e4961891df1.json +34 -0
  18. cores/pilot20_train/199275cd67660ac65be7f8e61c2683bc73e2c634e39a6e615f776dc168323516.json +47 -0
  19. cores/pilot20_train/19983dd99c6dcb4af3b5ff687baa1524e48ee26858c89b2aab8ec9ed058495b7.json +48 -0
  20. cores/pilot20_train/19a62f22a2f777a0b689bdb9693807f26bbf33e6fe66b1e2e3af5d34243c9d28.json +42 -0
  21. cores/pilot20_train/19ad4bffb5894e71cb363e915fa322a645132c504d51bb095119cd4fb75507d8.json +45 -0
  22. cores/pilot20_train/19b49b3978ded19a39baf1385cd2fa96d443108b39f6861908e9b26d488dc3fd.json +45 -0
  23. cores/pilot20_train/19dc610e2ed85bc27a2daee6a95d3516960473b80d8e2cbbefc630c2520ddef8.json +47 -0
  24. cores/pilot20_train/19f73937479f70d00693a591162beca648aff452bcbc1b72b75cb80dd6eb81c0.json +50 -0
  25. cores/pilot20_train/19ff73fd59c389aadf6de54f5742b87d2076d042fae4897f92d1c7263ba7e0a7.json +34 -0
  26. cores/pilot20_train/1a1885465a36f5ba2700171afd0481861ceee9ad708ff4c246c82c9199e5a239.json +50 -0
  27. cores/pilot20_train/1a1989ad0535595bb0343321e99258ca5dbb3cb60e6f8874e42615da1bdb0d9f.json +47 -0
  28. cores/pilot20_train/1a21570794a7890bb85ce22cae75e10e25566eb1caf0d8da2829964dda3a8570.json +51 -0
  29. cores/pilot20_train/1a554b3f2861618e36636973d43db8e476f99fec7506b1611658cdd9efb9f69b.json +45 -0
  30. cores/pilot20_train/1a555b2060005c5c0afb54c7f0274667c9b72d67591743926fd7e62e3df899d9.json +43 -0
  31. cores/pilot20_train/1a6367ce1f2ad3fb398916ce55f8bc6afa0a464a1345bfb409c689be36be0f89.json +49 -0
  32. cores/pilot20_train/1a6cb477f4483dece2960714111207ce39cfc7e48297c90b35627cd39c9fd1d4.json +44 -0
  33. cores/pilot20_train/1a703e9f9548d2f3ea21bbd95dc414e6edcce41595970786a6facfe832722081.json +51 -0
  34. cores/pilot20_train/1a74b453feae20f7b8f41eae1a2e1bf5ec1625c6169610b92b8bddb690c802ff.json +38 -0
  35. cores/pilot20_train/1a79dbaf86dc0bb580d89037485330c7b1ddeb9e5ca37687700112292233d08f.json +60 -0
  36. cores/pilot20_train/1a7a721e37f825220bb02669b03186ee006a11e0b9af5efbde7defec0dd6decb.json +42 -0
  37. cores/pilot20_train/1a7cbb39840a37721d04fa9078a5bf0b795eb4fbaf6cbcf5696c2992864ae93a.json +45 -0
  38. cores/pilot20_train/1a8544e3f652fc5c7c75341ac5246b74efea8516ac1336feeb2861ae600c80c9.json +45 -0
  39. cores/pilot20_train/1a94b8634a7ef38ade2153d9875b60733da8ccacd5d53c5c1edb0178fca79a25.json +47 -0
  40. cores/pilot20_train/1a950b4011af4291121118a9a3e68f355b757734bfa7b1cf40c13d9dc4ef422c.json +42 -0
  41. cores/pilot20_train/1aa522408b315bdbf4e151a630d5a79d36358df1ea0980bab975a639ac6802a7.json +40 -0
  42. cores/pilot20_train/1aa8687f5fb81aa429c4c25175bcc7b8f03e682061e555f59029e73a6be60b5f.json +35 -0
  43. cores/pilot20_train/1ab58e97938df7c7799799a374fe6b10ddb059b819437aad08df837f65e3b8ac.json +45 -0
  44. cores/pilot20_train/1abbc1c5df2c0a0acca8006c131fc8963797eb0ed9646d580fc6289e148fb4f7.json +47 -0
  45. cores/pilot20_train/1ac8f80d36287480a6b1ad35e907882ef1f657a74fb587f0421398cd93c65adc.json +48 -0
  46. cores/pilot20_train/1ad7bca314f24721325f7d0694a1e4df5e5c9bfdb76bb13b18e0de86defbcf0d.json +47 -0
  47. cores/pilot20_train/1af11ce467cec17b4d1944d2374c231aa81483b2f628e51a808aef6defc3c8be.json +51 -0
  48. cores/pilot20_train/1b11ef109f3a5e887693f9f0937ed246bae08ba46feb7e6f15331bfbd13ee084.json +42 -0
  49. cores/pilot20_train/1b1464d2189cab4f7f7ae16cec16de658f757e3035cef33b5cbd55478ecc82ce.json +45 -0
  50. cores/pilot20_train/1b1d1b9d7f7a8189b79b4975e9ad3d33f5df66c9be1eeb7bdf99b4275a658f1c.json +44 -0
cores/pilot20_train/18bf514860b3ce81cf1f3997d86092655218d4678e9330d643e9e21c8b823a8f.json ADDED
@@ -0,0 +1,51 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "18bf514860b3ce81cf1f3997d86092655218d4678e9330d643e9e21c8b823a8f",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "841d6ddeddd5f11ea8a8379bf48381012393133098c8f512d994f72f8eda0ed7",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 6,
9
+ 9,
10
+ 11,
11
+ 13,
12
+ 18,
13
+ 20,
14
+ 22,
15
+ 25,
16
+ 28,
17
+ 29,
18
+ 32,
19
+ 37,
20
+ 38,
21
+ 41,
22
+ 42,
23
+ 43,
24
+ 44,
25
+ 45,
26
+ 47,
27
+ 48,
28
+ 49,
29
+ 50,
30
+ 53,
31
+ 54,
32
+ 56,
33
+ 57,
34
+ 59,
35
+ 60,
36
+ 61,
37
+ 62,
38
+ 64,
39
+ 70,
40
+ 72,
41
+ 74,
42
+ 78,
43
+ 79,
44
+ 83,
45
+ 85
46
+ ],
47
+ "extractor": "pysat.MUSX/glucose4",
48
+ "python_sat_version": "1.9.dev17",
49
+ "minimality": "deletion-minimal; not minimum-cardinality",
50
+ "verification": "drat-and-deletion-witnesses"
51
+ }
cores/pilot20_train/18d02f8055234d8f49005198b87c47fd40a0740f8c54ddc1ce72f2e2d11a981b.json ADDED
@@ -0,0 +1,46 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "18d02f8055234d8f49005198b87c47fd40a0740f8c54ddc1ce72f2e2d11a981b",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "ea05b0780e96a5347b66f3c93be989e0c211cf9289884330ce5d743f7c0957e2",
6
+ "clause_indices_zero_based": [
7
+ 7,
8
+ 8,
9
+ 10,
10
+ 12,
11
+ 15,
12
+ 17,
13
+ 18,
14
+ 20,
15
+ 22,
16
+ 30,
17
+ 31,
18
+ 36,
19
+ 38,
20
+ 41,
21
+ 42,
22
+ 44,
23
+ 50,
24
+ 51,
25
+ 53,
26
+ 54,
27
+ 58,
28
+ 63,
29
+ 69,
30
+ 70,
31
+ 71,
32
+ 72,
33
+ 74,
34
+ 77,
35
+ 79,
36
+ 81,
37
+ 83,
38
+ 84,
39
+ 85,
40
+ 86
41
+ ],
42
+ "extractor": "pysat.MUSX/glucose4",
43
+ "python_sat_version": "1.9.dev17",
44
+ "minimality": "deletion-minimal; not minimum-cardinality",
45
+ "verification": "drat-and-deletion-witnesses"
46
+ }
cores/pilot20_train/18d65c49fa674db9b437aef718de0cb619a341fa11bca82b57bada3a962bbceb.json ADDED
@@ -0,0 +1,50 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "18d65c49fa674db9b437aef718de0cb619a341fa11bca82b57bada3a962bbceb",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "8acf15a9f30a6a7af0e724a3e226fa2616f0632c79895e6aa4f16f3e8d8ce5ad",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 2,
9
+ 3,
10
+ 11,
11
+ 12,
12
+ 13,
13
+ 14,
14
+ 24,
15
+ 25,
16
+ 30,
17
+ 33,
18
+ 36,
19
+ 37,
20
+ 39,
21
+ 41,
22
+ 42,
23
+ 45,
24
+ 48,
25
+ 50,
26
+ 56,
27
+ 58,
28
+ 59,
29
+ 61,
30
+ 62,
31
+ 67,
32
+ 69,
33
+ 71,
34
+ 73,
35
+ 74,
36
+ 76,
37
+ 77,
38
+ 78,
39
+ 80,
40
+ 81,
41
+ 84,
42
+ 86,
43
+ 88,
44
+ 89
45
+ ],
46
+ "extractor": "pysat.MUSX/glucose4",
47
+ "python_sat_version": "1.9.dev17",
48
+ "minimality": "deletion-minimal; not minimum-cardinality",
49
+ "verification": "drat-and-deletion-witnesses"
50
+ }
cores/pilot20_train/18e0019b0d588bb8c30fd0b20d28aa22ddaddf56531e561db4be703bfab5d735.json ADDED
@@ -0,0 +1,51 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "18e0019b0d588bb8c30fd0b20d28aa22ddaddf56531e561db4be703bfab5d735",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "b6cd3ca16f01f10a5476746ce3d3b97630b53e2f787cd247c98480cf98c676cd",
6
+ "clause_indices_zero_based": [
7
+ 2,
8
+ 6,
9
+ 8,
10
+ 13,
11
+ 14,
12
+ 18,
13
+ 21,
14
+ 22,
15
+ 23,
16
+ 28,
17
+ 30,
18
+ 32,
19
+ 33,
20
+ 36,
21
+ 40,
22
+ 41,
23
+ 42,
24
+ 43,
25
+ 44,
26
+ 45,
27
+ 47,
28
+ 49,
29
+ 50,
30
+ 55,
31
+ 56,
32
+ 59,
33
+ 60,
34
+ 61,
35
+ 64,
36
+ 65,
37
+ 69,
38
+ 74,
39
+ 75,
40
+ 77,
41
+ 78,
42
+ 80,
43
+ 84,
44
+ 86,
45
+ 87
46
+ ],
47
+ "extractor": "pysat.MUSX/glucose4",
48
+ "python_sat_version": "1.9.dev17",
49
+ "minimality": "deletion-minimal; not minimum-cardinality",
50
+ "verification": "drat-and-deletion-witnesses"
51
+ }
cores/pilot20_train/18ffaad91a727c4e7f3cd0bd7d13df88c015669a56a052989c685e30717d365d.json ADDED
@@ -0,0 +1,41 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "18ffaad91a727c4e7f3cd0bd7d13df88c015669a56a052989c685e30717d365d",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "9df33e8aab284125aac247b3ba7e0388dca73582c7f93b9f6a56489db760ad53",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 2,
9
+ 9,
10
+ 11,
11
+ 12,
12
+ 14,
13
+ 20,
14
+ 21,
15
+ 25,
16
+ 30,
17
+ 31,
18
+ 32,
19
+ 34,
20
+ 39,
21
+ 42,
22
+ 43,
23
+ 44,
24
+ 48,
25
+ 49,
26
+ 55,
27
+ 57,
28
+ 63,
29
+ 68,
30
+ 73,
31
+ 74,
32
+ 79,
33
+ 81,
34
+ 87,
35
+ 88
36
+ ],
37
+ "extractor": "pysat.MUSX/glucose4",
38
+ "python_sat_version": "1.9.dev17",
39
+ "minimality": "deletion-minimal; not minimum-cardinality",
40
+ "verification": "drat-and-deletion-witnesses"
41
+ }
cores/pilot20_train/190d3a1cd7d717ac3d32a8a48cf42a91ef7b1e08fd18c2e41dce35dc41a2d0c6.json ADDED
@@ -0,0 +1,43 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "190d3a1cd7d717ac3d32a8a48cf42a91ef7b1e08fd18c2e41dce35dc41a2d0c6",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "8ca71bce0878e321f7f2321f174349565b2a911a326ec4b4bd7a157db8039c35",
6
+ "clause_indices_zero_based": [
7
+ 5,
8
+ 10,
9
+ 12,
10
+ 19,
11
+ 20,
12
+ 21,
13
+ 23,
14
+ 24,
15
+ 25,
16
+ 30,
17
+ 31,
18
+ 42,
19
+ 44,
20
+ 47,
21
+ 52,
22
+ 56,
23
+ 57,
24
+ 58,
25
+ 59,
26
+ 61,
27
+ 62,
28
+ 71,
29
+ 72,
30
+ 73,
31
+ 77,
32
+ 78,
33
+ 81,
34
+ 83,
35
+ 85,
36
+ 87,
37
+ 89
38
+ ],
39
+ "extractor": "pysat.MUSX/glucose4",
40
+ "python_sat_version": "1.9.dev17",
41
+ "minimality": "deletion-minimal; not minimum-cardinality",
42
+ "verification": "drat-and-deletion-witnesses"
43
+ }
cores/pilot20_train/191a2ee22dff78c1f3273924191cdbfd1592dd8937255fee7165c7ad980537f8.json ADDED
@@ -0,0 +1,40 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "191a2ee22dff78c1f3273924191cdbfd1592dd8937255fee7165c7ad980537f8",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "0f7ac6cb5b97b0469301900ed63159b9c6a6ae2b1214d655f7649b577a062fec",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 3,
9
+ 7,
10
+ 8,
11
+ 10,
12
+ 13,
13
+ 19,
14
+ 20,
15
+ 24,
16
+ 33,
17
+ 37,
18
+ 38,
19
+ 40,
20
+ 42,
21
+ 49,
22
+ 51,
23
+ 55,
24
+ 56,
25
+ 68,
26
+ 72,
27
+ 73,
28
+ 75,
29
+ 77,
30
+ 80,
31
+ 82,
32
+ 83,
33
+ 84,
34
+ 89
35
+ ],
36
+ "extractor": "pysat.MUSX/glucose4",
37
+ "python_sat_version": "1.9.dev17",
38
+ "minimality": "deletion-minimal; not minimum-cardinality",
39
+ "verification": "drat-and-deletion-witnesses"
40
+ }
cores/pilot20_train/19258a096f65bc338bbad929c3b89180e1459196958e80e0118e91b4c0324a3a.json ADDED
@@ -0,0 +1,40 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19258a096f65bc338bbad929c3b89180e1459196958e80e0118e91b4c0324a3a",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "88a8eafe03b1a67599b4622638264681a277e171c3647a6258e7b98c9b3c182c",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 3,
9
+ 7,
10
+ 14,
11
+ 16,
12
+ 17,
13
+ 19,
14
+ 24,
15
+ 34,
16
+ 40,
17
+ 45,
18
+ 48,
19
+ 49,
20
+ 50,
21
+ 52,
22
+ 58,
23
+ 59,
24
+ 61,
25
+ 70,
26
+ 71,
27
+ 74,
28
+ 75,
29
+ 77,
30
+ 78,
31
+ 79,
32
+ 85,
33
+ 90,
34
+ 91
35
+ ],
36
+ "extractor": "pysat.MUSX/glucose4",
37
+ "python_sat_version": "1.9.dev17",
38
+ "minimality": "deletion-minimal; not minimum-cardinality",
39
+ "verification": "drat-and-deletion-witnesses"
40
+ }
cores/pilot20_train/192a40bbb3353aa09d422cd8d2ebfebb41ecfc7242d49e47a082937160593acf.json ADDED
@@ -0,0 +1,42 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "192a40bbb3353aa09d422cd8d2ebfebb41ecfc7242d49e47a082937160593acf",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "26582b4151ea7a4f5708d316c0b76a6344499f9d6bf19177ae02f9f5fecb5f7a",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 1,
9
+ 2,
10
+ 3,
11
+ 5,
12
+ 9,
13
+ 13,
14
+ 14,
15
+ 15,
16
+ 23,
17
+ 24,
18
+ 31,
19
+ 36,
20
+ 41,
21
+ 45,
22
+ 48,
23
+ 52,
24
+ 55,
25
+ 65,
26
+ 67,
27
+ 68,
28
+ 70,
29
+ 72,
30
+ 73,
31
+ 77,
32
+ 78,
33
+ 81,
34
+ 83,
35
+ 84,
36
+ 87
37
+ ],
38
+ "extractor": "pysat.MUSX/glucose4",
39
+ "python_sat_version": "1.9.dev17",
40
+ "minimality": "deletion-minimal; not minimum-cardinality",
41
+ "verification": "drat-and-deletion-witnesses"
42
+ }
cores/pilot20_train/193b636156095e45662e4450430c01f5480630a8d922a4e7883d60979ab24f6a.json ADDED
@@ -0,0 +1,39 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "193b636156095e45662e4450430c01f5480630a8d922a4e7883d60979ab24f6a",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "a928a1c3e02aaf114e75f74c61b8072235e2570fc4c1a6588b3da9f85b3554f1",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 6,
9
+ 9,
10
+ 15,
11
+ 17,
12
+ 18,
13
+ 20,
14
+ 21,
15
+ 28,
16
+ 33,
17
+ 34,
18
+ 36,
19
+ 37,
20
+ 38,
21
+ 39,
22
+ 42,
23
+ 43,
24
+ 48,
25
+ 52,
26
+ 57,
27
+ 60,
28
+ 62,
29
+ 64,
30
+ 67,
31
+ 70,
32
+ 78,
33
+ 87
34
+ ],
35
+ "extractor": "pysat.MUSX/glucose4",
36
+ "python_sat_version": "1.9.dev17",
37
+ "minimality": "deletion-minimal; not minimum-cardinality",
38
+ "verification": "drat-and-deletion-witnesses"
39
+ }
cores/pilot20_train/193bc9b0e77120e764e9447351d3b8d6bc7be2bff94026b31311005812755aa0.json ADDED
@@ -0,0 +1,48 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "193bc9b0e77120e764e9447351d3b8d6bc7be2bff94026b31311005812755aa0",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "c1dc4c9919ff7984bee2c03a64b89ac9cd5009b55811153f6e941489d6066481",
6
+ "clause_indices_zero_based": [
7
+ 2,
8
+ 3,
9
+ 6,
10
+ 8,
11
+ 12,
12
+ 15,
13
+ 19,
14
+ 20,
15
+ 24,
16
+ 28,
17
+ 29,
18
+ 34,
19
+ 37,
20
+ 39,
21
+ 41,
22
+ 43,
23
+ 44,
24
+ 45,
25
+ 46,
26
+ 47,
27
+ 48,
28
+ 50,
29
+ 52,
30
+ 53,
31
+ 54,
32
+ 55,
33
+ 60,
34
+ 66,
35
+ 70,
36
+ 71,
37
+ 75,
38
+ 78,
39
+ 79,
40
+ 85,
41
+ 87,
42
+ 89
43
+ ],
44
+ "extractor": "pysat.MUSX/glucose4",
45
+ "python_sat_version": "1.9.dev17",
46
+ "minimality": "deletion-minimal; not minimum-cardinality",
47
+ "verification": "drat-and-deletion-witnesses"
48
+ }
cores/pilot20_train/1956c657a204e662920aac4de9a97cb399749d22435f6e9d3127c75afe1d9486.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1956c657a204e662920aac4de9a97cb399749d22435f6e9d3127c75afe1d9486",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "79dddbe6098e76fd6456910ac0619065d900d725ec6b93e748e2b0a581421718",
6
+ "clause_indices_zero_based": [
7
+ 7,
8
+ 8,
9
+ 10,
10
+ 11,
11
+ 12,
12
+ 14,
13
+ 16,
14
+ 19,
15
+ 28,
16
+ 30,
17
+ 32,
18
+ 34,
19
+ 35,
20
+ 39,
21
+ 41,
22
+ 43,
23
+ 44,
24
+ 46,
25
+ 47,
26
+ 49,
27
+ 54,
28
+ 58,
29
+ 59,
30
+ 61,
31
+ 62,
32
+ 64,
33
+ 68,
34
+ 71,
35
+ 73,
36
+ 81,
37
+ 82,
38
+ 84,
39
+ 90
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/195a2621d2ba4c66ed9008780f440f08bcc9165588922da5ccf4942756b8a632.json ADDED
@@ -0,0 +1,43 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "195a2621d2ba4c66ed9008780f440f08bcc9165588922da5ccf4942756b8a632",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "1685521779057c6cbdacef3c69b67976799809209676def979a2adc823c4cd1d",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 3,
9
+ 5,
10
+ 6,
11
+ 8,
12
+ 14,
13
+ 16,
14
+ 17,
15
+ 18,
16
+ 21,
17
+ 25,
18
+ 27,
19
+ 28,
20
+ 31,
21
+ 34,
22
+ 37,
23
+ 39,
24
+ 42,
25
+ 47,
26
+ 51,
27
+ 52,
28
+ 57,
29
+ 58,
30
+ 62,
31
+ 69,
32
+ 75,
33
+ 80,
34
+ 85,
35
+ 87,
36
+ 90,
37
+ 91
38
+ ],
39
+ "extractor": "pysat.MUSX/glucose4",
40
+ "python_sat_version": "1.9.dev17",
41
+ "minimality": "deletion-minimal; not minimum-cardinality",
42
+ "verification": "drat-and-deletion-witnesses"
43
+ }
cores/pilot20_train/195d5449586fedda25b0d160865e7ea584f67d5dd07b4cc2955506fca2b67935.json ADDED
@@ -0,0 +1,50 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "195d5449586fedda25b0d160865e7ea584f67d5dd07b4cc2955506fca2b67935",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "2967970cc53f0bba7c509f1a0b32da2ffd25f29333a6581db9e9a31bf7c2bb97",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 5,
9
+ 7,
10
+ 10,
11
+ 11,
12
+ 13,
13
+ 14,
14
+ 18,
15
+ 19,
16
+ 20,
17
+ 22,
18
+ 23,
19
+ 27,
20
+ 29,
21
+ 30,
22
+ 33,
23
+ 37,
24
+ 40,
25
+ 43,
26
+ 44,
27
+ 46,
28
+ 48,
29
+ 52,
30
+ 53,
31
+ 56,
32
+ 60,
33
+ 64,
34
+ 67,
35
+ 69,
36
+ 72,
37
+ 73,
38
+ 75,
39
+ 76,
40
+ 80,
41
+ 81,
42
+ 84,
43
+ 87,
44
+ 88
45
+ ],
46
+ "extractor": "pysat.MUSX/glucose4",
47
+ "python_sat_version": "1.9.dev17",
48
+ "minimality": "deletion-minimal; not minimum-cardinality",
49
+ "verification": "drat-and-deletion-witnesses"
50
+ }
cores/pilot20_train/19613f45651bce4e0e768387eeade361bff87c2d42dd8f67df6a6f6c7b681e2a.json ADDED
@@ -0,0 +1,44 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19613f45651bce4e0e768387eeade361bff87c2d42dd8f67df6a6f6c7b681e2a",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "e136e15206cf9b86359ba482b54afbc6328075282afc8af961dd55a4f130e771",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 3,
9
+ 4,
10
+ 14,
11
+ 15,
12
+ 21,
13
+ 24,
14
+ 26,
15
+ 27,
16
+ 30,
17
+ 34,
18
+ 35,
19
+ 36,
20
+ 37,
21
+ 38,
22
+ 40,
23
+ 41,
24
+ 43,
25
+ 46,
26
+ 48,
27
+ 50,
28
+ 52,
29
+ 54,
30
+ 60,
31
+ 61,
32
+ 65,
33
+ 66,
34
+ 68,
35
+ 73,
36
+ 74,
37
+ 80,
38
+ 82
39
+ ],
40
+ "extractor": "pysat.MUSX/glucose4",
41
+ "python_sat_version": "1.9.dev17",
42
+ "minimality": "deletion-minimal; not minimum-cardinality",
43
+ "verification": "drat-and-deletion-witnesses"
44
+ }
cores/pilot20_train/197577f28207e9c48a358e9e933fb0c51760679db7750687b9cd6f587a85a657.json ADDED
@@ -0,0 +1,41 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "197577f28207e9c48a358e9e933fb0c51760679db7750687b9cd6f587a85a657",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "8cb47d1bc934f45381bd61ba3884f8dc4528d2cca30b421ca11dc1f325a97e80",
6
+ "clause_indices_zero_based": [
7
+ 2,
8
+ 6,
9
+ 9,
10
+ 11,
11
+ 14,
12
+ 19,
13
+ 20,
14
+ 22,
15
+ 30,
16
+ 31,
17
+ 33,
18
+ 45,
19
+ 47,
20
+ 51,
21
+ 56,
22
+ 59,
23
+ 64,
24
+ 65,
25
+ 67,
26
+ 71,
27
+ 75,
28
+ 76,
29
+ 77,
30
+ 80,
31
+ 81,
32
+ 84,
33
+ 86,
34
+ 90,
35
+ 91
36
+ ],
37
+ "extractor": "pysat.MUSX/glucose4",
38
+ "python_sat_version": "1.9.dev17",
39
+ "minimality": "deletion-minimal; not minimum-cardinality",
40
+ "verification": "drat-and-deletion-witnesses"
41
+ }
cores/pilot20_train/197a6f492c28461d0e43dab913889e55e215df3f6bdc218b01ed6e4961891df1.json ADDED
@@ -0,0 +1,34 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "197a6f492c28461d0e43dab913889e55e215df3f6bdc218b01ed6e4961891df1",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "67a1b76deae377324015f246e82f3e4abda7b5f2c4df82873f47799dea8c2a16",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 5,
9
+ 9,
10
+ 12,
11
+ 14,
12
+ 15,
13
+ 17,
14
+ 27,
15
+ 28,
16
+ 31,
17
+ 33,
18
+ 40,
19
+ 44,
20
+ 45,
21
+ 46,
22
+ 49,
23
+ 68,
24
+ 69,
25
+ 78,
26
+ 84,
27
+ 85,
28
+ 90
29
+ ],
30
+ "extractor": "pysat.MUSX/glucose4",
31
+ "python_sat_version": "1.9.dev17",
32
+ "minimality": "deletion-minimal; not minimum-cardinality",
33
+ "verification": "drat-and-deletion-witnesses"
34
+ }
cores/pilot20_train/199275cd67660ac65be7f8e61c2683bc73e2c634e39a6e615f776dc168323516.json ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "199275cd67660ac65be7f8e61c2683bc73e2c634e39a6e615f776dc168323516",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "eed2139168e432a904f3b134d09eb639c42a7b60a27ad24377382a977529c556",
6
+ "clause_indices_zero_based": [
7
+ 4,
8
+ 8,
9
+ 12,
10
+ 15,
11
+ 20,
12
+ 21,
13
+ 22,
14
+ 23,
15
+ 24,
16
+ 26,
17
+ 27,
18
+ 28,
19
+ 29,
20
+ 30,
21
+ 31,
22
+ 32,
23
+ 34,
24
+ 38,
25
+ 44,
26
+ 49,
27
+ 50,
28
+ 51,
29
+ 63,
30
+ 68,
31
+ 69,
32
+ 71,
33
+ 73,
34
+ 74,
35
+ 75,
36
+ 77,
37
+ 78,
38
+ 81,
39
+ 83,
40
+ 84,
41
+ 86
42
+ ],
43
+ "extractor": "pysat.MUSX/glucose4",
44
+ "python_sat_version": "1.9.dev17",
45
+ "minimality": "deletion-minimal; not minimum-cardinality",
46
+ "verification": "drat-and-deletion-witnesses"
47
+ }
cores/pilot20_train/19983dd99c6dcb4af3b5ff687baa1524e48ee26858c89b2aab8ec9ed058495b7.json ADDED
@@ -0,0 +1,48 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19983dd99c6dcb4af3b5ff687baa1524e48ee26858c89b2aab8ec9ed058495b7",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "6298a05c502e002ccc1a5354a1e4a9f004cda2cee8f8e7035a890c8f20107d06",
6
+ "clause_indices_zero_based": [
7
+ 2,
8
+ 3,
9
+ 4,
10
+ 6,
11
+ 8,
12
+ 10,
13
+ 11,
14
+ 13,
15
+ 14,
16
+ 15,
17
+ 18,
18
+ 20,
19
+ 22,
20
+ 26,
21
+ 33,
22
+ 34,
23
+ 37,
24
+ 40,
25
+ 44,
26
+ 46,
27
+ 48,
28
+ 50,
29
+ 55,
30
+ 57,
31
+ 59,
32
+ 60,
33
+ 61,
34
+ 62,
35
+ 63,
36
+ 65,
37
+ 70,
38
+ 77,
39
+ 81,
40
+ 83,
41
+ 86,
42
+ 87
43
+ ],
44
+ "extractor": "pysat.MUSX/glucose4",
45
+ "python_sat_version": "1.9.dev17",
46
+ "minimality": "deletion-minimal; not minimum-cardinality",
47
+ "verification": "drat-and-deletion-witnesses"
48
+ }
cores/pilot20_train/19a62f22a2f777a0b689bdb9693807f26bbf33e6fe66b1e2e3af5d34243c9d28.json ADDED
@@ -0,0 +1,42 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19a62f22a2f777a0b689bdb9693807f26bbf33e6fe66b1e2e3af5d34243c9d28",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "ea4912595f78138d931bf21cf0f6f29ca4ec7d2e1a276b59e133b42e08efb48f",
6
+ "clause_indices_zero_based": [
7
+ 7,
8
+ 8,
9
+ 10,
10
+ 11,
11
+ 14,
12
+ 19,
13
+ 22,
14
+ 23,
15
+ 24,
16
+ 25,
17
+ 27,
18
+ 31,
19
+ 34,
20
+ 39,
21
+ 43,
22
+ 44,
23
+ 50,
24
+ 54,
25
+ 55,
26
+ 56,
27
+ 58,
28
+ 60,
29
+ 62,
30
+ 64,
31
+ 70,
32
+ 72,
33
+ 78,
34
+ 83,
35
+ 84,
36
+ 87
37
+ ],
38
+ "extractor": "pysat.MUSX/glucose4",
39
+ "python_sat_version": "1.9.dev17",
40
+ "minimality": "deletion-minimal; not minimum-cardinality",
41
+ "verification": "drat-and-deletion-witnesses"
42
+ }
cores/pilot20_train/19ad4bffb5894e71cb363e915fa322a645132c504d51bb095119cd4fb75507d8.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19ad4bffb5894e71cb363e915fa322a645132c504d51bb095119cd4fb75507d8",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "991cc4da796ece704a0546bdb426735b5c43fd3316c26d012d3b57e149897592",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 4,
9
+ 6,
10
+ 9,
11
+ 13,
12
+ 16,
13
+ 19,
14
+ 22,
15
+ 28,
16
+ 29,
17
+ 31,
18
+ 36,
19
+ 38,
20
+ 40,
21
+ 42,
22
+ 43,
23
+ 47,
24
+ 48,
25
+ 50,
26
+ 51,
27
+ 52,
28
+ 57,
29
+ 66,
30
+ 70,
31
+ 73,
32
+ 74,
33
+ 75,
34
+ 78,
35
+ 80,
36
+ 84,
37
+ 86,
38
+ 87,
39
+ 89
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/19b49b3978ded19a39baf1385cd2fa96d443108b39f6861908e9b26d488dc3fd.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19b49b3978ded19a39baf1385cd2fa96d443108b39f6861908e9b26d488dc3fd",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "fb70611891cf7ec69cff0a9355480ca8ee67de5166b1cda753384be699da01d4",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 10,
9
+ 14,
10
+ 17,
11
+ 18,
12
+ 19,
13
+ 21,
14
+ 25,
15
+ 27,
16
+ 28,
17
+ 38,
18
+ 39,
19
+ 43,
20
+ 49,
21
+ 50,
22
+ 53,
23
+ 54,
24
+ 56,
25
+ 57,
26
+ 59,
27
+ 61,
28
+ 62,
29
+ 64,
30
+ 66,
31
+ 67,
32
+ 69,
33
+ 71,
34
+ 72,
35
+ 82,
36
+ 85,
37
+ 86,
38
+ 88,
39
+ 89
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/19dc610e2ed85bc27a2daee6a95d3516960473b80d8e2cbbefc630c2520ddef8.json ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19dc610e2ed85bc27a2daee6a95d3516960473b80d8e2cbbefc630c2520ddef8",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "d72397041a39a7de4ebc5766c8aead2a583a927260f3353092e769c810fb6513",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 12,
9
+ 14,
10
+ 15,
11
+ 20,
12
+ 21,
13
+ 23,
14
+ 28,
15
+ 32,
16
+ 34,
17
+ 36,
18
+ 37,
19
+ 38,
20
+ 39,
21
+ 41,
22
+ 44,
23
+ 50,
24
+ 54,
25
+ 63,
26
+ 65,
27
+ 69,
28
+ 70,
29
+ 71,
30
+ 73,
31
+ 74,
32
+ 75,
33
+ 76,
34
+ 77,
35
+ 78,
36
+ 79,
37
+ 80,
38
+ 81,
39
+ 82,
40
+ 87,
41
+ 88
42
+ ],
43
+ "extractor": "pysat.MUSX/glucose4",
44
+ "python_sat_version": "1.9.dev17",
45
+ "minimality": "deletion-minimal; not minimum-cardinality",
46
+ "verification": "drat-and-deletion-witnesses"
47
+ }
cores/pilot20_train/19f73937479f70d00693a591162beca648aff452bcbc1b72b75cb80dd6eb81c0.json ADDED
@@ -0,0 +1,50 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19f73937479f70d00693a591162beca648aff452bcbc1b72b75cb80dd6eb81c0",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "1636330f01aa8be11f4f55b741571f3c147eae6dc87377be79b334099dcfef51",
6
+ "clause_indices_zero_based": [
7
+ 4,
8
+ 8,
9
+ 9,
10
+ 12,
11
+ 16,
12
+ 17,
13
+ 20,
14
+ 22,
15
+ 24,
16
+ 28,
17
+ 31,
18
+ 32,
19
+ 34,
20
+ 38,
21
+ 39,
22
+ 40,
23
+ 42,
24
+ 44,
25
+ 48,
26
+ 51,
27
+ 52,
28
+ 53,
29
+ 54,
30
+ 57,
31
+ 59,
32
+ 60,
33
+ 61,
34
+ 63,
35
+ 64,
36
+ 67,
37
+ 69,
38
+ 71,
39
+ 73,
40
+ 79,
41
+ 81,
42
+ 82,
43
+ 90,
44
+ 91
45
+ ],
46
+ "extractor": "pysat.MUSX/glucose4",
47
+ "python_sat_version": "1.9.dev17",
48
+ "minimality": "deletion-minimal; not minimum-cardinality",
49
+ "verification": "drat-and-deletion-witnesses"
50
+ }
cores/pilot20_train/19ff73fd59c389aadf6de54f5742b87d2076d042fae4897f92d1c7263ba7e0a7.json ADDED
@@ -0,0 +1,34 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "19ff73fd59c389aadf6de54f5742b87d2076d042fae4897f92d1c7263ba7e0a7",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "0a1ce3097a42c6f1884d7d6ab7c7b90a0b6f10782240603b8b099bddecf325e2",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 8,
9
+ 14,
10
+ 23,
11
+ 24,
12
+ 32,
13
+ 36,
14
+ 42,
15
+ 44,
16
+ 55,
17
+ 63,
18
+ 64,
19
+ 67,
20
+ 68,
21
+ 69,
22
+ 72,
23
+ 77,
24
+ 79,
25
+ 82,
26
+ 83,
27
+ 84,
28
+ 88
29
+ ],
30
+ "extractor": "pysat.MUSX/glucose4",
31
+ "python_sat_version": "1.9.dev17",
32
+ "minimality": "deletion-minimal; not minimum-cardinality",
33
+ "verification": "drat-and-deletion-witnesses"
34
+ }
cores/pilot20_train/1a1885465a36f5ba2700171afd0481861ceee9ad708ff4c246c82c9199e5a239.json ADDED
@@ -0,0 +1,50 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a1885465a36f5ba2700171afd0481861ceee9ad708ff4c246c82c9199e5a239",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "06bfb55f3f3c6d34ba3273294b7bcf8545650fa48eadeab41a859fa2d00bdf86",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 7,
9
+ 9,
10
+ 10,
11
+ 21,
12
+ 22,
13
+ 23,
14
+ 25,
15
+ 27,
16
+ 28,
17
+ 29,
18
+ 33,
19
+ 35,
20
+ 36,
21
+ 37,
22
+ 39,
23
+ 41,
24
+ 42,
25
+ 44,
26
+ 49,
27
+ 51,
28
+ 54,
29
+ 55,
30
+ 58,
31
+ 60,
32
+ 62,
33
+ 63,
34
+ 64,
35
+ 68,
36
+ 69,
37
+ 70,
38
+ 71,
39
+ 74,
40
+ 75,
41
+ 78,
42
+ 81,
43
+ 84,
44
+ 85
45
+ ],
46
+ "extractor": "pysat.MUSX/glucose4",
47
+ "python_sat_version": "1.9.dev17",
48
+ "minimality": "deletion-minimal; not minimum-cardinality",
49
+ "verification": "drat-and-deletion-witnesses"
50
+ }
cores/pilot20_train/1a1989ad0535595bb0343321e99258ca5dbb3cb60e6f8874e42615da1bdb0d9f.json ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a1989ad0535595bb0343321e99258ca5dbb3cb60e6f8874e42615da1bdb0d9f",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "6d8ff69fde5a03e90764704249da0bd96ad51e81b2e0168732f73e7aa61fba98",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 5,
9
+ 7,
10
+ 8,
11
+ 10,
12
+ 11,
13
+ 15,
14
+ 16,
15
+ 17,
16
+ 20,
17
+ 23,
18
+ 24,
19
+ 26,
20
+ 29,
21
+ 30,
22
+ 41,
23
+ 43,
24
+ 44,
25
+ 47,
26
+ 50,
27
+ 52,
28
+ 53,
29
+ 54,
30
+ 55,
31
+ 58,
32
+ 62,
33
+ 63,
34
+ 71,
35
+ 73,
36
+ 74,
37
+ 76,
38
+ 82,
39
+ 84,
40
+ 87,
41
+ 91
42
+ ],
43
+ "extractor": "pysat.MUSX/glucose4",
44
+ "python_sat_version": "1.9.dev17",
45
+ "minimality": "deletion-minimal; not minimum-cardinality",
46
+ "verification": "drat-and-deletion-witnesses"
47
+ }
cores/pilot20_train/1a21570794a7890bb85ce22cae75e10e25566eb1caf0d8da2829964dda3a8570.json ADDED
@@ -0,0 +1,51 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a21570794a7890bb85ce22cae75e10e25566eb1caf0d8da2829964dda3a8570",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "f2b2e3485773a81270a4c4b29cbdf4a3badd5b2ce87f50c1beb66cbc4af61380",
6
+ "clause_indices_zero_based": [
7
+ 5,
8
+ 6,
9
+ 8,
10
+ 9,
11
+ 10,
12
+ 15,
13
+ 16,
14
+ 20,
15
+ 21,
16
+ 26,
17
+ 32,
18
+ 37,
19
+ 40,
20
+ 42,
21
+ 43,
22
+ 44,
23
+ 46,
24
+ 48,
25
+ 49,
26
+ 50,
27
+ 55,
28
+ 57,
29
+ 60,
30
+ 62,
31
+ 65,
32
+ 67,
33
+ 69,
34
+ 70,
35
+ 71,
36
+ 72,
37
+ 75,
38
+ 77,
39
+ 78,
40
+ 79,
41
+ 80,
42
+ 81,
43
+ 84,
44
+ 87,
45
+ 88
46
+ ],
47
+ "extractor": "pysat.MUSX/glucose4",
48
+ "python_sat_version": "1.9.dev17",
49
+ "minimality": "deletion-minimal; not minimum-cardinality",
50
+ "verification": "drat-and-deletion-witnesses"
51
+ }
cores/pilot20_train/1a554b3f2861618e36636973d43db8e476f99fec7506b1611658cdd9efb9f69b.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a554b3f2861618e36636973d43db8e476f99fec7506b1611658cdd9efb9f69b",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "1faa4e3f4178e32638c96331dc4f3d2cf1681161058ebaa70a5307bc08e2c24e",
6
+ "clause_indices_zero_based": [
7
+ 5,
8
+ 6,
9
+ 13,
10
+ 15,
11
+ 20,
12
+ 23,
13
+ 25,
14
+ 26,
15
+ 31,
16
+ 35,
17
+ 36,
18
+ 37,
19
+ 42,
20
+ 43,
21
+ 45,
22
+ 54,
23
+ 56,
24
+ 57,
25
+ 58,
26
+ 62,
27
+ 63,
28
+ 64,
29
+ 66,
30
+ 68,
31
+ 69,
32
+ 72,
33
+ 73,
34
+ 76,
35
+ 80,
36
+ 83,
37
+ 86,
38
+ 88,
39
+ 89
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/1a555b2060005c5c0afb54c7f0274667c9b72d67591743926fd7e62e3df899d9.json ADDED
@@ -0,0 +1,43 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a555b2060005c5c0afb54c7f0274667c9b72d67591743926fd7e62e3df899d9",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "ca330979bb96066e3a4b90250f82830a4786d2f5f190adb70db3cf9c2ae3b3ef",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 2,
9
+ 4,
10
+ 5,
11
+ 15,
12
+ 16,
13
+ 18,
14
+ 21,
15
+ 22,
16
+ 24,
17
+ 25,
18
+ 28,
19
+ 29,
20
+ 32,
21
+ 33,
22
+ 40,
23
+ 42,
24
+ 44,
25
+ 45,
26
+ 49,
27
+ 51,
28
+ 56,
29
+ 57,
30
+ 62,
31
+ 65,
32
+ 70,
33
+ 73,
34
+ 75,
35
+ 81,
36
+ 87,
37
+ 88
38
+ ],
39
+ "extractor": "pysat.MUSX/glucose4",
40
+ "python_sat_version": "1.9.dev17",
41
+ "minimality": "deletion-minimal; not minimum-cardinality",
42
+ "verification": "drat-and-deletion-witnesses"
43
+ }
cores/pilot20_train/1a6367ce1f2ad3fb398916ce55f8bc6afa0a464a1345bfb409c689be36be0f89.json ADDED
@@ -0,0 +1,49 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a6367ce1f2ad3fb398916ce55f8bc6afa0a464a1345bfb409c689be36be0f89",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "4bf0cd87e276c797be42394366356315c640a24fabe9964d05f4fbaa40a60cff",
6
+ "clause_indices_zero_based": [
7
+ 2,
8
+ 8,
9
+ 14,
10
+ 16,
11
+ 17,
12
+ 21,
13
+ 29,
14
+ 32,
15
+ 33,
16
+ 39,
17
+ 40,
18
+ 42,
19
+ 43,
20
+ 44,
21
+ 47,
22
+ 49,
23
+ 50,
24
+ 52,
25
+ 57,
26
+ 58,
27
+ 60,
28
+ 61,
29
+ 62,
30
+ 63,
31
+ 64,
32
+ 67,
33
+ 68,
34
+ 69,
35
+ 71,
36
+ 77,
37
+ 78,
38
+ 79,
39
+ 81,
40
+ 83,
41
+ 84,
42
+ 86,
43
+ 87
44
+ ],
45
+ "extractor": "pysat.MUSX/glucose4",
46
+ "python_sat_version": "1.9.dev17",
47
+ "minimality": "deletion-minimal; not minimum-cardinality",
48
+ "verification": "drat-and-deletion-witnesses"
49
+ }
cores/pilot20_train/1a6cb477f4483dece2960714111207ce39cfc7e48297c90b35627cd39c9fd1d4.json ADDED
@@ -0,0 +1,44 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a6cb477f4483dece2960714111207ce39cfc7e48297c90b35627cd39c9fd1d4",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "a111beda762f94b0b552d26d747035d7bb646848f8becda34958f96b49b52656",
6
+ "clause_indices_zero_based": [
7
+ 6,
8
+ 7,
9
+ 12,
10
+ 13,
11
+ 18,
12
+ 19,
13
+ 21,
14
+ 22,
15
+ 25,
16
+ 27,
17
+ 29,
18
+ 31,
19
+ 32,
20
+ 35,
21
+ 40,
22
+ 43,
23
+ 44,
24
+ 46,
25
+ 50,
26
+ 51,
27
+ 55,
28
+ 58,
29
+ 60,
30
+ 61,
31
+ 63,
32
+ 64,
33
+ 72,
34
+ 75,
35
+ 79,
36
+ 80,
37
+ 83,
38
+ 89
39
+ ],
40
+ "extractor": "pysat.MUSX/glucose4",
41
+ "python_sat_version": "1.9.dev17",
42
+ "minimality": "deletion-minimal; not minimum-cardinality",
43
+ "verification": "drat-and-deletion-witnesses"
44
+ }
cores/pilot20_train/1a703e9f9548d2f3ea21bbd95dc414e6edcce41595970786a6facfe832722081.json ADDED
@@ -0,0 +1,51 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a703e9f9548d2f3ea21bbd95dc414e6edcce41595970786a6facfe832722081",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "f9b94dab9390e0e0ef8cbbadf6a031f21c83dd40b0ddbb9c1dfcddad479c366a",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 8,
9
+ 9,
10
+ 10,
11
+ 12,
12
+ 13,
13
+ 14,
14
+ 16,
15
+ 18,
16
+ 21,
17
+ 25,
18
+ 26,
19
+ 30,
20
+ 32,
21
+ 33,
22
+ 34,
23
+ 35,
24
+ 37,
25
+ 39,
26
+ 40,
27
+ 41,
28
+ 43,
29
+ 47,
30
+ 48,
31
+ 51,
32
+ 54,
33
+ 57,
34
+ 61,
35
+ 63,
36
+ 64,
37
+ 66,
38
+ 74,
39
+ 78,
40
+ 79,
41
+ 81,
42
+ 83,
43
+ 85,
44
+ 89,
45
+ 90
46
+ ],
47
+ "extractor": "pysat.MUSX/glucose4",
48
+ "python_sat_version": "1.9.dev17",
49
+ "minimality": "deletion-minimal; not minimum-cardinality",
50
+ "verification": "drat-and-deletion-witnesses"
51
+ }
cores/pilot20_train/1a74b453feae20f7b8f41eae1a2e1bf5ec1625c6169610b92b8bddb690c802ff.json ADDED
@@ -0,0 +1,38 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a74b453feae20f7b8f41eae1a2e1bf5ec1625c6169610b92b8bddb690c802ff",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "ca71333a2a38ae0836033910933d03dc45334ec3279f3192eddca6c6d510faf8",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 1,
9
+ 3,
10
+ 5,
11
+ 21,
12
+ 22,
13
+ 26,
14
+ 28,
15
+ 29,
16
+ 30,
17
+ 36,
18
+ 37,
19
+ 41,
20
+ 43,
21
+ 45,
22
+ 50,
23
+ 52,
24
+ 59,
25
+ 63,
26
+ 66,
27
+ 67,
28
+ 73,
29
+ 80,
30
+ 84,
31
+ 86,
32
+ 91
33
+ ],
34
+ "extractor": "pysat.MUSX/glucose4",
35
+ "python_sat_version": "1.9.dev17",
36
+ "minimality": "deletion-minimal; not minimum-cardinality",
37
+ "verification": "drat-and-deletion-witnesses"
38
+ }
cores/pilot20_train/1a79dbaf86dc0bb580d89037485330c7b1ddeb9e5ca37687700112292233d08f.json ADDED
@@ -0,0 +1,60 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a79dbaf86dc0bb580d89037485330c7b1ddeb9e5ca37687700112292233d08f",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "be6249a896d04dc639bea5f3589c53e6e2bf13c77b881827195cd1ed6439e6dc",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 3,
9
+ 4,
10
+ 5,
11
+ 7,
12
+ 8,
13
+ 13,
14
+ 14,
15
+ 17,
16
+ 19,
17
+ 22,
18
+ 24,
19
+ 25,
20
+ 26,
21
+ 27,
22
+ 29,
23
+ 30,
24
+ 32,
25
+ 34,
26
+ 35,
27
+ 36,
28
+ 41,
29
+ 42,
30
+ 44,
31
+ 45,
32
+ 48,
33
+ 49,
34
+ 51,
35
+ 53,
36
+ 54,
37
+ 55,
38
+ 57,
39
+ 59,
40
+ 60,
41
+ 61,
42
+ 66,
43
+ 67,
44
+ 69,
45
+ 71,
46
+ 72,
47
+ 74,
48
+ 77,
49
+ 78,
50
+ 79,
51
+ 81,
52
+ 82,
53
+ 84,
54
+ 87
55
+ ],
56
+ "extractor": "pysat.MUSX/glucose4",
57
+ "python_sat_version": "1.9.dev17",
58
+ "minimality": "deletion-minimal; not minimum-cardinality",
59
+ "verification": "drat-and-deletion-witnesses"
60
+ }
cores/pilot20_train/1a7a721e37f825220bb02669b03186ee006a11e0b9af5efbde7defec0dd6decb.json ADDED
@@ -0,0 +1,42 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a7a721e37f825220bb02669b03186ee006a11e0b9af5efbde7defec0dd6decb",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "599c9051f9c26f16b9d33946d95580b0b7449a4e6f0bc55ef80bfcad1ce44a90",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 2,
9
+ 6,
10
+ 8,
11
+ 10,
12
+ 13,
13
+ 20,
14
+ 24,
15
+ 25,
16
+ 30,
17
+ 31,
18
+ 32,
19
+ 34,
20
+ 36,
21
+ 37,
22
+ 45,
23
+ 52,
24
+ 56,
25
+ 62,
26
+ 65,
27
+ 68,
28
+ 69,
29
+ 70,
30
+ 72,
31
+ 76,
32
+ 79,
33
+ 80,
34
+ 81,
35
+ 82,
36
+ 89
37
+ ],
38
+ "extractor": "pysat.MUSX/glucose4",
39
+ "python_sat_version": "1.9.dev17",
40
+ "minimality": "deletion-minimal; not minimum-cardinality",
41
+ "verification": "drat-and-deletion-witnesses"
42
+ }
cores/pilot20_train/1a7cbb39840a37721d04fa9078a5bf0b795eb4fbaf6cbcf5696c2992864ae93a.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a7cbb39840a37721d04fa9078a5bf0b795eb4fbaf6cbcf5696c2992864ae93a",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "191bbcfbe4cd0163837b719bb14e9d655ff46e36ef2061a4762ca87ce84ba6bc",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 3,
9
+ 13,
10
+ 14,
11
+ 19,
12
+ 24,
13
+ 26,
14
+ 27,
15
+ 30,
16
+ 32,
17
+ 34,
18
+ 36,
19
+ 39,
20
+ 41,
21
+ 45,
22
+ 48,
23
+ 50,
24
+ 51,
25
+ 53,
26
+ 54,
27
+ 60,
28
+ 64,
29
+ 66,
30
+ 67,
31
+ 69,
32
+ 72,
33
+ 74,
34
+ 75,
35
+ 77,
36
+ 78,
37
+ 80,
38
+ 85,
39
+ 88
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/1a8544e3f652fc5c7c75341ac5246b74efea8516ac1336feeb2861ae600c80c9.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a8544e3f652fc5c7c75341ac5246b74efea8516ac1336feeb2861ae600c80c9",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "3b59b02c4f3d93062cb08e8ac01fc5aa096143bec1536c65b1691dba8c8c7402",
6
+ "clause_indices_zero_based": [
7
+ 3,
8
+ 4,
9
+ 10,
10
+ 11,
11
+ 14,
12
+ 16,
13
+ 18,
14
+ 19,
15
+ 20,
16
+ 21,
17
+ 23,
18
+ 26,
19
+ 28,
20
+ 34,
21
+ 36,
22
+ 43,
23
+ 45,
24
+ 47,
25
+ 50,
26
+ 56,
27
+ 59,
28
+ 61,
29
+ 63,
30
+ 65,
31
+ 68,
32
+ 69,
33
+ 70,
34
+ 78,
35
+ 79,
36
+ 80,
37
+ 81,
38
+ 84,
39
+ 85
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/1a94b8634a7ef38ade2153d9875b60733da8ccacd5d53c5c1edb0178fca79a25.json ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a94b8634a7ef38ade2153d9875b60733da8ccacd5d53c5c1edb0178fca79a25",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "c88930500e7b8d13fa3308d4612b5a53efa25a95a6b79c26d8752619952887e9",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 4,
9
+ 8,
10
+ 9,
11
+ 10,
12
+ 13,
13
+ 14,
14
+ 16,
15
+ 17,
16
+ 21,
17
+ 22,
18
+ 25,
19
+ 26,
20
+ 28,
21
+ 30,
22
+ 33,
23
+ 36,
24
+ 37,
25
+ 38,
26
+ 42,
27
+ 48,
28
+ 49,
29
+ 53,
30
+ 54,
31
+ 56,
32
+ 58,
33
+ 59,
34
+ 61,
35
+ 67,
36
+ 71,
37
+ 76,
38
+ 81,
39
+ 82,
40
+ 83,
41
+ 84
42
+ ],
43
+ "extractor": "pysat.MUSX/glucose4",
44
+ "python_sat_version": "1.9.dev17",
45
+ "minimality": "deletion-minimal; not minimum-cardinality",
46
+ "verification": "drat-and-deletion-witnesses"
47
+ }
cores/pilot20_train/1a950b4011af4291121118a9a3e68f355b757734bfa7b1cf40c13d9dc4ef422c.json ADDED
@@ -0,0 +1,42 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1a950b4011af4291121118a9a3e68f355b757734bfa7b1cf40c13d9dc4ef422c",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "54ed860b756d3acb5711bed7ef234424b94d94215bb2c5d0ced45da8c0ff50a0",
6
+ "clause_indices_zero_based": [
7
+ 5,
8
+ 11,
9
+ 13,
10
+ 14,
11
+ 15,
12
+ 20,
13
+ 24,
14
+ 25,
15
+ 29,
16
+ 30,
17
+ 32,
18
+ 34,
19
+ 36,
20
+ 38,
21
+ 40,
22
+ 42,
23
+ 44,
24
+ 45,
25
+ 48,
26
+ 49,
27
+ 52,
28
+ 53,
29
+ 56,
30
+ 60,
31
+ 68,
32
+ 71,
33
+ 74,
34
+ 77,
35
+ 78,
36
+ 79
37
+ ],
38
+ "extractor": "pysat.MUSX/glucose4",
39
+ "python_sat_version": "1.9.dev17",
40
+ "minimality": "deletion-minimal; not minimum-cardinality",
41
+ "verification": "drat-and-deletion-witnesses"
42
+ }
cores/pilot20_train/1aa522408b315bdbf4e151a630d5a79d36358df1ea0980bab975a639ac6802a7.json ADDED
@@ -0,0 +1,40 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1aa522408b315bdbf4e151a630d5a79d36358df1ea0980bab975a639ac6802a7",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "8043889247f09c7ffdfe877dec0e8dbf05929d40437f2f01059e866b4b33192e",
6
+ "clause_indices_zero_based": [
7
+ 5,
8
+ 6,
9
+ 11,
10
+ 12,
11
+ 13,
12
+ 14,
13
+ 16,
14
+ 18,
15
+ 25,
16
+ 29,
17
+ 32,
18
+ 34,
19
+ 38,
20
+ 39,
21
+ 40,
22
+ 44,
23
+ 45,
24
+ 46,
25
+ 49,
26
+ 53,
27
+ 57,
28
+ 60,
29
+ 68,
30
+ 71,
31
+ 72,
32
+ 74,
33
+ 76,
34
+ 81
35
+ ],
36
+ "extractor": "pysat.MUSX/glucose4",
37
+ "python_sat_version": "1.9.dev17",
38
+ "minimality": "deletion-minimal; not minimum-cardinality",
39
+ "verification": "drat-and-deletion-witnesses"
40
+ }
cores/pilot20_train/1aa8687f5fb81aa429c4c25175bcc7b8f03e682061e555f59029e73a6be60b5f.json ADDED
@@ -0,0 +1,35 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1aa8687f5fb81aa429c4c25175bcc7b8f03e682061e555f59029e73a6be60b5f",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "a74a33b24bada97519e2c47040d6c10f24be2f09717cea5d90427167dc00c85d",
6
+ "clause_indices_zero_based": [
7
+ 4,
8
+ 9,
9
+ 13,
10
+ 21,
11
+ 25,
12
+ 28,
13
+ 29,
14
+ 32,
15
+ 36,
16
+ 38,
17
+ 40,
18
+ 41,
19
+ 42,
20
+ 44,
21
+ 51,
22
+ 53,
23
+ 54,
24
+ 65,
25
+ 68,
26
+ 70,
27
+ 73,
28
+ 80,
29
+ 88
30
+ ],
31
+ "extractor": "pysat.MUSX/glucose4",
32
+ "python_sat_version": "1.9.dev17",
33
+ "minimality": "deletion-minimal; not minimum-cardinality",
34
+ "verification": "drat-and-deletion-witnesses"
35
+ }
cores/pilot20_train/1ab58e97938df7c7799799a374fe6b10ddb059b819437aad08df837f65e3b8ac.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1ab58e97938df7c7799799a374fe6b10ddb059b819437aad08df837f65e3b8ac",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "31ff7165ed7d55cb2e6afcb9ad660cadcf38f5725cc6f2bdcd350a331b5263e9",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 6,
9
+ 8,
10
+ 12,
11
+ 13,
12
+ 22,
13
+ 27,
14
+ 29,
15
+ 30,
16
+ 31,
17
+ 32,
18
+ 33,
19
+ 36,
20
+ 39,
21
+ 41,
22
+ 44,
23
+ 45,
24
+ 50,
25
+ 54,
26
+ 57,
27
+ 60,
28
+ 61,
29
+ 63,
30
+ 66,
31
+ 67,
32
+ 71,
33
+ 72,
34
+ 76,
35
+ 77,
36
+ 79,
37
+ 84,
38
+ 87,
39
+ 88
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/1abbc1c5df2c0a0acca8006c131fc8963797eb0ed9646d580fc6289e148fb4f7.json ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1abbc1c5df2c0a0acca8006c131fc8963797eb0ed9646d580fc6289e148fb4f7",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "594d012bab275d2e1807aff83fb395483faac1f56c36afe10d14fbaada393e13",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 2,
9
+ 3,
10
+ 4,
11
+ 6,
12
+ 7,
13
+ 18,
14
+ 19,
15
+ 20,
16
+ 25,
17
+ 26,
18
+ 27,
19
+ 32,
20
+ 37,
21
+ 38,
22
+ 41,
23
+ 48,
24
+ 50,
25
+ 51,
26
+ 56,
27
+ 57,
28
+ 59,
29
+ 60,
30
+ 63,
31
+ 64,
32
+ 68,
33
+ 70,
34
+ 73,
35
+ 74,
36
+ 75,
37
+ 77,
38
+ 78,
39
+ 83,
40
+ 84,
41
+ 85
42
+ ],
43
+ "extractor": "pysat.MUSX/glucose4",
44
+ "python_sat_version": "1.9.dev17",
45
+ "minimality": "deletion-minimal; not minimum-cardinality",
46
+ "verification": "drat-and-deletion-witnesses"
47
+ }
cores/pilot20_train/1ac8f80d36287480a6b1ad35e907882ef1f657a74fb587f0421398cd93c65adc.json ADDED
@@ -0,0 +1,48 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1ac8f80d36287480a6b1ad35e907882ef1f657a74fb587f0421398cd93c65adc",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "c50777873c77815df729a77fcf8b3004d181dee4015fd86ac31dd84a9b9b7ce0",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 2,
9
+ 4,
10
+ 6,
11
+ 12,
12
+ 15,
13
+ 18,
14
+ 19,
15
+ 22,
16
+ 24,
17
+ 25,
18
+ 29,
19
+ 30,
20
+ 31,
21
+ 36,
22
+ 38,
23
+ 39,
24
+ 43,
25
+ 45,
26
+ 46,
27
+ 47,
28
+ 53,
29
+ 57,
30
+ 59,
31
+ 60,
32
+ 61,
33
+ 62,
34
+ 63,
35
+ 68,
36
+ 71,
37
+ 73,
38
+ 77,
39
+ 79,
40
+ 81,
41
+ 83,
42
+ 87
43
+ ],
44
+ "extractor": "pysat.MUSX/glucose4",
45
+ "python_sat_version": "1.9.dev17",
46
+ "minimality": "deletion-minimal; not minimum-cardinality",
47
+ "verification": "drat-and-deletion-witnesses"
48
+ }
cores/pilot20_train/1ad7bca314f24721325f7d0694a1e4df5e5c9bfdb76bb13b18e0de86defbcf0d.json ADDED
@@ -0,0 +1,47 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1ad7bca314f24721325f7d0694a1e4df5e5c9bfdb76bb13b18e0de86defbcf0d",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "73a4558a5947f1a971d395d8f66a6e672551e8321dc5047d0aaf0534a1483218",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 2,
9
+ 7,
10
+ 8,
11
+ 13,
12
+ 17,
13
+ 18,
14
+ 20,
15
+ 25,
16
+ 26,
17
+ 27,
18
+ 29,
19
+ 31,
20
+ 33,
21
+ 34,
22
+ 35,
23
+ 43,
24
+ 44,
25
+ 46,
26
+ 47,
27
+ 50,
28
+ 51,
29
+ 58,
30
+ 59,
31
+ 62,
32
+ 64,
33
+ 67,
34
+ 72,
35
+ 73,
36
+ 74,
37
+ 81,
38
+ 82,
39
+ 83,
40
+ 84,
41
+ 85
42
+ ],
43
+ "extractor": "pysat.MUSX/glucose4",
44
+ "python_sat_version": "1.9.dev17",
45
+ "minimality": "deletion-minimal; not minimum-cardinality",
46
+ "verification": "drat-and-deletion-witnesses"
47
+ }
cores/pilot20_train/1af11ce467cec17b4d1944d2374c231aa81483b2f628e51a808aef6defc3c8be.json ADDED
@@ -0,0 +1,51 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1af11ce467cec17b4d1944d2374c231aa81483b2f628e51a808aef6defc3c8be",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "561fb2bf1cb17d6b51c7a84acfd41f962ddc80d16430b93837562ca5a769adb0",
6
+ "clause_indices_zero_based": [
7
+ 4,
8
+ 5,
9
+ 8,
10
+ 9,
11
+ 15,
12
+ 17,
13
+ 25,
14
+ 30,
15
+ 31,
16
+ 32,
17
+ 34,
18
+ 35,
19
+ 37,
20
+ 38,
21
+ 39,
22
+ 41,
23
+ 43,
24
+ 45,
25
+ 48,
26
+ 51,
27
+ 53,
28
+ 54,
29
+ 55,
30
+ 57,
31
+ 64,
32
+ 65,
33
+ 66,
34
+ 70,
35
+ 73,
36
+ 75,
37
+ 76,
38
+ 78,
39
+ 82,
40
+ 83,
41
+ 84,
42
+ 85,
43
+ 87,
44
+ 88,
45
+ 89
46
+ ],
47
+ "extractor": "pysat.MUSX/glucose4",
48
+ "python_sat_version": "1.9.dev17",
49
+ "minimality": "deletion-minimal; not minimum-cardinality",
50
+ "verification": "drat-and-deletion-witnesses"
51
+ }
cores/pilot20_train/1b11ef109f3a5e887693f9f0937ed246bae08ba46feb7e6f15331bfbd13ee084.json ADDED
@@ -0,0 +1,42 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1b11ef109f3a5e887693f9f0937ed246bae08ba46feb7e6f15331bfbd13ee084",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "f7cd7c11088387654191bdcd39d80badf9e07c97d84b19bbe035dfc31db80152",
6
+ "clause_indices_zero_based": [
7
+ 0,
8
+ 2,
9
+ 6,
10
+ 7,
11
+ 8,
12
+ 13,
13
+ 17,
14
+ 20,
15
+ 21,
16
+ 24,
17
+ 26,
18
+ 28,
19
+ 29,
20
+ 32,
21
+ 34,
22
+ 35,
23
+ 36,
24
+ 38,
25
+ 48,
26
+ 49,
27
+ 51,
28
+ 54,
29
+ 61,
30
+ 62,
31
+ 63,
32
+ 66,
33
+ 70,
34
+ 76,
35
+ 86,
36
+ 87
37
+ ],
38
+ "extractor": "pysat.MUSX/glucose4",
39
+ "python_sat_version": "1.9.dev17",
40
+ "minimality": "deletion-minimal; not minimum-cardinality",
41
+ "verification": "drat-and-deletion-witnesses"
42
+ }
cores/pilot20_train/1b1464d2189cab4f7f7ae16cec16de658f757e3035cef33b5cbd55478ecc82ce.json ADDED
@@ -0,0 +1,45 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1b1464d2189cab4f7f7ae16cec16de658f757e3035cef33b5cbd55478ecc82ce",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "2cceae3765e8741da931fb5fa17d8e95d93623e8c6257db7b6eb0dbb819e83df",
6
+ "clause_indices_zero_based": [
7
+ 2,
8
+ 3,
9
+ 4,
10
+ 8,
11
+ 9,
12
+ 10,
13
+ 16,
14
+ 17,
15
+ 27,
16
+ 28,
17
+ 31,
18
+ 33,
19
+ 34,
20
+ 38,
21
+ 44,
22
+ 45,
23
+ 47,
24
+ 50,
25
+ 51,
26
+ 52,
27
+ 53,
28
+ 54,
29
+ 57,
30
+ 58,
31
+ 61,
32
+ 63,
33
+ 64,
34
+ 65,
35
+ 66,
36
+ 69,
37
+ 78,
38
+ 79,
39
+ 85
40
+ ],
41
+ "extractor": "pysat.MUSX/glucose4",
42
+ "python_sat_version": "1.9.dev17",
43
+ "minimality": "deletion-minimal; not minimum-cardinality",
44
+ "verification": "drat-and-deletion-witnesses"
45
+ }
cores/pilot20_train/1b1d1b9d7f7a8189b79b4975e9ad3d33f5df66c9be1eeb7bdf99b4275a658f1c.json ADDED
@@ -0,0 +1,44 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "schema_version": 1,
3
+ "formula_hash": "1b1d1b9d7f7a8189b79b4975e9ad3d33f5df66c9be1eeb7bdf99b4275a658f1c",
4
+ "dataset": "pilot20_train",
5
+ "ordered_cnf_sha256": "8aa0eadffab92572a99c53b6fc518848b190499fc541533be215dc72668d3abd",
6
+ "clause_indices_zero_based": [
7
+ 1,
8
+ 4,
9
+ 7,
10
+ 8,
11
+ 11,
12
+ 14,
13
+ 15,
14
+ 16,
15
+ 18,
16
+ 22,
17
+ 25,
18
+ 28,
19
+ 35,
20
+ 36,
21
+ 39,
22
+ 42,
23
+ 46,
24
+ 47,
25
+ 48,
26
+ 51,
27
+ 53,
28
+ 54,
29
+ 55,
30
+ 59,
31
+ 60,
32
+ 63,
33
+ 65,
34
+ 77,
35
+ 83,
36
+ 85,
37
+ 86,
38
+ 88
39
+ ],
40
+ "extractor": "pysat.MUSX/glucose4",
41
+ "python_sat_version": "1.9.dev17",
42
+ "minimality": "deletion-minimal; not minimum-cardinality",
43
+ "verification": "drat-and-deletion-witnesses"
44
+ }