17 c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading alldiff_32_34_17-bij.cnf c found header 'p cnf 3706 30965' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 16 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 29166 3157 549 0 0 0 0 0.0 0 3 @c: s 0.1 20669 715 619 1126 1246 0 0 0.0 0 3 @c: l 0.1 20669 715 619 1126 1246 0 19922 0.0 0 3 @c: R 0.1 20669 715 619 1126 1246 102 102 76.9 3 3 @c: R 0.1 20671 715 619 1126 1246 202 201 51.1 9 3 @c: B 0.1 20959 553 773 1134 1246 1000 991 78.6 16 3 @c: B 0.2 21101 529 783 1148 1246 2000 1989 88.9 20 4 @c: R 0.2 21151 526 785 1149 1246 2883 2866 94.6 21 4 @c: R 0.2 21288 509 793 1158 1246 5976 5950 96.8 25 4 @c: B 0.2 21323 482 830 1148 1246 8003 7975 96.0 23 5 @c: + 0.3 21874 387 947 1126 1246 19922 21914 94.1 22 7 @c: B 0.4 21943 387 947 1126 1246 24006 21979 93.5 20 7 @c: R 0.4 21973 387 947 1126 1246 24524 21971 93.4 20 7 @c: + 0.4 22021 387 947 1126 1246 24901 24105 93.2 22 7 @c: + 0.5 22161 387 947 1126 1246 31126 26515 91.5 20 8 @c: R 0.5 22163 387 947 1126 1246 34137 26616 90.8 23 8 @c: + 0.6 22202 386 947 1127 1246 38905 29166 89.8 20 9 @c: s 0.7 11459 368 949 1128 1261 40951 26547 89.5 21 5 @c: - 0.7 11459 368 949 1128 1261 40951 16333 89.5 21 5 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 0.7 11459 368 949 1128 1261 40951 17966 89.5 21 4 @c: + 0.9 11485 363 951 1131 1261 51185 19762 87.8 27 6 @c: + 1.1 11490 363 951 1131 1261 63980 21738 86.8 21 8 @c: B 1.1 11490 363 951 1131 1261 64013 19874 86.8 21 8 @c: + 1.4 11509 363 951 1131 1261 79975 23911 85.5 28 8 @c: N 1.5 11509 363 951 1131 1261 82547 23990 85.5 28 8 @c: s 1.6 11321 363 951 1131 1261 87778 24982 85.4 30 7 @c: + 1.9 11321 363 951 1131 1261 99967 26302 84.6 24 9 @c: + 2.4 11321 363 951 1131 1261 124955 28932 82.9 29 11 @c: R 2.7 11321 363 951 1131 1261 133837 37210 82.2 24 14 @c: + 3.4 11321 363 951 1131 1261 156190 31825 81.8 27 14 @c: B 3.4 11321 363 951 1131 1261 160034 31900 81.9 22 14 @c: s 3.5 11322 363 951 1131 1261 163249 31905 81.8 27 9 @c: + 4.3 11339 363 951 1131 1261 195235 35007 80.9 21 12 @c: s 4.8 11338 363 951 1131 1261 214037 35057 80.5 20 8 @c: + 5.6 11339 363 951 1131 1261 244042 38507 80.0 29 16 @c: N 5.8 11339 363 951 1131 1261 249201 52931 79.9 27 17 @c: s 6.4 10973 363 951 1131 1261 268801 38586 79.6 26 12 @c: - 6.4 10973 363 951 1131 1261 268801 37352 79.6 26 12 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 7.1 11017 363 951 1131 1261 295900 41087 79.5 26 14 @c: s 8.1 11035 363 951 1131 1261 326648 41169 79.0 29 12 @c: + 9.2 11037 363 951 1131 1261 369876 45195 78.8 27 16 @c: B 9.7 11040 363 951 1131 1261 384072 45254 78.6 27 18 @c: s 9.7 11040 363 951 1131 1261 385746 45280 78.6 24 12 @c: + 12.0 11040 363 951 1131 1261 462347 49714 78.0 26 18 @c: N 13.7 11040 363 951 1131 1261 505556 52852 77.3 27 23 @c: s 16.1 11041 363 951 1131 1261 563635 49787 76.7 24 15 @c: + 16.7 11041 363 951 1131 1261 577931 54685 76.6 20 18 @c: s 20.5 11042 363 951 1131 1261 669473 54743 76.3 26 16 @c: + 22.8 11074 363 951 1131 1261 722411 60153 76.0 26 21 @c: s 23.8 11088 363 951 1131 1261 742304 60241 75.9 23 16 @c: s 28.0 11089 363 951 1131 1261 811557 60214 75.4 19 19 @c: B 32.4 11089 363 951 1131 1261 896156 60215 75.2 26 28 @c: + 32.8 11089 363 951 1131 1261 903011 66168 75.2 26 28 @c: s 33.3 11090 363 951 1131 1261 914363 66202 75.2 22 21 @c: s 37.2 11095 363 951 1131 1261 998545 69354 75.1 34 20 @c: R 41.0 11095 363 951 1131 1261 1069464 63776 74.9 25 23 @c: + 44.1 11095 363 951 1131 1261 1128760 72784 74.7 26 28 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 61.1 11096 363 951 1131 1261 1302271 66583 74.0 22 21 @c: s 66.7 10669 361 951 1133 1261 1383444 72843 74.0 24 21 @c: - 66.7 10669 361 951 1133 1261 1383444 70601 74.0 24 21 @c: + 66.7 10669 361 951 1133 1261 1383444 77661 74.0 24 22 @c: s 79.0 10671 361 951 1133 1261 1533904 77737 73.8 25 25 @c: + 98.7 10671 361 951 1133 1261 1729306 85427 73.9 27 30 @c: s 101.4 10672 361 951 1133 1261 1763145 85475 74.0 26 24 @c: s 110.7 10673 361 951 1133 1261 1882988 85456 73.8 24 24 @c: s 119.8 10675 361 951 1133 1261 1976872 85533 73.7 30 24 @c: B 126.4 10675 361 951 1133 1261 2048340 85765 73.7 26 33 @c: + 140.7 10675 361 951 1133 1261 2161630 93969 73.5 25 42 @c: R 168.8 10675 361 951 1133 1261 2299718 94008 73.0 25 49 @c: s 170.4 10676 361 951 1133 1261 2308415 94004 73.0 24 29 @c: + 241.4 10676 361 951 1133 1261 2702036 103365 72.0 26 43 @c: s 253.0 10677 361 951 1133 1261 2760948 103448 72.0 24 33 @c: s 274.1 10678 361 951 1133 1261 2879352 103438 72.1 28 28 @c: + 361.3 10678 361 951 1133 1261 3377546 113701 72.1 25 43 @c: + 514.9 10678 361 951 1133 1261 4221931 125071 72.3 33 46 @c: B 581.0 10678 361 951 1133 1261 4608686 125125 72.6 33 52 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: R 678.8 10678 361 951 1133 1261 4964935 128020 72.0 25 48 @c: + 760.3 10678 361 951 1133 1261 5277412 137578 71.4 25 50 @c: s 921.2 10679 361 951 1133 1261 5999517 111206 71.2 22 35 @c: + 1048.2 10679 361 951 1133 1261 6596765 151335 71.5 27 61 @c: s 1202.6 10680 361 951 1133 1261 7179347 151424 71.3 23 46 @c: s 1452.8 10681 361 951 1133 1261 8065977 141157 71.0 23 50 @c: s 1484.3 10683 361 951 1133 1261 8227837 151427 71.0 28 45 @c: + 1487.4 10683 361 951 1133 1261 8245957 166468 71.0 30 53 @c: s 1797.1 10684 361 951 1133 1261 9503464 138151 70.9 21 48 @c: B 1991.9 10684 361 951 1133 1261 10241435 166979 70.7 25 58 @c: N 2136.2 10684 361 951 1133 1261 10705141 166528 70.6 25 73 @c: s 3201.4 10685 361 951 1133 1261 14562518 166558 70.1 24 52 @c: s 4000.1 10686 361 951 1133 1261 17218884 166498 69.9 24 52 @c: s 4034.5 10702 361 951 1133 1261 17378779 166553 70.0 28 50 @c: - 4566.5 10535 360 951 1134 1261 19336184 164804 69.8 23 42 @c: s 4566.9 10472 360 951 1134 1261 19336184 166472 69.8 23 48 @c: - 4566.9 10472 360 951 1134 1261 19336184 163156 69.8 23 48 @c: + 4566.9 10472 360 951 1134 1261 19336184 179471 69.8 23 48 @c: B 5525.8 10472 360 951 1134 1261 22530917 167811 69.2 24 58 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 5528.1 10473 360 951 1134 1261 22537565 174458 69.2 22 51 @c: R 5676.4 10473 360 951 1134 1261 23005094 179532 69.1 24 73 @c: s 6780.6 10474 360 951 1134 1261 27381789 179514 68.5 23 50 @c: s 8058.6 10475 360 951 1134 1261 32769666 179533 68.6 27 51 @c: s 9629.5 10476 360 951 1134 1261 39714388 230214 68.6 21 77 @c: B 11285.5 10476 360 951 1134 1261 49157983 179509 68.4 25 71 @c: R 11298.4 10476 360 951 1134 1261 49243409 195149 68.4 21 81 @c: s 12436.8 10477 360 951 1134 1261 56643936 188976 67.6 24 55 @c: s 12472.3 10477 360 951 1134 1261 56854680 196826 67.6 25 58 @c: s 13681.8 10478 360 951 1134 1261 65133325 179527 67.7 24 55 @c: s 15526.5 10479 360 951 1134 1261 77121796 179505 67.6 21 52 @c: s 16055.0 10480 360 951 1134 1261 80741999 140293 67.7 24 40 @c: R 19821.2 10480 360 951 1134 1261 104996890 166390 67.3 21 55 @c: B 20121.2 10480 360 951 1134 1261 106508046 217105 67.2 20 71 @c: s 23029.8 10481 360 951 1134 1261 125660001 179558 67.1 25 52 @c: s 23421.8 10482 360 951 1134 1261 128480003 179521 67.1 23 52 @c: s 25934.2 10483 360 951 1134 1261 144967956 179541 67.3 25 52 @c: s 26395.6 10484 360 951 1134 1261 147631563 220660 67.2 21 62 @c: s 27795.5 10485 360 951 1134 1261 156895584 159568 67.4 24 46 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: - 28198.6 10348 359 951 1135 1261 159356044 177677 67.4 20 64 @c: s 28198.9 10276 359 951 1135 1261 159356044 255342 67.4 20 75 @c: - 28198.9 10276 359 951 1135 1261 159356044 174124 67.4 20 75 @c: + 28199.0 10276 359 951 1135 1261 159356044 191536 67.4 20 80 @c: s 28248.4 10277 359 951 1135 1261 159594051 242235 67.4 25 84 @c: s 28336.7 10278 359 951 1135 1261 160059262 143820 67.4 23 42 @c: s 28705.3 10279 359 951 1135 1261 162147198 143868 67.3 23 41 @c: s 30089.6 10280 359 951 1135 1261 170565082 191602 67.3 27 54 @c: - 30126.0 10251 358 951 1136 1261 170796692 189621 67.3 32 46 @c: s 30126.2 10170 356 951 1136 1263 170796692 191633 67.3 32 53 @c: - 30126.2 10170 356 951 1136 1263 170796692 187725 67.3 32 53 @c: + 30126.2 10170 356 951 1136 1263 170796692 206497 67.3 32 53 @c: s 30653.4 10171 356 951 1136 1263 174015446 155349 67.3 25 43 @c: - 35018.5 10053 355 951 1137 1263 198219893 204433 67.4 23 54 @c: s 35018.8 9977 352 951 1137 1266 198219893 206503 67.4 23 62 @c: - 35018.8 9977 352 951 1137 1266 198219893 200345 67.4 23 62 @c: + 35018.8 9977 352 951 1137 1266 198219893 220379 67.4 23 62 @c: s 36130.2 9978 352 951 1137 1266 204054575 166474 67.4 22 45 @c: s 36898.6 9979 352 951 1137 1266 207977964 220451 67.4 24 62 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 38783.8 9980 352 951 1137 1266 217259064 220424 67.1 29 63 @c: R 39947.0 9980 352 951 1137 1266 223057644 220416 66.9 23 68 @c: B 41202.4 9980 352 951 1137 1266 229400379 220441 66.6 22 80 @c: s 42312.5 9981 352 951 1137 1266 235029424 165344 66.5 26 46 @c: s 42788.4 9982 352 951 1137 1266 237650474 200069 66.4 28 59 @c: s 47023.2 9983 352 951 1137 1266 260768212 224669 66.4 23 69 @c: s 47726.9 9984 352 951 1137 1266 264670509 220456 66.4 26 66 @c: s 48672.3 9985 352 951 1137 1266 269946975 220474 66.4 28 60 @c: s 56765.6 9986 352 951 1137 1266 313269989 220441 66.5 23 66 @c: s 56880.1 9987 352 951 1137 1266 313868655 220409 66.6 24 64 @c: s 57074.4 9988 352 951 1137 1266 314922189 165405 66.6 25 43 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33