25631 142227 1650 600 aaai10-planning-ipc5-pathways-13-step17.cnf 50277 283903 610 690 aaai10-planning-ipc5-pathways-17-step20.cnf 53919 308235 2730 500 aaai10-planning-ipc5-pathways-17-step21.cnf 63349 943492 530 520 aaai10-planning-ipc5-pipesworld-12-step15.cnf 68952 1029036 10 50 aaai10-planning-ipc5-pipesworld-12-step16.cnf 130021 2509375 20 20 aaai10-planning-ipc5-pipesworld-18-step15.cnf 141856 2742601 80 1140 aaai10-planning-ipc5-pipesworld-18-step16.cnf 224228 5314673 90 90 aaai10-planning-ipc5-pipesworld-27-step13.cnf 249618 5949456 110 70 aaai10-planning-ipc5-pipesworld-27-step14.cnf 29317 277090 10 10 aaai10-planning-ipc5-rovers-18-step11.cnf 32523 308440 10 10 aaai10-planning-ipc5-rovers-18-step12.cnf 99736 783991 5020 3380 aaai10-planning-ipc5-TPP-21-step11.cnf 314455 2920820 20 20 aaai10-planning-ipc5-TPP-30-step11.cnf 8080 96704 10000 10000 aes_128_10_keyfind_1.cnf 1192 10656 10000 10000 aes_128_1_keyfind_1.cnf 2000 20544 10000 10000 aes_128_2_keyfind_1.cnf 2808 30432 10000 10000 aes_128_3_keyfind_1.cnf 300 1016 10 10 aes_32_1_keyfind_1.cnf 504 1840 10 10 aes_32_2_keyfind_1.cnf 708 2664 810 440 aes_32_3_keyfind_1.cnf 912 3488 10000 10000 aes_32_4_keyfind_1.cnf 1116 4312 10000 10000 aes_32_5_keyfind_1.cnf 596 2780 90 3390 aes_64_1_keyfind_1.cnf 1000 5176 10000 10000 aes_64_2_keyfind_1.cnf 1404 7572 10000 10000 aes_64_3_keyfind_1.cnf 1808 9968 10000 10000 aes_64_4_keyfind_1.cnf 214734 743081 10 10 AProVE11-02.cnf 302076 1039056 1420 1640 AProVE11-06.cnf 233177 782677 10 10 AProVE11-07.cnf 68779 234693 10 10 AProVE11-09.cnf 289828 1008603 30 10 AProVE11-10.cnf 96526 325263 20 20 AProVE11-11.cnf 44805 149118 10 10 AProVE11-12.cnf 504189 1742927 10 10 AProVE11-13.cnf 66715 228274 10 10 AProVE11-15.cnf 84025 282766 10 10 AProVE11-16.cnf 489685 8779920 2700 2360 blocks-blocks-36-0.120-NOTKNOWN.cnf 652445 11706080 30 90 blocks-blocks-36-0.160-NOTKNOWN.cnf 693135 12437620 140 160 blocks-blocks-36-0.170-NOTKNOWN.cnf 733825 13169160 50 110 blocks-blocks-36-0.180-SAT.cnf 516641 9436757 90 120 blocks-blocks-37-1.120-NOTKNOWN.cnf 559571 10223027 1880 1820 blocks-blocks-37-1.130-NOTKNOWN.cnf 645431 11795567 30 30 blocks-blocks-37-1.150-SAT.cnf 15364 2210893 10000 10000 E00N23.cnf 15364 2133873 10000 10000 E00X23.cnf 6664 69700 60 30 E02F17.cnf 10420 395383 100 300 E02F20.cnf 13574 1301188 330 590 E02F22.cnf 6664 93544 10 10 E03N17.cnf 9044 295685 80 30 E04F19.cnf 10420 484053 80 110 E04F20.cnf 7794 120068 10 10 E04N18.cnf 7794 126826 20 20 E05F18.cnf 10420 481346 80 80 E05F20.cnf 4740 41379 10 10 E05X15.cnf 4740 41363 10 10 E07N15.cnf 4740 44327 10 10 E15N15.cnf 257380 2139615 510 490 grid-strips-grid-y-3.035-NOTKNOWN.cnf 281936 2464339 20 20 grid-strips-grid-y-4.025-NOTKNOWN.cnf 63327 174791 10 10 hwmcc10-timeframe-expansion-k45-bc57sensorsp1-tseitin.cnf 82007 241364 100 90 hwmcc10-timeframe-expansion-k45-bobsm5378d2-tseitin.cnf 44692 129620 10000 10000 hwmcc10-timeframe-expansion-k45-bobsmhdlc2-tseitin.cnf 98935 296405 620 610 hwmcc10-timeframe-expansion-k45-pdtpmsgoodbakery-tseitin.cnf 89190 265718 10000 10000 hwmcc10-timeframe-expansion-k45-pdtpmspalu-tseitin.cnf 156721 469046 10 10 hwmcc10-timeframe-expansion-k45-pdtswvqis8x8p2-tseitin.cnf 160244 479591 10 10 hwmcc10-timeframe-expansion-k45-pdtswvrod6x8p1-tseitin.cnf 96095 285404 10 10 hwmcc10-timeframe-expansion-k45-pdtswvtms14x8p1-tseitin.cnf 102621 307469 60 50 hwmcc10-timeframe-expansion-k45-pdtviseisenberg1-tseitin.cnf 163622 488120 10000 10000 hwmcc10-timeframe-expansion-k45-pdtvisns3p02-tseitin.cnf 156058 466691 2460 3370 hwmcc10-timeframe-expansion-k45-pdtvissoap1-tseitin.cnf 71285 196970 10 10 hwmcc10-timeframe-expansion-k50-bc57sensorsp2-tseitin.cnf 70297 194006 10 10 hwmcc10-timeframe-expansion-k50-bc57sensorsp3-tseitin.cnf 70167 209513 10 10 hwmcc10-timeframe-expansion-k50-bjrb07amba2andenv-tseitin.cnf 192503 564953 10000 10000 hwmcc10-timeframe-expansion-k50-eijkbs6669-tseitin.cnf 56536 158531 10 10 hwmcc10-timeframe-expansion-k50-nusmvreactorp4-tseitin.cnf 88352 262658 2510 3160 hwmcc10-timeframe-expansion-k50-pdtpmsns2-tseitin.cnf 154038 460862 10 10 hwmcc10-timeframe-expansion-k50-pdtswvsam6x8p3-tseitin.cnf 115266 345359 40 40 hwmcc10-timeframe-expansion-k50-pdtviseisenberg2-tseitin.cnf 116405 346850 10 10 hwmcc10-timeframe-expansion-k50-pdtvisns2p3-tseitin.cnf 183325 546914 10000 10000 hwmcc10-timeframe-expansion-k50-pdtvisns3p00-tseitin.cnf 4740 45569 30 10 korf-15.cnf 6664 89966 410 200 korf-17.cnf 7794 186934 10000 370 korf-18.cnf 95456 477186 10000 10000 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_1.025-NOTKNOWN.cnf 133566 667976 10000 10000 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_1.035-NOTKNOWN.cnf 171676 858766 10000 10000 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_1.045-NOTKNOWN.cnf 95456 483561 10000 10000 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_3.025-NOTKNOWN.cnf 133566 676901 10000 10000 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_3.035-NOTKNOWN.cnf 171676 870241 10000 10000 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_3.045-NOTKNOWN.cnf 324116 1643601 10 40 openstacks-sequencedstrips-nonadl-nonnegated-ossequencedstrips-p30_3.085-SAT.cnf 17298 57292 200 90 slp-synthesis-aes-bottom12.cnf 19995 66333 3370 740 slp-synthesis-aes-bottom13.cnf 22886 76038 10000 10000 slp-synthesis-aes-bottom14.cnf 25972 86411 10000 10000 slp-synthesis-aes-bottom15.cnf 29254 97456 10000 10000 slp-synthesis-aes-bottom16.cnf 32733 109177 10000 10000 slp-synthesis-aes-bottom17.cnf 36410 121578 10000 10000 slp-synthesis-aes-bottom18.cnf 40286 134663 10000 10000 slp-synthesis-aes-bottom19.cnf 44362 148436 10000 10000 slp-synthesis-aes-bottom20.cnf 48639 162901 10000 10000 slp-synthesis-aes-bottom21.cnf 53118 178062 10000 10000 slp-synthesis-aes-bottom22.cnf 57800 193923 10000 10000 slp-synthesis-aes-bottom23.cnf 62686 210488 10000 10000 slp-synthesis-aes-bottom24.cnf 67777 227761 10000 10000 slp-synthesis-aes-bottom25.cnf 73074 245746 10000 10000 slp-synthesis-aes-bottom26.cnf 51138 162526 10000 10000 slp-synthesis-aes-top21.cnf 55875 177646 10000 10000 slp-synthesis-aes-top22.cnf 60823 193450 10000 10000 slp-synthesis-aes-top23.cnf 65983 209942 10000 10000 slp-synthesis-aes-top24.cnf 71356 227126 9930 2930 slp-synthesis-aes-top25.cnf 76943 245006 800 1140 slp-synthesis-aes-top26.cnf 88763 282870 540 650 slp-synthesis-aes-top28.cnf 94998 302862 250 560 slp-synthesis-aes-top29.cnf 101451 323566 410 370 slp-synthesis-aes-top30.cnf 206768 599363 10 10 smtlib-qfbv-aigs-bin_libmsrpc_vc1225336-tseitin.cnf 266663 768347 10 10 smtlib-qfbv-aigs-bin_libsmbclient_vc1228502-tseitin.cnf 164758 456350 10 10 smtlib-qfbv-aigs-bin_libsmbsharemodes_vc5759-tseitin.cnf 95810 287045 10000 10000 smtlib-qfbv-aigs-countbits128-tseitin.cnf 27224 68879 10000 10 smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf 350506 878969 10 10 smtlib-qfbv-aigs-lfsr_004_127_112-tseitin.cnf 259762 656573 20 20 smtlib-qfbv-aigs-lfsr_008_063_080-tseitin.cnf 448370 1130525 20 20 smtlib-qfbv-aigs-lfsr_008_079_112-tseitin.cnf 361856 1084031 20 20 smtlib-qfbv-aigs-nlzbe256-tseitin.cnf 266805 720122 10 10 smtlib-qfbv-aigs-rfunit_flat-64-tseitin.cnf 360364 1076507 10 10 smtlib-qfbv-aigs-servers_slapd_a_vc149789-tseitin.cnf 180045 538304 10 10 smtlib-qfbv-aigs-src_wget_vc18517-tseitin.cnf 257030 769313 10000 10000 smtlib-qfbv-aigs-VS3-benchmark-S2-tseitin.cnf 66084 1060536 190 290 sokoban-sequential-p145-microban-sequential.030-NOTKNOWN.cnf 87884 1413816 8860 10000 sokoban-sequential-p145-microban-sequential.040-NOTKNOWN.cnf 109684 1767096 10000 10000 sokoban-sequential-p145-microban-sequential.050-NOTKNOWN.cnf 131484 2120376 10000 10000 sokoban-sequential-p145-microban-sequential.060-NOTKNOWN.cnf 153284 2473656 10000 10000 sokoban-sequential-p145-microban-sequential.070-NOTKNOWN.cnf 175084 2826936 10000 10000 sokoban-sequential-p145-microban-sequential.080-SAT.cnf 39151 533919 310 340 traffic_3b_unknown.cnf 142205 1312352 120 150 traffic_3_uc_sat.cnf 26061 742909 290 280 traffic_b_unsat.cnf 35819 773506 250 290 traffic_fb_unknown.cnf 33320 763101 270 260 traffic_f_unknown.cnf 34510 701694 290 340 traffic_kkb_unknown.cnf 33320 766757 340 320 traffic_pcb_unknown.cnf 98651 3362666 10 20 traffic_r_sat.cnf 467551 4467733 110 250 traffic_r_uc_sat.cnf 723130 3869060 760 370 transport-transport-citysequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.060-SAT.cnf 945406 5079060 3540 3590 transport-transport-citysequential-35nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.030-NOTKNOWN.cnf 1260306 6771840 1140 6000 transport-transport-citysequential-35nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.040-NOTKNOWN.cnf 1575206 8464620 1230 10000 transport-transport-citysequential-35nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.050-SAT.cnf 756832 4116966 6130 10000 transport-transport-three-citiessequential-14nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.020-NOTKNOWN.cnf 1134832 6175026 10000 10000 transport-transport-three-citiessequential-14nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.030-NOTKNOWN.cnf 1512832 8233086 10000 10000 transport-transport-three-citiessequential-14nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.040-NOTKNOWN.cnf 580875 3140965 2920 2640 transport-transport-two-citiessequential-15nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.040-SAT.cnf 88289 4187694 10000 10000 11pipe_11_ooo.cnf 89315 5584003 10000 10000 11pipe_k.cnf 138563 4675040 50 60 12pipe_bug4_q0.used-as.sat04-723.cnf 138795 4671352 40 50 12pipe_bug6_q0.used-as.sat04-725.cnf 569795 8562505 1130 1190 1dlx_c_iq57_a.cnf 651875 9927770 1040 1560 1dlx_c_iq60_a.cnf 202253 4313014 10000 10000 2dlx_ca_bp_f_liveness.cnf 17064 545612 50 40 6pipe_6_ooo.shuffled-as.sat03-413.cnf 209724 3634677 10000 10000 9dlx_vliw_at_b_iq6.used-as.sat04-347.cnf 306095 6069108 10000 10000 9dlx_vliw_at_b_iq7.cnf 371419 7170909 10000 10000 9dlx_vliw_at_b_iq8.used-as.sat04-718.cnf 482093 9676386 10000 10000 9dlx_vliw_at_b_iq9.used-as.sat04-719.cnf 520770 13380350 60 60 9vliw_m_9stages_iq3_C1_bug5.cnf 521192 13378781 60 70 9vliw_m_9stages_iq3_C1_bug6.cnf 6228 484871 10000 10000 abb313GPIA-9-c.used-as.sat04-317.cnf 14013 481761 10 10 abb313GPIA-9-tr.used-as.sat04-321.cnf 155107 675624 40 60 ACG-10-10p0.cnf 218990 943377 80 110 ACG-15-5p1.cnf 21317 63664 40 40 all.used-as.sat04-986.cnf 4264 14751 10000 10000 am_7_7.shuffled-as.sat03-363.cnf 7502 28770 10000 10000 AProVE07-01.cnf 3114 10827 1430 1440 AProVE07-03.cnf 3189 11039 110 320 AProVE07-21.cnf 231 1166 10 10 bart17.shuffled.cnf 435701 1379987 1420 1970 bc57-sensors-1-k303-unsat.shuffledas.sat03-406.cnf 136756 905980 20 20 blocks-4-ipc5-h21-unknown.cnf 196306 582994 40 50 c10idw_i.cnf 9540 61421 10000 10000 c6288mul.miter.shuffled-as.sat03-346.cnf 1461771 5687554 200 220 clauses-8.renamed-as.sat05-1964.cnf 5910 16804 680 720 comb1.shuffled.cnf 8750 25865 10000 10000 countbitsarray04_32.cnf 8527 25484 10000 10000 countbitsrotate032.cnf 75103 225116 10000 10000 countbitssrl064.cnf 98048 293759 10000 10000 countbitswegner128.cnf 509512 1529045 930 970 cube-11-h14-sat.cnf 229544 1070757 10000 9590 dated-10-17-u.cnf 108786 482639 40 50 dated-5-11-u.cnf 138808 626501 9700 10000 dated-5-13-u.cnf 19473 58308 30 20 dekker.used-as.sat04-989.cnf 261352 773077 10000 10000 dme-03-1-k247-unsat.shuffled-as.sat03-407.cnf 1075 3152 10 10 dp04s04.shuffled.cnf 825 2411 10 10 dp04u03.shuffled.cnf 7759 23004 10 10 dp10s10.shuffled.cnf 207 588 10 10 driverlog1_ks99i.renamed-as.sat05-3951.cnf 170 1559 10 10 driverlog3_v01a.renamed-as.sat05-3963.cnf 112728 360099 10 10 dspam_dump_vc949.cnf 1400 4732 5160 4060 eq.atree.braun.11.unsat.cnf 1694 5726 10000 10000 eq.atree.braun.12.unsat.cnf 984 8702 10 10 ferry5_ks99i.renamed-as.sat05-3994.cnf 4268 38965 8530 5420 gripper13u.shuffled-as.sat03-395.cnf 31229 93855 20 10 gss-14-s100.cnf 31248 93904 10 90 gss-16-s100.cnf 31435 94548 290 120 gss-19-s100.cnf 31613 95104 5170 3790 gss-21-s100.cnf 31616 95110 10000 1030 gss-22-s100.cnf 31951 96161 10000 10000 gss-27-s100.cnf 69561 226787 1420 1870 gus-md5-11.cnf 69553 226752 5190 8910 gus-md5-12.cnf 1987351 5963534 20 30 hard-18-U-10652.cnf 541150 1645836 10 10 hard-25-U-7061.cnf 370048 1118066 10 10 hard-6-U-7061.cnf 300 2130 2250 950 homer14.shuffled.cnf 264 1476 3790 3890 homer16.shuffled.cnf 286 1742 10000 10000 homer17.shuffled.cnf 200230 566857 10 10 hsat_vc12062.cnf 191522 788339 10 10 ibm-2002-21r-k95.cnf 181484 890298 40 90 ibm-2002-30r-k85.cnf 64699 276210 20 10 ibm-2004-01-k90.cnf 207606 861175 80 90 ibm-2004-23-k100.cnf 112764 468539 770 540 IBM_FV_2004_rule_batch_30_SAT_dat.k55.cnf 165064 686589 50 370 IBM_FV_2004_rule_batch_30_SAT_dat.k80.cnf 10056 271393 10000 10000 k2fix_gr_rcs_w8.shuffled.cnf 11313 305160 110 110 k2fix_gr_rcs_w9.shuffled.cnf 11680 74581 7240 7600 k2mul.miter.shuffled-as.sat03-355.cnf 28147 108436 10000 10000 li-exam-61.shuffled-as.sat03-366.cnf 36809 142491 10000 10000 li-test4-100.shuffled-as.sat03-370.cnf 433601 1291714 280 500 manol-pipe-c10nidw.cnf 96089 283993 20 30 manol-pipe-c6bidw_i.cnf 263022 782329 1770 350 manol-pipe-f7idw.cnf 310434 923497 1990 180 manol-pipe-f7nidw.cnf 200308 598619 10000 10000 maxor128.cnf 13240 39143 1140 1300 maxxor032.cnf 51064 152039 10000 10000 maxxor064.cnf 200440 599015 10000 10000 maxxor128.cnf 92464 276623 10000 10000 maxxororand064.cnf 66892 279258 70 100 md5_48_3.cnf 4271 12620 10 10 minandmaxor016.cnf 249327 746444 6410 7000 minandmaxor128.cnf 153834 459965 1790 1860 minxorminand128.cnf 50073 210239 1130 350 mizh-sha0-36-2.cnf 50073 210235 590 180 mizh-sha0-36-4.cnf 4656 13871 10000 10000 mulhs016.cnf 570 4625 4900 7740 myciel6-tr.used-as.sat04-320.cnf 4020 466486 1830 340 ndhf_xits_19_UNKNOWN.cnf 234673 1071339 10000 10000 partial-10-13-s.cnf 261020 1211106 480 720 partial-10-15-s.cnf 298900 1409628 10000 10000 partial-10-17-s.cnf 164158 730719 10000 10000 partial-5-11-u.cnf 135543 404326 80 80 post-c32s-gcdm16-23.cnf 10950109 32697150 50 80 post-cbmc-zfcp-2.8-u2-noholes.cnf 486992 2456708 100 110 q_query_3_L150_coli.sat.cnf 33090 165828 80 120 q_query_3_l46_lambda.cnf 218792 1020908 30 30 q_query_3_L70_coli.sat.cnf 3000 8881 10 10 rand_net60-25-10.shuffled.cnf 3600 10681 10 10 rand_net60-30-1.shuffled.cnf 4800 14281 1370 170 rand_net60-40-10.shuffled.cnf 8400 25061 870 710 rand_net70-60-10.shuffled.cnf 1278 68055 1170 2120 rbcl_xits_08_UNSAT.cnf 1430 79453 10000 10000 rbcl_xits_09_UNKNOWN.cnf 2384 164746 10 10 rbcl_xits_15_SAT.cnf 2888 218530 10 10 rbcl_xits_18_SAT.cnf 439 5423 10 10 rovers1_ks99i.renamed-as.sat05-3971.cnf 1430 87044 10000 10000 rpoc_xits_09_UNSAT.cnf 50797 177980 3160 1660 SAT_dat.k100.cnf 31357 133420 2390 1660 SAT_dat.k20.cnf 37432 147345 1650 1880 SAT_dat.k45.cnf 104450 457628 20 20 SAT_dat.k80_04.cnf 45937 166840 2830 2680 SAT_dat.k80.cnf 181484 890298 40 90 SAT_dat.k85.cnf 50073 210223 430 210 sha0_36_5.cnf 47129 141002 10000 10000 smulo064.cnf 106701 374254 10000 10000 sortnet-7-ipc5-h15-unsat.cnf 361125 1254773 10000 10000 sortnet-8-ipc5-h19-sat.cnf 293864 1370917 10000 10000 total-10-17-u.cnf 199304 1005834 390 340 UCG-15-10p0.cnf 200003 1019221 370 510 UCG-15-10p1.cnf 162696 821000 50 40 UCG-15-5p0.cnf 224986 1204430 340 420 UCG-20-5p1.cnf 131228 635871 80 80 UR-10-10p1.cnf 258781 1372095 7760 8280 UR-20-10p0.cnf 259234 1387934 8110 6920 UR-20-10p1.cnf 108508 527595 10 10 UTI-10-5t1.cnf 259616 1374599 2000 1830 UTI-20-10p0.cnf 260342 1391257 2660 4240 UTI-20-10p1.cnf 237336 1262609 10 10 UTI-20-10t0.cnf 238008 1278025 10 10 UTI-20-10t1.cnf 985042 3113540 2040 3380 valves-gates-1-k617-unsat.shuffled-as.sat03-412.cnf 6498 130997 10 10 vda_gr_rcs_w9.shuffled.cnf 889302 14582074 60 650 velev-npe-1.0-9dlx-b71.cnf 24415 711050 480 230 velev-pipe-o-uns-1.0-7.cnf 17710 304026 900 90 velev-pipe-o-uns-1.1-6.cnf 118038 8780591 80 80 velev-pipe-sat-1.0-b9.cnf 154309 3230738 10000 8790 velev-vliw-uns-4.0-9-i1.cnf 625 76775 10 10 vmpc_25.renamed-as.sat05-1913.cnf 841 120147 220 20 vmpc_29.renamed-as.sat05-1916.cnf 1024 161664 6070 3880 vmpc_32.renamed-as.sat05-1919.cnf 1156 194072 10000 2710 vmpc_34.renamed-as.sat05-1926.cnf 1225 211785 10000 5200 vmpc_35.renamed-as.sat05-1921.cnf 1296 230544 4540 10000 vmpc_36.renamed-as.sat05-1922.cnf 8756 55571 8190 6860 x1mul.miter.shuffled-as.sat03-359.cnf