{{"ezfact64_3.sat05-450.reshuffled-07.cnf",UNK,3600.00},{"ezfact256_1.sat05-464.reshuffled-07.cnf",UNK,3600.00},{"ezfact64_4.sat05-451.reshuffled-07.cnf",UNK,3600.00},{"ezfact64_5.sat05-452.reshuffled-07.cnf",UNK,3600.00},{"hgen2-v500-s1216665065.sat05-467.reshuffled-07.cnf",UNK,3600.00},{"ezfact64_6.sat05-453.reshuffled-07.cnf",UNK,3600.00},{"hgen3-v400-s553296708.sat05-471.reshuffled-07.cnf",UNK,3600.00},{"hgen3-v400-s344840348.sat05-470.reshuffled-07.cnf",UNK,3600.00},{"hgen3-v500-s1349121860.sat05-473.reshuffled-07.cnf",UNK,3600.00},{"pyhala-braun-unsat-40-4-02.sat05-459.reshuffled-07.cnf",UNK,3600.00},{"hgen6-4-24-n650-03-S528656311.sat05-477.reshuffled-07.cnf",UNK,3600.00},{"hidden-k3-s0-r5-n700-02-S350203913.sat05-486.reshuffled-07.cnf",UNK,3600.00},{"hidden-k3-s0-r5-n700-01-S2069048075.sat05-488.reshuffled-07.cnf",UNK,3600.00},{"hgen8-n320-02-S1127428711.sat05-484.reshuffled-07.cnf",UNK,3600.00},{"hgen8-n320-01-S1432474240.sat05-483.reshuffled-07.cnf",UNK,3600.00},{"hgen7-n390-01-S248216171.sat05-478.reshuffled-07.cnf",UNK,3600.00},{"hgen7-n390-02-S178568232.sat05-479.reshuffled-07.cnf",UNK,3600.00},{"hgen8-n260-03-S722413478.sat05-482.reshuffled-07.cnf",UNK,3600.00},{"hidden-k3-s0-r5-n700-03-S1609878926.sat05-487.reshuffled-07.cnf",UNK,3600.00},{"hgen8-n320-03-S1572374531.sat05-485.reshuffled-07.cnf",UNK,3600.00},{"999999000001nw.sat05-447.reshuffled-07.cnf",UNS,3055.69},{"bqwh.40.reg.520.sat05-433.reshuffled-07.cnf",UNK,3600.00},{"hwb-n32-01-S1491788039.sat05-497.reshuffled-07.cnf",UNK,3600.00},{"hwb-n28-02-S818962541.sat05-492.reshuffled-07.cnf",UNK,3600.00},{"color-18-4.sat05-443.reshuffled-07.cnf",UNK,3600.00},{"color-11-3.sat05-445.reshuffled-07.cnf",UNK,3600.00},{"bqwh.60.1080.sat05-436.reshuffled-07.cnf",UNK,3600.00},{"hwb-n28-01-S136611085.sat05-491.reshuffled-07.cnf",UNS,2448.38},{"hwb-n26-03-S540351185.sat05-490.reshuffled-07.cnf",UNS,1726.72},{"mm-2x3-8-8-sb.1.sat05-475.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n800-d-0.02-s1542454144.sat05-533.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n1200-d0.00-s1756632460.sat05-526.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n800-d0.02-s925928766.sat05-538.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n800-d0.02-s111845174.sat05-536.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n1200-d-0.02-s405595518.sat05-531.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n1200-d-0.02-s383740539.sat05-534.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n1200-d0.00-s1875077647.sat05-530.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n800-d0.04-s1788334438.sat05-543.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n1200-d0.02-s1099787414.sat05-542.reshuffled-07.cnf",UNK,3600.00},{"connm-ue-csp-sat-n1200-d0.04-s736572600.sat05-546.reshuffled-07.cnf",UNK,3600.00},{"Composite-096BitPrimes-0.sat05-507.reshuffled-07.cnf",UNK,3600.00},{"equilarge_l3.sat05-520.reshuffled-07.cnf",UNK,3600.00},{"ramsey.sat05-511.reshuffled-07.cnf",UNK,3600.00},{"equilarge_l4.sat05-521.reshuffled-07.cnf",UNK,3600.00},{"Composite-048BitPrimes-0.sat05-503.reshuffled-07.cnf",UNK,3600.00},{"equilarge_l5.sat05-522.reshuffled-07.cnf",UNK,3600.00},{"equilarge_l2.sat05-519.reshuffled-07.cnf",UNK,3600.00},{"Composite-064BitPrimes-1.sat05-506.reshuffled-07.cnf",UNK,3600.00},{"Composite-048BitPrimes-1.sat05-504.reshuffled-07.cnf",UNK,3600.00},{"CompositeRSA576.sat05-509.reshuffled-07.cnf",UNK,3600.00},{"QG7a-gensys-icl004.sat05-3825.reshuffled-07.cnf",UNK,3600.00},{"QG7-gensys-icl100.sat05-3226.reshuffled-07.cnf",UNK,3600.00},{"QG7-gensys-ukn003.sat05-3346.reshuffled-07.cnf",UNS,2205.18},{"QG7a-gensys-ukn002.sat05-3842.reshuffled-07.cnf",UNK,3600.00},{"QG7a-gensys-ukn009.sat05-3849.reshuffled-07.cnf",UNK,3600.00},{"QG7-dead-dnd005.sat05-3111.reshuffled-07.cnf",UNS,348.09},{"QG7a-gensys-icl009.sat05-3830.reshuffled-07.cnf",UNK,3600.00},{"QG7-dead-dnd002.sat05-3108.reshuffled-07.cnf",UNS,1542.60},{"QG7a-gensys-icl001.sat05-3822.reshuffled-07.cnf",UNK,3600.00},{"QG7-dead-dnd001.sat05-3419.reshuffled-07.cnf",UNS,1032.85},{"phnf-size10-exclusive-philo.used-as.sat04-988.sat05-4195.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-equilarge_l3.used-as.sat04-895.sat05-4189.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-all.used-as.sat04-986.sat05-4198.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-equilarge_l2.used-as.sat04-894.sat05-4188.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-luckySeven.used-as.sat04-990.sat05-4196.reshuffled-07.cnf",UNS,2289.51},{"phnf-size10-exclusive-equilarge_l1.used-as.sat04-893.sat05-4187.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-myciel6-cn.used-as.sat04-319.sat05-4201.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-equilarge_m3.used-as.sat04-900.sat05-4186.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-FIFO.used-as.sat04-991.sat05-4192.reshuffled-07.cnf",UNK,3600.00},{"phnf-size10-exclusive-gigamax.used-as.sat04-984.sat05-4194.reshuffled-07.cnf",UNS,1100.50},{"unsat-set-a-fclqcolor-10-06-07.sat05-1274.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-b-fclqcolor-25-18-23.sat05-1287.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-a-clqcolor-12-07-08.sat05-1251.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-a-fclqcolor-20-13-14.sat05-1278.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-a-clqcolor-30-19-20.sat05-1256.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-b-clqcolor-16-11-14.sat05-1261.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-b-fclqcolor-10-07-09.sat05-1282.reshuffled-07.cnf",UNS,2111.77},{"unsat-set-b-clqcolor-30-20-26.sat05-1264.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-a-clqcolor-10-06-07.sat05-1250.reshuffled-07.cnf",UNK,3600.00},{"unsat-set-a-clqcolor-16-10-11.sat05-1253.reshuffled-07.cnf",UNK,3600.00},{"easier-fphp-035-029.sat05-1221.reshuffled-07.cnf",UNK,3600.00},{"harder-php-045-044.sat05-1195.reshuffled-07.cnf",UNK,3600.00},{"harder-fphp-018-017.sat05-1231.reshuffled-07.cnf",UNK,3600.00},{"easier-php-035-029.sat05-1179.reshuffled-07.cnf",UNK,3600.00},{"easier-fphp-020-015.sat05-1218.reshuffled-07.cnf",UNK,3600.00},{"harder-php-025-024.sat05-1191.reshuffled-07.cnf",UNK,3600.00},{"harder-fphp-070-069.sat05-1240.reshuffled-07.cnf",UNK,3600.00},{"harder-fphp-035-034.sat05-1235.reshuffled-07.cnf",UNK,3600.00},{"harder-fphp-016-015.sat05-1230.reshuffled-07.cnf",UNK,3600.00},{"harder-fphp-050-049.sat05-1238.reshuffled-07.cnf",UNK,3600.00},{"mod2c-rand3bip-sat-220-2.sat05-2489.reshuffled-07.cnf",UNK,3600.00},{"linvrinv9.sat05-568.reshuffled-07.cnf",UNK,3600.00},{"eulcbip-8-UNSAT.sat05-3937.reshuffled-07.cnf",UNK,3600.00},{"sgp_5-6-8.sat05-2669.reshuffled-07.cnf",UNK,3600.00},{"linvrinv6.sat05-565.reshuffled-07.cnf",UNK,3600.00},{"sgp_9-8-8.sat05-2674.reshuffled-07.cnf",UNK,3600.00},{"strips-gripper-12t22.sat05-1151.reshuffled-07.cnf",UNK,3600.00},{"mod2c-rand3bip-sat-220-1.sat05-2488.reshuffled-07.cnf",UNK,3600.00},{"linvrinv8.sat05-567.reshuffled-07.cnf",UNK,3600.00},{"strips-gripper-18t35.sat05-1147.reshuffled-07.cnf",UNK,3600.00},{"counting-easier-fphp-012-010.sat05-1214.reshuffled-07.cnf",UNS,111.69},{"sat-strips-gripper-12t23.sat05-1144.reshuffled-07.cnf",SAT,151.79},{"unsat-logistics-rotate-09t5.sat05-1139.reshuffled-07.cnf",UNS,20.32},{"gt-ordering-unsat-gt-035.sat05-1308.reshuffled-07.cnf",UNK,3600.00},{"gt-ordering-unsat-gt-030.sat05-1307.reshuffled-07.cnf",UNK,3600.00},{"counting-clqcolor-unsat-set-b-clqcolor-08-06-07.sat05-1257.reshuffled-07.cnf",UNS,8.09},{"gt-ordering-unsat-gt-025.sat05-1306.reshuffled-07.cnf",UNK,3600.00},{"gt-ordering-sat-gt-030.sat05-1295.reshuffled-07.cnf",UNK,3600.00},{"sat-strips-gripper-10t19.sat05-1143.reshuffled-07.cnf",SAT,34.64},{"counting-easier-php-012-010.sat05-1172.reshuffled-07.cnf",UNS,113.25},{"QG7a-gensys-ukn001.sat05-3841.reshuffled-07.cnf",SAT,127.85},{"pmg-11-UNSAT.sat05-3939.reshuffled-07.cnf",UNS,1255.76},{"QG8-gensys-ukn005.sat05-3584.reshuffled-07.cnf",UNS,201.15},{"gensys-ukn002.sat05-2744.reshuffled-07.cnf",UNS,206.80},{"QG-gensys-brn008.sat05-2685.reshuffled-07.cnf",UNS,90.33},{"QG7a-gensys-brn004.sat05-3669.reshuffled-07.cnf",SAT,79.95},{"QG7-gensys-icl001.sat05-2926.reshuffled-07.cnf",UNS,37.33},{"QG-gensys-icl003.sat05-2715.reshuffled-07.cnf",UNS,109.79},{"QG7a-gensys-ukn005.sat05-3845.reshuffled-07.cnf",SAT,105.18},{"QG7a-gensys-brn100.sat05-3765.reshuffled-07.cnf",SAT,25.20},{"mod2-rand3bip-sat-240-3.sat05-2205.reshuffled-07.cnf",SAT,489.60},{"mod2-rand3bip-sat-220-2.sat05-2174.reshuffled-07.cnf",SAT,1013.72},{"mod2-3cage-unsat-9-12.sat05-2587.reshuffled-07.cnf",UNS,124.69},{"mod2-rand3bip-sat-230-2.sat05-2189.reshuffled-07.cnf",SAT,121.53},{"mod2-rand3bip-sat-210-1.sat05-2158.reshuffled-07.cnf",SAT,54.31},{"mod2-3cage-unsat-9-14.sat05-2589.reshuffled-07.cnf",UNS,107.54},{"mod2-rand3bip-sat-210-2.sat05-2159.reshuffled-07.cnf",SAT,12.96},{"mod2-rand3bip-sat-250-3.sat05-2220.reshuffled-07.cnf",SAT,3031.82},{"mod2c-rand3bip-sat-190-3.sat05-2445.reshuffled-07.cnf",SAT,154.66},{"mod2-rand3bip-sat-220-1.sat05-2173.reshuffled-07.cnf",SAT,288.65},{"unsat-grid-pbl-0080.sat05-1344.reshuffled-07.cnf",UNK,3600.00},{"unsat-pbl-00250.sat05-1330.reshuffled-07.cnf",UNK,3600.00},{"unsat-pbl-00070.sat05-1324.reshuffled-07.cnf",UNK,3600.00},{"unsat-pbl-00080.sat05-1325.reshuffled-07.cnf",UNK,3600.00},{"unsat-pbl-00200.sat05-1329.reshuffled-07.cnf",UNK,3600.00},{"unsat-pbl-00090.sat05-1326.reshuffled-07.cnf",UNK,3600.00},{"unsat-pbl-00150.sat05-1328.reshuffled-07.cnf",UNK,3600.00},{"sat-pbl-00400.sat05-1322.reshuffled-07.cnf",SAT,5.21},{"sat-grid-pbl-0070.sat05-1334.reshuffled-07.cnf",SAT,27.97},{"sat-grid-pbl-0200.sat05-1339.reshuffled-07.cnf",SAT,1638.03},{"QG6-dead-dnd001.sat05-2742.reshuffled-07.cnf",UNS,126.78},{"QG6-gensys-icl004.sat05-2716.reshuffled-07.cnf",UNS,178.59},{"QG6-gensys-icl001.sat05-2695.reshuffled-07.cnf",UNS,526.75},{"QG6-gensys-ukn003.sat05-2726.reshuffled-07.cnf",UNS,793.86},{"QG6-gensys-icl008.sat05-2720.reshuffled-07.cnf",UNS,2767.83},{"QG6-gensys-icl009.sat05-2721.reshuffled-07.cnf",UNS,226.57},{"QG6-gensys-icl006.sat05-2718.reshuffled-07.cnf",UNS,127.97},{"QG7-gensys-icl006.sat05-3132.reshuffled-07.cnf",UNS,685.91},{"QG6-gensys-brn007.sat05-2684.reshuffled-07.cnf",UNS,274.79},{"QG6-dead-dnd002.sat05-2713.reshuffled-07.cnf",UNK,3600.00},{"counting-easier-php-018-014.sat05-1175.reshuffled-07.cnf",UNK,3600.00},{"gt-ordering-unsat-gt-045.sat05-1310.reshuffled-07.cnf",UNK,3600.00},{"gt-ordering-sat-gt-040.sat05-1297.reshuffled-07.cnf",UNK,3600.00},{"counting-easier-fphp-014-012.sat05-1215.reshuffled-07.cnf",UNK,3600.00},{"grid-pebbling-unsat-grid-pbl-0300.sat05-1350.sat05-1350.reshuffled-07.cnf",UNK,3600.00},{"grid-pebbling-sat-grid-pbl-0300.sat05-1341.sat05-1341.reshuffled-07.cnf",UNK,3600.00},{"counting-harder-php-014-013.sat05-1187.reshuffled-07.cnf",UNK,3600.00},{"logistics-unsat-logistics-rotate-11t5.sat05-1141.reshuffled-07.cnf",UNK,3600.00},{"gt-ordering-unsat-gt-060.sat05-1312.reshuffled-07.cnf",UNK,3600.00},{"counting-harder-php-018-017.sat05-1189.reshuffled-07.cnf",UNK,3600.00},{"pmg-14-UNSAT.sat05-3942.reshuffled-07.cnf",UNK,3600.00},{"pmg-13-UNSAT.sat05-3941.reshuffled-07.cnf",UNK,3600.00},{"pmg-12-UNSAT.sat05-3940.reshuffled-07.cnf",UNK,3600.00},{"linvrinv5.sat05-564.reshuffled-07.cnf",UNK,3600.00},{"sgp_6-6-10.sat05-2670.reshuffled-07.cnf",SAT,1571.68},{"sgp_5-5-6.sat05-2675.reshuffled-07.cnf",UNK,3600.00},{"mod2c-rand3bip-sat-210-3.sat05-2475.reshuffled-07.cnf",UNK,3600.00},{"mod2-rand3bip-sat-280-1.sat05-2263.reshuffled-07.cnf",SAT,2615.72},{"mod2-rand3bip-sat-280-2.sat05-2264.reshuffled-07.cnf",UNK,3600.00},{"mod2-rand3bip-sat-280-3.sat05-2265.reshuffled-07.cnf",SAT,724.52},{"mod2-rand3bip-sat-270-1.sat05-2248.reshuffled-07.cnf",UNK,3600.00},{"mod2-rand3bip-sat-270-2.sat05-2249.reshuffled-07.cnf",UNK,3600.00},{"mod2c-3cage-unsat-10-2.sat05-2567.reshuffled-07.cnf",UNK,3600.00},{"mod2c-rand3bip-unsat-120-3.sat05-2340.reshuffled-07.cnf",UNS,381.54},{"mod2c-3cage-unsat-10-3.sat05-2568.reshuffled-07.cnf",UNK,3600.00},{"mod2c-rand3bip-unsat-135-2.sat05-2354.reshuffled-07.cnf",UNS,984.18},{"contest04-connm-ue-csp-sat-n800-d0.04-s362703357.sat05-548.reshuffled-07.cnf",UNS,1388.96},{"contest04-lksat-n1000-m6860-k4-l4-s1935114289.sat05-523.reshuffled-07.cnf",UNS,1608.38},{"contest03-hwb-n26-01-S1957858365.sat05-500.reshuffled-07.cnf",UNS,1027.86},{"contest02-ezfact64_10.sat05-449.reshuffled-07.cnf",UNK,3600.00},{"contest04-lksat-n1100-m7545-k4-l4-s310659001.sat05-524.reshuffled-07.cnf",UNS,736.39},{"contest03-SGI_30_50_30_20_1-dir.sat05-439.reshuffled-07.cnf",UNS,186.19},{"contest04-connm-ue-csp-sat-n600-d0.02-s1676244754.sat05-535.reshuffled-07.cnf",UNS,570.61},{"contest03-SGI_30_50_30_20_3-dir.sat05-440.reshuffled-07.cnf",UNS,301.43},{"contest02-Mat26.sat05-457.reshuffled-07.cnf",UNS,435.17},{"s101-100.cnf",UNK,3600.00},{"s105-100.cnf",UNK,3600.00},{"s113-100.cnf",UNK,3600.00},{"s109-100.cnf",UNK,3600.00},{"s97-100.cnf",UNK,3600.00},{"s117-100.cnf",UNK,3600.00},{"s81-100.cnf",UNS,256.76},{"s69-100.cnf",UNS,10.70},{"s77-100.cnf",UNS,59.56},{"s85-100.cnf",UNS,381.82},{"s93-100.cnf",UNS,1033.40},{"s61-100.cnf",UNS,1.75},{"s89-100.cnf",UNS,668.33},{"s57-100.cnf",UNS,1.37},{"s65-100.cnf",UNS,7.22},{"s73-100.cnf",UNS,40.25},{"AProVE07-01.cnf",UNK,3600.00},{"AProVE07-03.cnf",UNS,1516.07},{"AProVE07-08.cnf",UNS,2017.77},{"AProVE07-25.cnf",UNK,3600.00},{"AProVE07-26.cnf",UNK,3600.00},{"AProVE07-27.cnf",UNK,3600.00},{"AProVE07-02.cnf",UNS,970.00},{"AProVE07-04.cnf",UNS,255.13},{"AProVE07-06.cnf",UNS,464.34},{"AProVE07-09.cnf",UNK,3600.00},{"AProVE07-11.cnf",SAT,229.77},{"AProVE07-15.cnf",UNS,266.65},{"AProVE07-16.cnf",UNS,2552.03},{"AProVE07-20.cnf",UNS,292.92},{"AProVE07-21.cnf",UNS,863.76},{"AProVE07-22.cnf",UNS,240.90},{"dspam_dump_vc949.cnf",UNS,1.08},{"dspam_dump_vc950.cnf",UNS,2.45},{"dspam_dump_vc962.cnf",UNK,3600.00},{"dspam_dump_vc972.cnf",UNS,55.15},{"dspam_dump_vc973.cnf",UNK,3600.00},{"dspam_dump_vc1080.cnf",UNK,3600.00},{"dspam_dump_vc1081.cnf",UNK,3600.00},{"dspam_dump_vc1093.cnf",UNK,3600.00},{"dspam_dump_vc1103.cnf",UNK,3600.00},{"dspam_dump_vc1104.cnf",UNK,3600.00},{"itox_vc909.cnf",SAT,118.39},{"itox_vc1033.cnf",SAT,81.01},{"itox_vc1044.cnf",SAT,61.56},{"itox_vc965.cnf",UNS,0.30},{"itox_vc979.cnf",UNS,0.32},{"itox_vc1130.cnf",UNK,3600.00},{"itox_vc1138.cnf",SAT,124.88},{"xinetd_vc56687.cnf",UNS,0.28},{"xinetd_vc56703.cnf",UNS,0.22},{"itox_vc1216.cnf",UNS,0.43},{"hsat_vc11817.cnf",UNS,6.29},{"hsat_vc11935.cnf",UNS,3.53},{"hsat_vc11944.cnf",UNS,5.09},{"hsat_vc12016.cnf",UNS,8.28},{"hsat_vc12062.cnf",UNS,9.66},{"hsat_vc12070.cnf",UNS,4.76},{"hsat_vc12072.cnf",UNS,2.42},{"hsat_vc11773.cnf",UNS,6.56},{"hsat_vc11803.cnf",UNS,33.07},{"hsat_vc11813.cnf",UNS,42.94},{"vmpc_24.cnf",SAT,99.09},{"vmpc_25.cnf",SAT,149.95},{"vmpc_26.cnf",SAT,207.60},{"vmpc_27.cnf",SAT,114.45},{"vmpc_28.cnf",SAT,901.75},{"vmpc_29.cnf",UNK,3600.00},{"vmpc_30.cnf",SAT,1524.16},{"vmpc_31.cnf",UNK,3600.00},{"vmpc_33.cnf",UNK,3600.00},{"vmpc_34.cnf",UNK,3600.00},{"uts-l05-ipc5-h27-unknown.cnf",UNS,289.80},{"uts-l06-ipc5-h33-unknown.cnf",UNS,1749.29},{"uts-l06-ipc5-h34-unknown.cnf",SAT,160.37},{"uts-l06-ipc5-h30-unknown.cnf",UNS,396.79},{"uts-l06-ipc5-h35-unknown.cnf",SAT,92.72},{"uts-l06-ipc5-h31-unknown.cnf",UNS,459.80},{"uts-l06-ipc5-h28-unknown.cnf",UNS,325.05},{"uts-l06-ipc5-h32-unknown.cnf",UNS,2900.47},{"uts-l06-ipc5-h29-unknown.cnf",UNS,603.61},{"uts-l05-ipc5-h26-unsat.cnf",UNS,131.83},{"sortnet-8-ipc5-h19-sat.cnf",UNK,3600.00},{"safe-50-h49-unsat.cnf",UNK,3600.00},{"sortnet-8-ipc5-h18-unsat.cnf",UNK,3600.00},{"safe-30-h29-unsat.cnf",UNK,3600.00},{"safe-50-h50-sat.cnf",UNK,3600.00},{"sortnet-6-ipc5-h11-unsat.cnf",UNK,3600.00},{"sortnet-7-ipc5-h15-unsat.cnf",UNK,3600.00},{"cube-9-h10-unsat.cnf",UNS,179.23},{"blocks-4-ipc5-h22-unknown.cnf",UNS,388.40},{"cube-11-h14-sat.cnf",UNK,3600.00},{"emptyroom-4-h22-sat.cnf",UNK,3600.00},{"safe-30-h30-sat.cnf",SAT,1671.73},{"cube-9-h11-sat.cnf",SAT,807.90},{"cube-11-h13-unsat.cnf",UNS,3315.89},{"emptyroom-4-h21-unsat.cnf",UNK,3600.00},{"sortnet-7-ipc5-h16-sat.cnf",UNK,3600.00},{"blocks-4-ipc5-h21-unknown.cnf",UNS,259.00},{"9dlx_vliw_at_b_iq1.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq2.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq3.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq4.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq5.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq6.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq7.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq8.cnf",UNK,3600.00},{"9dlx_vliw_at_b_iq9.cnf",UNK,3600.00},{"manol-pipe-f10ni.cnf",UNK,3600.00},{"manol-pipe-f9b.cnf",UNK,3600.00},{"manol-pipe-f9n.cnf",UNK,3600.00},{"manol-pipe-g10bidw.cnf",UNK,3600.00},{"manol-pipe-c7nidw.cnf",UNK,3600.00},{"manol-pipe-g10nid.cnf",UNK,3600.00},{"manol-pipe-c10nidw_s.cnf",UNK,3600.00},{"manol-pipe-c7bidw_i.cnf",UNK,3600.00},{"manol-pipe-c6nidw_i.cnf",UNS,661.92},{"manol-pipe-f7idw.cnf",UNS,2168.78},{"mizh-sha0-35-2.cnf",SAT,87.25},{"mizh-sha0-35-3.cnf",SAT,237.44},{"mizh-sha0-35-4.cnf",SAT,120.25},{"mizh-sha0-35-5.cnf",SAT,182.73},{"mizh-sha0-36-2.cnf",SAT,836.97},{"mizh-md5-47-3.cnf",SAT,163.52},{"mizh-md5-47-4.cnf",SAT,112.17},{"mizh-md5-47-5.cnf",SAT,140.21},{"mizh-md5-48-2.cnf",SAT,153.12},{"mizh-md5-48-5.cnf",SAT,358.15},{"IBM_FV_2004_rule_batch_30_SAT_dat.k100.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k10.cnf",UNS,7.01},{"IBM_FV_2004_rule_batch_30_SAT_dat.k15.cnf",UNS,497.35},{"IBM_FV_2004_rule_batch_30_SAT_dat.k20.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k25.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k30.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k35.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k40.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k45.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k50.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k55.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k60.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k65.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k70.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k75.cnf",SAT,652.49},{"IBM_FV_2004_rule_batch_30_SAT_dat.k80.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k85.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k90.cnf",UNK,3600.00},{"IBM_FV_2004_rule_batch_30_SAT_dat.k95.cnf",UNK,3600.00},{"clauses-10.cnf",UNS,125.60},{"clauses-2.cnf",SAT,3.23},{"clauses-4.cnf",SAT,1482.99},{"clauses-6.cnf",UNK,3600.00},{"clauses-8.cnf",UNK,3600.00},{"9vliw_m_9stages_iq3_C1_bug1.cnf",SAT,86.57},{"9vliw_m_9stages_iq3_C1_bug2.cnf",SAT,93.60},{"9vliw_m_9stages_iq3_C1_bug3.cnf",SAT,72.90},{"9vliw_m_9stages_iq3_C1_bug4.cnf",SAT,32.57},{"9vliw_m_9stages_iq3_C1_bug5.cnf",SAT,133.99},{"9vliw_m_9stages_iq3_C1_bug6.cnf",SAT,65.31},{"9vliw_m_9stages_iq3_C1_bug7.cnf",SAT,47.22},{"9vliw_m_9stages_iq3_C1_bug8.cnf",SAT,101.66},{"9vliw_m_9stages_iq3_C1_bug9.cnf",SAT,32.08},{"9vliw_m_9stages_iq3_C1_bug10.cnf",SAT,47.10},{"eq.atree.braun.10.unsat.cnf",UNS,487.14},{"eq.atree.braun.9.unsat.cnf",UNS,104.81},{"eq.atree.braun.13.unsat.cnf",UNK,3600.00},{"eq.atree.braun.8.unsat.cnf",UNS,28.44},{"eq.atree.braun.12.unsat.cnf",UNK,3600.00},{"eq.atree.braun.7.unsat.cnf",UNS,2.47},{"eq.atree.braun.11.unsat.cnf",UNS,2660.79},{"SAT_dat.k70.cnf",UNK,3600.00},{"SAT_dat.k75.cnf",UNK,3600.00},{"SAT_dat.k80.cnf",UNK,3600.00},{"SAT_dat.k85.cnf",UNK,3600.00},{"SAT_dat.k90.cnf",UNK,3600.00},{"SAT_dat.k95.cnf",UNK,3600.00},{"SAT_dat.k100.cnf",UNK,3600.00},{"SAT_dat.k1.cnf",UNS,0.09},{"SAT_dat.k10.cnf",UNS,0.15},{"SAT_dat.k15.cnf",UNS,1.91},{"SAT_dat.k20.cnf",UNS,15.76},{"SAT_dat.k25.cnf",UNS,192.71},{"SAT_dat.k30.cnf",UNK,3600.00},{"SAT_dat.k35.cnf",UNK,3600.00},{"SAT_dat.k40.cnf",UNK,3600.00},{"SAT_dat.k45.cnf",UNK,3600.00},{"SAT_dat.k50.cnf",UNK,3600.00},{"SAT_dat.k55.cnf",UNK,3600.00},{"SAT_dat.k60.cnf",UNK,3600.00},{"SAT_dat.k65.cnf",UNK,3600.00},{"dated-5-15-s.cnf",SAT,3.51},{"total-5-11-s.cnf",SAT,35.31},{"dated-10-11-s.cnf",SAT,231.66},{"dated-10-19-s.cnf",SAT,39.24},{"dated-5-17-s.cnf",SAT,6.26},{"total-5-13-s.cnf",SAT,4.42},{"dated-5-11-s.cnf",SAT,12.08},{"total-10-11-s.cnf",SAT,13.71},{"dated-5-19-s.cnf",SAT,7.67},{"total-5-15-s.cnf",SAT,6.16},{"dated-10-15-s.cnf",SAT,32.21},{"dated-5-13-s.cnf",SAT,26.52},{"total-10-13-s.cnf",SAT,163.03},{"dated-5-15-u.cnf",UNS,1451.00},{"dated-10-11-u.cnf",UNK,3600.00},{"partial-5-11-u.cnf",UNK,3600.00},{"partial-10-13-u.cnf",UNK,3600.00},{"total-10-15-u.cnf",UNK,3600.00},{"total-5-19-u.cnf",UNK,3600.00},{"dated-10-19-u.cnf",UNK,3600.00},{"partial-5-19-u.cnf",UNK,3600.00},{"dated-5-17-u.cnf",UNS,2408.63},{"dated-10-13-u.cnf",UNK,3600.00},{"partial-5-13-u.cnf",UNK,3600.00},{"partial-10-15-u.cnf",UNK,3600.00},{"total-10-17-u.cnf",UNK,3600.00},{"dated-5-19-u.cnf",UNK,3600.00},{"total-5-15-u.cnf",UNK,3600.00},{"partial-5-15-u.cnf",UNK,3600.00},{"partial-10-17-u.cnf",UNK,3600.00},{"total-10-19-u.cnf",UNK,3600.00},{"dated-5-13-u.cnf",UNK,3600.00},{"partial-10-11-u.cnf",UNK,3600.00},{"total-5-17-u.cnf",UNK,3600.00},{"dated-10-17-u.cnf",UNK,3600.00},{"partial-5-17-u.cnf",UNK,3600.00},{"partial-10-19-u.cnf",UNK,3600.00},{"partial-10-13-s.cnf",UNK,3600.00},{"partial-5-19-s.cnf",UNK,3600.00},{"partial-10-15-s.cnf",UNK,3600.00},{"partial-10-17-s.cnf",UNK,3600.00},{"partial-10-11-s.cnf",UNK,3600.00},{"partial-5-17-s.cnf",UNK,3600.00},{"partial-10-19-s.cnf",UNK,3600.00},{"total-5-11-u.cnf",UNS,23.02},{"total-5-13-u.cnf",UNS,125.48},{"dated-5-11-u.cnf",UNS,290.07},{"total-10-11-u.cnf",UNS,152.92},{"dated-10-15-u.cnf",UNS,47.21},{"total-10-13-u.cnf",UNK,3600.00},{"partial-5-11-s.cnf",UNK,3600.00},{"total-10-15-s.cnf",UNK,3600.00},{"total-5-19-s.cnf",UNK,3600.00},{"dated-10-13-s.cnf",SAT,956.17},{"partial-5-13-s.cnf",UNK,3600.00},{"total-10-17-s.cnf",UNK,3600.00},{"partial-5-15-s.cnf",UNK,3600.00},{"total-10-19-s.cnf",SAT,183.55},{"total-5-17-s.cnf",SAT,1606.26},{"dated-10-17-s.cnf",UNK,3600.00}}