Created
March 2, 2022 16:46
-
-
Save JohnnyJayJay/6996c7afafc806f5358554b058437491 to your computer and use it in GitHub Desktop.
Plotting variable interaction graph layout mesasurement results
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [ { | |
| "variables" : 250, | |
| "clauses" : 1065, | |
| "name" : "https://gbd.iti.kit.edu/file/6ffbc2b1851be02a3b040af9b7d15a42/", | |
| "time" : 526 | |
| }, { | |
| "variables" : 430, | |
| "clauses" : 9080, | |
| "name" : "https://gbd.iti.kit.edu/file/218aba6ee61e235dfb9bcde2894a007c/", | |
| "time" : 1502 | |
| }, { | |
| "variables" : 7467, | |
| "clauses" : 21421, | |
| "name" : "https://gbd.iti.kit.edu/file/0b548243045e74982b57a53b3fdeaede/", | |
| "time" : 6013 | |
| }, { | |
| "variables" : 220, | |
| "clauses" : 9467, | |
| "name" : "https://gbd.iti.kit.edu/file/0b54b2a921d3ead9cced275c24bc8668/", | |
| "time" : 591 | |
| }, { | |
| "variables" : 5000, | |
| "clauses" : 21250, | |
| "name" : "https://gbd.iti.kit.edu/file/429f43bde1b1e5196bcb5f44316172d5/", | |
| "time" : 4187 | |
| }, { | |
| "variables" : 13709, | |
| "clauses" : 42201, | |
| "name" : "https://gbd.iti.kit.edu/file/a6f081826cc948105b3a6c2983cba230/", | |
| "time" : 9659 | |
| }, { | |
| "variables" : 480, | |
| "clauses" : 2498, | |
| "name" : "https://gbd.iti.kit.edu/file/42a268d96d1fddceeba15e7f87aba92d/", | |
| "time" : 1131 | |
| }, { | |
| "variables" : 5633, | |
| "clauses" : 19519, | |
| "name" : "https://gbd.iti.kit.edu/file/a6f110128d063c6f746b6dc04f2c85c5/", | |
| "time" : 4267 | |
| }, { | |
| "variables" : 31486, | |
| "clauses" : 91888, | |
| "name" : "https://gbd.iti.kit.edu/file/00063d88244921d6ec46aeab6866a8e2/", | |
| "time" : 24570 | |
| }, { | |
| "variables" : 300, | |
| "clauses" : 1275, | |
| "name" : "https://gbd.iti.kit.edu/file/00072cf107ae1349c8c59a15c5ce4af1/", | |
| "time" : 644 | |
| }, { | |
| "variables" : 26395, | |
| "clauses" : 582949, | |
| "name" : "https://gbd.iti.kit.edu/file/e9af691a6189df71ae8864860fdbfe34/", | |
| "time" : 25184 | |
| }, { | |
| "variables" : 5789, | |
| "clauses" : 20082, | |
| "name" : "https://gbd.iti.kit.edu/file/e9b4c68df6d99977ab56c8e774b7f5d0/", | |
| "time" : 4787 | |
| }, { | |
| "variables" : 3309, | |
| "clauses" : 9057, | |
| "name" : "https://gbd.iti.kit.edu/file/e9b98d4f4057808abd37b85f9206e25d/", | |
| "time" : 2593 | |
| }, { | |
| "variables" : 27760, | |
| "clauses" : 640229, | |
| "name" : "https://gbd.iti.kit.edu/file/a6f42e7b9a295b598cd3fb41baefda69/", | |
| "time" : 28691 | |
| }, { | |
| "variables" : 29855, | |
| "clauses" : 730520, | |
| "name" : "https://gbd.iti.kit.edu/file/218eb193562465cf27307fab1b6de36d/", | |
| "time" : 30758 | |
| }, { | |
| "variables" : 32127, | |
| "clauses" : 843784, | |
| "name" : "https://gbd.iti.kit.edu/file/42a67891f4ab6576da14fdd2b29d1fa6/", | |
| "time" : 35002 | |
| }, { | |
| "variables" : 82973, | |
| "clauses" : 297795, | |
| "name" : "https://gbd.iti.kit.edu/file/7004f7aecfafe647e52648fb9662b3e0/", | |
| "time" : 62874 | |
| }, { | |
| "variables" : 31033, | |
| "clauses" : 780012, | |
| "name" : "https://gbd.iti.kit.edu/file/a6f5281547356c9a4ac22c4e73f406b7/", | |
| "time" : 36704 | |
| }, { | |
| "variables" : 3420, | |
| "clauses" : 1120760, | |
| "name" : "https://gbd.iti.kit.edu/file/42a8e6f6bd74402cc376ae6ac2a31ff4/", | |
| "time" : 16496 | |
| }, { | |
| "variables" : 33253, | |
| "clauses" : 906876, | |
| "name" : "https://gbd.iti.kit.edu/file/e9bac56aacb05e92c24a002a19a7a34f/", | |
| "time" : 40337 | |
| }, { | |
| "variables" : 16297, | |
| "clauses" : 1562268, | |
| "name" : "https://gbd.iti.kit.edu/file/00076733bdbce94d7e44eca84f1425f0/", | |
| "time" : 32529 | |
| }, { | |
| "variables" : 40000, | |
| "clauses" : 168000, | |
| "name" : "https://gbd.iti.kit.edu/file/2191c05c52a08dc4669bfad6eaa20e57/", | |
| "time" : 43016 | |
| }, { | |
| "variables" : 4724, | |
| "clauses" : 16293, | |
| "name" : "https://gbd.iti.kit.edu/file/a6f96d354d2c5498b746ef3705faa3f7/", | |
| "time" : 3892 | |
| }, { | |
| "variables" : 35620, | |
| "clauses" : 1015172, | |
| "name" : "https://gbd.iti.kit.edu/file/700637890b36cbd09af403260e355f4b/", | |
| "time" : 41384 | |
| }, { | |
| "variables" : 9528, | |
| "clauses" : 1018562, | |
| "name" : "https://gbd.iti.kit.edu/file/0b588a6e45c73bce7c7fed2bf2415c22/", | |
| "time" : 18082 | |
| }, { | |
| "variables" : 34503, | |
| "clauses" : 118118, | |
| "name" : "https://gbd.iti.kit.edu/file/7008a874e413d4c87025b32c025bf45e/", | |
| "time" : 26691 | |
| }, { | |
| "variables" : 47129, | |
| "clauses" : 141002, | |
| "name" : "https://gbd.iti.kit.edu/file/a6f9888133aa12dfff27831645bd0eb3/", | |
| "time" : 38740 | |
| }, { | |
| "variables" : 29584, | |
| "clauses" : 717731, | |
| "name" : "https://gbd.iti.kit.edu/file/42ae516991f48ac939ed77f5e86b6014/", | |
| "time" : 32920 | |
| }, { | |
| "variables" : 28706, | |
| "clauses" : 687089, | |
| "name" : "https://gbd.iti.kit.edu/file/e9bb5b6c197500631d8da14aedfd1ce6/", | |
| "time" : 34538 | |
| }, { | |
| "variables" : 25740, | |
| "clauses" : 554909, | |
| "name" : "https://gbd.iti.kit.edu/file/0b598b147891d9de75c04753dcb49279/", | |
| "time" : 26461 | |
| }, { | |
| "variables" : 3220, | |
| "clauses" : 12439, | |
| "name" : "https://gbd.iti.kit.edu/file/e9bd4a210195e83cf64cae1aaf5a36a0/", | |
| "time" : 2673 | |
| }, { | |
| "variables" : 4851, | |
| "clauses" : 13263, | |
| "name" : "https://gbd.iti.kit.edu/file/0b5c4ba260d2c27eee349128cdfc409a/", | |
| "time" : 3655 | |
| }, { | |
| "variables" : 28135, | |
| "clauses" : 653485, | |
| "name" : "https://gbd.iti.kit.edu/file/000781b7a545fe723159e53127aff659/", | |
| "time" : 30901 | |
| }, { | |
| "variables" : 36778, | |
| "clauses" : 1071606, | |
| "name" : "https://gbd.iti.kit.edu/file/21921f5748cefede002c9a7f511ae147/", | |
| "time" : 43149 | |
| }, { | |
| "variables" : 15232, | |
| "clauses" : 259243, | |
| "name" : "https://gbd.iti.kit.edu/file/70098e87af7e1b512b50985e1b319e0c/", | |
| "time" : 16432 | |
| }, { | |
| "variables" : 25597, | |
| "clauses" : 545533, | |
| "name" : "https://gbd.iti.kit.edu/file/2193e6ef17575755e9509e224f22b231/", | |
| "time" : 26060 | |
| }, { | |
| "variables" : 29890, | |
| "clauses" : 732526, | |
| "name" : "https://gbd.iti.kit.edu/file/e9bd5c3516630bd0edac5f2f5c994a14/", | |
| "time" : 33025 | |
| }, { | |
| "variables" : 30619, | |
| "clauses" : 762075, | |
| "name" : "https://gbd.iti.kit.edu/file/42b1cc15e0e8f5e157caa708bc1cbe73/", | |
| "time" : 32919 | |
| }, { | |
| "variables" : 480, | |
| "clauses" : 2040, | |
| "name" : "https://gbd.iti.kit.edu/file/e9c157fe4000046e59c860e5cdca06fd/", | |
| "time" : 1214 | |
| }, { | |
| "variables" : 200, | |
| "clauses" : 3440, | |
| "name" : "https://gbd.iti.kit.edu/file/e9c98bae822be6a56ac441bde54c8de4/", | |
| "time" : 523 | |
| }, { | |
| "variables" : 32965, | |
| "clauses" : 885524, | |
| "name" : "https://gbd.iti.kit.edu/file/2193eeb75c8245c28914620a1475d03d/", | |
| "time" : 36572 | |
| }, { | |
| "variables" : 25788, | |
| "clauses" : 553694, | |
| "name" : "https://gbd.iti.kit.edu/file/42b2529f4a0af4f8cf6841db6ec6a4f7/", | |
| "time" : 27468 | |
| }, { | |
| "variables" : 27159, | |
| "clauses" : 618172, | |
| "name" : "https://gbd.iti.kit.edu/file/e9cd31ce56ff9fa534e82d571975701b/", | |
| "time" : 28926 | |
| }, { | |
| "variables" : 31778, | |
| "clauses" : 825184, | |
| "name" : "https://gbd.iti.kit.edu/file/21991757ba265405fda6363b695fd458/", | |
| "time" : 35303 | |
| }, { | |
| "variables" : 13709, | |
| "clauses" : 41234, | |
| "name" : "https://gbd.iti.kit.edu/file/e9d2b8c57b02c9fa9788e42a5a2fdb79/", | |
| "time" : 9933 | |
| }, { | |
| "variables" : 135, | |
| "clauses" : 672, | |
| "name" : "https://gbd.iti.kit.edu/file/e9d3a00b12d744f582fe2159e74b1389/", | |
| "time" : 178 | |
| }, { | |
| "variables" : 22641, | |
| "clauses" : 444645, | |
| "name" : "https://gbd.iti.kit.edu/file/42b94d4191bb3a5464af85887ac3bbbe/", | |
| "time" : 22412 | |
| }, { | |
| "variables" : 28679, | |
| "clauses" : 678512, | |
| "name" : "https://gbd.iti.kit.edu/file/e9d3bf22c695e2f1344f19ddb369c320/", | |
| "time" : 30630 | |
| }, { | |
| "variables" : 30292, | |
| "clauses" : 746133, | |
| "name" : "https://gbd.iti.kit.edu/file/219a6cd38163c777513c3d1b0f493aec/", | |
| "time" : 33421 | |
| }, { | |
| "variables" : 17833, | |
| "clauses" : 301547, | |
| "name" : "https://gbd.iti.kit.edu/file/219e0c8c306eee3611d011a93c7d0135/", | |
| "time" : 16966 | |
| }, { | |
| "variables" : 25060, | |
| "clauses" : 526096, | |
| "name" : "https://gbd.iti.kit.edu/file/e9d6c47a3351af11ad28e02a3ecadbac/", | |
| "time" : 26270 | |
| }, { | |
| "variables" : 350, | |
| "clauses" : 1225, | |
| "name" : "https://gbd.iti.kit.edu/file/e9dcdfd1ef885092a5ff09b4e7dbe753/", | |
| "time" : 764 | |
| }, { | |
| "variables" : 26307, | |
| "clauses" : 578356, | |
| "name" : "https://gbd.iti.kit.edu/file/e9de19fc3cacef860ffef982fb220746/", | |
| "time" : 28218 | |
| }, { | |
| "variables" : 33500, | |
| "clauses" : 910901, | |
| "name" : "https://gbd.iti.kit.edu/file/219ff948e64d69eefa6a5c8f6deccc8d/", | |
| "time" : 39808 | |
| }, { | |
| "variables" : 98935, | |
| "clauses" : 296405, | |
| "name" : "https://gbd.iti.kit.edu/file/42bae687b8c0f3061b135ddc21b24d7a/", | |
| "time" : 80267 | |
| }, { | |
| "variables" : 4536, | |
| "clauses" : 12423, | |
| "name" : "https://gbd.iti.kit.edu/file/42bc1cc1cb8e612838893cfa85ba7646/", | |
| "time" : 3551 | |
| }, { | |
| "variables" : 22455, | |
| "clauses" : 436394, | |
| "name" : "https://gbd.iti.kit.edu/file/21a22444a2e05221a5db7cbfa013864e/", | |
| "time" : 22914 | |
| }, { | |
| "variables" : 27399, | |
| "clauses" : 618221, | |
| "name" : "https://gbd.iti.kit.edu/file/42bf552803efb0dff2c4da48d85f92f7/", | |
| "time" : 30257 | |
| }, { | |
| "variables" : 148, | |
| "clauses" : 12993, | |
| "name" : "https://gbd.iti.kit.edu/file/42bf6152680534fa9a92de50161a942e/", | |
| "time" : 330 | |
| }, { | |
| "variables" : 560, | |
| "clauses" : 2380, | |
| "name" : "https://gbd.iti.kit.edu/file/42c005c0b1f4743e2f56b71bd814489f/", | |
| "time" : 462 | |
| }, { | |
| "variables" : 31101, | |
| "clauses" : 789011, | |
| "name" : "https://gbd.iti.kit.edu/file/e9dfdab407e58098f3247a2017314e5f/", | |
| "time" : 35398 | |
| }, { | |
| "variables" : 25051, | |
| "clauses" : 523470, | |
| "name" : "https://gbd.iti.kit.edu/file/21a422e84c8b8856552af0a1e2c3330d/", | |
| "time" : 26066 | |
| }, { | |
| "variables" : 15000, | |
| "clauses" : 63000, | |
| "name" : "https://gbd.iti.kit.edu/file/e9e5515e73e586ebc00c1cf15034acf3/", | |
| "time" : 12907 | |
| }, { | |
| "variables" : 27787, | |
| "clauses" : 641247, | |
| "name" : "https://gbd.iti.kit.edu/file/42c0426460add25e817466adceb2d25c/", | |
| "time" : 29910 | |
| }, { | |
| "variables" : 600, | |
| "clauses" : 2520, | |
| "name" : "https://gbd.iti.kit.edu/file/42c133aedbc9ad63cdbdac1412bdc66a/", | |
| "time" : 450 | |
| }, { | |
| "variables" : 11915, | |
| "clauses" : 191025, | |
| "name" : "https://gbd.iti.kit.edu/file/42c38cb31b2445f0a7e82a901e9a28c5/", | |
| "time" : 11051 | |
| }, { | |
| "variables" : 80, | |
| "clauses" : 14400, | |
| "name" : "https://gbd.iti.kit.edu/file/42c517fbeacff62c4262bff30ee73406/", | |
| "time" : 92 | |
| }, { | |
| "variables" : 25313, | |
| "clauses" : 541042, | |
| "name" : "https://gbd.iti.kit.edu/file/e9e6266fe97573ad2000ef0b6886875c/", | |
| "time" : 27163 | |
| }, { | |
| "variables" : 1295, | |
| "clauses" : 4026, | |
| "name" : "https://gbd.iti.kit.edu/file/e9e87dcc0be226279f8e8c172b90ae8b/", | |
| "time" : 989 | |
| }, { | |
| "variables" : 160, | |
| "clauses" : 21744, | |
| "name" : "https://gbd.iti.kit.edu/file/e9e97d615acd64245a83f425ee25760e/", | |
| "time" : 249 | |
| }, { | |
| "variables" : 2522, | |
| "clauses" : 243459, | |
| "name" : "https://gbd.iti.kit.edu/file/e9ec22a0e1fe46ab5665862472161eb1/", | |
| "time" : 5097 | |
| }, { | |
| "variables" : 27606, | |
| "clauses" : 636405, | |
| "name" : "https://gbd.iti.kit.edu/file/21a43de08d84957455b7fda34a75b8c2/", | |
| "time" : 30534 | |
| }, { | |
| "variables" : 22486, | |
| "clauses" : 439410, | |
| "name" : "https://gbd.iti.kit.edu/file/e9ec70837b05aa54819fc7e647516f66/", | |
| "time" : 23533 | |
| }, { | |
| "variables" : 140, | |
| "clauses" : 12291, | |
| "name" : "https://gbd.iti.kit.edu/file/e9ee5e6b0a64882e2bda43055df10489/", | |
| "time" : 336 | |
| }, { | |
| "variables" : 77262, | |
| "clauses" : 263137, | |
| "name" : "https://gbd.iti.kit.edu/file/42ca0146eec5e5ae1c487d6a4c2459b0/", | |
| "time" : 62824 | |
| }, { | |
| "variables" : 3026, | |
| "clauses" : 8394, | |
| "name" : "https://gbd.iti.kit.edu/file/42cbec6edb9f3f2ccb461c800db0707a/", | |
| "time" : 2465 | |
| }, { | |
| "variables" : 25014, | |
| "clauses" : 527277, | |
| "name" : "https://gbd.iti.kit.edu/file/21a635006882a1689d18b163951a1fca/", | |
| "time" : 26435 | |
| }, { | |
| "variables" : 6376, | |
| "clauses" : 22047, | |
| "name" : "https://gbd.iti.kit.edu/file/42d51666a1128f547c93b9c5ca423ded/", | |
| "time" : 4943 | |
| }, { | |
| "variables" : 142, | |
| "clauses" : 12466, | |
| "name" : "https://gbd.iti.kit.edu/file/21a66133354a1684187995696dc20a98/", | |
| "time" : 257 | |
| }, { | |
| "variables" : 22784, | |
| "clauses" : 450047, | |
| "name" : "https://gbd.iti.kit.edu/file/e9f526d2119a3d9b21e9326c8dfdceb1/", | |
| "time" : 23657 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87779, | |
| "name" : "https://gbd.iti.kit.edu/file/42d9e5cccfb93236b618792df9f1d9f1/", | |
| "time" : 19502 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 2925, | |
| "name" : "https://gbd.iti.kit.edu/file/42dd958cd10259b6ee65e554f65454c8/", | |
| "time" : 1075 | |
| }, { | |
| "variables" : 26834, | |
| "clauses" : 595671, | |
| "name" : "https://gbd.iti.kit.edu/file/e9f543642092fea17b4eaf81c79dfd3f/", | |
| "time" : 29043 | |
| }, { | |
| "variables" : 25690, | |
| "clauses" : 550159, | |
| "name" : "https://gbd.iti.kit.edu/file/42e66e13f5b7c31b6aef43342d0e136e/", | |
| "time" : 27414 | |
| }, { | |
| "variables" : 11025, | |
| "clauses" : 180047, | |
| "name" : "https://gbd.iti.kit.edu/file/42e9109983618515a5a369a3e308fbc5/", | |
| "time" : 12158 | |
| }, { | |
| "variables" : 600, | |
| "clauses" : 1200, | |
| "name" : "https://gbd.iti.kit.edu/file/42eae63bea7f0f02206eff7240be11f5/", | |
| "time" : 446 | |
| }, { | |
| "variables" : 1295, | |
| "clauses" : 24309, | |
| "name" : "https://gbd.iti.kit.edu/file/42ed227bc5b6e9fbb40699f87dc4d161/", | |
| "time" : 1233 | |
| }, { | |
| "variables" : 176, | |
| "clauses" : 1748, | |
| "name" : "https://gbd.iti.kit.edu/file/42ed31c1a36c9c2fba4210a81a81520d/", | |
| "time" : 384 | |
| }, { | |
| "variables" : 6369, | |
| "clauses" : 17872, | |
| "name" : "https://gbd.iti.kit.edu/file/42ef7800f9c6e426e2ff44a0d78285df/", | |
| "time" : 5294 | |
| }, { | |
| "variables" : 3534, | |
| "clauses" : 9642, | |
| "name" : "https://gbd.iti.kit.edu/file/42efc6c698d287932a883db10d28e515/", | |
| "time" : 2897 | |
| }, { | |
| "variables" : 26866, | |
| "clauses" : 594284, | |
| "name" : "https://gbd.iti.kit.edu/file/e9f730e5f66471a492771cb18295d67b/", | |
| "time" : 30875 | |
| }, { | |
| "variables" : 193, | |
| "clauses" : 1113, | |
| "name" : "https://gbd.iti.kit.edu/file/e9f92272ae6a21a0448ce9bcf6187256/", | |
| "time" : 340 | |
| }, { | |
| "variables" : 8510, | |
| "clauses" : 30097, | |
| "name" : "https://gbd.iti.kit.edu/file/42fb5b73354e1cdd1cff334cccc974f7/", | |
| "time" : 6682 | |
| }, { | |
| "variables" : 27656, | |
| "clauses" : 631371, | |
| "name" : "https://gbd.iti.kit.edu/file/ea0174d2c4054053892114b7a26efc39/", | |
| "time" : 31828 | |
| }, { | |
| "variables" : 5418, | |
| "clauses" : 16171, | |
| "name" : "https://gbd.iti.kit.edu/file/ea0aa5248f55688a6e344ce03ebab18b/", | |
| "time" : 4341 | |
| }, { | |
| "variables" : 25963, | |
| "clauses" : 563772, | |
| "name" : "https://gbd.iti.kit.edu/file/42fbe8262c39a080480210b696d882eb/", | |
| "time" : 29087 | |
| }, { | |
| "variables" : 15061, | |
| "clauses" : 241759, | |
| "name" : "https://gbd.iti.kit.edu/file/ea0abc7dbcfe1494f1e0d7cc6f129bb0/", | |
| "time" : 14849 | |
| }, { | |
| "variables" : 600, | |
| "clauses" : 2100, | |
| "name" : "https://gbd.iti.kit.edu/file/ea0bc8a28aa1c901997d4b04731693b4/", | |
| "time" : 487 | |
| }, { | |
| "variables" : 31672, | |
| "clauses" : 826832, | |
| "name" : "https://gbd.iti.kit.edu/file/42fd20663ebca6ca92a3d74241baad66/", | |
| "time" : 37670 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 14000, | |
| "name" : "https://gbd.iti.kit.edu/file/063beadfa9d6dbd569d12aacbcb300c5/", | |
| "time" : 1011 | |
| }, { | |
| "variables" : 470, | |
| "clauses" : 9925, | |
| "name" : "https://gbd.iti.kit.edu/file/012cb0a6678bbeb7d08bd7b0ccb65d3f/", | |
| "time" : 1692 | |
| }, { | |
| "variables" : 3750, | |
| "clauses" : 10420, | |
| "name" : "https://gbd.iti.kit.edu/file/26eafee09ec7f9ba7594b2a37d5a689e/", | |
| "time" : 3260 | |
| }, { | |
| "variables" : 2421, | |
| "clauses" : 20443, | |
| "name" : "https://gbd.iti.kit.edu/file/5f73d11d8fc79ea749597eb76c6a802e/", | |
| "time" : 1918 | |
| }, { | |
| "variables" : 2200, | |
| "clauses" : 9086, | |
| "name" : "https://gbd.iti.kit.edu/file/169b832e8ad5102801bc5390663b0a81/", | |
| "time" : 1721 | |
| }, { | |
| "variables" : 500, | |
| "clauses" : 1750, | |
| "name" : "https://gbd.iti.kit.edu/file/5f74904d384778c577e32052623f2661/", | |
| "time" : 1242 | |
| }, { | |
| "variables" : 4254, | |
| "clauses" : 11537, | |
| "name" : "https://gbd.iti.kit.edu/file/d84fc81b50b0f440f001e6de6c8f7368/", | |
| "time" : 3396 | |
| }, { | |
| "variables" : 4260, | |
| "clauses" : 11590, | |
| "name" : "https://gbd.iti.kit.edu/file/012e56e8b23c29cb222b64bdeb523409/", | |
| "time" : 3356 | |
| }, { | |
| "variables" : 17221, | |
| "clauses" : 51474, | |
| "name" : "https://gbd.iti.kit.edu/file/37d91934e9534f7c2f770adc1a651458/", | |
| "time" : 11924 | |
| }, { | |
| "variables" : 4128, | |
| "clauses" : 126580, | |
| "name" : "https://gbd.iti.kit.edu/file/5f7f856de96da47473f4400f5cb46a3a/", | |
| "time" : 4969 | |
| }, { | |
| "variables" : 2421, | |
| "clauses" : 20443, | |
| "name" : "https://gbd.iti.kit.edu/file/5f73d11d8fc79ea749597eb76c6a802e/", | |
| "time" : 1787 | |
| }, { | |
| "variables" : 3750, | |
| "clauses" : 10420, | |
| "name" : "https://gbd.iti.kit.edu/file/26eafee09ec7f9ba7594b2a37d5a689e/", | |
| "time" : 2959 | |
| }, { | |
| "variables" : 4254, | |
| "clauses" : 11537, | |
| "name" : "https://gbd.iti.kit.edu/file/d84fc81b50b0f440f001e6de6c8f7368/", | |
| "time" : 3288 | |
| }, { | |
| "variables" : 2200, | |
| "clauses" : 9086, | |
| "name" : "https://gbd.iti.kit.edu/file/169b832e8ad5102801bc5390663b0a81/", | |
| "time" : 1655 | |
| }, { | |
| "variables" : 500, | |
| "clauses" : 1750, | |
| "name" : "https://gbd.iti.kit.edu/file/5f74904d384778c577e32052623f2661/", | |
| "time" : 1124 | |
| }, { | |
| "variables" : 4128, | |
| "clauses" : 126580, | |
| "name" : "https://gbd.iti.kit.edu/file/5f7f856de96da47473f4400f5cb46a3a/", | |
| "time" : 2790 | |
| }, { | |
| "variables" : 17221, | |
| "clauses" : 51474, | |
| "name" : "https://gbd.iti.kit.edu/file/37d91934e9534f7c2f770adc1a651458/", | |
| "time" : 12465 | |
| }, { | |
| "variables" : 19540, | |
| "clauses" : 350401, | |
| "name" : "https://gbd.iti.kit.edu/file/064cf5ae720265bdb95f553557e41f18/", | |
| "time" : 24791 | |
| }, { | |
| "variables" : 24186, | |
| "clauses" : 498215, | |
| "name" : "https://gbd.iti.kit.edu/file/3d3a547c1e026ae0df8f238154d278dc/", | |
| "time" : 37643 | |
| }, { | |
| "variables" : 440, | |
| "clauses" : 1892, | |
| "name" : "https://gbd.iti.kit.edu/file/3d4067a5a22f7c0ce0f86b2c305530ce/", | |
| "time" : 1694 | |
| }, { | |
| "variables" : 23582, | |
| "clauses" : 471906, | |
| "name" : "https://gbd.iti.kit.edu/file/d851a48646a43f5d50ed2f78f32be193/", | |
| "time" : 38432 | |
| }, { | |
| "variables" : 27834, | |
| "clauses" : 643010, | |
| "name" : "https://gbd.iti.kit.edu/file/10fa92d2409fe3215f35771be0debdca/", | |
| "time" : 45874 | |
| }, { | |
| "variables" : 26558, | |
| "clauses" : 584091, | |
| "name" : "https://gbd.iti.kit.edu/file/326327e02749db0196bd920d1b4bc914/", | |
| "time" : 43630 | |
| }, { | |
| "variables" : 28078, | |
| "clauses" : 650955, | |
| "name" : "https://gbd.iti.kit.edu/file/169e4279304ae948428c0706270781f5/", | |
| "time" : 48434 | |
| }, { | |
| "variables" : 29860, | |
| "clauses" : 728578, | |
| "name" : "https://gbd.iti.kit.edu/file/2c8b2f4d9df1b77bf5e1304201a094ed/", | |
| "time" : 48519 | |
| }, { | |
| "variables" : 7935, | |
| "clauses" : 22570, | |
| "name" : "https://gbd.iti.kit.edu/file/d8583cdb99aa7adeecf1e9033fa86261/", | |
| "time" : 10817 | |
| }, { | |
| "variables" : 27961, | |
| "clauses" : 646239, | |
| "name" : "https://gbd.iti.kit.edu/file/5f809243de4d99e0119abb98f9cd2f1a/", | |
| "time" : 44128 | |
| }, { | |
| "variables" : 4128, | |
| "clauses" : 126564, | |
| "name" : "https://gbd.iti.kit.edu/file/10faafc5aaf72ba900b723ba97500c74/", | |
| "time" : 4364 | |
| }, { | |
| "variables" : 480, | |
| "clauses" : 2040, | |
| "name" : "https://gbd.iti.kit.edu/file/d85ca9deae350ae70db1a81ce80a3154/", | |
| "time" : 1578 | |
| }, { | |
| "variables" : 4584, | |
| "clauses" : 43390, | |
| "name" : "https://gbd.iti.kit.edu/file/169e8bcebaebcbb9ff2ba8233fea0dd3/", | |
| "time" : 4824 | |
| }, { | |
| "variables" : 27830, | |
| "clauses" : 642746, | |
| "name" : "https://gbd.iti.kit.edu/file/4e2a3cd0836ea69de6df98b0344642e1/", | |
| "time" : 40354 | |
| }, { | |
| "variables" : 2000, | |
| "clauses" : 8534, | |
| "name" : "https://gbd.iti.kit.edu/file/169f2359a69f617b164eb64d2245c6ab/", | |
| "time" : 2016 | |
| }, { | |
| "variables" : 24377, | |
| "clauses" : 498963, | |
| "name" : "https://gbd.iti.kit.edu/file/065036e33ca5a147c353956348fc8cc5/", | |
| "time" : 35127 | |
| }, { | |
| "variables" : 8760, | |
| "clauses" : 55571, | |
| "name" : "https://gbd.iti.kit.edu/file/2c91a3369964c1261b69c1fdabd0e85f/", | |
| "time" : 11124 | |
| }, { | |
| "variables" : 80, | |
| "clauses" : 7120, | |
| "name" : "https://gbd.iti.kit.edu/file/065775fe69392642261b1436fbd6bab4/", | |
| "time" : 120 | |
| }, { | |
| "variables" : 4959, | |
| "clauses" : 14017, | |
| "name" : "https://gbd.iti.kit.edu/file/4e2d735a79aa5ca641368724757a6786/", | |
| "time" : 5192 | |
| }, { | |
| "variables" : 18810, | |
| "clauses" : 327415, | |
| "name" : "https://gbd.iti.kit.edu/file/3264422a2e13b8f7850fab80fa170577/", | |
| "time" : 22528 | |
| }, { | |
| "variables" : 14552, | |
| "clauses" : 232899, | |
| "name" : "https://gbd.iti.kit.edu/file/10fe86295409337b96b519511d8440af/", | |
| "time" : 18948 | |
| }, { | |
| "variables" : 1850, | |
| "clauses" : 18372, | |
| "name" : "https://gbd.iti.kit.edu/file/1101f973bea6c31e86e361302b5131d0/", | |
| "time" : 3279 | |
| }, { | |
| "variables" : 26243, | |
| "clauses" : 92072, | |
| "name" : "https://gbd.iti.kit.edu/file/16a14e055d12795a46915db84daf9794/", | |
| "time" : 24519 | |
| }, { | |
| "variables" : 28613, | |
| "clauses" : 670638, | |
| "name" : "https://gbd.iti.kit.edu/file/3d46928c1e3a698743ff0dad4fadbaea/", | |
| "time" : 42384 | |
| }, { | |
| "variables" : 28069, | |
| "clauses" : 647269, | |
| "name" : "https://gbd.iti.kit.edu/file/d863c68c31de9033fb54a0190df02a0f/", | |
| "time" : 41205 | |
| }, { | |
| "variables" : 29502, | |
| "clauses" : 714813, | |
| "name" : "https://gbd.iti.kit.edu/file/5f811e38a50492cd71628ae94325b709/", | |
| "time" : 41474 | |
| }, { | |
| "variables" : 90211, | |
| "clauses" : 304013, | |
| "name" : "https://gbd.iti.kit.edu/file/26ebc9d7ac26683dd22e6afb067c2401/", | |
| "time" : 110198 | |
| }, { | |
| "variables" : 98048, | |
| "clauses" : 293759, | |
| "name" : "https://gbd.iti.kit.edu/file/37dfb9d60131ccd4b6d5b2ac50ab6fb2/", | |
| "time" : 105565 | |
| }, { | |
| "variables" : 29626, | |
| "clauses" : 722079, | |
| "name" : "https://gbd.iti.kit.edu/file/4e32695d1bcd7dfc733ec2822458f59f/", | |
| "time" : 37553 | |
| }, { | |
| "variables" : 95816, | |
| "clauses" : 313805, | |
| "name" : "https://gbd.iti.kit.edu/file/0151bedac526ee195bc52e4134cd80e7/", | |
| "time" : 119928 | |
| }, { | |
| "variables" : 25088, | |
| "clauses" : 530327, | |
| "name" : "https://gbd.iti.kit.edu/file/1104c4ae145a5edcb9edd3b15c7e2c5b/", | |
| "time" : 26566 | |
| }, { | |
| "variables" : 32965, | |
| "clauses" : 885524, | |
| "name" : "https://gbd.iti.kit.edu/file/3264f1c7951441c6961d3dff5e4dfe31/", | |
| "time" : 39825 | |
| }, { | |
| "variables" : 36535, | |
| "clauses" : 1062260, | |
| "name" : "https://gbd.iti.kit.edu/file/0657d7556552d692a009861a8df0187d/", | |
| "time" : 50424 | |
| }, { | |
| "variables" : 33377, | |
| "clauses" : 911613, | |
| "name" : "https://gbd.iti.kit.edu/file/3d482e4176e9bff76241baa59378d986/", | |
| "time" : 43690 | |
| }, { | |
| "variables" : 42053, | |
| "clauses" : 157769, | |
| "name" : "https://gbd.iti.kit.edu/file/d864081af60a00a9c4025ee873fb1a8d/", | |
| "time" : 48285 | |
| }, { | |
| "variables" : 31267, | |
| "clauses" : 800249, | |
| "name" : "https://gbd.iti.kit.edu/file/16a3ee772bef92e8defd2dfa2aaa65c4/", | |
| "time" : 48280 | |
| }, { | |
| "variables" : 34678, | |
| "clauses" : 101319, | |
| "name" : "https://gbd.iti.kit.edu/file/4e32e5d9f532872ebb6462c47c902a53/", | |
| "time" : 38246 | |
| }, { | |
| "variables" : 29818, | |
| "clauses" : 726589, | |
| "name" : "https://gbd.iti.kit.edu/file/26edd739605d1dd1a83fbf3482735548/", | |
| "time" : 41855 | |
| }, { | |
| "variables" : 27768, | |
| "clauses" : 641035, | |
| "name" : "https://gbd.iti.kit.edu/file/37e50dd510616d8a83eb838203fe640c/", | |
| "time" : 44131 | |
| }, { | |
| "variables" : 29893, | |
| "clauses" : 732719, | |
| "name" : "https://gbd.iti.kit.edu/file/5f82183e1d7b1db15adaa42a33d49f64/", | |
| "time" : 45571 | |
| }, { | |
| "variables" : 729, | |
| "clauses" : 96849, | |
| "name" : "https://gbd.iti.kit.edu/file/3d485f7153c8f84f932bd15a8e0654ae/", | |
| "time" : 1726 | |
| }, { | |
| "variables" : 26888, | |
| "clauses" : 597155, | |
| "name" : "https://gbd.iti.kit.edu/file/32683b7b1f142e444230fa706354e672/", | |
| "time" : 39660 | |
| }, { | |
| "variables" : 8814, | |
| "clauses" : 25187, | |
| "name" : "https://gbd.iti.kit.edu/file/26f66f5e5c1f85c9383cf851d28c9dcc/", | |
| "time" : 11453 | |
| }, { | |
| "variables" : 38383, | |
| "clauses" : 137559, | |
| "name" : "https://gbd.iti.kit.edu/file/1105d3e6f4eb84f94bc175994347963b/", | |
| "time" : 49563 | |
| }, { | |
| "variables" : 5307, | |
| "clauses" : 14626, | |
| "name" : "https://gbd.iti.kit.edu/file/5f89e528a8c3501359c24b83b8bec7f9/", | |
| "time" : 6304 | |
| }, { | |
| "variables" : 32252, | |
| "clauses" : 841934, | |
| "name" : "https://gbd.iti.kit.edu/file/0151ced92d88d7b46424ccf1d26d7716/", | |
| "time" : 47029 | |
| }, { | |
| "variables" : 12000, | |
| "clauses" : 50400, | |
| "name" : "https://gbd.iti.kit.edu/file/d8691c9450f283becfb2a551e5c60565/", | |
| "time" : 15974 | |
| }, { | |
| "variables" : 48917, | |
| "clauses" : 144691, | |
| "name" : "https://gbd.iti.kit.edu/file/065882225b28a15ec62af09030001ee5/", | |
| "time" : 53252 | |
| }, { | |
| "variables" : 17600, | |
| "clauses" : 215290, | |
| "name" : "https://gbd.iti.kit.edu/file/4e366e723d75fe39bf6db9a24ffb059b/", | |
| "time" : 16354 | |
| }, { | |
| "variables" : 21680, | |
| "clauses" : 77452, | |
| "name" : "https://gbd.iti.kit.edu/file/37e63d435f7979eaf79c8fedf8afdc5a/", | |
| "time" : 19851 | |
| }, { | |
| "variables" : 10000, | |
| "clauses" : 42000, | |
| "name" : "https://gbd.iti.kit.edu/file/d8754f715284ecb8b5423fea38733cee/", | |
| "time" : 9400 | |
| }, { | |
| "variables" : 28854, | |
| "clauses" : 103079, | |
| "name" : "https://gbd.iti.kit.edu/file/16a5ddbf28b64175999ef96e2fa8c6fd/", | |
| "time" : 29247 | |
| }, { | |
| "variables" : 30349, | |
| "clauses" : 762312, | |
| "name" : "https://gbd.iti.kit.edu/file/2c9820dcba2492b678d6c9b40d965b56/", | |
| "time" : 39749 | |
| }, { | |
| "variables" : 15233, | |
| "clauses" : 211949, | |
| "name" : "https://gbd.iti.kit.edu/file/4e36fd96262a32fd673e2b16b967993c/", | |
| "time" : 18739 | |
| }, { | |
| "variables" : 44058, | |
| "clauses" : 117720, | |
| "name" : "https://gbd.iti.kit.edu/file/5f8d22684f7e5b98493ee9daa609b47f/", | |
| "time" : 43199 | |
| }, { | |
| "variables" : 32733, | |
| "clauses" : 109177, | |
| "name" : "https://gbd.iti.kit.edu/file/37e6cf756d59143153ef3a0ff8804747/", | |
| "time" : 31371 | |
| }, { | |
| "variables" : 30299, | |
| "clauses" : 758206, | |
| "name" : "https://gbd.iti.kit.edu/file/3d4a54d37687f22a8a26b56b4592e2e2/", | |
| "time" : 37081 | |
| }, { | |
| "variables" : 27741, | |
| "clauses" : 647551, | |
| "name" : "https://gbd.iti.kit.edu/file/1106cefb8972be2896b97d8266bc219f/", | |
| "time" : 37128 | |
| }, { | |
| "variables" : 27992, | |
| "clauses" : 647084, | |
| "name" : "https://gbd.iti.kit.edu/file/065b141f5b24a1ea858f9e63bf13d0cf/", | |
| "time" : 37413 | |
| }, { | |
| "variables" : 28511, | |
| "clauses" : 671636, | |
| "name" : "https://gbd.iti.kit.edu/file/0152ba35c2942027426ebe4a074f5fdf/", | |
| "time" : 37783 | |
| }, { | |
| "variables" : 32599, | |
| "clauses" : 873196, | |
| "name" : "https://gbd.iti.kit.edu/file/3268e415d3a4b6b83b3d6457e143b763/", | |
| "time" : 39730 | |
| }, { | |
| "variables" : 30, | |
| "clauses" : 3137, | |
| "name" : "https://gbd.iti.kit.edu/file/0662df257be6c6d0691729cb23a17386/", | |
| "time" : 33 | |
| }, { | |
| "variables" : 2514, | |
| "clauses" : 10733, | |
| "name" : "https://gbd.iti.kit.edu/file/d8755fbffec770ee33cb4169b91b77d9/", | |
| "time" : 1974 | |
| }, { | |
| "variables" : 769, | |
| "clauses" : 4777, | |
| "name" : "https://gbd.iti.kit.edu/file/066813ab5f3b7b1cc6d2847c37f5fae7/", | |
| "time" : 575 | |
| }, { | |
| "variables" : 125, | |
| "clauses" : 51274, | |
| "name" : "https://gbd.iti.kit.edu/file/26f6f04b35d4c04710ef22df7922ea04/", | |
| "time" : 84 | |
| }, { | |
| "variables" : 8591, | |
| "clauses" : 65322, | |
| "name" : "https://gbd.iti.kit.edu/file/d87734c5e82a7ab0ea4e21fdcaad81f1/", | |
| "time" : 7404 | |
| }, { | |
| "variables" : 3438, | |
| "clauses" : 9334, | |
| "name" : "https://gbd.iti.kit.edu/file/d87895a8a3f808e52b42bd22c6cd419d/", | |
| "time" : 2753 | |
| }, { | |
| "variables" : 3531, | |
| "clauses" : 9788, | |
| "name" : "https://gbd.iti.kit.edu/file/16a67ab2825f9da74fe2187d670fd660/", | |
| "time" : 4438 | |
| }, { | |
| "variables" : 3194, | |
| "clauses" : 11211, | |
| "name" : "https://gbd.iti.kit.edu/file/3d4be5a280acbde7f70e4d7c03d7b04e/", | |
| "time" : 4102 | |
| }, { | |
| "variables" : 28489, | |
| "clauses" : 99584, | |
| "name" : "https://gbd.iti.kit.edu/file/37e98fa585be62095e17ad5c36d6f739/", | |
| "time" : 27574 | |
| }, { | |
| "variables" : 20869, | |
| "clauses" : 389406, | |
| "name" : "https://gbd.iti.kit.edu/file/0668d86f91d0e8aeea2e3fe722047363/", | |
| "time" : 26067 | |
| }, { | |
| "variables" : 2454, | |
| "clauses" : 6627, | |
| "name" : "https://gbd.iti.kit.edu/file/3d51d3ed03b01a567dc132041935a5e5/", | |
| "time" : 3188 | |
| }, { | |
| "variables" : 60, | |
| "clauses" : 5340, | |
| "name" : "https://gbd.iti.kit.edu/file/3d5818c023a1a5fa203c29943e175f41/", | |
| "time" : 101 | |
| }, { | |
| "variables" : 40177, | |
| "clauses" : 140996, | |
| "name" : "https://gbd.iti.kit.edu/file/3269bb8df0051eae9abcd150b065242d/", | |
| "time" : 38997 | |
| }, { | |
| "variables" : 19493, | |
| "clauses" : 346438, | |
| "name" : "https://gbd.iti.kit.edu/file/d87b6052cdeef61cef0eafad77d2d33a/", | |
| "time" : 26446 | |
| }, { | |
| "variables" : 24778, | |
| "clauses" : 517103, | |
| "name" : "https://gbd.iti.kit.edu/file/4e3a8bea49cd47d982df6ce4081b1119/", | |
| "time" : 36723 | |
| }, { | |
| "variables" : 29674, | |
| "clauses" : 714379, | |
| "name" : "https://gbd.iti.kit.edu/file/5f8d885d13a5605279532a8e7dfb9cbe/", | |
| "time" : 46699 | |
| }, { | |
| "variables" : 28645, | |
| "clauses" : 676757, | |
| "name" : "https://gbd.iti.kit.edu/file/26f90e183a60e0571fc50bbff53e9026/", | |
| "time" : 46274 | |
| }, { | |
| "variables" : 49508, | |
| "clauses" : 140091, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca078e0c97758850af51ed9a6a41991/", | |
| "time" : 55486 | |
| }, { | |
| "variables" : 174, | |
| "clauses" : 16458, | |
| "name" : "https://gbd.iti.kit.edu/file/26fbd274abc5e602c85a592073de98fb/", | |
| "time" : 1036 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87568, | |
| "name" : "https://gbd.iti.kit.edu/file/d87b710078b8fa953b5756ce2189ea75/", | |
| "time" : 29740 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 1800, | |
| "name" : "https://gbd.iti.kit.edu/file/26fdd7d81b17ab84d6a8b665654447f0/", | |
| "time" : 1583 | |
| }, { | |
| "variables" : 6000, | |
| "clauses" : 25602, | |
| "name" : "https://gbd.iti.kit.edu/file/5f91888f411f4934f9e836f7ec1d4153/", | |
| "time" : 8122 | |
| }, { | |
| "variables" : 27214, | |
| "clauses" : 617529, | |
| "name" : "https://gbd.iti.kit.edu/file/16a990450028e49aa903141fe63a6440/", | |
| "time" : 43246 | |
| }, { | |
| "variables" : 300, | |
| "clauses" : 12506, | |
| "name" : "https://gbd.iti.kit.edu/file/26ff89388c9b8eb6c8c83ecca6e7b869/", | |
| "time" : 1455 | |
| }, { | |
| "variables" : 1000, | |
| "clauses" : 20516, | |
| "name" : "https://gbd.iti.kit.edu/file/5f92ced2a3df797d90bd17204c54a5d1/", | |
| "time" : 2725 | |
| }, { | |
| "variables" : 2243, | |
| "clauses" : 29451, | |
| "name" : "https://gbd.iti.kit.edu/file/2709fc2279d361c2b19e36522c239965/", | |
| "time" : 2696 | |
| }, { | |
| "variables" : 31094, | |
| "clauses" : 791029, | |
| "name" : "https://gbd.iti.kit.edu/file/0154182ac2508df34a7bf7120a368e70/", | |
| "time" : 54190 | |
| }, { | |
| "variables" : 28916, | |
| "clauses" : 696301, | |
| "name" : "https://gbd.iti.kit.edu/file/110abea2cac57d734683619f799bf18a/", | |
| "time" : 49943 | |
| }, { | |
| "variables" : 28490, | |
| "clauses" : 665943, | |
| "name" : "https://gbd.iti.kit.edu/file/37eab74b5d5e6bbe0f1124156daabfc4/", | |
| "time" : 43348 | |
| }, { | |
| "variables" : 19614, | |
| "clauses" : 62140, | |
| "name" : "https://gbd.iti.kit.edu/file/16ad0f4e6759ead8d0cff5349f0136a2/", | |
| "time" : 21712 | |
| }, { | |
| "variables" : 33334, | |
| "clauses" : 908303, | |
| "name" : "https://gbd.iti.kit.edu/file/066ade1d9e5bede84a078012ee14fdc5/", | |
| "time" : 52566 | |
| }, { | |
| "variables" : 15562, | |
| "clauses" : 252785, | |
| "name" : "https://gbd.iti.kit.edu/file/5f96425c86fee94b2c04f76a99fa360b/", | |
| "time" : 17227 | |
| }, { | |
| "variables" : 28089, | |
| "clauses" : 649815, | |
| "name" : "https://gbd.iti.kit.edu/file/4e3ed6a8b1e5e514fdb1094e09bbe7b7/", | |
| "time" : 46918 | |
| }, { | |
| "variables" : 23744, | |
| "clauses" : 479543, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca324f3b34c0f206adfdab6bd334e39/", | |
| "time" : 32554 | |
| }, { | |
| "variables" : 280, | |
| "clauses" : 11766, | |
| "name" : "https://gbd.iti.kit.edu/file/5f97e6d9722ccf079cf2f7edb5802009/", | |
| "time" : 1487 | |
| }, { | |
| "variables" : 33651, | |
| "clauses" : 922200, | |
| "name" : "https://gbd.iti.kit.edu/file/326bc28d1a2b4c47b10564b37da358d9/", | |
| "time" : 55464 | |
| }, { | |
| "variables" : 7383, | |
| "clauses" : 24320, | |
| "name" : "https://gbd.iti.kit.edu/file/16afc4779f2d718b64d7309da9f10921/", | |
| "time" : 9196 | |
| }, { | |
| "variables" : 8800, | |
| "clauses" : 80265, | |
| "name" : "https://gbd.iti.kit.edu/file/015a78f0b46546a98970be8f3101443c/", | |
| "time" : 14144 | |
| }, { | |
| "variables" : 38376, | |
| "clauses" : 1162573, | |
| "name" : "https://gbd.iti.kit.edu/file/3d5c1f2cf68dc70f0382e350952ed44d/", | |
| "time" : 56968 | |
| }, { | |
| "variables" : 120, | |
| "clauses" : 10468, | |
| "name" : "https://gbd.iti.kit.edu/file/015a8c86d53869abb26f9dbe4a5f1e54/", | |
| "time" : 280 | |
| }, { | |
| "variables" : 220, | |
| "clauses" : 1145, | |
| "name" : "https://gbd.iti.kit.edu/file/01653db16d6cedc27f5314d680efc055/", | |
| "time" : 802 | |
| }, { | |
| "variables" : 7089, | |
| "clauses" : 121197, | |
| "name" : "https://gbd.iti.kit.edu/file/326d2f05b98c9f3d14112c6bc07da792/", | |
| "time" : 8680 | |
| }, { | |
| "variables" : 31607, | |
| "clauses" : 814868, | |
| "name" : "https://gbd.iti.kit.edu/file/d87f5262b254be96c8320f574cd7014d/", | |
| "time" : 44366 | |
| }, { | |
| "variables" : 140, | |
| "clauses" : 69060, | |
| "name" : "https://gbd.iti.kit.edu/file/01657386753a1369dd286a3fee9062e4/", | |
| "time" : 172 | |
| }, { | |
| "variables" : 26254, | |
| "clauses" : 575513, | |
| "name" : "https://gbd.iti.kit.edu/file/37ece64f301544cd9cabf192fe6b569e/", | |
| "time" : 33705 | |
| }, { | |
| "variables" : 892, | |
| "clauses" : 3006, | |
| "name" : "https://gbd.iti.kit.edu/file/37ef650fc84423091eab84282d2a9b26/", | |
| "time" : 972 | |
| }, { | |
| "variables" : 28366, | |
| "clauses" : 657372, | |
| "name" : "https://gbd.iti.kit.edu/file/270b05a537db9cf760caeec2f2d26102/", | |
| "time" : 34108 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 2800, | |
| "name" : "https://gbd.iti.kit.edu/file/270c8649f2d49726181205c0f90fefbe/", | |
| "time" : 890 | |
| }, { | |
| "variables" : 54, | |
| "clauses" : 171, | |
| "name" : "https://gbd.iti.kit.edu/file/270cc23b01cb0752f3c2f2bc77b0e9ad/", | |
| "time" : 95 | |
| }, { | |
| "variables" : 30867, | |
| "clauses" : 92735, | |
| "name" : "https://gbd.iti.kit.edu/file/5f9c3750ba6e40479eca39b22337ced0/", | |
| "time" : 35091 | |
| }, { | |
| "variables" : 26965, | |
| "clauses" : 607578, | |
| "name" : "https://gbd.iti.kit.edu/file/4e44a6c8d38bad7bc4cafcbe47a6670a/", | |
| "time" : 39103 | |
| }, { | |
| "variables" : 24349, | |
| "clauses" : 497531, | |
| "name" : "https://gbd.iti.kit.edu/file/3d5f95dec9ec467794e8571eb0ef2adb/", | |
| "time" : 36467 | |
| }, { | |
| "variables" : 26862, | |
| "clauses" : 593951, | |
| "name" : "https://gbd.iti.kit.edu/file/16b0ced3c8f00ac803d8032bbfd260b7/", | |
| "time" : 46383 | |
| }, { | |
| "variables" : 27786, | |
| "clauses" : 638444, | |
| "name" : "https://gbd.iti.kit.edu/file/066cc2796adfff0382fed7ae88d5b41d/", | |
| "time" : 46742 | |
| }, { | |
| "variables" : 10991, | |
| "clauses" : 179985, | |
| "name" : "https://gbd.iti.kit.edu/file/270df61b01e7496ee36e4a70a5a6a7c0/", | |
| "time" : 18280 | |
| }, { | |
| "variables" : 64159, | |
| "clauses" : 211975, | |
| "name" : "https://gbd.iti.kit.edu/file/110af2afd3e89094cf05319de8d0cb46/", | |
| "time" : 68010 | |
| }, { | |
| "variables" : 27903, | |
| "clauses" : 643192, | |
| "name" : "https://gbd.iti.kit.edu/file/d882812ec930f35b5f44f7bb6e50a4de/", | |
| "time" : 44560 | |
| }, { | |
| "variables" : 530, | |
| "clauses" : 11192, | |
| "name" : "https://gbd.iti.kit.edu/file/1110363d1b2dd5f19b7446a62981ca59/", | |
| "time" : 1126 | |
| }, { | |
| "variables" : 32084, | |
| "clauses" : 112450, | |
| "name" : "https://gbd.iti.kit.edu/file/37f109b243eb881f4befaf78471c71aa/", | |
| "time" : 40942 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 1800, | |
| "name" : "https://gbd.iti.kit.edu/file/111223e43c8e96f04a5cd23c3b3d452b/", | |
| "time" : 1679 | |
| }, { | |
| "variables" : 27785, | |
| "clauses" : 640439, | |
| "name" : "https://gbd.iti.kit.edu/file/326df0d2db2b36e9fcc4bf0605a7080d/", | |
| "time" : 44910 | |
| }, { | |
| "variables" : 2000, | |
| "clauses" : 40000, | |
| "name" : "https://gbd.iti.kit.edu/file/2724e2234d22e9cc04a6a43c2544bd41/", | |
| "time" : 5559 | |
| }, { | |
| "variables" : 224, | |
| "clauses" : 9715, | |
| "name" : "https://gbd.iti.kit.edu/file/27256daabb0a0817e9387e5a13885fd0/", | |
| "time" : 1093 | |
| }, { | |
| "variables" : 4662, | |
| "clauses" : 16112, | |
| "name" : "https://gbd.iti.kit.edu/file/327168a5b395a1f9ceb6c74ad4ca58db/", | |
| "time" : 5810 | |
| }, { | |
| "variables" : 4128, | |
| "clauses" : 126564, | |
| "name" : "https://gbd.iti.kit.edu/file/1113541da043983ac674e70d62f3aab6/", | |
| "time" : 5139 | |
| }, { | |
| "variables" : 600, | |
| "clauses" : 2520, | |
| "name" : "https://gbd.iti.kit.edu/file/11135f9daae702f2c2331c9b24760dec/", | |
| "time" : 729 | |
| }, { | |
| "variables" : 28787, | |
| "clauses" : 679987, | |
| "name" : "https://gbd.iti.kit.edu/file/5f9e9f0465dd958302f012f1e368ffe3/", | |
| "time" : 46452 | |
| }, { | |
| "variables" : 29254, | |
| "clauses" : 97456, | |
| "name" : "https://gbd.iti.kit.edu/file/066d6a47dfd9648d913ba8dbce722d75/", | |
| "time" : 34690 | |
| }, { | |
| "variables" : 32603, | |
| "clauses" : 868628, | |
| "name" : "https://gbd.iti.kit.edu/file/01665130994f549bc94ea4b1e91111cd/", | |
| "time" : 55964 | |
| }, { | |
| "variables" : 14896, | |
| "clauses" : 153982, | |
| "name" : "https://gbd.iti.kit.edu/file/16b5ccee102406efd1924d8f1c7a1cc6/", | |
| "time" : 23040 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 2800, | |
| "name" : "https://gbd.iti.kit.edu/file/066f7dc6f15dfe89172f4b32e50ac826/", | |
| "time" : 803 | |
| }, { | |
| "variables" : 28423, | |
| "clauses" : 672236, | |
| "name" : "https://gbd.iti.kit.edu/file/4e461ced58df623f153f61e32655cc6c/", | |
| "time" : 49118 | |
| }, { | |
| "variables" : 22022, | |
| "clauses" : 171614, | |
| "name" : "https://gbd.iti.kit.edu/file/d88295f02603eeb05099686b4cc6bd82/", | |
| "time" : 25111 | |
| }, { | |
| "variables" : 31634, | |
| "clauses" : 819661, | |
| "name" : "https://gbd.iti.kit.edu/file/3d648f6a5365740fcc37279dd6d8501e/", | |
| "time" : 53577 | |
| }, { | |
| "variables" : 4740, | |
| "clauses" : 37893, | |
| "name" : "https://gbd.iti.kit.edu/file/3d6978ed5a15b6338e355146202518ed/", | |
| "time" : 5376 | |
| }, { | |
| "variables" : 27065, | |
| "clauses" : 54607, | |
| "name" : "https://gbd.iti.kit.edu/file/0167ead7da1e981805564ca981f64bea/", | |
| "time" : 22939 | |
| }, { | |
| "variables" : 5590, | |
| "clauses" : 55135, | |
| "name" : "https://gbd.iti.kit.edu/file/3d6d0acfaf4df8e3f282b580d97af17c/", | |
| "time" : 7895 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87593, | |
| "name" : "https://gbd.iti.kit.edu/file/0671f3013bf168f4660edfb4b40fbfa5/", | |
| "time" : 25376 | |
| }, { | |
| "variables" : 990, | |
| "clauses" : 3582, | |
| "name" : "https://gbd.iti.kit.edu/file/06767f7b8e23fd24f6df74fefef9c48c/", | |
| "time" : 1170 | |
| }, { | |
| "variables" : 40, | |
| "clauses" : 176, | |
| "name" : "https://gbd.iti.kit.edu/file/067dc6945c4aec1c2bc1fdc2e5819124/", | |
| "time" : 34 | |
| }, { | |
| "variables" : 5333, | |
| "clauses" : 18462, | |
| "name" : "https://gbd.iti.kit.edu/file/016fa607917cff1ece5bd5c624a49491/", | |
| "time" : 5728 | |
| }, { | |
| "variables" : 90, | |
| "clauses" : 1917, | |
| "name" : "https://gbd.iti.kit.edu/file/0684c9b8439112b0e3202dc1f13bae65/", | |
| "time" : 270 | |
| }, { | |
| "variables" : 5000, | |
| "clauses" : 21250, | |
| "name" : "https://gbd.iti.kit.edu/file/3d728011fe9549138477d202bfdce1d7/", | |
| "time" : 6994 | |
| }, { | |
| "variables" : 810, | |
| "clauses" : 2931, | |
| "name" : "https://gbd.iti.kit.edu/file/3d76cf1a55ac6948d29e2e7f6038b3b7/", | |
| "time" : 751 | |
| }, { | |
| "variables" : 27042, | |
| "clauses" : 609174, | |
| "name" : "https://gbd.iti.kit.edu/file/272632e23471f421a4e42910c3a51452/", | |
| "time" : 42466 | |
| }, { | |
| "variables" : 300, | |
| "clauses" : 1350, | |
| "name" : "https://gbd.iti.kit.edu/file/3d781cd4e6db7d1bfbba791698b1d212/", | |
| "time" : 853 | |
| }, { | |
| "variables" : 31672, | |
| "clauses" : 827201, | |
| "name" : "https://gbd.iti.kit.edu/file/37f896f9a729836613a3620220b540c9/", | |
| "time" : 54346 | |
| }, { | |
| "variables" : 30045, | |
| "clauses" : 741975, | |
| "name" : "https://gbd.iti.kit.edu/file/3272010a1f70fc7f851e49492bdb96cf/", | |
| "time" : 38765 | |
| }, { | |
| "variables" : 30137, | |
| "clauses" : 744532, | |
| "name" : "https://gbd.iti.kit.edu/file/11159e75cc3c7245ddd8879d1cc2260d/", | |
| "time" : 46098 | |
| }, { | |
| "variables" : 31501, | |
| "clauses" : 809528, | |
| "name" : "https://gbd.iti.kit.edu/file/5fa090bb7cf25e0f1fc04732e131e420/", | |
| "time" : 44533 | |
| }, { | |
| "variables" : 25773, | |
| "clauses" : 551974, | |
| "name" : "https://gbd.iti.kit.edu/file/d885a6911af76350d50bc924f687dae5/", | |
| "time" : 32856 | |
| }, { | |
| "variables" : 300, | |
| "clauses" : 1400, | |
| "name" : "https://gbd.iti.kit.edu/file/d8866f96b2799cdcb25d558c809727a1/", | |
| "time" : 1027 | |
| }, { | |
| "variables" : 95456, | |
| "clauses" : 477186, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca513f98cb00bf9ff0ff1f8a9caaf78/", | |
| "time" : 129434 | |
| }, { | |
| "variables" : 300, | |
| "clauses" : 1400, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca61e3f3d1a844f229071a6cd120f6b/", | |
| "time" : 943 | |
| }, { | |
| "variables" : 26256, | |
| "clauses" : 77806, | |
| "name" : "https://gbd.iti.kit.edu/file/3d790a6e900932248da26ae6d3374eda/", | |
| "time" : 30500 | |
| }, { | |
| "variables" : 29855, | |
| "clauses" : 731187, | |
| "name" : "https://gbd.iti.kit.edu/file/4e4a3b62544acec4a6b1f5173597a91f/", | |
| "time" : 47780 | |
| }, { | |
| "variables" : 22427, | |
| "clauses" : 440107, | |
| "name" : "https://gbd.iti.kit.edu/file/37f8d8d51728e93d9341b80ab654d853/", | |
| "time" : 31751 | |
| }, { | |
| "variables" : 6000, | |
| "clauses" : 25200, | |
| "name" : "https://gbd.iti.kit.edu/file/3d7ab8c343529787eea949878de6ed83/", | |
| "time" : 8084 | |
| }, { | |
| "variables" : 31118, | |
| "clauses" : 790689, | |
| "name" : "https://gbd.iti.kit.edu/file/068594cad63ad63966d00272acbe72f7/", | |
| "time" : 54062 | |
| }, { | |
| "variables" : 24338, | |
| "clauses" : 505748, | |
| "name" : "https://gbd.iti.kit.edu/file/5fa379c4558dea282d4777e01fb690e4/", | |
| "time" : 38339 | |
| }, { | |
| "variables" : 238, | |
| "clauses" : 15812, | |
| "name" : "https://gbd.iti.kit.edu/file/06872e73223dc74c76b06f37a185dc22/", | |
| "time" : 835 | |
| }, { | |
| "variables" : 25332, | |
| "clauses" : 536739, | |
| "name" : "https://gbd.iti.kit.edu/file/272d1dba6fb94a0b175f239f789e6d3a/", | |
| "time" : 39849 | |
| }, { | |
| "variables" : 41305, | |
| "clauses" : 154997, | |
| "name" : "https://gbd.iti.kit.edu/file/327479b90e9ab90de5964edd2bafb274/", | |
| "time" : 53382 | |
| }, { | |
| "variables" : 27353, | |
| "clauses" : 623184, | |
| "name" : "https://gbd.iti.kit.edu/file/112077ee2bc8658d7d17a760ed5b47fd/", | |
| "time" : 46890 | |
| }, { | |
| "variables" : 26904, | |
| "clauses" : 604703, | |
| "name" : "https://gbd.iti.kit.edu/file/0174593b6652936010405e3f4b6799c1/", | |
| "time" : 45806 | |
| }, { | |
| "variables" : 17644, | |
| "clauses" : 297800, | |
| "name" : "https://gbd.iti.kit.edu/file/3d7d705c7ef4bbd3fb23c0b526282057/", | |
| "time" : 23049 | |
| }, { | |
| "variables" : 6000, | |
| "clauses" : 25602, | |
| "name" : "https://gbd.iti.kit.edu/file/327508b1be702844d898c9df3c0abc5e/", | |
| "time" : 8476 | |
| }, { | |
| "variables" : 28489, | |
| "clauses" : 99744, | |
| "name" : "https://gbd.iti.kit.edu/file/37fab6091c16d340d29bd58e3af981c9/", | |
| "time" : 31825 | |
| }, { | |
| "variables" : 851, | |
| "clauses" : 2702, | |
| "name" : "https://gbd.iti.kit.edu/file/37fde221cfa265eb7ec2c221e5272686/", | |
| "time" : 891 | |
| }, { | |
| "variables" : 26093, | |
| "clauses" : 565570, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca61ecfe27f48cc95d3cb79ad872dac/", | |
| "time" : 41514 | |
| }, { | |
| "variables" : 350, | |
| "clauses" : 1491, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca75150c25258e862e346ca1dfcd121/", | |
| "time" : 1254 | |
| }, { | |
| "variables" : 18000, | |
| "clauses" : 75600, | |
| "name" : "https://gbd.iti.kit.edu/file/27308296c1433137bfa8ff5191198a22/", | |
| "time" : 25035 | |
| }, { | |
| "variables" : 27233, | |
| "clauses" : 609846, | |
| "name" : "https://gbd.iti.kit.edu/file/4e4aa7e883a02a6d6330a668ac9a1a50/", | |
| "time" : 44407 | |
| }, { | |
| "variables" : 27762, | |
| "clauses" : 639031, | |
| "name" : "https://gbd.iti.kit.edu/file/5fa5188c5da7a741be5825103f46b85d/", | |
| "time" : 36772 | |
| }, { | |
| "variables" : 26326, | |
| "clauses" : 581430, | |
| "name" : "https://gbd.iti.kit.edu/file/0177419016ca9d3abad0c15998bdf72f/", | |
| "time" : 40387 | |
| }, { | |
| "variables" : 23089, | |
| "clauses" : 456984, | |
| "name" : "https://gbd.iti.kit.edu/file/3d7f93399d87d72e77a3ea32e989afb5/", | |
| "time" : 36023 | |
| }, { | |
| "variables" : 75528, | |
| "clauses" : 272784, | |
| "name" : "https://gbd.iti.kit.edu/file/d8886b003c8c690a8c481c88dc87947e/", | |
| "time" : 90223 | |
| }, { | |
| "variables" : 11674, | |
| "clauses" : 167554, | |
| "name" : "https://gbd.iti.kit.edu/file/273d42b3d97294b660745c7bc632474e/", | |
| "time" : 21453 | |
| }, { | |
| "variables" : 29483, | |
| "clauses" : 714214, | |
| "name" : "https://gbd.iti.kit.edu/file/068f2d23820541fe4eaebfb072bd6cbb/", | |
| "time" : 49356 | |
| }, { | |
| "variables" : 190, | |
| "clauses" : 3268, | |
| "name" : "https://gbd.iti.kit.edu/file/3d82acd0c9d3f9516f909727cc0302ae/", | |
| "time" : 628 | |
| }, { | |
| "variables" : 300, | |
| "clauses" : 1278, | |
| "name" : "https://gbd.iti.kit.edu/file/d88a936d2735c325fbcd5d96550b4a8d/", | |
| "time" : 697 | |
| }, { | |
| "variables" : 25924, | |
| "clauses" : 563188, | |
| "name" : "https://gbd.iti.kit.edu/file/32757af75cc35fa4537819228f83da12/", | |
| "time" : 38773 | |
| }, { | |
| "variables" : 26164, | |
| "clauses" : 573925, | |
| "name" : "https://gbd.iti.kit.edu/file/37fde45519c5dbc5f57a218bcd13ec07/", | |
| "time" : 43112 | |
| }, { | |
| "variables" : 28054, | |
| "clauses" : 652991, | |
| "name" : "https://gbd.iti.kit.edu/file/5fa536224812ca4b9c5ed627229e7a7d/", | |
| "time" : 35436 | |
| }, { | |
| "variables" : 25848, | |
| "clauses" : 564905, | |
| "name" : "https://gbd.iti.kit.edu/file/4e4c92376ad0898b884b50117356ba51/", | |
| "time" : 42477 | |
| }, { | |
| "variables" : 39434, | |
| "clauses" : 887706, | |
| "name" : "https://gbd.iti.kit.edu/file/2ca82d36bf188d2078831a1e82e9aac0/", | |
| "time" : 52228 | |
| }, { | |
| "variables" : 90, | |
| "clauses" : 1917, | |
| "name" : "https://gbd.iti.kit.edu/file/4e57d0c6441705b624863ce57ce6aa09/", | |
| "time" : 159 | |
| }, { | |
| "variables" : 350, | |
| "clauses" : 1225, | |
| "name" : "https://gbd.iti.kit.edu/file/4e5bd654abc6d650ab33948aea178d7f/", | |
| "time" : 1146 | |
| }, { | |
| "variables" : 3486, | |
| "clauses" : 8496, | |
| "name" : "https://gbd.iti.kit.edu/file/5fa640170c8d2897694ddbdb37e6dedf/", | |
| "time" : 3877 | |
| }, { | |
| "variables" : 31951, | |
| "clauses" : 96161, | |
| "name" : "https://gbd.iti.kit.edu/file/d88baaa735c644728b0d0cb3f015708b/", | |
| "time" : 36312 | |
| }, { | |
| "variables" : 169, | |
| "clauses" : 1183, | |
| "name" : "https://gbd.iti.kit.edu/file/d88c6afc13cdad0e2c8371a879692b39/", | |
| "time" : 443 | |
| }, { | |
| "variables" : 25801, | |
| "clauses" : 559599, | |
| "name" : "https://gbd.iti.kit.edu/file/0696cb4f18fd63cc94f319fab92119e5/", | |
| "time" : 37326 | |
| }, { | |
| "variables" : 30855, | |
| "clauses" : 774795, | |
| "name" : "https://gbd.iti.kit.edu/file/3d848c52b1cedeafd926ecb05bfb53c0/", | |
| "time" : 43794 | |
| }, { | |
| "variables" : 27140, | |
| "clauses" : 604165, | |
| "name" : "https://gbd.iti.kit.edu/file/32769a654dca0c00cf3f8c9b44f26eba/", | |
| "time" : 41697 | |
| }, { | |
| "variables" : 30031, | |
| "clauses" : 105359, | |
| "name" : "https://gbd.iti.kit.edu/file/2cb0f49bce0ff101e94fc42e5a32d6bd/", | |
| "time" : 34123 | |
| }, { | |
| "variables" : 27967, | |
| "clauses" : 643848, | |
| "name" : "https://gbd.iti.kit.edu/file/01796eb1fc5b82e2d36e60dacb631250/", | |
| "time" : 49224 | |
| }, { | |
| "variables" : 2604, | |
| "clauses" : 36994, | |
| "name" : "https://gbd.iti.kit.edu/file/017bba0f995e6d9921253e5a59521435/", | |
| "time" : 3834 | |
| }, { | |
| "variables" : 26049, | |
| "clauses" : 571893, | |
| "name" : "https://gbd.iti.kit.edu/file/5fa7a3a2f8264ee35fbe9dcebbbb5f76/", | |
| "time" : 36743 | |
| }, { | |
| "variables" : 30577, | |
| "clauses" : 766965, | |
| "name" : "https://gbd.iti.kit.edu/file/3800fd090616b24aa756866059bcd155/", | |
| "time" : 44968 | |
| }, { | |
| "variables" : 400, | |
| "clauses" : 1700, | |
| "name" : "https://gbd.iti.kit.edu/file/5faaff78f73a7f8673efedeffd217d4f/", | |
| "time" : 1556 | |
| }, { | |
| "variables" : 637, | |
| "clauses" : 1468, | |
| "name" : "https://gbd.iti.kit.edu/file/5fae97fdc8208de522104f5191cd7ad1/", | |
| "time" : 431 | |
| }, { | |
| "variables" : 13692, | |
| "clauses" : 217179, | |
| "name" : "https://gbd.iti.kit.edu/file/327a32cb6e2acec0aaca022f2b37356c/", | |
| "time" : 17200 | |
| }, { | |
| "variables" : 550, | |
| "clauses" : 2425, | |
| "name" : "https://gbd.iti.kit.edu/file/5fb19e3a8ba7fa67d1b4d39e4e6cb240/", | |
| "time" : 605 | |
| }, { | |
| "variables" : 560, | |
| "clauses" : 2380, | |
| "name" : "https://gbd.iti.kit.edu/file/327a978b5e3d3b9b66abdc916d2180ab/", | |
| "time" : 697 | |
| }, { | |
| "variables" : 32022, | |
| "clauses" : 838062, | |
| "name" : "https://gbd.iti.kit.edu/file/273e7ea2f180bc1d45871ea272b1ccc4/", | |
| "time" : 46736 | |
| }, { | |
| "variables" : 29855, | |
| "clauses" : 730808, | |
| "name" : "https://gbd.iti.kit.edu/file/d88cbcbb459a21af00216b41441b2bba/", | |
| "time" : 40942 | |
| }, { | |
| "variables" : 250, | |
| "clauses" : 1250, | |
| "name" : "https://gbd.iti.kit.edu/file/6a49dbdf0f8a8e373a7b093e3e0d1f26/", | |
| "time" : 492 | |
| }, { | |
| "variables" : 4254, | |
| "clauses" : 11537, | |
| "name" : "https://gbd.iti.kit.edu/file/d84fc81b50b0f440f001e6de6c8f7368/", | |
| "time" : 3050 | |
| }, { | |
| "variables" : 2421, | |
| "clauses" : 20443, | |
| "name" : "https://gbd.iti.kit.edu/file/5f73d11d8fc79ea749597eb76c6a802e/", | |
| "time" : 1903 | |
| }, { | |
| "variables" : 2200, | |
| "clauses" : 9086, | |
| "name" : "https://gbd.iti.kit.edu/file/169b832e8ad5102801bc5390663b0a81/", | |
| "time" : 1757 | |
| }, { | |
| "variables" : 7467, | |
| "clauses" : 21421, | |
| "name" : "https://gbd.iti.kit.edu/file/0b548243045e74982b57a53b3fdeaede/", | |
| "time" : 5987 | |
| }, { | |
| "variables" : 500, | |
| "clauses" : 1750, | |
| "name" : "https://gbd.iti.kit.edu/file/5f74904d384778c577e32052623f2661/", | |
| "time" : 1207 | |
| }, { | |
| "variables" : 17221, | |
| "clauses" : 51474, | |
| "name" : "https://gbd.iti.kit.edu/file/37d91934e9534f7c2f770adc1a651458/", | |
| "time" : 11290 | |
| }, { | |
| "variables" : 220, | |
| "clauses" : 9467, | |
| "name" : "https://gbd.iti.kit.edu/file/0b54b2a921d3ead9cced275c24bc8668/", | |
| "time" : 732 | |
| }, { | |
| "variables" : 4128, | |
| "clauses" : 126580, | |
| "name" : "https://gbd.iti.kit.edu/file/5f7f856de96da47473f4400f5cb46a3a/", | |
| "time" : 4453 | |
| }, { | |
| "variables" : 22254, | |
| "clauses" : 83318, | |
| "name" : "https://gbd.iti.kit.edu/file/1be909b58fd0fb4efbbd35a2c84831ef/", | |
| "time" : 19819 | |
| }, { | |
| "variables" : 23582, | |
| "clauses" : 471906, | |
| "name" : "https://gbd.iti.kit.edu/file/d851a48646a43f5d50ed2f78f32be193/", | |
| "time" : 22300 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87776, | |
| "name" : "https://gbd.iti.kit.edu/file/07aeafc4ee93bb832fa134d4f5971cf6/", | |
| "time" : 19781 | |
| }, { | |
| "variables" : 630, | |
| "clauses" : 2280, | |
| "name" : "https://gbd.iti.kit.edu/file/07b22dd6ccdd07fa12548656c4ea97a6/", | |
| "time" : 684 | |
| }, { | |
| "variables" : 25829, | |
| "clauses" : 553336, | |
| "name" : "https://gbd.iti.kit.edu/file/03c41956324a467d4f265ee58af51f25/", | |
| "time" : 26653 | |
| }, { | |
| "variables" : 7935, | |
| "clauses" : 22570, | |
| "name" : "https://gbd.iti.kit.edu/file/d8583cdb99aa7adeecf1e9033fa86261/", | |
| "time" : 6292 | |
| }, { | |
| "variables" : 25077, | |
| "clauses" : 529541, | |
| "name" : "https://gbd.iti.kit.edu/file/6a4fc917dfa55957fd5f5549384c6069/", | |
| "time" : 27963 | |
| }, { | |
| "variables" : 480, | |
| "clauses" : 2040, | |
| "name" : "https://gbd.iti.kit.edu/file/d85ca9deae350ae70db1a81ce80a3154/", | |
| "time" : 1459 | |
| }, { | |
| "variables" : 27830, | |
| "clauses" : 642746, | |
| "name" : "https://gbd.iti.kit.edu/file/4e2a3cd0836ea69de6df98b0344642e1/", | |
| "time" : 28119 | |
| }, { | |
| "variables" : 4959, | |
| "clauses" : 14017, | |
| "name" : "https://gbd.iti.kit.edu/file/4e2d735a79aa5ca641368724757a6786/", | |
| "time" : 4073 | |
| }, { | |
| "variables" : 29671, | |
| "clauses" : 714367, | |
| "name" : "https://gbd.iti.kit.edu/file/9c0481ebdba6addb9302aa745ed8fd2f/", | |
| "time" : 30799 | |
| }, { | |
| "variables" : 120, | |
| "clauses" : 10535, | |
| "name" : "https://gbd.iti.kit.edu/file/9c083ff62ba134e9cd222a512fded53b/", | |
| "time" : 183 | |
| }, { | |
| "variables" : 28078, | |
| "clauses" : 650955, | |
| "name" : "https://gbd.iti.kit.edu/file/169e4279304ae948428c0706270781f5/", | |
| "time" : 28045 | |
| }, { | |
| "variables" : 27961, | |
| "clauses" : 646239, | |
| "name" : "https://gbd.iti.kit.edu/file/5f809243de4d99e0119abb98f9cd2f1a/", | |
| "time" : 27810 | |
| }, { | |
| "variables" : 4584, | |
| "clauses" : 43390, | |
| "name" : "https://gbd.iti.kit.edu/file/169e8bcebaebcbb9ff2ba8233fea0dd3/", | |
| "time" : 3643 | |
| }, { | |
| "variables" : 15232, | |
| "clauses" : 147244, | |
| "name" : "https://gbd.iti.kit.edu/file/03c44a93577c98119dc498053888937a/", | |
| "time" : 14153 | |
| }, { | |
| "variables" : 2000, | |
| "clauses" : 8534, | |
| "name" : "https://gbd.iti.kit.edu/file/169f2359a69f617b164eb64d2245c6ab/", | |
| "time" : 1980 | |
| }, { | |
| "variables" : 20057, | |
| "clauses" : 60849, | |
| "name" : "https://gbd.iti.kit.edu/file/9c162333ef5c123acf4ee71ca909a450/", | |
| "time" : 14270 | |
| }, { | |
| "variables" : 98048, | |
| "clauses" : 293759, | |
| "name" : "https://gbd.iti.kit.edu/file/37dfb9d60131ccd4b6d5b2ac50ab6fb2/", | |
| "time" : 70777 | |
| }, { | |
| "variables" : 28069, | |
| "clauses" : 647269, | |
| "name" : "https://gbd.iti.kit.edu/file/d863c68c31de9033fb54a0190df02a0f/", | |
| "time" : 27814 | |
| }, { | |
| "variables" : 105, | |
| "clauses" : 36422, | |
| "name" : "https://gbd.iti.kit.edu/file/03c5fef8cb8957ecf687548c8d504d10/", | |
| "time" : 58 | |
| }, { | |
| "variables" : 500, | |
| "clauses" : 2000, | |
| "name" : "https://gbd.iti.kit.edu/file/03c7c131fc68f902620c24f5f28cd179/", | |
| "time" : 1332 | |
| }, { | |
| "variables" : 29626, | |
| "clauses" : 722079, | |
| "name" : "https://gbd.iti.kit.edu/file/4e32695d1bcd7dfc733ec2822458f59f/", | |
| "time" : 31938 | |
| }, { | |
| "variables" : 600, | |
| "clauses" : 2556, | |
| "name" : "https://gbd.iti.kit.edu/file/03cb9868146a1c420ba8e3b1b08865b8/", | |
| "time" : 384 | |
| }, { | |
| "variables" : 26243, | |
| "clauses" : 92072, | |
| "name" : "https://gbd.iti.kit.edu/file/16a14e055d12795a46915db84daf9794/", | |
| "time" : 20297 | |
| }, { | |
| "variables" : 29502, | |
| "clauses" : 714813, | |
| "name" : "https://gbd.iti.kit.edu/file/5f811e38a50492cd71628ae94325b709/", | |
| "time" : 32061 | |
| }, { | |
| "variables" : 105, | |
| "clauses" : 512, | |
| "name" : "https://gbd.iti.kit.edu/file/07b476c83150d3cb7e08f5d045e255ab/", | |
| "time" : 121 | |
| }, { | |
| "variables" : 28069, | |
| "clauses" : 650462, | |
| "name" : "https://gbd.iti.kit.edu/file/6a5212e70dee1799dfa4739a947078c2/", | |
| "time" : 29004 | |
| }, { | |
| "variables" : 27768, | |
| "clauses" : 641035, | |
| "name" : "https://gbd.iti.kit.edu/file/37e50dd510616d8a83eb838203fe640c/", | |
| "time" : 27258 | |
| }, { | |
| "variables" : 34678, | |
| "clauses" : 101319, | |
| "name" : "https://gbd.iti.kit.edu/file/4e32e5d9f532872ebb6462c47c902a53/", | |
| "time" : 26457 | |
| }, { | |
| "variables" : 21680, | |
| "clauses" : 77452, | |
| "name" : "https://gbd.iti.kit.edu/file/37e63d435f7979eaf79c8fedf8afdc5a/", | |
| "time" : 16539 | |
| }, { | |
| "variables" : 18477, | |
| "clauses" : 319087, | |
| "name" : "https://gbd.iti.kit.edu/file/9c163e9ec93a18189f34cf328c6edc43/", | |
| "time" : 18714 | |
| }, { | |
| "variables" : 17600, | |
| "clauses" : 215290, | |
| "name" : "https://gbd.iti.kit.edu/file/4e366e723d75fe39bf6db9a24ffb059b/", | |
| "time" : 12745 | |
| }, { | |
| "variables" : 30113, | |
| "clauses" : 739219, | |
| "name" : "https://gbd.iti.kit.edu/file/07b55eb389b521faf2ea347a14b68938/", | |
| "time" : 31131 | |
| }, { | |
| "variables" : 350, | |
| "clauses" : 1225, | |
| "name" : "https://gbd.iti.kit.edu/file/07b6f34060b07d837482bfc3f238b252/", | |
| "time" : 762 | |
| }, { | |
| "variables" : 27741, | |
| "clauses" : 647241, | |
| "name" : "https://gbd.iti.kit.edu/file/03cd587fe1f5eb6c6c10ede767571241/", | |
| "time" : 29373 | |
| }, { | |
| "variables" : 32733, | |
| "clauses" : 109177, | |
| "name" : "https://gbd.iti.kit.edu/file/37e6cf756d59143153ef3a0ff8804747/", | |
| "time" : 27378 | |
| }, { | |
| "variables" : 6381, | |
| "clauses" : 18078, | |
| "name" : "https://gbd.iti.kit.edu/file/07b8a0ca2372125b645a2fa257367ea9/", | |
| "time" : 5124 | |
| }, { | |
| "variables" : 31267, | |
| "clauses" : 800249, | |
| "name" : "https://gbd.iti.kit.edu/file/16a3ee772bef92e8defd2dfa2aaa65c4/", | |
| "time" : 33771 | |
| }, { | |
| "variables" : 29893, | |
| "clauses" : 732719, | |
| "name" : "https://gbd.iti.kit.edu/file/5f82183e1d7b1db15adaa42a33d49f64/", | |
| "time" : 32065 | |
| }, { | |
| "variables" : 150, | |
| "clauses" : 6506, | |
| "name" : "https://gbd.iti.kit.edu/file/07b9e86b020a209bd76474c4db8ab14d/", | |
| "time" : 289 | |
| }, { | |
| "variables" : 5307, | |
| "clauses" : 14626, | |
| "name" : "https://gbd.iti.kit.edu/file/5f89e528a8c3501359c24b83b8bec7f9/", | |
| "time" : 3898 | |
| }, { | |
| "variables" : 28489, | |
| "clauses" : 99584, | |
| "name" : "https://gbd.iti.kit.edu/file/37e98fa585be62095e17ad5c36d6f739/", | |
| "time" : 21327 | |
| }, { | |
| "variables" : 28854, | |
| "clauses" : 103079, | |
| "name" : "https://gbd.iti.kit.edu/file/16a5ddbf28b64175999ef96e2fa8c6fd/", | |
| "time" : 21417 | |
| }, { | |
| "variables" : 19493, | |
| "clauses" : 346521, | |
| "name" : "https://gbd.iti.kit.edu/file/16a677f8b27a896bf81a2650ddded49b/", | |
| "time" : 17333 | |
| }, { | |
| "variables" : 3531, | |
| "clauses" : 9788, | |
| "name" : "https://gbd.iti.kit.edu/file/16a67ab2825f9da74fe2187d670fd660/", | |
| "time" : 2601 | |
| }, { | |
| "variables" : 28406, | |
| "clauses" : 662641, | |
| "name" : "https://gbd.iti.kit.edu/file/9c1b153065b8d04c6f94592881e2ddf0/", | |
| "time" : 27780 | |
| }, { | |
| "variables" : 549, | |
| "clauses" : 2562, | |
| "name" : "https://gbd.iti.kit.edu/file/9c1d75473b437057fabffe88fbdff97a/", | |
| "time" : 392 | |
| }, { | |
| "variables" : 27214, | |
| "clauses" : 617529, | |
| "name" : "https://gbd.iti.kit.edu/file/16a990450028e49aa903141fe63a6440/", | |
| "time" : 27884 | |
| }, { | |
| "variables" : 19614, | |
| "clauses" : 62140, | |
| "name" : "https://gbd.iti.kit.edu/file/16ad0f4e6759ead8d0cff5349f0136a2/", | |
| "time" : 13184 | |
| }, { | |
| "variables" : 25833, | |
| "clauses" : 554230, | |
| "name" : "https://gbd.iti.kit.edu/file/9c2067aa41d627ebfda7c4742151b332/", | |
| "time" : 25060 | |
| }, { | |
| "variables" : 7383, | |
| "clauses" : 24320, | |
| "name" : "https://gbd.iti.kit.edu/file/16afc4779f2d718b64d7309da9f10921/", | |
| "time" : 6083 | |
| }, { | |
| "variables" : 29551, | |
| "clauses" : 152151, | |
| "name" : "https://gbd.iti.kit.edu/file/9c20fada8bf1fa54b8f49dc69080bf3f/", | |
| "time" : 20391 | |
| }, { | |
| "variables" : 3114, | |
| "clauses" : 8467, | |
| "name" : "https://gbd.iti.kit.edu/file/9c2583ea5334662bac721ff5b260f5cd/", | |
| "time" : 2333 | |
| }, { | |
| "variables" : 765, | |
| "clauses" : 28457, | |
| "name" : "https://gbd.iti.kit.edu/file/9c25951c5d39191e33e88a711b4c2d67/", | |
| "time" : 1013 | |
| }, { | |
| "variables" : 26862, | |
| "clauses" : 593951, | |
| "name" : "https://gbd.iti.kit.edu/file/16b0ced3c8f00ac803d8032bbfd260b7/", | |
| "time" : 27248 | |
| }, { | |
| "variables" : 14896, | |
| "clauses" : 153982, | |
| "name" : "https://gbd.iti.kit.edu/file/16b5ccee102406efd1924d8f1c7a1cc6/", | |
| "time" : 14245 | |
| }, { | |
| "variables" : 98746, | |
| "clauses" : 307346, | |
| "name" : "https://gbd.iti.kit.edu/file/9c2e721df8fabf9bbbae23910443ea4a/", | |
| "time" : 76968 | |
| }, { | |
| "variables" : 19247, | |
| "clauses" : 58383, | |
| "name" : "https://gbd.iti.kit.edu/file/9c2e734d6c0faeef8a89aa84436fc42d/", | |
| "time" : 12456 | |
| }, { | |
| "variables" : 3352, | |
| "clauses" : 29412, | |
| "name" : "https://gbd.iti.kit.edu/file/9c2f29599b7f105d5478735d244743f5/", | |
| "time" : 2453 | |
| }, { | |
| "variables" : 11529, | |
| "clauses" : 184143, | |
| "name" : "https://gbd.iti.kit.edu/file/9c30928725297bd1a262aed472805bac/", | |
| "time" : 11293 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 3500, | |
| "name" : "https://gbd.iti.kit.edu/file/9c31e46e6e7775284e7627a4cbcb1ad6/", | |
| "time" : 511 | |
| }, { | |
| "variables" : 324, | |
| "clauses" : 756, | |
| "name" : "https://gbd.iti.kit.edu/file/9c34300615109a8f111055a9b48c13d6/", | |
| "time" : 356 | |
| }, { | |
| "variables" : 80, | |
| "clauses" : 346, | |
| "name" : "https://gbd.iti.kit.edu/file/9c37d38895b75c2165b8995436fbbf47/", | |
| "time" : 75 | |
| }, { | |
| "variables" : 270, | |
| "clauses" : 5702, | |
| "name" : "https://gbd.iti.kit.edu/file/9c3880a6f00736c0d75e5b0f7088e11b/", | |
| "time" : 725 | |
| }, { | |
| "variables" : 29327, | |
| "clauses" : 714286, | |
| "name" : "https://gbd.iti.kit.edu/file/9c38868da621e9ee9d45ea88c604021f/", | |
| "time" : 30930 | |
| }, { | |
| "variables" : 41146, | |
| "clauses" : 143872, | |
| "name" : "https://gbd.iti.kit.edu/file/9c39127cfaa48caf6751c03282189317/", | |
| "time" : 31649 | |
| }, { | |
| "variables" : 31153, | |
| "clauses" : 800033, | |
| "name" : "https://gbd.iti.kit.edu/file/9c3a1b39e0a5a77a0bc88b0fc86c42ef/", | |
| "time" : 34169 | |
| }, { | |
| "variables" : 528, | |
| "clauses" : 5016, | |
| "name" : "https://gbd.iti.kit.edu/file/048a70da40ea4908c783b8314be2da97/", | |
| "time" : 391 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 1912, | |
| "name" : "https://gbd.iti.kit.edu/file/048ddbb09453a83d40fa85110d0958f3/", | |
| "time" : 1005 | |
| }, { | |
| "variables" : 1278, | |
| "clauses" : 68055, | |
| "name" : "https://gbd.iti.kit.edu/file/049072033960eab882a3b0933d414f36/", | |
| "time" : 1588 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 2100, | |
| "name" : "https://gbd.iti.kit.edu/file/04909da47036ae2ccf4fd8d025b83344/", | |
| "time" : 885 | |
| }, { | |
| "variables" : 945, | |
| "clauses" : 61409, | |
| "name" : "https://gbd.iti.kit.edu/file/0491901f00c8663e5b49a0dbbf96412f/", | |
| "time" : 1072 | |
| }, { | |
| "variables" : 29522, | |
| "clauses" : 716259, | |
| "name" : "https://gbd.iti.kit.edu/file/0494c37fc0ae2de1550eea216cfc1752/", | |
| "time" : 28693 | |
| }, { | |
| "variables" : 20195, | |
| "clauses" : 365875, | |
| "name" : "https://gbd.iti.kit.edu/file/049775f8bfc13fefc68f086cd3667df4/", | |
| "time" : 17789 | |
| }, { | |
| "variables" : 26757, | |
| "clauses" : 596785, | |
| "name" : "https://gbd.iti.kit.edu/file/0498569a656eb22b361a106e0cecff9b/", | |
| "time" : 25796 | |
| }, { | |
| "variables" : 25830, | |
| "clauses" : 553451, | |
| "name" : "https://gbd.iti.kit.edu/file/049a5615101bbe36f025a7b87d3c7360/", | |
| "time" : 25301 | |
| }, { | |
| "variables" : 29889, | |
| "clauses" : 732471, | |
| "name" : "https://gbd.iti.kit.edu/file/049ddd5ace159bd3d3363c9c36217d6d/", | |
| "time" : 30551 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 1890, | |
| "name" : "https://gbd.iti.kit.edu/file/04a05b619dfddaebbe864e7b94e108c1/", | |
| "time" : 967 | |
| }, { | |
| "variables" : 4230, | |
| "clauses" : 11645, | |
| "name" : "https://gbd.iti.kit.edu/file/04a3e6aed6697c05b23934f51e9d5321/", | |
| "time" : 3094 | |
| }, { | |
| "variables" : 10130, | |
| "clauses" : 31644, | |
| "name" : "https://gbd.iti.kit.edu/file/04a7b805cf12ae898f723b735fa959df/", | |
| "time" : 6265 | |
| }, { | |
| "variables" : 4740, | |
| "clauses" : 38883, | |
| "name" : "https://gbd.iti.kit.edu/file/04a97eb41fd59e3495641ea2442177c9/", | |
| "time" : 3114 | |
| }, { | |
| "variables" : 50, | |
| "clauses" : 820, | |
| "name" : "https://gbd.iti.kit.edu/file/04aa3db794a4a1129b037aac393e0bb5/", | |
| "time" : 43 | |
| }, { | |
| "variables" : 27725, | |
| "clauses" : 640529, | |
| "name" : "https://gbd.iti.kit.edu/file/04afde06992c1171bbcac67b3b58c53c/", | |
| "time" : 28266 | |
| }, { | |
| "variables" : 22551, | |
| "clauses" : 437326, | |
| "name" : "https://gbd.iti.kit.edu/file/04b1f0add9aaef195413ca4c03ea58ba/", | |
| "time" : 21523 | |
| }, { | |
| "variables" : 27568, | |
| "clauses" : 80439, | |
| "name" : "https://gbd.iti.kit.edu/file/04b2a7f442ed1b15439d0678ce902d6f/", | |
| "time" : 21807 | |
| }, { | |
| "variables" : 34331, | |
| "clauses" : 958744, | |
| "name" : "https://gbd.iti.kit.edu/file/04b58fb62b01369ce326152f7c7416e9/", | |
| "time" : 36571 | |
| }, { | |
| "variables" : 26411, | |
| "clauses" : 577130, | |
| "name" : "https://gbd.iti.kit.edu/file/04b88891edf088b990a3b3b81763efdd/", | |
| "time" : 26200 | |
| }, { | |
| "variables" : 4800, | |
| "clauses" : 45725, | |
| "name" : "https://gbd.iti.kit.edu/file/04c03de21b275b4e5e9f5882bf2c5ec1/", | |
| "time" : 4944 | |
| }, { | |
| "variables" : 28089, | |
| "clauses" : 649380, | |
| "name" : "https://gbd.iti.kit.edu/file/04d00ada667e60a3153fb811809d7e34/", | |
| "time" : 29075 | |
| }, { | |
| "variables" : 220, | |
| "clauses" : 18700, | |
| "name" : "https://gbd.iti.kit.edu/file/04d1b01eb1d69df1e9951f5243295833/", | |
| "time" : 580 | |
| }, { | |
| "variables" : 25662, | |
| "clauses" : 551002, | |
| "name" : "https://gbd.iti.kit.edu/file/04d22a87377168b4bae34b530adee132/", | |
| "time" : 26019 | |
| }, { | |
| "variables" : 74804, | |
| "clauses" : 395772, | |
| "name" : "https://gbd.iti.kit.edu/file/04d28cb98f3362dfcd4ab74d4bb82de3/", | |
| "time" : 52762 | |
| }, { | |
| "variables" : 44822, | |
| "clauses" : 232559, | |
| "name" : "https://gbd.iti.kit.edu/file/04d2cca932a87b98ebfc7bbd0fe6ed5d/", | |
| "time" : 31621 | |
| }, { | |
| "variables" : 25677, | |
| "clauses" : 550427, | |
| "name" : "https://gbd.iti.kit.edu/file/04d964003e9d42e6f2483e64564c1f54/", | |
| "time" : 25395 | |
| }, { | |
| "variables" : 26678, | |
| "clauses" : 595589, | |
| "name" : "https://gbd.iti.kit.edu/file/04dee0e90b8ce346e65a60c81f6687df/", | |
| "time" : 25581 | |
| }, { | |
| "variables" : 6360, | |
| "clauses" : 25200, | |
| "name" : "https://gbd.iti.kit.edu/file/04e219c640ed59dc68ea2d50493de5b5/", | |
| "time" : 5280 | |
| }, { | |
| "variables" : 40, | |
| "clauses" : 176, | |
| "name" : "https://gbd.iti.kit.edu/file/04e47e6635908600ef3938b32644825a/", | |
| "time" : 14 | |
| }, { | |
| "variables" : 360, | |
| "clauses" : 4869, | |
| "name" : "https://gbd.iti.kit.edu/file/04e50bc7a121716e396dc538ab24490e/", | |
| "time" : 757 | |
| }, { | |
| "variables" : 75, | |
| "clauses" : 1597, | |
| "name" : "https://gbd.iti.kit.edu/file/04e54fdde41e2e623789c3f7df6d274d/", | |
| "time" : 98 | |
| }, { | |
| "variables" : 27727, | |
| "clauses" : 646244, | |
| "name" : "https://gbd.iti.kit.edu/file/04e6e374423615babd4062f67a532c5e/", | |
| "time" : 27372 | |
| }, { | |
| "variables" : 33651, | |
| "clauses" : 921760, | |
| "name" : "https://gbd.iti.kit.edu/file/04ed29d91e703f9ebfd81d2d4fa97103/", | |
| "time" : 35105 | |
| }, { | |
| "variables" : 868, | |
| "clauses" : 200942, | |
| "name" : "https://gbd.iti.kit.edu/file/04ef162792ce0f1d675cf363db2fd99b/", | |
| "time" : 3822 | |
| }, { | |
| "variables" : 240, | |
| "clauses" : 1249, | |
| "name" : "https://gbd.iti.kit.edu/file/04f0b56ff8811424c3f44cb7662b3faf/", | |
| "time" : 503 | |
| }, { | |
| "variables" : 460, | |
| "clauses" : 1978, | |
| "name" : "https://gbd.iti.kit.edu/file/04f1442bafdd6433d41588d2c2e72e0b/", | |
| "time" : 1009 | |
| }, { | |
| "variables" : 27162, | |
| "clauses" : 607642, | |
| "name" : "https://gbd.iti.kit.edu/file/04f542671e8167741228d22abd0303db/", | |
| "time" : 27089 | |
| }, { | |
| "variables" : 11427, | |
| "clauses" : 33530, | |
| "name" : "https://gbd.iti.kit.edu/file/04f6dd1892f3382e8356d107ba156256/", | |
| "time" : 7756 | |
| }, { | |
| "variables" : 150, | |
| "clauses" : 12959, | |
| "name" : "https://gbd.iti.kit.edu/file/04f7b0f8afc58d5b7be2c486c01e8164/", | |
| "time" : 324 | |
| }, { | |
| "variables" : 400, | |
| "clauses" : 1720, | |
| "name" : "https://gbd.iti.kit.edu/file/04f7b83bdf8d56116cc9d7a659464c37/", | |
| "time" : 872 | |
| }, { | |
| "variables" : 33175, | |
| "clauses" : 899325, | |
| "name" : "https://gbd.iti.kit.edu/file/04f9cf38c15c4f048fc25f03cb621536/", | |
| "time" : 35628 | |
| }, { | |
| "variables" : 520, | |
| "clauses" : 2216, | |
| "name" : "https://gbd.iti.kit.edu/file/04f9f1f61d99108b7ad0fa77d275dc4c/", | |
| "time" : 332 | |
| }, { | |
| "variables" : 4940, | |
| "clauses" : 93221, | |
| "name" : "https://gbd.iti.kit.edu/file/04fa0a71339fa76067a75ff448ef6f67/", | |
| "time" : 4879 | |
| }, { | |
| "variables" : 18754, | |
| "clauses" : 327726, | |
| "name" : "https://gbd.iti.kit.edu/file/04fb14e644b1858851c739b1a2170334/", | |
| "time" : 16951 | |
| }, { | |
| "variables" : 30, | |
| "clauses" : 3201, | |
| "name" : "https://gbd.iti.kit.edu/file/04fef94bab64c9e3cc8b2b696f38f7be/", | |
| "time" : 22 | |
| }, { | |
| "variables" : 1015, | |
| "clauses" : 17290, | |
| "name" : "https://gbd.iti.kit.edu/file/050214ecbd9e96136fe1bc73447f1303/", | |
| "time" : 518 | |
| }, { | |
| "variables" : 18709, | |
| "clauses" : 325978, | |
| "name" : "https://gbd.iti.kit.edu/file/0502f436e37331d0b92274e0db73b134/", | |
| "time" : 17578 | |
| }, { | |
| "variables" : 20477, | |
| "clauses" : 370971, | |
| "name" : "https://gbd.iti.kit.edu/file/05065ca3c3a5b2b415d7e9afd0bd2c16/", | |
| "time" : 18976 | |
| }, { | |
| "variables" : 66274, | |
| "clauses" : 168471, | |
| "name" : "https://gbd.iti.kit.edu/file/0506afbcee2355dd568a2923e4461649/", | |
| "time" : 58559 | |
| }, { | |
| "variables" : 1677, | |
| "clauses" : 15063, | |
| "name" : "https://gbd.iti.kit.edu/file/0506d033a4ca469af10d95dbf36a86e9/", | |
| "time" : 1183 | |
| }, { | |
| "variables" : 440, | |
| "clauses" : 9239, | |
| "name" : "https://gbd.iti.kit.edu/file/05070c567100ecb6cdbc2ffe0fae57e2/", | |
| "time" : 1604 | |
| }, { | |
| "variables" : 5851, | |
| "clauses" : 20316, | |
| "name" : "https://gbd.iti.kit.edu/file/0513c7d43a5874fa6a17a184091b3d68/", | |
| "time" : 4415 | |
| }, { | |
| "variables" : 240, | |
| "clauses" : 20400, | |
| "name" : "https://gbd.iti.kit.edu/file/0515bc0e0f1028fd4d086139035f5f38/", | |
| "time" : 662 | |
| }, { | |
| "variables" : 699, | |
| "clauses" : 3262, | |
| "name" : "https://gbd.iti.kit.edu/file/0518b5dc204f26b356671785e02852e1/", | |
| "time" : 515 | |
| }, { | |
| "variables" : 33564, | |
| "clauses" : 916383, | |
| "name" : "https://gbd.iti.kit.edu/file/0518c5a3eb17ee72f00424e63bd7940b/", | |
| "time" : 39472 | |
| }, { | |
| "variables" : 90, | |
| "clauses" : 1901, | |
| "name" : "https://gbd.iti.kit.edu/file/051b63ae234e63226a7984d76f9dc331/", | |
| "time" : 168 | |
| }, { | |
| "variables" : 25055, | |
| "clauses" : 529044, | |
| "name" : "https://gbd.iti.kit.edu/file/051c7db6f9d6daa9238ad64ddae6cea0/", | |
| "time" : 26257 | |
| }, { | |
| "variables" : 29992, | |
| "clauses" : 744606, | |
| "name" : "https://gbd.iti.kit.edu/file/051cb2ec3e94e7f2a72232530f847408/", | |
| "time" : 32562 | |
| }, { | |
| "variables" : 3331, | |
| "clauses" : 11086, | |
| "name" : "https://gbd.iti.kit.edu/file/0520814ad7ca7c063109ee7a28e89de8/", | |
| "time" : 2559 | |
| }, { | |
| "variables" : 28385, | |
| "clauses" : 662573, | |
| "name" : "https://gbd.iti.kit.edu/file/0524e21cb713c3ba78906a6716409c80/", | |
| "time" : 27693 | |
| }, { | |
| "variables" : 31777, | |
| "clauses" : 827289, | |
| "name" : "https://gbd.iti.kit.edu/file/052e03355eef1d923d532699e04f0eb2/", | |
| "time" : 32068 | |
| }, { | |
| "variables" : 870, | |
| "clauses" : 71374, | |
| "name" : "https://gbd.iti.kit.edu/file/0533a1506eb61460bee3917f61ca4c49/", | |
| "time" : 1171 | |
| }, { | |
| "variables" : 1046, | |
| "clauses" : 22965, | |
| "name" : "https://gbd.iti.kit.edu/file/053543abce7e09d1f623ac43fb67888b/", | |
| "time" : 657 | |
| }, { | |
| "variables" : 26428, | |
| "clauses" : 577312, | |
| "name" : "https://gbd.iti.kit.edu/file/05373ec86c44b2afb60fb93316b30001/", | |
| "time" : 25176 | |
| }, { | |
| "variables" : 26114, | |
| "clauses" : 562335, | |
| "name" : "https://gbd.iti.kit.edu/file/053c477a86dac016582436e67ecf0bc3/", | |
| "time" : 26203 | |
| }, { | |
| "variables" : 29687, | |
| "clauses" : 719786, | |
| "name" : "https://gbd.iti.kit.edu/file/0541dc77ecea9c210d3c4231d97c02de/", | |
| "time" : 31012 | |
| }, { | |
| "variables" : 23209, | |
| "clauses" : 463927, | |
| "name" : "https://gbd.iti.kit.edu/file/05423f54e9e0bf97ce3fca2abe2ba3e6/", | |
| "time" : 22498 | |
| }, { | |
| "variables" : 5508, | |
| "clauses" : 19108, | |
| "name" : "https://gbd.iti.kit.edu/file/05469ff4aedf9286f024177d0d09fbd5/", | |
| "time" : 4035 | |
| }, { | |
| "variables" : 5301, | |
| "clauses" : 14898, | |
| "name" : "https://gbd.iti.kit.edu/file/054c1e5254cdc36bb85e06e53cafe8eb/", | |
| "time" : 4135 | |
| }, { | |
| "variables" : 19531, | |
| "clauses" : 348714, | |
| "name" : "https://gbd.iti.kit.edu/file/054c7052d5110e9731a9d0bf34d651ec/", | |
| "time" : 17929 | |
| }, { | |
| "variables" : 60, | |
| "clauses" : 5340, | |
| "name" : "https://gbd.iti.kit.edu/file/05513edb5e778987bd727804ed4fa01e/", | |
| "time" : 54 | |
| }, { | |
| "variables" : 13966, | |
| "clauses" : 222380, | |
| "name" : "https://gbd.iti.kit.edu/file/0553f2a01f0838c1f3347f622cc3c30c/", | |
| "time" : 12864 | |
| }, { | |
| "variables" : 32701, | |
| "clauses" : 873631, | |
| "name" : "https://gbd.iti.kit.edu/file/0556cacde8ebb77956342a6e81309553/", | |
| "time" : 35209 | |
| }, { | |
| "variables" : 648, | |
| "clauses" : 2149, | |
| "name" : "https://gbd.iti.kit.edu/file/0557d21452d411c00f766973a59837a5/", | |
| "time" : 405 | |
| }, { | |
| "variables" : 320, | |
| "clauses" : 1366, | |
| "name" : "https://gbd.iti.kit.edu/file/055836a43eb318de92f09c555ba4f3b5/", | |
| "time" : 590 | |
| }, { | |
| "variables" : 26575, | |
| "clauses" : 442285, | |
| "name" : "https://gbd.iti.kit.edu/file/055db8f900741c7b8d7b731e99662588/", | |
| "time" : 21870 | |
| }, { | |
| "variables" : 61642, | |
| "clauses" : 644099, | |
| "name" : "https://gbd.iti.kit.edu/file/055f942145df4b6c9fd0d10a3f1da98e/", | |
| "time" : 57788 | |
| }, { | |
| "variables" : 22250, | |
| "clauses" : 427981, | |
| "name" : "https://gbd.iti.kit.edu/file/056263f3ef83f1b0c0fd48cab346e8e4/", | |
| "time" : 21588 | |
| }, { | |
| "variables" : 95816, | |
| "clauses" : 313805, | |
| "name" : "https://gbd.iti.kit.edu/file/05650550f21d60a3989cae43fb5ebd93/", | |
| "time" : 81185 | |
| }, { | |
| "variables" : 25201, | |
| "clauses" : 533538, | |
| "name" : "https://gbd.iti.kit.edu/file/05670a916f890c9c4345ff4fd19561bf/", | |
| "time" : 25564 | |
| }, { | |
| "variables" : 4210, | |
| "clauses" : 12053, | |
| "name" : "https://gbd.iti.kit.edu/file/05680de3febd39916e496dd772cb8c19/", | |
| "time" : 2872 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87881, | |
| "name" : "https://gbd.iti.kit.edu/file/0568bb0b42891e57247ed4b436dff85d/", | |
| "time" : 18639 | |
| }, { | |
| "variables" : 33679, | |
| "clauses" : 927608, | |
| "name" : "https://gbd.iti.kit.edu/file/0568ff4af327110a55355527e3c454e2/", | |
| "time" : 37403 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87761, | |
| "name" : "https://gbd.iti.kit.edu/file/0569ecb5da00dd3ffc8cdfab85a4956c/", | |
| "time" : 18735 | |
| }, { | |
| "variables" : 28961, | |
| "clauses" : 685361, | |
| "name" : "https://gbd.iti.kit.edu/file/056acec954f198b911fd8c6894a6fad4/", | |
| "time" : 31538 | |
| }, { | |
| "variables" : 26728, | |
| "clauses" : 596535, | |
| "name" : "https://gbd.iti.kit.edu/file/0574a9f4769dfe44ea0680aa8d935f13/", | |
| "time" : 27846 | |
| }, { | |
| "variables" : 20081, | |
| "clauses" : 361266, | |
| "name" : "https://gbd.iti.kit.edu/file/0575710ecfdc61ede3807eb1c6a1b01f/", | |
| "time" : 19178 | |
| }, { | |
| "variables" : 31821, | |
| "clauses" : 828387, | |
| "name" : "https://gbd.iti.kit.edu/file/0578dbb863e1dccfd5d352c1b8ba198c/", | |
| "time" : 35735 | |
| }, { | |
| "variables" : 31607, | |
| "clauses" : 819494, | |
| "name" : "https://gbd.iti.kit.edu/file/0579fb9d75e018b9366db9150db7453a/", | |
| "time" : 34725 | |
| }, { | |
| "variables" : 23266, | |
| "clauses" : 81430, | |
| "name" : "https://gbd.iti.kit.edu/file/057ee74505bbc50bfb10d6814c5a3c4d/", | |
| "time" : 17394 | |
| }, { | |
| "variables" : 26228, | |
| "clauses" : 579091, | |
| "name" : "https://gbd.iti.kit.edu/file/058129d7cf63b8a0a10e932a0728ac36/", | |
| "time" : 27662 | |
| }, { | |
| "variables" : 32313, | |
| "clauses" : 161529, | |
| "name" : "https://gbd.iti.kit.edu/file/05817b4e1add561af0e1165e01fb48cc/", | |
| "time" : 27496 | |
| }, { | |
| "variables" : 29858, | |
| "clauses" : 728684, | |
| "name" : "https://gbd.iti.kit.edu/file/05833c2c6953b76638748b3b5152b17f/", | |
| "time" : 33073 | |
| }, { | |
| "variables" : 36734, | |
| "clauses" : 1075990, | |
| "name" : "https://gbd.iti.kit.edu/file/058414cd650e2309e2d3df6b3ac80f37/", | |
| "time" : 43133 | |
| }, { | |
| "variables" : 250, | |
| "clauses" : 1104, | |
| "name" : "https://gbd.iti.kit.edu/file/05860ef5bb55efbd4bb5ec8b0de13d03/", | |
| "time" : 442 | |
| }, { | |
| "variables" : 5266, | |
| "clauses" : 15322, | |
| "name" : "https://gbd.iti.kit.edu/file/05879c0b6a41bf08f08ea2f58a931146/", | |
| "time" : 3784 | |
| }, { | |
| "variables" : 135, | |
| "clauses" : 5251, | |
| "name" : "https://gbd.iti.kit.edu/file/0587f345cca3ef8340e8e71829dce130/", | |
| "time" : 255 | |
| }, { | |
| "variables" : 3288, | |
| "clauses" : 8959, | |
| "name" : "https://gbd.iti.kit.edu/file/0587fa4c5dc214a7470cfab3712f4699/", | |
| "time" : 2688 | |
| }, { | |
| "variables" : 76326, | |
| "clauses" : 373504, | |
| "name" : "https://gbd.iti.kit.edu/file/058b69e7c7923e2c71070c9f934f2c2e/", | |
| "time" : 53588 | |
| }, { | |
| "variables" : 3513, | |
| "clauses" : 9559, | |
| "name" : "https://gbd.iti.kit.edu/file/058d2ff55a09eac11780d6a368b48a80/", | |
| "time" : 2587 | |
| }, { | |
| "variables" : 4931, | |
| "clauses" : 32184, | |
| "name" : "https://gbd.iti.kit.edu/file/0593e6814f02ec9749e87bdc6aff8275/", | |
| "time" : 3289 | |
| }, { | |
| "variables" : 26055, | |
| "clauses" : 570771, | |
| "name" : "https://gbd.iti.kit.edu/file/05997924d9bb4497f0f8a027caad6bbd/", | |
| "time" : 27581 | |
| }, { | |
| "variables" : 7428, | |
| "clauses" : 20744, | |
| "name" : "https://gbd.iti.kit.edu/file/0599c0cc9fb43d1eb90c5590d4ecbf39/", | |
| "time" : 5933 | |
| }, { | |
| "variables" : 28054, | |
| "clauses" : 653300, | |
| "name" : "https://gbd.iti.kit.edu/file/059aae70d73e0101c492106c4d214774/", | |
| "time" : 30074 | |
| }, { | |
| "variables" : 220, | |
| "clauses" : 1210, | |
| "name" : "https://gbd.iti.kit.edu/file/059f3479ab76bc97c3db74efc8558482/", | |
| "time" : 437 | |
| }, { | |
| "variables" : 50, | |
| "clauses" : 4450, | |
| "name" : "https://gbd.iti.kit.edu/file/05a14c9084e09730c52b65732fe19d90/", | |
| "time" : 34 | |
| }, { | |
| "variables" : 26275, | |
| "clauses" : 572883, | |
| "name" : "https://gbd.iti.kit.edu/file/05a5c4f83946f8390e561e006f39f0e9/", | |
| "time" : 27722 | |
| }, { | |
| "variables" : 348, | |
| "clauses" : 1624, | |
| "name" : "https://gbd.iti.kit.edu/file/05aaff6058ca0088f54881003c1eb57b/", | |
| "time" : 664 | |
| }, { | |
| "variables" : 1458, | |
| "clauses" : 280144, | |
| "name" : "https://gbd.iti.kit.edu/file/05b04d362b374569a4eb63c4e4e132b7/", | |
| "time" : 8972 | |
| }, { | |
| "variables" : 26411, | |
| "clauses" : 582860, | |
| "name" : "https://gbd.iti.kit.edu/file/05b095301362cf626067acd18590ea03/", | |
| "time" : 28515 | |
| }, { | |
| "variables" : 29784, | |
| "clauses" : 733602, | |
| "name" : "https://gbd.iti.kit.edu/file/05b20aaa3665b3688fe91e63b1d416b1/", | |
| "time" : 33028 | |
| }, { | |
| "variables" : 32969, | |
| "clauses" : 885896, | |
| "name" : "https://gbd.iti.kit.edu/file/05b373515e803818e8991e855a1d500d/", | |
| "time" : 38951 | |
| }, { | |
| "variables" : 30663, | |
| "clauses" : 768506, | |
| "name" : "https://gbd.iti.kit.edu/file/05bddbf878fc3fd6becc0b13ae747bdb/", | |
| "time" : 34171 | |
| }, { | |
| "variables" : 27554, | |
| "clauses" : 633866, | |
| "name" : "https://gbd.iti.kit.edu/file/05bea7b46a68c2bc7761ff2424c5e58f/", | |
| "time" : 30103 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87664, | |
| "name" : "https://gbd.iti.kit.edu/file/05c042ebd6f763d072a86cac025584f0/", | |
| "time" : 18913 | |
| }, { | |
| "variables" : 140, | |
| "clauses" : 12134, | |
| "name" : "https://gbd.iti.kit.edu/file/05c46c3abf7acb1337d74ce98da20ec3/", | |
| "time" : 246 | |
| }, { | |
| "variables" : 450, | |
| "clauses" : 1984, | |
| "name" : "https://gbd.iti.kit.edu/file/05c5ed370ea11a2c19c111f4a5979921/", | |
| "time" : 1076 | |
| }, { | |
| "variables" : 3073, | |
| "clauses" : 19785, | |
| "name" : "https://gbd.iti.kit.edu/file/05c5ff612371a5773e857212174f625b/", | |
| "time" : 2545 | |
| }, { | |
| "variables" : 29439, | |
| "clauses" : 720698, | |
| "name" : "https://gbd.iti.kit.edu/file/05c75485e42f747b9dba8da1aa1133ea/", | |
| "time" : 32782 | |
| }, { | |
| "variables" : 2000, | |
| "clauses" : 8400, | |
| "name" : "https://gbd.iti.kit.edu/file/05c7d8c4a5be0da9995e180fe65f0d9e/", | |
| "time" : 1573 | |
| }, { | |
| "variables" : 8000, | |
| "clauses" : 34136, | |
| "name" : "https://gbd.iti.kit.edu/file/05cc4564c3160e7da7be1142f0448771/", | |
| "time" : 6328 | |
| }, { | |
| "variables" : 22896, | |
| "clauses" : 453787, | |
| "name" : "https://gbd.iti.kit.edu/file/05cca3e64d2d7766f5eb8eaff105eb40/", | |
| "time" : 23238 | |
| }, { | |
| "variables" : 29850, | |
| "clauses" : 730506, | |
| "name" : "https://gbd.iti.kit.edu/file/05cf9b400cec8d7e6a606b8a2087ea3e/", | |
| "time" : 32386 | |
| }, { | |
| "variables" : 31511, | |
| "clauses" : 820043, | |
| "name" : "https://gbd.iti.kit.edu/file/05cfa69444404b03cce3310bfd633119/", | |
| "time" : 35877 | |
| }, { | |
| "variables" : 18000, | |
| "clauses" : 75600, | |
| "name" : "https://gbd.iti.kit.edu/file/05d14498d98fd6ea69d30136eb95dcb3/", | |
| "time" : 16707 | |
| }, { | |
| "variables" : 36972, | |
| "clauses" : 1090136, | |
| "name" : "https://gbd.iti.kit.edu/file/05d1a5e83b3a86de7598a1e089a86b21/", | |
| "time" : 43716 | |
| }, { | |
| "variables" : 31103, | |
| "clauses" : 789421, | |
| "name" : "https://gbd.iti.kit.edu/file/05d1e403eb79a9a1b4fd0182be89299b/", | |
| "time" : 34927 | |
| }, { | |
| "variables" : 400, | |
| "clauses" : 1800, | |
| "name" : "https://gbd.iti.kit.edu/file/05d545d220f72a6d28004dd5b092594d/", | |
| "time" : 895 | |
| }, { | |
| "variables" : 24232, | |
| "clauses" : 495703, | |
| "name" : "https://gbd.iti.kit.edu/file/05d6efa039dad1b207f1649aa4449fd2/", | |
| "time" : 24985 | |
| }, { | |
| "variables" : 20054, | |
| "clauses" : 364144, | |
| "name" : "https://gbd.iti.kit.edu/file/05ddfe38031a7974a3d0510018ab253c/", | |
| "time" : 19398 | |
| }, { | |
| "variables" : 115, | |
| "clauses" : 41532, | |
| "name" : "https://gbd.iti.kit.edu/file/05df4430054ceba4fa065806e8c65041/", | |
| "time" : 139 | |
| }, { | |
| "variables" : 29751, | |
| "clauses" : 727280, | |
| "name" : "https://gbd.iti.kit.edu/file/05e291c40b85447a181d7de47ae1a2bf/", | |
| "time" : 32745 | |
| }, { | |
| "variables" : 25219, | |
| "clauses" : 532003, | |
| "name" : "https://gbd.iti.kit.edu/file/05e877d2709b8c20b3485e6b68c98bc0/", | |
| "time" : 27535 | |
| }, { | |
| "variables" : 296, | |
| "clauses" : 47000, | |
| "name" : "https://gbd.iti.kit.edu/file/05eb87eb6fecb7a8a3bdc25154412c1d/", | |
| "time" : 1653 | |
| }, { | |
| "variables" : 53118, | |
| "clauses" : 178062, | |
| "name" : "https://gbd.iti.kit.edu/file/05eee75ab69270c322b9ef6bc1ee8604/", | |
| "time" : 42182 | |
| }, { | |
| "variables" : 85, | |
| "clauses" : 180, | |
| "name" : "https://gbd.iti.kit.edu/file/05f3a48298721d68cded8618b432e7c3/", | |
| "time" : 96 | |
| }, { | |
| "variables" : 230, | |
| "clauses" : 552, | |
| "name" : "https://gbd.iti.kit.edu/file/05f5567936f582edc0d3ea9903f540bc/", | |
| "time" : 374 | |
| }, { | |
| "variables" : 24200, | |
| "clauses" : 501086, | |
| "name" : "https://gbd.iti.kit.edu/file/05f7448ef6a998da4d58a15cebe0b6ba/", | |
| "time" : 26945 | |
| }, { | |
| "variables" : 160, | |
| "clauses" : 13779, | |
| "name" : "https://gbd.iti.kit.edu/file/05f8ffcc6372f5475a0b7c61b46c162e/", | |
| "time" : 337 | |
| }, { | |
| "variables" : 32084, | |
| "clauses" : 112535, | |
| "name" : "https://gbd.iti.kit.edu/file/05fa3b96505ec198385ce8bbb02d27df/", | |
| "time" : 24962 | |
| }, { | |
| "variables" : 24192, | |
| "clauses" : 499732, | |
| "name" : "https://gbd.iti.kit.edu/file/05fa862fc7acabb822b6f2afb5fb6973/", | |
| "time" : 25542 | |
| }, { | |
| "variables" : 672, | |
| "clauses" : 16824, | |
| "name" : "https://gbd.iti.kit.edu/file/05fbbab9f0baf819ed9593cca8587629/", | |
| "time" : 537 | |
| }, { | |
| "variables" : 27576, | |
| "clauses" : 630709, | |
| "name" : "https://gbd.iti.kit.edu/file/05ffa991da7ff48826faa3607de22e60/", | |
| "time" : 30316 | |
| }, { | |
| "variables" : 29323, | |
| "clauses" : 710336, | |
| "name" : "https://gbd.iti.kit.edu/file/0601e6379f576d6ad6eaddcb5798c13c/", | |
| "time" : 32632 | |
| }, { | |
| "variables" : 25140, | |
| "clauses" : 531087, | |
| "name" : "https://gbd.iti.kit.edu/file/06049cbbea67b138b7900b6c7c5730de/", | |
| "time" : 26115 | |
| }, { | |
| "variables" : 13409, | |
| "clauses" : 478985, | |
| "name" : "https://gbd.iti.kit.edu/file/060ad8240dd120ae1017c31c17fa88e9/", | |
| "time" : 10246 | |
| }, { | |
| "variables" : 130, | |
| "clauses" : 5638, | |
| "name" : "https://gbd.iti.kit.edu/file/060eaa97b6072e7d3ef9087d2421ddeb/", | |
| "time" : 229 | |
| }, { | |
| "variables" : 36666, | |
| "clauses" : 1071448, | |
| "name" : "https://gbd.iti.kit.edu/file/0611c9a290bc9dc289bc097c9662913c/", | |
| "time" : 44164 | |
| }, { | |
| "variables" : 6569, | |
| "clauses" : 22864, | |
| "name" : "https://gbd.iti.kit.edu/file/0612deb9e6268ddf1381d042ab2e52ce/", | |
| "time" : 5015 | |
| }, { | |
| "variables" : 226, | |
| "clauses" : 1078, | |
| "name" : "https://gbd.iti.kit.edu/file/0614e1ae5100ee0aca4ea24424479fa3/", | |
| "time" : 403 | |
| }, { | |
| "variables" : 405, | |
| "clauses" : 86429, | |
| "name" : "https://gbd.iti.kit.edu/file/06172049e6804cbfb07f993023f2684f/", | |
| "time" : 2849 | |
| }, { | |
| "variables" : 5200, | |
| "clauses" : 22188, | |
| "name" : "https://gbd.iti.kit.edu/file/06221f824342f77b3d6cce7f05d70fe2/", | |
| "time" : 4304 | |
| }, { | |
| "variables" : 720, | |
| "clauses" : 14944, | |
| "name" : "https://gbd.iti.kit.edu/file/062b340de8f5fdb7ad62c3ec8a7d50ac/", | |
| "time" : 1163 | |
| }, { | |
| "variables" : 165, | |
| "clauses" : 7156, | |
| "name" : "https://gbd.iti.kit.edu/file/062c3f614211a999d533cf5ba9108e5e/", | |
| "time" : 343 | |
| }, { | |
| "variables" : 26253, | |
| "clauses" : 575143, | |
| "name" : "https://gbd.iti.kit.edu/file/062ecaf3e25632b7b6a20134f11c27e4/", | |
| "time" : 28217 | |
| }, { | |
| "variables" : 7089, | |
| "clauses" : 121197, | |
| "name" : "https://gbd.iti.kit.edu/file/063486c4a139ae7a3874a5bac3459217/", | |
| "time" : 4946 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 14000, | |
| "name" : "https://gbd.iti.kit.edu/file/063beadfa9d6dbd569d12aacbcb300c5/", | |
| "time" : 919 | |
| }, { | |
| "variables" : 25173, | |
| "clauses" : 536079, | |
| "name" : "https://gbd.iti.kit.edu/file/06441d7b824ead0325b07d7d7e943ddb/", | |
| "time" : 23725 | |
| }, { | |
| "variables" : 25029, | |
| "clauses" : 528545, | |
| "name" : "https://gbd.iti.kit.edu/file/064850977be6689e4aa2165adbd8e866/", | |
| "time" : 23961 | |
| }, { | |
| "variables" : 26823, | |
| "clauses" : 100499, | |
| "name" : "https://gbd.iti.kit.edu/file/064ba3c61c5f105104edec8305853711/", | |
| "time" : 21524 | |
| }, { | |
| "variables" : 28489, | |
| "clauses" : 101796, | |
| "name" : "https://gbd.iti.kit.edu/file/064bf6dbb752a83b4d3602779a4f5795/", | |
| "time" : 20756 | |
| }, { | |
| "variables" : 19540, | |
| "clauses" : 350401, | |
| "name" : "https://gbd.iti.kit.edu/file/064cf5ae720265bdb95f553557e41f18/", | |
| "time" : 17932 | |
| }, { | |
| "variables" : 24377, | |
| "clauses" : 498963, | |
| "name" : "https://gbd.iti.kit.edu/file/065036e33ca5a147c353956348fc8cc5/", | |
| "time" : 23440 | |
| }, { | |
| "variables" : 80, | |
| "clauses" : 7120, | |
| "name" : "https://gbd.iti.kit.edu/file/065775fe69392642261b1436fbd6bab4/", | |
| "time" : 92 | |
| }, { | |
| "variables" : 36535, | |
| "clauses" : 1062260, | |
| "name" : "https://gbd.iti.kit.edu/file/0657d7556552d692a009861a8df0187d/", | |
| "time" : 38622 | |
| }, { | |
| "variables" : 48917, | |
| "clauses" : 144691, | |
| "name" : "https://gbd.iti.kit.edu/file/065882225b28a15ec62af09030001ee5/", | |
| "time" : 36358 | |
| }, { | |
| "variables" : 27992, | |
| "clauses" : 647084, | |
| "name" : "https://gbd.iti.kit.edu/file/065b141f5b24a1ea858f9e63bf13d0cf/", | |
| "time" : 28792 | |
| }, { | |
| "variables" : 30, | |
| "clauses" : 3137, | |
| "name" : "https://gbd.iti.kit.edu/file/0662df257be6c6d0691729cb23a17386/", | |
| "time" : 32 | |
| }, { | |
| "variables" : 769, | |
| "clauses" : 4777, | |
| "name" : "https://gbd.iti.kit.edu/file/066813ab5f3b7b1cc6d2847c37f5fae7/", | |
| "time" : 575 | |
| }, { | |
| "variables" : 20869, | |
| "clauses" : 389406, | |
| "name" : "https://gbd.iti.kit.edu/file/0668d86f91d0e8aeea2e3fe722047363/", | |
| "time" : 19790 | |
| }, { | |
| "variables" : 33334, | |
| "clauses" : 908303, | |
| "name" : "https://gbd.iti.kit.edu/file/066ade1d9e5bede84a078012ee14fdc5/", | |
| "time" : 37487 | |
| }, { | |
| "variables" : 27786, | |
| "clauses" : 638444, | |
| "name" : "https://gbd.iti.kit.edu/file/066cc2796adfff0382fed7ae88d5b41d/", | |
| "time" : 30286 | |
| }, { | |
| "variables" : 29254, | |
| "clauses" : 97456, | |
| "name" : "https://gbd.iti.kit.edu/file/066d6a47dfd9648d913ba8dbce722d75/", | |
| "time" : 23323 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 2800, | |
| "name" : "https://gbd.iti.kit.edu/file/066f7dc6f15dfe89172f4b32e50ac826/", | |
| "time" : 518 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87593, | |
| "name" : "https://gbd.iti.kit.edu/file/0671f3013bf168f4660edfb4b40fbfa5/", | |
| "time" : 19930 | |
| }, { | |
| "variables" : 990, | |
| "clauses" : 3582, | |
| "name" : "https://gbd.iti.kit.edu/file/06767f7b8e23fd24f6df74fefef9c48c/", | |
| "time" : 748 | |
| }, { | |
| "variables" : 40, | |
| "clauses" : 176, | |
| "name" : "https://gbd.iti.kit.edu/file/067dc6945c4aec1c2bc1fdc2e5819124/", | |
| "time" : 23 | |
| }, { | |
| "variables" : 90, | |
| "clauses" : 1917, | |
| "name" : "https://gbd.iti.kit.edu/file/0684c9b8439112b0e3202dc1f13bae65/", | |
| "time" : 133 | |
| }, { | |
| "variables" : 31118, | |
| "clauses" : 790689, | |
| "name" : "https://gbd.iti.kit.edu/file/068594cad63ad63966d00272acbe72f7/", | |
| "time" : 33831 | |
| }, { | |
| "variables" : 238, | |
| "clauses" : 15812, | |
| "name" : "https://gbd.iti.kit.edu/file/06872e73223dc74c76b06f37a185dc22/", | |
| "time" : 751 | |
| }, { | |
| "variables" : 29483, | |
| "clauses" : 714214, | |
| "name" : "https://gbd.iti.kit.edu/file/068f2d23820541fe4eaebfb072bd6cbb/", | |
| "time" : 31502 | |
| }, { | |
| "variables" : 25801, | |
| "clauses" : 559599, | |
| "name" : "https://gbd.iti.kit.edu/file/0696cb4f18fd63cc94f319fab92119e5/", | |
| "time" : 26798 | |
| }, { | |
| "variables" : 26995, | |
| "clauses" : 599517, | |
| "name" : "https://gbd.iti.kit.edu/file/069978487284dbdafb1bb8860adf19f0/", | |
| "time" : 26483 | |
| }, { | |
| "variables" : 12368, | |
| "clauses" : 197245, | |
| "name" : "https://gbd.iti.kit.edu/file/069c9e38f21a431a293c2c158e43f1f1/", | |
| "time" : 11925 | |
| }, { | |
| "variables" : 840, | |
| "clauses" : 71206, | |
| "name" : "https://gbd.iti.kit.edu/file/069f7d519e820f6b879f880703907bb3/", | |
| "time" : 1161 | |
| }, { | |
| "variables" : 33547, | |
| "clauses" : 914721, | |
| "name" : "https://gbd.iti.kit.edu/file/06a91842354cefee9d432cfd3ed50100/", | |
| "time" : 35942 | |
| }, { | |
| "variables" : 130, | |
| "clauses" : 2769, | |
| "name" : "https://gbd.iti.kit.edu/file/06ab2f3544c15dad7b9e4bfbce9982cf/", | |
| "time" : 262 | |
| }, { | |
| "variables" : 33604, | |
| "clauses" : 910786, | |
| "name" : "https://gbd.iti.kit.edu/file/06ac25321a9e8a0e2653ae9fc72ff939/", | |
| "time" : 33778 | |
| }, { | |
| "variables" : 28489, | |
| "clauses" : 99650, | |
| "name" : "https://gbd.iti.kit.edu/file/06ac45adf49f5e65a05904420e22def6/", | |
| "time" : 20977 | |
| }, { | |
| "variables" : 28489, | |
| "clauses" : 99603, | |
| "name" : "https://gbd.iti.kit.edu/file/06af18723348ccdd9b0fc20bfda1d7ff/", | |
| "time" : 21103 | |
| }, { | |
| "variables" : 50000, | |
| "clauses" : 210000, | |
| "name" : "https://gbd.iti.kit.edu/file/06afd800584013b69acf3ceb8a92dd39/", | |
| "time" : 48487 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87756, | |
| "name" : "https://gbd.iti.kit.edu/file/06b234d992399a10a26d5be67230a20c/", | |
| "time" : 18458 | |
| }, { | |
| "variables" : 1805, | |
| "clauses" : 7337, | |
| "name" : "https://gbd.iti.kit.edu/file/06b238df161c9e24a31890a08bca22df/", | |
| "time" : 633 | |
| }, { | |
| "variables" : 9142, | |
| "clauses" : 155730, | |
| "name" : "https://gbd.iti.kit.edu/file/06b3fbd3e0d8f0679e979e88d852089a/", | |
| "time" : 8591 | |
| }, { | |
| "variables" : 7989, | |
| "clauses" : 24056, | |
| "name" : "https://gbd.iti.kit.edu/file/06b4ea25b64b0ea42d68fb06534a7e7b/", | |
| "time" : 5356 | |
| }, { | |
| "variables" : 7200, | |
| "clauses" : 30722, | |
| "name" : "https://gbd.iti.kit.edu/file/06b6606fd021e9b4412bfc2fc42d7b0a/", | |
| "time" : 5686 | |
| }, { | |
| "variables" : 28854, | |
| "clauses" : 103090, | |
| "name" : "https://gbd.iti.kit.edu/file/06b6d7b1e7f26c4290413956ada422a2/", | |
| "time" : 21523 | |
| }, { | |
| "variables" : 26903, | |
| "clauses" : 605066, | |
| "name" : "https://gbd.iti.kit.edu/file/06bb08c9c8624d8f6d795d1127eebffe/", | |
| "time" : 27483 | |
| }, { | |
| "variables" : 440, | |
| "clauses" : 2420, | |
| "name" : "https://gbd.iti.kit.edu/file/06bfd83d0fba6a831d1f6db32b587d2b/", | |
| "time" : 1004 | |
| }, { | |
| "variables" : 156, | |
| "clauses" : 949, | |
| "name" : "https://gbd.iti.kit.edu/file/06c07aba06d90e0d08f122d33ef30c0a/", | |
| "time" : 236 | |
| }, { | |
| "variables" : 29830, | |
| "clauses" : 726354, | |
| "name" : "https://gbd.iti.kit.edu/file/06c4a06f6c791ebcbd2e90f94d898cee/", | |
| "time" : 30992 | |
| }, { | |
| "variables" : 35130, | |
| "clauses" : 985664, | |
| "name" : "https://gbd.iti.kit.edu/file/06c6e5b5ec743e16bc55089bf42546ad/", | |
| "time" : 38751 | |
| }, { | |
| "variables" : 150, | |
| "clauses" : 3195, | |
| "name" : "https://gbd.iti.kit.edu/file/06c9e7d682595a3ea26501bd57bc36a7/", | |
| "time" : 367 | |
| }, { | |
| "variables" : 18162, | |
| "clauses" : 53637, | |
| "name" : "https://gbd.iti.kit.edu/file/06d2543c151c2478fde159c6dc0424ac/", | |
| "time" : 12178 | |
| }, { | |
| "variables" : 18580, | |
| "clauses" : 321125, | |
| "name" : "https://gbd.iti.kit.edu/file/06d38596ee5a5fd90877de6c04ede06b/", | |
| "time" : 17173 | |
| }, { | |
| "variables" : 25148, | |
| "clauses" : 87632, | |
| "name" : "https://gbd.iti.kit.edu/file/06d6f4f8c3ac52d034143eca8d62d1e7/", | |
| "time" : 19385 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 2940, | |
| "name" : "https://gbd.iti.kit.edu/file/06d7ddacd91c84d9c6be5ace491b410a/", | |
| "time" : 524 | |
| }, { | |
| "variables" : 31450, | |
| "clauses" : 810570, | |
| "name" : "https://gbd.iti.kit.edu/file/06df09f5ff0b34724a6f43c12560c0b1/", | |
| "time" : 35063 | |
| }, { | |
| "variables" : 27058, | |
| "clauses" : 608976, | |
| "name" : "https://gbd.iti.kit.edu/file/06df75fc09ba7eb9f0ffb8d45aa8edfb/", | |
| "time" : 27987 | |
| }, { | |
| "variables" : 110, | |
| "clauses" : 2343, | |
| "name" : "https://gbd.iti.kit.edu/file/06e13d42320e5c9d06d63abce2e978fe/", | |
| "time" : 193 | |
| }, { | |
| "variables" : 1000, | |
| "clauses" : 73331, | |
| "name" : "https://gbd.iti.kit.edu/file/06e46ab0acac57a61638cbb741949a98/", | |
| "time" : 1429 | |
| }, { | |
| "variables" : 29888, | |
| "clauses" : 732547, | |
| "name" : "https://gbd.iti.kit.edu/file/06e5233a7d177a4f94b8a05eadb45368/", | |
| "time" : 32399 | |
| }, { | |
| "variables" : 3450, | |
| "clauses" : 9515, | |
| "name" : "https://gbd.iti.kit.edu/file/06eca5bfcdc4fbde5715c34c87f9ab75/", | |
| "time" : 2513 | |
| }, { | |
| "variables" : 55809, | |
| "clauses" : 179806, | |
| "name" : "https://gbd.iti.kit.edu/file/06f692ab71fb031118f4c946556eca52/", | |
| "time" : 30236 | |
| }, { | |
| "variables" : 3126, | |
| "clauses" : 10972, | |
| "name" : "https://gbd.iti.kit.edu/file/0701a1e3481e99b590185bd6a3f8631c/", | |
| "time" : 2328 | |
| }, { | |
| "variables" : 22207, | |
| "clauses" : 424438, | |
| "name" : "https://gbd.iti.kit.edu/file/07022ad84cf8decdf213d2fd2c59fbae/", | |
| "time" : 21404 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 14000, | |
| "name" : "https://gbd.iti.kit.edu/file/07037b045d5d9dd7d777fa8a3b0366a3/", | |
| "time" : 1021 | |
| }, { | |
| "variables" : 12030, | |
| "clauses" : 191848, | |
| "name" : "https://gbd.iti.kit.edu/file/0703f9c5516bcc84a0c03e872066523f/", | |
| "time" : 10900 | |
| }, { | |
| "variables" : 28301, | |
| "clauses" : 670579, | |
| "name" : "https://gbd.iti.kit.edu/file/0704b6d19c7f53060c2e6b918b955226/", | |
| "time" : 30211 | |
| }, { | |
| "variables" : 27353, | |
| "clauses" : 623249, | |
| "name" : "https://gbd.iti.kit.edu/file/070679b773977c574b9c7b14c7bd923f/", | |
| "time" : 28082 | |
| }, { | |
| "variables" : 22763, | |
| "clauses" : 449651, | |
| "name" : "https://gbd.iti.kit.edu/file/070837da5e4923b6a5f8c0ba0e6ce0e2/", | |
| "time" : 22401 | |
| }, { | |
| "variables" : 29626, | |
| "clauses" : 722387, | |
| "name" : "https://gbd.iti.kit.edu/file/0709175593f5f943e5a793e15ae08395/", | |
| "time" : 31976 | |
| }, { | |
| "variables" : 81672, | |
| "clauses" : 246655, | |
| "name" : "https://gbd.iti.kit.edu/file/070fde310eca4ddf6967896052efcb30/", | |
| "time" : 67590 | |
| }, { | |
| "variables" : 25029, | |
| "clauses" : 528129, | |
| "name" : "https://gbd.iti.kit.edu/file/071e54205d91b7c174af2ca7f686f09b/", | |
| "time" : 25426 | |
| }, { | |
| "variables" : 21897, | |
| "clauses" : 420486, | |
| "name" : "https://gbd.iti.kit.edu/file/072199fed1704b4d1e60b996931c3d6b/", | |
| "time" : 21261 | |
| }, { | |
| "variables" : 320, | |
| "clauses" : 1120, | |
| "name" : "https://gbd.iti.kit.edu/file/072785fd927ff0fd180ce8b9cc00078f/", | |
| "time" : 631 | |
| }, { | |
| "variables" : 27562, | |
| "clauses" : 629451, | |
| "name" : "https://gbd.iti.kit.edu/file/07284bf15be6d7faa78d4deb46c6b275/", | |
| "time" : 28711 | |
| }, { | |
| "variables" : 26225, | |
| "clauses" : 574898, | |
| "name" : "https://gbd.iti.kit.edu/file/072af700ad0e8957ebbaf2993d850923/", | |
| "time" : 26455 | |
| }, { | |
| "variables" : 650, | |
| "clauses" : 2275, | |
| "name" : "https://gbd.iti.kit.edu/file/072cef48d683bfde42340d0ba84c5b1a/", | |
| "time" : 440 | |
| }, { | |
| "variables" : 600, | |
| "clauses" : 3900, | |
| "name" : "https://gbd.iti.kit.edu/file/0733ae02d303c907fa2887f9fbb4ff55/", | |
| "time" : 464 | |
| }, { | |
| "variables" : 28637, | |
| "clauses" : 677907, | |
| "name" : "https://gbd.iti.kit.edu/file/0737a716930b33a5979d86c1eebd835b/", | |
| "time" : 30850 | |
| }, { | |
| "variables" : 26488, | |
| "clauses" : 586429, | |
| "name" : "https://gbd.iti.kit.edu/file/0739014c268a5a12568d0e641f88ad3c/", | |
| "time" : 26914 | |
| }, { | |
| "variables" : 25794, | |
| "clauses" : 554815, | |
| "name" : "https://gbd.iti.kit.edu/file/0739de5c877d844ce28f81e00916a884/", | |
| "time" : 27171 | |
| }, { | |
| "variables" : 23416, | |
| "clauses" : 466802, | |
| "name" : "https://gbd.iti.kit.edu/file/073a405fde5b5c7434281729f24d8728/", | |
| "time" : 24363 | |
| }, { | |
| "variables" : 26275, | |
| "clauses" : 572810, | |
| "name" : "https://gbd.iti.kit.edu/file/0742147dd68e5410c79a8506a7f54a1d/", | |
| "time" : 27972 | |
| }, { | |
| "variables" : 178, | |
| "clauses" : 1768, | |
| "name" : "https://gbd.iti.kit.edu/file/07434c4f17715737ade130bc6c57cf9d/", | |
| "time" : 359 | |
| }, { | |
| "variables" : 28685, | |
| "clauses" : 678561, | |
| "name" : "https://gbd.iti.kit.edu/file/074394da9029d9c82840091246607065/", | |
| "time" : 31331 | |
| }, { | |
| "variables" : 700, | |
| "clauses" : 2450, | |
| "name" : "https://gbd.iti.kit.edu/file/074433cf882b1a959c89579f00593b8b/", | |
| "time" : 495 | |
| }, { | |
| "variables" : 13409, | |
| "clauses" : 478985, | |
| "name" : "https://gbd.iti.kit.edu/file/0746ab2982f4d8c28f10df0900857dd5/", | |
| "time" : 10221 | |
| }, { | |
| "variables" : 24803, | |
| "clauses" : 520373, | |
| "name" : "https://gbd.iti.kit.edu/file/074ff9642153695f0fe804049c743f69/", | |
| "time" : 25481 | |
| }, { | |
| "variables" : 31624, | |
| "clauses" : 816734, | |
| "name" : "https://gbd.iti.kit.edu/file/0754e62937ec75e569b8b4122ad77d7d/", | |
| "time" : 35579 | |
| }, { | |
| "variables" : 190, | |
| "clauses" : 506, | |
| "name" : "https://gbd.iti.kit.edu/file/075c4fe7ae4cef57f1a4c00e58142e23/", | |
| "time" : 259 | |
| }, { | |
| "variables" : 280, | |
| "clauses" : 1196, | |
| "name" : "https://gbd.iti.kit.edu/file/075e1eef00500b25ceb5ea4823ccf1b0/", | |
| "time" : 491 | |
| }, { | |
| "variables" : 10000, | |
| "clauses" : 42670, | |
| "name" : "https://gbd.iti.kit.edu/file/07638411f023fe6a4334c53384415f11/", | |
| "time" : 8258 | |
| }, { | |
| "variables" : 25742, | |
| "clauses" : 558545, | |
| "name" : "https://gbd.iti.kit.edu/file/076955ba5ecdc2feb4587a8abdbe334b/", | |
| "time" : 25952 | |
| }, { | |
| "variables" : 29276, | |
| "clauses" : 702355, | |
| "name" : "https://gbd.iti.kit.edu/file/076ab0a078db7377f3e7cfd6c2aab988/", | |
| "time" : 31921 | |
| }, { | |
| "variables" : 46, | |
| "clauses" : 122, | |
| "name" : "https://gbd.iti.kit.edu/file/076d4d6f83306ee69c35e3c99e30d8f8/", | |
| "time" : 56 | |
| }, { | |
| "variables" : 32084, | |
| "clauses" : 112495, | |
| "name" : "https://gbd.iti.kit.edu/file/076d84ee418eb4192d427e34d8829b93/", | |
| "time" : 23965 | |
| }, { | |
| "variables" : 4412, | |
| "clauses" : 28950, | |
| "name" : "https://gbd.iti.kit.edu/file/076fba8945d3a54a06f326474477077d/", | |
| "time" : 3104 | |
| }, { | |
| "variables" : 24336, | |
| "clauses" : 289842, | |
| "name" : "https://gbd.iti.kit.edu/file/0779cddacfa34241cdf579cb2370ab8e/", | |
| "time" : 26700 | |
| }, { | |
| "variables" : 4128, | |
| "clauses" : 126548, | |
| "name" : "https://gbd.iti.kit.edu/file/0779ed19ae69bf464cce003d1a573246/", | |
| "time" : 2874 | |
| }, { | |
| "variables" : 28641, | |
| "clauses" : 679362, | |
| "name" : "https://gbd.iti.kit.edu/file/077a92393c59108b44554b67217c8d7a/", | |
| "time" : 30604 | |
| }, { | |
| "variables" : 29865, | |
| "clauses" : 734556, | |
| "name" : "https://gbd.iti.kit.edu/file/07896fe3639c24cd24bb032ae19199cc/", | |
| "time" : 32403 | |
| } ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import matplotlib.pyplot as plt | |
| import json | |
| f = open("measurements.json", "r") | |
| l = json.load(f) | |
| print(f"{len(l)} instances") | |
| clauses = list(map(lambda r: r["clauses"], l)) | |
| variables = list(map(lambda r: r["variables"], l)) | |
| time = list(map(lambda r: r["time"] / 1000, l)) | |
| fig = plt.figure() | |
| ax = fig.add_subplot(projection="3d") | |
| ax.scatter(variables, clauses, time) | |
| plt.title("Time to calculate initial layout") | |
| plt.ylabel("clauses") | |
| plt.xlabel("variables") | |
| #ax.zlabel("time") | |
| plt.show() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment