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-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 = 0 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 15193 6363 549 0 0 0 0 0.0 0 2 @c: s 0.0 9699 2941 1617 102 2252 0 0 0.0 0 2 @c: l 0.0 9699 2941 1617 102 2252 0 9617 0.0 0 2 @c: R 0.0 9699 2941 1617 102 2252 100 100 108.6 4 2 @c: R 0.0 9699 2941 1617 102 2252 200 200 142.7 7 2 @c: R 0.0 9699 2941 1617 102 2252 806 806 121.0 7 2 @c: B 0.0 9699 2941 1617 102 2252 1001 1001 121.9 6 2 @c: B 0.1 9699 2941 1617 102 2252 2002 2002 121.8 7 2 @c: R 0.1 9699 2941 1617 102 2252 2413 2413 120.4 7 3 @c: R 0.1 9699 2941 1617 102 2252 6421 6421 121.0 6 3 @c: B 0.1 9699 2941 1617 102 2252 8005 8005 133.2 7 4 @c: + 0.2 9699 2941 1617 102 2252 9618 10578 132.1 6 4 @c: + 0.2 9699 2941 1617 102 2252 12021 11635 126.7 6 4 @c: + 0.2 9699 2941 1617 102 2252 15026 12798 127.4 4 5 @c: R 0.3 9699 2941 1617 102 2252 16040 12667 126.0 6 5 @c: + 0.3 9699 2941 1617 102 2252 18780 14077 130.0 6 5 @c: + 0.4 9699 2941 1617 102 2252 23475 15484 135.0 5 6 @c: B 0.4 9699 2941 1617 102 2252 24008 14633 134.0 7 6 @c: + 0.5 9699 2941 1617 102 2252 29340 17032 130.5 7 6 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 0.6 9701 2941 1617 102 2252 35264 17049 127.7 6 5 @c: + 0.6 9701 2941 1617 102 2252 36675 18735 126.6 7 5 @c: R 0.7 9701 2941 1617 102 2252 38465 18750 125.2 5 6 @c: s 0.8 9703 2941 1617 102 2252 44865 18758 120.7 6 5 @c: + 0.8 9703 2941 1617 102 2252 45842 20608 120.9 6 6 @c: + 1.0 9703 2941 1617 102 2252 57300 22668 129.0 5 8 @c: B 1.2 9703 2941 1617 102 2252 64019 22694 125.7 7 8 @c: + 1.3 9703 2941 1617 102 2252 71626 24934 122.5 6 8 @c: + 1.7 9703 2941 1617 102 2252 89531 27427 117.1 6 9 @c: R 1.7 9703 2941 1617 102 2252 89740 25161 117.1 6 9 @c: + 2.2 9703 2941 1617 102 2252 111911 30169 116.1 8 11 @c: + 2.8 9703 2941 1617 102 2252 139886 33185 118.5 7 11 @c: B 3.2 9703 2941 1617 102 2252 160043 33208 116.4 7 12 @c: + 3.6 9703 2941 1617 102 2252 174855 36503 114.9 7 13 @c: R 4.3 9703 2941 1617 102 2252 205079 36526 113.1 5 15 @c: + 4.7 9703 2941 1617 102 2252 218566 40153 111.6 6 16 @c: + 6.2 9703 2941 1617 102 2252 273206 44168 111.1 5 16 @c: + 8.1 9703 2941 1617 102 2252 341505 48584 110.5 7 18 @c: B 9.2 9703 2941 1617 102 2252 384080 48612 109.7 5 19 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: + 10.3 9703 2941 1617 102 2252 426881 53442 108.3 6 19 @c: R 11.3 9703 2941 1617 102 2252 461392 53474 106.3 5 21 @c: + 13.8 9703 2941 1617 102 2252 533601 58786 103.9 8 26 @c: + 18.0 9703 2941 1617 102 2252 667000 64664 102.9 5 26 @c: s 22.2 9706 2941 1617 102 2252 788150 64691 102.2 4 14 @c: + 23.6 9706 2941 1617 102 2252 833750 71130 102.0 7 20 @c: B 25.7 9706 2941 1617 102 2252 896169 71160 101.8 6 24 @c: R 30.1 9706 2941 1617 102 2252 1025160 71161 98.9 5 29 @c: + 30.7 9706 2941 1617 102 2252 1042185 78243 98.5 8 29 @c: + 42.4 9706 2941 1617 102 2252 1302730 86067 97.3 8 34 @c: + 56.3 9706 2941 1617 102 2252 1628410 94673 94.3 8 44 @c: s 70.8 9711 2941 1617 102 2252 1915653 94697 93.6 5 21 @c: s 72.7 9713 2941 1617 102 2252 1948530 94683 93.9 6 20 @c: + 77.4 9713 2941 1617 102 2252 2035510 104140 93.8 5 30 @c: B 78.1 9713 2941 1617 102 2252 2048334 104180 93.7 5 32 @c: R 89.1 9713 2941 1617 102 2252 2255093 104169 91.5 6 41 @c: + 122.3 9713 2941 1617 102 2252 2544386 114554 90.4 7 36 @c: s 152.5 9714 2941 1617 102 2252 2884459 114580 90.0 6 25 @c: + 185.2 9714 2941 1617 102 2252 3180480 126009 89.6 6 41 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: s 189.4 9715 2941 1617 102 2252 3211577 126048 89.5 6 28 @c: s 195.6 9719 2941 1617 102 2252 3254946 126032 89.5 5 27 @c: s 214.7 9726 2941 1617 102 2252 3378021 126043 89.1 8 26 @c: s 220.3 9730 2941 1617 102 2252 3418380 126054 89.0 4 26 @c: + 316.9 9730 2941 1617 102 2252 3975602 138609 88.0 7 52 @c: B 394.4 9730 2941 1617 102 2252 4608675 138638 86.7 6 64 @c: R 434.6 9730 2941 1617 102 2252 4919743 204517 85.5 6 97 @c: + 442.4 9730 2941 1617 102 2252 4969501 152469 85.3 7 80 @c: + 597.3 9730 2941 1617 102 2252 6211875 167715 83.9 5 70 @c: s 659.2 9745 2941 1617 102 2252 6711617 167745 83.6 5 35 @c: s 736.1 9760 2941 1617 102 2252 7376180 167749 83.3 6 34 @c: s 741.8 9766 2941 1617 102 2252 7430194 167748 83.1 6 36 @c: + 795.2 9766 2941 1617 102 2252 7764840 184486 82.3 3 73 @c: s 981.9 9787 2941 1617 102 2252 9121838 184514 82.4 5 37 @c: s 989.5 9824 2941 1617 102 2252 9176986 184521 82.4 5 37 @c: s 997.9 9830 2941 1617 102 2252 9236962 184515 82.4 6 38 @c: + 1054.9 9830 2941 1617 102 2252 9706051 202934 82.1 6 66 @c: B 1126.3 9830 2941 1617 102 2252 10241341 202959 81.4 6 87 @c: R 1231.5 9830 2941 1617 102 2252 10658756 202953 80.9 5 110 c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: B 3486.3 9830 2941 1617 102 2252 22530593 202943 77.8 7 136 @c: R 3647.4 9830 2941 1617 102 2252 22956206 202964 77.5 6 146 c c *** CAUGHT SIGNAL 2 *** c c 33371319 conflicts, 55746939 decisions, 27895 random c 0 iterations, 47098 restarts, 0 skipped c 32 enlarged, 138 shrunken, 326254 rescored, 6008 rebiased c 17 simplifications, 8 reductions c c vars: 1617 fixed, 102 equiv, 2252 elim, 131 merged c elim: 76418 resolutions, 1 phases, 1 rounds c sbst: 2% substituted, 0.0% nots, 100.0% ands, 0.0% xors, 0.0% ites c arty: 2.05 and 0.00 xor average arity c prbe: 12408293 probed, 2107 phases, 2108 rounds c prbe: 29 failed, 0 lifted, 12 merged c sccs: 3 non trivial, 0 fixed, 6 merged c hash: 0 units, 113 merged c mins: 1218755054 learned, 9% deleted, 106 strong, 16 depth c subs: 128 forward, 137 backward, 266 doms c strs: 131 forward, 53 backward c doms: 350 dominators, 0 high, 0 low c prps: 4047785643 propagations, 0.64 megaprops c c 6316.3 seconds, 200 MB max, 5638 MB recycled c c *** CAUGHT SIGNAL 2 *** c