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-std.cnf c found header 'p cnf 6912 16992' 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 15195 6351 561 0 0 0 0 0.0 0 2 @c: s 0.0 8808 2557 1650 95 2610 0 0 0.0 0 2 @c: l 0.0 8808 2557 1650 95 2610 0 8762 0.0 0 2 @c: R 0.0 8808 2557 1650 95 2610 100 100 99.0 4 2 @c: R 0.0 8808 2557 1650 95 2610 201 201 101.5 7 2 @c: R 0.0 8808 2557 1650 95 2610 802 802 103.9 9 2 @c: B 0.0 8808 2557 1650 95 2610 1001 1001 102.9 9 2 @c: B 0.0 8808 2557 1650 95 2610 2002 2002 92.1 6 2 @c: R 0.1 8808 2557 1650 95 2610 2404 2404 89.3 7 2 @c: R 0.1 8808 2557 1650 95 2610 6407 6407 80.8 7 3 @c: B 0.1 8808 2557 1650 95 2610 8008 8008 78.4 6 4 @c: + 0.1 8808 2557 1650 95 2610 8762 9638 78.4 8 4 @c: + 0.2 8808 2557 1650 95 2610 10950 10601 74.8 6 4 @c: + 0.2 8808 2557 1650 95 2610 13685 11661 73.7 9 4 @c: R 0.2 8808 2557 1650 95 2610 16025 11685 72.0 6 5 @c: + 0.3 8808 2557 1650 95 2610 17105 12827 71.2 7 5 @c: + 0.3 8808 2557 1650 95 2610 21380 14109 69.4 7 5 @c: B 0.4 8808 2557 1650 95 2610 24012 14135 69.0 7 5 @c: + 0.4 8808 2557 1650 95 2610 26727 15519 67.9 6 5 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 0.5 8808 2557 1650 95 2610 33406 17070 67.2 8 6 @c: R 0.6 8808 2557 1650 95 2610 38460 17093 65.7 6 6 @c: + 0.6 8808 2557 1650 95 2610 41755 18777 65.5 9 6 @c: + 0.8 8808 2557 1650 95 2610 52190 20654 64.3 6 7 @c: B 1.0 8808 2557 1650 95 2610 64019 20681 62.9 8 7 @c: + 1.1 8808 2557 1650 95 2610 65236 22719 63.0 9 7 @c: + 1.4 8808 2557 1650 95 2610 81546 24990 61.0 7 8 @c: R 1.5 8808 2557 1650 95 2610 89726 25016 60.1 7 8 @c: + 1.8 8808 2557 1650 95 2610 101931 27489 58.9 8 9 @c: + 2.3 8808 2557 1650 95 2610 127410 30237 59.2 8 10 @c: + 3.0 8808 2557 1650 95 2610 159261 33260 58.1 8 11 @c: B 3.0 8808 2557 1650 95 2610 160033 31035 58.1 8 11 @c: + 3.9 8808 2557 1650 95 2610 199079 36586 56.2 5 12 @c: R 4.0 8808 2557 1650 95 2610 205064 36611 56.0 5 12 @c: + 5.1 8808 2557 1650 95 2610 248846 40244 55.0 7 13 @c: + 6.8 8808 2557 1650 95 2610 311055 44268 54.4 8 15 @c: B 8.6 8808 2557 1650 95 2610 384072 44286 53.4 7 16 @c: + 8.8 8808 2557 1650 95 2610 388816 48694 53.4 9 16 @c: R 10.7 8808 2557 1650 95 2610 461376 48724 52.1 5 19 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 11.3 8808 2557 1650 95 2610 486021 53563 51.7 7 19 @c: + 15.6 8808 2557 1650 95 2610 607526 58919 51.5 7 23 @c: + 20.6 8808 2557 1650 95 2610 759405 64810 50.8 8 26 @c: B 25.1 8808 2557 1650 95 2610 896169 64817 50.6 7 27 @c: + 26.8 8808 2557 1650 95 2610 949256 71291 50.3 7 28 @c: R 29.6 8808 2557 1650 95 2610 1025168 71312 49.6 7 31 @c: + 38.0 8808 2557 1650 95 2610 1186570 78420 49.4 8 32 @c: + 51.6 8808 2557 1650 95 2610 1483210 86262 49.0 8 35 @c: + 70.5 8808 2557 1650 95 2610 1854011 94888 48.6 6 38 @c: B 80.2 8808 2557 1650 95 2610 2048340 94908 48.2 6 39 @c: R 93.4 8808 2557 1650 95 2610 2255209 104311 47.5 5 46 @c: + 97.7 8808 2557 1650 95 2610 2317510 104376 47.2 10 46 @c: s 142.6 8809 2557 1650 95 2610 2895769 104389 46.4 7 19 @c: + 142.7 8809 2557 1650 95 2610 2896885 114813 46.4 8 22 @c: + 190.8 8809 2557 1650 95 2610 3621106 126294 45.7 5 47 @c: + 250.0 8809 2557 1650 95 2610 4526384 138923 45.2 6 54 @c: B 254.2 8809 2557 1650 95 2610 4608671 138939 45.0 8 55 @c: R 283.8 8809 2557 1650 95 2610 4919967 138943 44.7 8 67 @c: + 353.9 8809 2557 1650 95 2610 5657981 152815 44.6 8 58 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 456.2 8809 2557 1650 95 2610 7072475 168096 44.0 6 75 @c: + 601.6 8809 2557 1650 95 2610 8840590 184905 43.7 6 88 @c: B 730.6 8809 2557 1650 95 2610 10241306 184922 43.3 6 99 @c: R 785.9 8809 2557 1650 95 2610 10659170 184915 43.0 11 107