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_15-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 29168 3145 561 0 0 0 0 0.0 0 3 @c: s 0.1 19962 695 640 1119 1252 0 0 0.0 0 3 @c: l 0.1 19962 695 640 1119 1252 0 19221 0.0 0 3 @c: R 0.1 19962 695 640 1119 1252 100 100 69.7 2 3 @c: R 0.1 19963 694 640 1120 1252 201 200 53.4 4 3 @c: B 0.1 20309 636 696 1122 1252 1001 988 68.1 17 3 @c: B 0.1 20668 532 792 1130 1252 2001 1979 77.4 21 4 @c: R 0.1 20682 532 792 1130 1252 2254 2232 78.3 21 4 @c: R 0.2 20831 516 802 1136 1252 4963 4938 81.8 25 4 @c: B 0.2 20849 365 970 1119 1252 8003 7974 77.2 26 5 @c: N 0.2 20875 365 970 1119 1252 12018 11987 73.1 26 6 @c: + 0.3 21005 360 971 1123 1252 19222 21143 70.0 24 7 @c: N 0.4 21005 360 971 1123 1252 21631 21184 69.7 26 8 @c: B 0.4 21005 360 971 1123 1252 24009 21171 69.2 27 8 @c: + 0.4 21005 360 971 1123 1252 24028 23257 69.2 26 8 @c: + 0.5 21020 353 981 1120 1252 30035 25582 67.1 23 9 @c: - 0.6 11526 344 981 1120 1261 32416 25327 65.9 24 6 @c: - 0.6 10210 334 981 1120 1271 32416 25074 65.9 24 6 @c: - 0.6 10097 333 981 1120 1272 32416 24824 65.9 24 6 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: - 0.6 9983 332 981 1120 1273 32416 24576 65.9 24 6 @c: - 0.6 9906 331 981 1120 1274 32416 24331 65.9 24 6 @c: s 0.6 9798 331 981 1120 1274 32416 21360 65.9 24 5 @c: - 0.6 9798 331 981 1120 1274 32416 12166 65.9 24 5 @c: + 0.6 9798 331 981 1120 1274 32416 13382 65.9 24 3 @c: + 0.7 9812 329 983 1120 1274 40520 14720 63.0 23 5 @c: + 0.9 9816 329 983 1120 1274 50650 16192 60.6 26 6 @c: + 1.2 9816 329 983 1120 1274 63310 17811 58.8 29 8 @c: B 1.2 9816 329 983 1120 1274 64017 20685 58.7 28 9 @c: s 1.5 9711 327 985 1120 1274 71970 15261 58.3 22 5 @c: - 1.5 9711 327 985 1120 1274 71970 17633 58.3 22 5 @c: + 1.6 9711 327 985 1120 1274 78344 19396 58.1 23 6 @c: + 1.9 9711 327 985 1120 1274 97931 21335 56.8 24 7 @c: N 2.1 9711 327 985 1120 1274 109695 21376 56.0 26 8 @c: + 2.4 9711 327 985 1120 1274 122411 23468 55.2 26 9 @c: s 2.4 9716 327 985 1120 1274 125526 23481 55.1 22 6 @c: + 3.0 9719 327 985 1120 1274 153011 25814 54.3 26 9 @c: B 3.2 9719 327 985 1120 1274 160037 25842 54.1 24 9 @c: R 3.2 9719 327 985 1120 1274 160980 25850 54.1 23 10 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 3.3 9719 327 985 1120 1274 165223 25845 54.0 26 7 @c: + 3.8 9719 327 985 1120 1274 191260 28395 53.3 24 9 @c: - 4.6 9640 327 985 1120 1274 223589 28112 52.7 23 7 @c: s 4.6 9402 326 985 1120 1275 223589 27944 52.7 23 7 @c: - 4.6 9402 326 985 1120 1275 223589 27550 52.7 23 7 @c: + 4.8 9410 326 985 1120 1275 231952 30305 52.5 27 9 @c: s 5.7 10463 326 985 1120 1275 268471 30358 51.4 23 7 @c: R 5.9 10463 326 985 1120 1275 276342 30327 51.3 24 9 @c: + 6.3 10463 326 985 1120 1275 289940 33335 50.9 25 10 @c: s 7.5 10464 326 985 1120 1275 332367 33400 50.4 23 8 @c: + 8.4 10464 326 985 1120 1275 362426 36668 50.3 25 12 @c: B 9.0 10464 326 985 1120 1275 384065 36706 50.0 26 13 @c: + 10.8 10464 326 985 1120 1275 453030 40334 49.3 22 15 @c: R 13.2 10464 326 985 1120 1275 532694 40389 48.4 24 17 @c: + 14.2 10464 326 985 1120 1275 566285 44367 48.0 21 18 @c: s 15.0 10466 326 985 1120 1275 587581 44427 47.9 22 10 @c: s 17.0 10468 326 985 1120 1275 655734 44395 47.6 24 10 @c: + 18.7 10469 326 985 1120 1275 707858 48803 47.3 29 15 @c: s 18.9 10469 326 985 1120 1275 714142 48864 47.3 26 11 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 23.6 10470 326 985 1120 1275 838527 44986 46.8 24 11 @c: + 25.1 10471 325 985 1121 1275 884820 53683 46.7 25 16 @c: B 25.5 10471 325 985 1121 1275 896153 53700 46.6 26 17 @c: - 25.8 10338 325 985 1121 1275 905480 53147 46.5 26 10 @c: - 25.8 10239 325 985 1121 1275 905480 52616 46.5 26 10 @c: - 25.8 9551 324 985 1121 1276 905480 52090 46.5 26 10 @c: s 25.9 9527 324 985 1121 1276 905480 53695 46.5 26 11 @c: - 25.9 9527 324 985 1121 1276 905480 50528 46.5 26 11 @c: + 31.3 9527 324 985 1121 1276 1040983 55580 46.2 25 23 @c: N 33.9 9527 324 985 1121 1276 1096596 55623 46.0 25 17 @c: s 40.1 9528 324 985 1121 1276 1205434 55595 45.2 24 14 @c: + 44.1 9528 324 985 1121 1276 1301225 61138 45.4 28 20 @c: + 60.3 9528 324 985 1121 1276 1626532 67251 44.9 27 27 @c: + 83.5 9528 324 985 1121 1276 2033165 73976 44.6 22 33 @c: B 84.4 9528 324 985 1121 1276 2048328 74019 44.5 27 35 @c: R 105.8 9528 324 985 1121 1276 2326775 103465 43.9 23 46 @c: s 106.0 9529 324 985 1121 1276 2326979 102648 43.9 23 22 @c: + 122.1 9529 324 985 1121 1276 2541455 81373 44.1 26 27 @c: s 163.9 9530 324 985 1121 1276 3169502 81387 43.9 27 18 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 164.3 9531 324 985 1121 1276 3176821 89510 43.9 26 21 @c: - 170.8 9361 323 986 1121 1276 3273786 88615 43.9 26 16 @c: - 170.8 9263 323 986 1121 1276 3273786 87729 43.9 26 16 @c: s 170.9 9250 323 986 1121 1276 3273786 89558 43.9 26 19 @c: - 170.9 9250 323 986 1121 1276 3273786 85098 43.9 26 19 @c: + 205.0 9250 323 986 1121 1276 3775243 93607 43.5 25 42 @c: B 252.6 9250 323 986 1121 1276 4608685 93653 43.1 26 50 @c: s 259.5 9251 323 986 1121 1276 4704887 93609 43.0 23 20 @c: + 260.2 9252 323 986 1121 1276 4719051 102967 43.0 26 23 @c: - 266.1 9164 322 987 1121 1276 4818282 101938 42.9 23 20 @c: s 266.2 9109 322 987 1121 1276 4818282 102995 42.9 23 23 @c: - 266.2 9109 322 987 1121 1276 4818282 100919 42.9 23 23 @c: R 280.8 9109 322 987 1121 1276 4992104 100955 42.8 24 38 @c: s 318.0 9110 322 987 1121 1276 5406134 100944 42.5 24 22 @c: - 325.8 9064 321 988 1121 1276 5541921 99910 42.5 30 19 @c: s 325.9 8997 321 988 1121 1276 5541921 100962 42.5 30 22 @c: - 325.9 8997 321 988 1121 1276 5541921 98911 42.5 30 22 @c: + 333.4 8997 321 988 1121 1276 5666376 108802 42.4 23 33 @c: s 342.9 8998 321 988 1121 1276 5820922 108821 42.4 25 24 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: - 351.5 8865 320 989 1121 1276 5954429 107714 42.4 28 19 @c: - 351.5 8863 319 989 1121 1277 5954429 106637 42.4 28 19 @c: s 351.6 8800 318 989 1121 1278 5954429 108835 42.4 28 23 @c: - 351.6 8800 318 989 1121 1278 5954429 104505 42.4 28 23 @c: s 373.8 8801 318 989 1121 1278 6322988 104524 42.4 26 21 @c: + 404.9 8801 318 989 1121 1278 6803181 114955 42.3 25 45 @c: s 458.9 8802 318 989 1121 1278 7579529 114972 42.1 23 24 @c: s 469.2 8803 318 989 1121 1278 7720062 114992 42.1 26 27 @c: s 484.0 8804 318 989 1121 1278 7888300 114982 42.0 23 26 @c: - 493.7 8669 317 990 1121 1278 8030168 113806 42.1 28 20 @c: s 493.8 8583 317 990 1121 1278 8030168 114999 42.1 28 24 @c: - 493.8 8583 317 990 1121 1278 8030168 111530 42.1 28 24 @c: + 507.5 8583 317 990 1121 1278 8250560 122683 42.1 27 38 @c: s 521.0 8584 317 990 1121 1278 8454232 122720 42.0 24 25 @c: s 589.7 8585 317 990 1121 1278 9361409 122732 41.8 25 26 @c: B 660.7 8585 317 990 1121 1278 10241434 122701 41.6 27 56 @c: s 678.1 8476 315 990 1122 1279 10414257 122697 41.5 24 25 @c: - 678.1 8476 315 990 1122 1279 10414257 121457 41.5 24 25 @c: + 678.1 8476 315 990 1122 1279 10414257 133602 41.5 24 25 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 724.0 8477 315 990 1122 1279 11011341 133611 41.2 24 27 @c: - 798.8 8362 314 990 1123 1279 11951979 132266 41.0 28 24 @c: s 799.0 8260 310 990 1123 1283 11951979 133639 41.0 28 29 @c: - 799.0 8260 310 990 1123 1283 11951979 128299 41.0 28 29 @c: + 799.0 8260 310 990 1123 1283 11951979 141128 41.0 28 31 @c: s 933.1 8261 310 990 1123 1283 13228351 141162 40.6 21 32 @c: s 948.9 8077 307 992 1124 1283 13413435 141147 40.6 27 29 @c: - 948.9 8077 307 992 1124 1283 13413435 139717 40.6 27 29 @c: + 948.9 8077 307 992 1124 1283 13413435 153688 40.6 27 29 @c: s 1055.4 8078 307 992 1124 1283 14371025 117718 40.4 24 25 @c: s 1084.9 8079 307 992 1124 1283 14659340 153700 40.5 23 30 @c: s 1305.3 8081 307 992 1124 1283 16454030 153726 40.0 25 29 @c: s 1327.6 8412 307 992 1124 1283 16680571 153721 39.9 27 31 @c: s 1349.0 8413 307 992 1124 1283 16901256 153710 39.9 22 31 @c: - 1367.4 8310 306 992 1125 1283 17120738 152152 39.9 26 25 @c: s 1367.5 8234 304 992 1125 1285 17120738 153725 39.9 26 30 @c: - 1367.5 8234 304 992 1125 1285 17120738 149109 39.9 26 30 @c: + 1367.5 8234 304 992 1125 1285 17120738 164019 39.9 26 30 @c: s 1407.4 8235 304 992 1125 1285 17559398 164080 39.8 23 36 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: N 1550.0 8235 304 992 1125 1285 18557522 164041 39.5 27 76 @c: s 1697.9 8236 304 992 1125 1285 19496564 164038 39.2 25 31 @c: s 1800.5 8198 303 992 1126 1285 20633330 164051 39.1 28 34 @c: - 1800.5 8198 303 992 1126 1285 20633330 162379 39.1 28 34 @c: + 1800.5 8198 303 992 1126 1285 20633330 178616 39.1 28 34