-------------------------------------------------------- 01_rule SAT_dat.k10.cnf p cnf 9299 46511 SAT_dat.k15.cnf p cnf 13818 69795 SAT_dat.k1.cnf p cnf 996 3868 SAT_dat.k20.cnf p cnf 18373 93235 SAT_dat.k25.cnf p cnf 22928 116675 SAT_dat.k30.cnf p cnf 27483 140115 SAT_dat.k35.cnf p cnf 32038 163555 SAT_dat.k40.cnf p cnf 36593 186995 SAT_dat.k45.cnf p cnf 41148 210435 SAT_dat.k50.cnf p cnf 45703 233875 -------------------------------------------------------- 02_1_rule_1 SAT_dat.k10.cnf p cnf 6881 24555 SAT_dat.k15.cnf p cnf 10561 37785 SAT_dat.k1.cnf p cnf 511 1429 SAT_dat.k20.cnf p cnf 14256 51160 SAT_dat.k25.cnf p cnf 17951 64535 SAT_dat.k30.cnf p cnf 21646 77910 SAT_dat.k35.cnf p cnf 25341 91285 SAT_dat.k40.cnf p cnf 29036 104660 SAT_dat.k45.cnf p cnf 32731 118035 SAT_dat.k50.cnf p cnf 36426 131410 -------------------------------------------------------- 02_1_rule_2 SAT_dat.k10.cnf p cnf 6762 23947 SAT_dat.k15.cnf p cnf 10442 37037 SAT_dat.k1.cnf p cnf 417 1148 SAT_dat.k20.cnf p cnf 14132 50257 SAT_dat.k25.cnf p cnf 17822 63477 SAT_dat.k30.cnf p cnf 21512 76697 SAT_dat.k35.cnf p cnf 25202 89917 SAT_dat.k40.cnf p cnf 28892 103137 SAT_dat.k45.cnf p cnf 32582 116357 SAT_dat.k50.cnf p cnf 36272 129577 -------------------------------------------------------- 02_1_rule_3 SAT_dat.k10.cnf p cnf 6141 21671 SAT_dat.k15.cnf p cnf 9601 34011 SAT_dat.k1.cnf p cnf 206 552 SAT_dat.k20.cnf p cnf 13071 46401 SAT_dat.k25.cnf p cnf 16541 58791 SAT_dat.k30.cnf p cnf 20011 71181 SAT_dat.k35.cnf p cnf 23481 83571 SAT_dat.k40.cnf p cnf 26951 95961 SAT_dat.k45.cnf p cnf 30421 108351 SAT_dat.k50.cnf p cnf 33891 120741 -------------------------------------------------------- 02_1_rule_4 SAT_dat.k10.cnf p cnf 6241 21749 SAT_dat.k15.cnf p cnf 9746 34124 SAT_dat.k1.cnf p cnf 225 567 SAT_dat.k20.cnf p cnf 13261 46549 SAT_dat.k25.cnf p cnf 16776 58974 SAT_dat.k30.cnf p cnf 20291 71399 SAT_dat.k35.cnf p cnf 23806 83824 SAT_dat.k40.cnf p cnf 27321 96249 SAT_dat.k45.cnf p cnf 30836 108674 SAT_dat.k50.cnf p cnf 34351 121099 -------------------------------------------------------- 02_1_rule_5 SAT_dat.k10.cnf p cnf 6110 21548 SAT_dat.k15.cnf p cnf 9555 33828 SAT_dat.k1.cnf p cnf 202 537 SAT_dat.k20.cnf p cnf 13010 46158 SAT_dat.k25.cnf p cnf 16465 58488 SAT_dat.k30.cnf p cnf 19920 70818 SAT_dat.k35.cnf p cnf 23375 83148 SAT_dat.k40.cnf p cnf 26830 95478 SAT_dat.k45.cnf p cnf 30285 107808 SAT_dat.k50.cnf p cnf 33740 120138 -------------------------------------------------------- 02_2_rule SAT_dat.k10.cnf p cnf 5958 20876 SAT_dat.k15.cnf p cnf 9358 32946 SAT_dat.k1.cnf p cnf 149 333 SAT_dat.k20.cnf p cnf 12763 45041 SAT_dat.k25.cnf p cnf 16168 57136 SAT_dat.k30.cnf p cnf 19573 69231 SAT_dat.k35.cnf p cnf 22978 81326 SAT_dat.k40.cnf p cnf 26383 93421 SAT_dat.k45.cnf p cnf 29788 105516 SAT_dat.k50.cnf p cnf 33193 117611 -------------------------------------------------------- 02_3_rule_1 SAT_dat.k10.cnf p cnf 7921 29977 SAT_dat.k15.cnf p cnf 12231 46417 SAT_dat.k1.cnf p cnf 261 741 SAT_dat.k20.cnf p cnf 16546 62892 SAT_dat.k25.cnf p cnf 20861 79367 SAT_dat.k30.cnf p cnf 25176 95842 SAT_dat.k35.cnf p cnf 29491 112317 SAT_dat.k40.cnf p cnf 33806 128792 SAT_dat.k45.cnf p cnf 38121 145267 SAT_dat.k50.cnf p cnf 42436 161742 -------------------------------------------------------- 02_3_rule_2 SAT_dat.k10.cnf p cnf 7920 29995 SAT_dat.k15.cnf p cnf 12230 46425 SAT_dat.k1.cnf p cnf 260 741 SAT_dat.k20.cnf p cnf 16545 62900 SAT_dat.k25.cnf p cnf 20860 79375 SAT_dat.k30.cnf p cnf 25175 95850 SAT_dat.k35.cnf p cnf 29490 112325 SAT_dat.k40.cnf p cnf 33805 128800 SAT_dat.k45.cnf p cnf 38120 145275 SAT_dat.k50.cnf p cnf 42435 161750 -------------------------------------------------------- 02_3_rule_3 SAT_dat.k10.cnf p cnf 7921 29977 SAT_dat.k15.cnf p cnf 12231 46417 SAT_dat.k1.cnf p cnf 261 741 SAT_dat.k20.cnf p cnf 16546 62892 SAT_dat.k25.cnf p cnf 20861 79367 SAT_dat.k30.cnf p cnf 25176 95842 SAT_dat.k35.cnf p cnf 29491 112317 SAT_dat.k40.cnf p cnf 33806 128792 SAT_dat.k45.cnf p cnf 38121 145267 SAT_dat.k50.cnf p cnf 42436 161742 -------------------------------------------------------- 02_3_rule_4 SAT_dat.k10.cnf p cnf 7920 29995 SAT_dat.k15.cnf p cnf 12230 46425 SAT_dat.k1.cnf p cnf 260 741 SAT_dat.k20.cnf p cnf 16545 62900 SAT_dat.k25.cnf p cnf 20860 79375 SAT_dat.k30.cnf p cnf 25175 95850 SAT_dat.k35.cnf p cnf 29490 112325 SAT_dat.k40.cnf p cnf 33805 128800 SAT_dat.k45.cnf p cnf 38120 145275 SAT_dat.k50.cnf p cnf 42435 161750 -------------------------------------------------------- 02_3_rule_5 SAT_dat.k10.cnf p cnf 7921 29977 SAT_dat.k15.cnf p cnf 12231 46417 SAT_dat.k1.cnf p cnf 261 741 SAT_dat.k20.cnf p cnf 16546 62892 SAT_dat.k25.cnf p cnf 20861 79367 SAT_dat.k30.cnf p cnf 25176 95842 SAT_dat.k35.cnf p cnf 29491 112317 SAT_dat.k40.cnf p cnf 33806 128792 SAT_dat.k45.cnf p cnf 38121 145267 SAT_dat.k50.cnf p cnf 42436 161742 -------------------------------------------------------- 02_3_rule_6 SAT_dat.k10.cnf p cnf 7920 29995 SAT_dat.k15.cnf p cnf 12230 46425 SAT_dat.k1.cnf p cnf 260 741 SAT_dat.k20.cnf p cnf 16545 62900 SAT_dat.k25.cnf p cnf 20860 79375 SAT_dat.k30.cnf p cnf 25175 95850 SAT_dat.k35.cnf p cnf 29490 112325 SAT_dat.k40.cnf p cnf 33805 128800 SAT_dat.k45.cnf p cnf 38120 145275 SAT_dat.k50.cnf p cnf 42435 161750 -------------------------------------------------------- 02_3_rule_7 SAT_dat.k10.cnf p cnf 7588 28657 SAT_dat.k15.cnf p cnf 11813 44727 SAT_dat.k1.cnf p cnf 225 623 SAT_dat.k20.cnf p cnf 16058 60892 SAT_dat.k25.cnf p cnf 20303 77057 SAT_dat.k30.cnf p cnf 24548 93222 SAT_dat.k35.cnf p cnf 28793 109387 SAT_dat.k40.cnf p cnf 33038 125552 SAT_dat.k45.cnf p cnf 37283 141717 SAT_dat.k50.cnf p cnf 41528 157882 -------------------------------------------------------- 03_rule SAT_dat.k10.cnf p cnf 9691 41102 SAT_dat.k15.cnf p cnf 15321 64907 SAT_dat.k1.cnf p cnf 300 966 SAT_dat.k20.cnf p cnf 20961 88767 SAT_dat.k25.cnf p cnf 26601 112627 SAT_dat.k30.cnf p cnf 32241 136487 SAT_dat.k35.cnf p cnf 37881 160347 SAT_dat.k40.cnf p cnf 43521 184207 SAT_dat.k45.cnf p cnf 49161 208067 SAT_dat.k50.cnf p cnf 54801 231927 -------------------------------------------------------- 04_rule SAT_dat.k10.cnf p cnf 10165 44388 SAT_dat.k15.cnf p cnf 16895 73868 SAT_dat.k1.cnf p cnf 456 1035 SAT_dat.k20.cnf p cnf 23630 103388 SAT_dat.k25.cnf p cnf 30365 132908 SAT_dat.k30.cnf p cnf 37100 162428 SAT_dat.k35.cnf p cnf 43835 191948 SAT_dat.k40.cnf p cnf 50570 221468 SAT_dat.k45.cnf p cnf 57305 250988 SAT_dat.k50.cnf p cnf 64040 280508 -------------------------------------------------------- 05_rule SAT_dat.k10.cnf p cnf 16705 89286 SAT_dat.k15.cnf p cnf 26915 144666 SAT_dat.k1.cnf p cnf 712 1791 SAT_dat.k20.cnf p cnf 37130 200101 SAT_dat.k25.cnf p cnf 47345 255536 SAT_dat.k30.cnf p cnf 57560 310971 SAT_dat.k35.cnf p cnf 67775 366406 SAT_dat.k40.cnf p cnf 77990 421841 SAT_dat.k45.cnf p cnf 88205 477276 SAT_dat.k50.cnf p cnf 98420 532711 -------------------------------------------------------- 06_rule SAT_dat.k10.cnf p cnf 12830 57204 SAT_dat.k15.cnf p cnf 19765 88084 SAT_dat.k1.cnf p cnf 753 3010 SAT_dat.k20.cnf p cnf 26735 119124 SAT_dat.k25.cnf p cnf 33705 150164 SAT_dat.k30.cnf p cnf 40675 181204 SAT_dat.k35.cnf p cnf 47645 212244 SAT_dat.k40.cnf p cnf 54615 243284 SAT_dat.k45.cnf p cnf 61585 274324 SAT_dat.k50.cnf p cnf 68555 305364 -------------------------------------------------------- 07_rule SAT_dat.k10.cnf p cnf 8403 26314 SAT_dat.k15.cnf p cnf 6747 19473 SAT_dat.k1.cnf p cnf 1257 3778 SAT_dat.k20.cnf p cnf 7807 21938 SAT_dat.k25.cnf p cnf 8867 24403 SAT_dat.k30.cnf p cnf 9927 26868 SAT_dat.k35.cnf p cnf 10987 29333 SAT_dat.k40.cnf p cnf 12047 31798 SAT_dat.k45.cnf p cnf 13107 34263 SAT_dat.k50.cnf p cnf 14167 36728 -------------------------------------------------------- 09_rule SAT_dat.k10.cnf p cnf 6139 26305 SAT_dat.k15.cnf p cnf 9637 41644 SAT_dat.k1.cnf p cnf 270 647 SAT_dat.k20.cnf p cnf 13152 57074 SAT_dat.k25.cnf p cnf 16667 72504 SAT_dat.k30.cnf p cnf 20182 87934 SAT_dat.k35.cnf p cnf 23697 103364 SAT_dat.k40.cnf p cnf 27212 118794 SAT_dat.k45.cnf p cnf 30727 134224 SAT_dat.k50.cnf p cnf 34242 149654 -------------------------------------------------------- 11_rule_1 SAT_dat.k10.cnf p cnf 32696 133153 SAT_dat.k15.cnf p cnf 50396 205258 SAT_dat.k1.cnf p cnf 3294 12402 SAT_dat.k20.cnf p cnf 68101 277403 SAT_dat.k25.cnf p cnf 85806 349548 SAT_dat.k30.cnf p cnf 103511 421693 SAT_dat.k35.cnf p cnf 121216 493838 SAT_dat.k40.cnf p cnf 138921 565983 SAT_dat.k45.cnf p cnf 156626 638128 SAT_dat.k50.cnf p cnf 174331 710273 -------------------------------------------------------- 11_rule_2 SAT_dat.k10.cnf p cnf 32455 132095 SAT_dat.k15.cnf p cnf 50020 203550 SAT_dat.k1.cnf p cnf 3285 12385 SAT_dat.k20.cnf p cnf 67595 275095 SAT_dat.k25.cnf p cnf 85170 346640 SAT_dat.k30.cnf p cnf 102745 418185 SAT_dat.k35.cnf p cnf 120320 489730 SAT_dat.k40.cnf p cnf 137895 561275 SAT_dat.k45.cnf p cnf 155470 632820 SAT_dat.k50.cnf p cnf 173045 704365 -------------------------------------------------------- 11_rule_3 SAT_dat.k10.cnf p cnf 32650 133321 SAT_dat.k15.cnf p cnf 50235 204991 SAT_dat.k1.cnf p cnf 3340 12673 SAT_dat.k20.cnf p cnf 67830 276781 SAT_dat.k25.cnf p cnf 85425 348571 SAT_dat.k30.cnf p cnf 103020 420361 SAT_dat.k35.cnf p cnf 120615 492151 SAT_dat.k40.cnf p cnf 138210 563941 SAT_dat.k45.cnf p cnf 155805 635731 SAT_dat.k50.cnf p cnf 173400 707521 -------------------------------------------------------- 12_rule SAT_dat.k10.cnf p cnf 1 2 SAT_dat.k15.cnf p cnf 1 2 SAT_dat.k1.cnf p cnf 1 2 SAT_dat.k20.cnf p cnf 1 2 SAT_dat.k25.cnf p cnf 1 2 SAT_dat.k30.cnf p cnf 1 2 SAT_dat.k35.cnf p cnf 1 2 SAT_dat.k40.cnf p cnf 1 2 SAT_dat.k45.cnf p cnf 1 2 SAT_dat.k50.cnf p cnf 1 2 -------------------------------------------------------- 13_rule_1 SAT_dat.k10.cnf p cnf 46169 207720 SAT_dat.k15.cnf p cnf 30142 130635 SAT_dat.k1.cnf p cnf 5192 23022 SAT_dat.k20.cnf p cnf 31357 133420 SAT_dat.k25.cnf p cnf 32572 136205 SAT_dat.k30.cnf p cnf 33787 138990 SAT_dat.k35.cnf p cnf 35002 141775 SAT_dat.k40.cnf p cnf 36217 144560 SAT_dat.k45.cnf p cnf 37432 147345 SAT_dat.k50.cnf p cnf 38647 150130 -------------------------------------------------------- 14_rule_1 SAT_dat.k10.cnf p cnf 14133 51761 SAT_dat.k15.cnf p cnf 21473 78981 SAT_dat.k1.cnf p cnf 1119 3380 SAT_dat.k20.cnf p cnf 28818 106256 SAT_dat.k25.cnf p cnf 36163 133531 SAT_dat.k30.cnf p cnf 43508 160806 SAT_dat.k35.cnf p cnf 50853 188081 SAT_dat.k40.cnf p cnf 58198 215356 SAT_dat.k45.cnf p cnf 65543 242631 SAT_dat.k50.cnf p cnf 72888 269906 -------------------------------------------------------- 14_rule_2 SAT_dat.k10.cnf p cnf 14308 52517 SAT_dat.k15.cnf p cnf 21733 80102 SAT_dat.k1.cnf p cnf 1141 3461 SAT_dat.k20.cnf p cnf 29163 107747 SAT_dat.k25.cnf p cnf 36593 135392 SAT_dat.k30.cnf p cnf 44023 163037 SAT_dat.k35.cnf p cnf 51453 190682 SAT_dat.k40.cnf p cnf 58883 218327 SAT_dat.k45.cnf p cnf 66313 245972 SAT_dat.k50.cnf p cnf 73743 273617 -------------------------------------------------------- 15_rule SAT_dat.k10.cnf p cnf 22194 83241 SAT_dat.k15.cnf p cnf 33934 127936 SAT_dat.k1.cnf p cnf 1520 4378 SAT_dat.k20.cnf p cnf 45679 172661 SAT_dat.k25.cnf p cnf 57424 217386 SAT_dat.k30.cnf p cnf 69169 262111 SAT_dat.k35.cnf p cnf 80914 306836 SAT_dat.k40.cnf p cnf 92659 351561 SAT_dat.k45.cnf p cnf 104404 396286 SAT_dat.k50.cnf p cnf 116149 441011 -------------------------------------------------------- 16_2_rule_1 SAT_dat.k10.cnf p cnf 3645 14681 SAT_dat.k15.cnf p cnf 5590 22661 SAT_dat.k1.cnf p cnf 281 856 SAT_dat.k20.cnf p cnf 7540 30661 SAT_dat.k25.cnf p cnf 9490 38661 SAT_dat.k30.cnf p cnf 11440 46661 SAT_dat.k35.cnf p cnf 13390 54661 SAT_dat.k40.cnf p cnf 15340 62661 SAT_dat.k45.cnf p cnf 17290 70661 SAT_dat.k50.cnf p cnf 19240 78661 -------------------------------------------------------- 16_2_rule_2 SAT_dat.k10.cnf p cnf 3651 14720 SAT_dat.k15.cnf p cnf 5596 22685 SAT_dat.k1.cnf p cnf 287 868 SAT_dat.k20.cnf p cnf 7546 30685 SAT_dat.k25.cnf p cnf 9496 38685 SAT_dat.k30.cnf p cnf 11446 46685 SAT_dat.k35.cnf p cnf 13396 54685 SAT_dat.k40.cnf p cnf 15346 62685 SAT_dat.k45.cnf p cnf 17296 70685 SAT_dat.k50.cnf p cnf 19246 78685 -------------------------------------------------------- 16_2_rule_3 SAT_dat.k10.cnf p cnf 3662 14742 SAT_dat.k15.cnf p cnf 5602 22697 SAT_dat.k1.cnf p cnf 289 872 SAT_dat.k20.cnf p cnf 7552 30697 SAT_dat.k25.cnf p cnf 9502 38697 SAT_dat.k30.cnf p cnf 11452 46697 SAT_dat.k35.cnf p cnf 13402 54697 SAT_dat.k40.cnf p cnf 15352 62697 SAT_dat.k45.cnf p cnf 17302 70697 SAT_dat.k50.cnf p cnf 19252 78697 -------------------------------------------------------- 16_2_rule_4 SAT_dat.k10.cnf p cnf 5687 22854 SAT_dat.k15.cnf p cnf 7966 32338 SAT_dat.k1.cnf p cnf 514 1668 SAT_dat.k20.cnf p cnf 10566 43068 SAT_dat.k25.cnf p cnf 13166 53798 SAT_dat.k30.cnf p cnf 15766 64528 SAT_dat.k35.cnf p cnf 18366 75258 SAT_dat.k40.cnf p cnf 20966 85988 SAT_dat.k45.cnf p cnf 23566 96718 SAT_dat.k50.cnf p cnf 26166 107448 -------------------------------------------------------- 16_2_rule_5 SAT_dat.k10.cnf p cnf 5459 21905 SAT_dat.k15.cnf p cnf 7743 31424 SAT_dat.k1.cnf p cnf 396 1168 SAT_dat.k20.cnf p cnf 10343 42154 SAT_dat.k25.cnf p cnf 12943 52884 SAT_dat.k30.cnf p cnf 15543 63614 SAT_dat.k35.cnf p cnf 18143 74344 SAT_dat.k40.cnf p cnf 20743 85074 SAT_dat.k45.cnf p cnf 23343 95804 SAT_dat.k50.cnf p cnf 25943 106534 -------------------------------------------------------- 16_2_rule_6 SAT_dat.k10.cnf p cnf 5471 21950 SAT_dat.k15.cnf p cnf 7755 31454 SAT_dat.k1.cnf p cnf 402 1180 SAT_dat.k20.cnf p cnf 10355 42184 SAT_dat.k25.cnf p cnf 12955 52914 SAT_dat.k30.cnf p cnf 15555 63644 SAT_dat.k35.cnf p cnf 18155 74374 SAT_dat.k40.cnf p cnf 20755 85104 SAT_dat.k45.cnf p cnf 23355 95834 SAT_dat.k50.cnf p cnf 25955 106564 -------------------------------------------------------- 17_1_rule_1 SAT_dat.k10.cnf p cnf 8096 31135 SAT_dat.k15.cnf p cnf 13551 52605 SAT_dat.k1.cnf p cnf 331 507 SAT_dat.k20.cnf p cnf 19006 74085 SAT_dat.k25.cnf p cnf 24461 95565 SAT_dat.k30.cnf p cnf 29916 117045 SAT_dat.k35.cnf p cnf 35371 138525 SAT_dat.k40.cnf p cnf 40826 160005 SAT_dat.k45.cnf p cnf 46281 181485 SAT_dat.k50.cnf p cnf 51736 202965 -------------------------------------------------------- 17_1_rule_2 SAT_dat.k10.cnf p cnf 7313 27682 SAT_dat.k15.cnf p cnf 12807 49267 SAT_dat.k1.cnf p cnf 321 411 SAT_dat.k20.cnf p cnf 18342 70977 SAT_dat.k25.cnf p cnf 23877 92687 SAT_dat.k30.cnf p cnf 29412 114397 SAT_dat.k35.cnf p cnf 34947 136107 SAT_dat.k40.cnf p cnf 40482 157817 SAT_dat.k45.cnf p cnf 46017 179527 SAT_dat.k50.cnf p cnf 51552 201237 -------------------------------------------------------- 17_2_rule_1 SAT_dat.k10.cnf p cnf 8797 33743 SAT_dat.k15.cnf p cnf 15212 59068 SAT_dat.k1.cnf p cnf 428 664 SAT_dat.k20.cnf p cnf 21627 84398 SAT_dat.k25.cnf p cnf 28042 109728 SAT_dat.k30.cnf p cnf 34457 135058 SAT_dat.k35.cnf p cnf 40872 160388 SAT_dat.k40.cnf p cnf 47287 185718 SAT_dat.k45.cnf p cnf 53702 211048 SAT_dat.k50.cnf p cnf 60117 236378 -------------------------------------------------------- 17_2_rule_2 SAT_dat.k10.cnf p cnf 9443 36386 SAT_dat.k15.cnf p cnf 15853 61696 SAT_dat.k1.cnf p cnf 439 697 SAT_dat.k20.cnf p cnf 22268 87026 SAT_dat.k25.cnf p cnf 28683 112356 SAT_dat.k30.cnf p cnf 35098 137686 SAT_dat.k35.cnf p cnf 41513 163016 SAT_dat.k40.cnf p cnf 47928 188346 SAT_dat.k45.cnf p cnf 54343 213676 SAT_dat.k50.cnf p cnf 60758 239006 -------------------------------------------------------- 18_rule SAT_dat.k10.cnf p cnf 19061 77876 SAT_dat.k15.cnf p cnf 28816 118096 SAT_dat.k1.cnf p cnf 1854 6923 SAT_dat.k20.cnf p cnf 38576 158361 SAT_dat.k25.cnf p cnf 48336 198626 SAT_dat.k30.cnf p cnf 58096 238891 SAT_dat.k35.cnf p cnf 67856 279156 SAT_dat.k40.cnf p cnf 77616 319421 SAT_dat.k45.cnf p cnf 87376 359686 SAT_dat.k50.cnf p cnf 97136 399951 -------------------------------------------------------- 19_rule SAT_dat.k10.cnf p cnf 29987 115034 SAT_dat.k15.cnf p cnf 45547 174949 SAT_dat.k1.cnf p cnf 2693 9778 SAT_dat.k20.cnf p cnf 61112 234899 SAT_dat.k25.cnf p cnf 76677 294849 SAT_dat.k30.cnf p cnf 92242 354799 SAT_dat.k35.cnf p cnf 107807 414749 SAT_dat.k40.cnf p cnf 123372 474699 SAT_dat.k45.cnf p cnf 138937 534649 SAT_dat.k50.cnf p cnf 154502 594599 -------------------------------------------------------- 20_rule SAT_dat.k10.cnf p cnf 19777 80933 SAT_dat.k15.cnf p cnf 29882 122668 SAT_dat.k1.cnf p cnf 1940 7253 SAT_dat.k20.cnf p cnf 39992 164448 SAT_dat.k25.cnf p cnf 50102 206228 SAT_dat.k30.cnf p cnf 60212 248008 SAT_dat.k35.cnf p cnf 70322 289788 SAT_dat.k40.cnf p cnf 80432 331568 SAT_dat.k45.cnf p cnf 90542 373348 SAT_dat.k50.cnf p cnf 100652 415128 -------------------------------------------------------- 21_rule SAT_dat.k10.cnf p cnf 19742 80627 SAT_dat.k15.cnf p cnf 29842 122252 SAT_dat.k1.cnf p cnf 1914 7181 SAT_dat.k20.cnf p cnf 39947 163912 SAT_dat.k25.cnf p cnf 50052 205572 SAT_dat.k30.cnf p cnf 60157 247232 SAT_dat.k35.cnf p cnf 70262 288892 SAT_dat.k40.cnf p cnf 80367 330552 SAT_dat.k45.cnf p cnf 90472 372212 SAT_dat.k50.cnf p cnf 100577 413872 -------------------------------------------------------- 22_rule SAT_dat.k10.cnf p cnf 24836 102932 SAT_dat.k15.cnf p cnf 37626 156437 SAT_dat.k1.cnf p cnf 2175 8093 SAT_dat.k20.cnf p cnf 50421 209977 SAT_dat.k25.cnf p cnf 63216 263517 SAT_dat.k30.cnf p cnf 76011 317057 SAT_dat.k35.cnf p cnf 88806 370597 SAT_dat.k40.cnf p cnf 101601 424137 SAT_dat.k45.cnf p cnf 114396 477677 SAT_dat.k50.cnf p cnf 127191 531217 -------------------------------------------------------- 23_rule SAT_dat.k10.cnf p cnf 24056 99683 SAT_dat.k15.cnf p cnf 36441 151448 SAT_dat.k1.cnf p cnf 2120 7832 SAT_dat.k20.cnf p cnf 48831 203283 SAT_dat.k25.cnf p cnf 61221 255118 SAT_dat.k30.cnf p cnf 73611 306953 SAT_dat.k35.cnf p cnf 86001 358788 SAT_dat.k40.cnf p cnf 98391 410623 SAT_dat.k45.cnf p cnf 110781 462458 SAT_dat.k50.cnf p cnf 123171 514293 -------------------------------------------------------- 26_rule SAT_dat.k10.cnf p cnf 55592 291138 SAT_dat.k15.cnf p cnf 77297 408328 SAT_dat.k1.cnf p cnf 6353 29868 SAT_dat.k20.cnf p cnf 101827 539498 SAT_dat.k25.cnf p cnf 126357 670668 SAT_dat.k30.cnf p cnf 150887 801838 SAT_dat.k35.cnf p cnf 175417 933008 SAT_dat.k40.cnf p cnf 199947 1064178 SAT_dat.k45.cnf p cnf 224477 1195348 SAT_dat.k50.cnf p cnf 249007 1326518 -------------------------------------------------------- 27_rule SAT_dat.k10.cnf p cnf 7579 29632 SAT_dat.k15.cnf p cnf 11584 45577 SAT_dat.k1.cnf p cnf 445 974 SAT_dat.k20.cnf p cnf 15599 61612 SAT_dat.k25.cnf p cnf 19614 77647 SAT_dat.k30.cnf p cnf 23629 93682 SAT_dat.k35.cnf p cnf 27644 109717 SAT_dat.k40.cnf p cnf 31659 125752 SAT_dat.k45.cnf p cnf 35674 141787 SAT_dat.k50.cnf p cnf 39689 157822 -------------------------------------------------------- 28_rule SAT_dat.k10.cnf p cnf 8015 41599 SAT_dat.k15.cnf p cnf 11462 59989 SAT_dat.k1.cnf p cnf 924 4374 SAT_dat.k20.cnf p cnf 15152 79519 SAT_dat.k25.cnf p cnf 18842 99049 SAT_dat.k30.cnf p cnf 22532 118579 SAT_dat.k35.cnf p cnf 26222 138109 SAT_dat.k40.cnf p cnf 29912 157639 SAT_dat.k45.cnf p cnf 33602 177169 SAT_dat.k50.cnf p cnf 37292 196699 -------------------------------------------------------- 29_rule SAT_dat.k10.cnf p cnf 8871 44994 SAT_dat.k15.cnf p cnf 13086 66989 SAT_dat.k1.cnf p cnf 980 4129 SAT_dat.k20.cnf p cnf 17386 89339 SAT_dat.k25.cnf p cnf 21686 111689 SAT_dat.k30.cnf p cnf 25986 134039 SAT_dat.k35.cnf p cnf 30286 156389 SAT_dat.k40.cnf p cnf 34586 178739 SAT_dat.k45.cnf p cnf 38886 201089 SAT_dat.k50.cnf p cnf 43186 223439 -------------------------------------------------------- 30_rule SAT_dat.k10.cnf p cnf 20599 99673 SAT_dat.k15.cnf p cnf 31264 152148 SAT_dat.k1.cnf p cnf 1618 6139 SAT_dat.k20.cnf p cnf 41994 204873 SAT_dat.k25.cnf p cnf 52724 257598 SAT_dat.k30.cnf p cnf 63454 310323 SAT_dat.k35.cnf p cnf 74184 363048 SAT_dat.k40.cnf p cnf 84914 415773 SAT_dat.k45.cnf p cnf 95644 468498 SAT_dat.k50.cnf p cnf 106374 521223