PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc05.opb
MD5SUM	4f7891bf040f9fa135208e1a9808a8bc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1430464
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	81788220
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.00309
Number of variables	1320
Total number of constraints	374
Number of constraints which are clauses	155
Number of constraints which are cardinality constraints (but not clauses)	82
Number of constraints which are nor clauses,nor cardinality constraints	137
Minimum length of a constraint	1
Maximum length of a constraint	301
Trace number 19111

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 18:02:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16991 boxname=wulflinc24 idbench=1307 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f7891bf040f9fa135208e1a9808a8bc  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-misc05.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-misc05.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-misc05.opb
IDLAUNCH: 16991
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        781144 kB
Buffers:         30064 kB
Cached:         198708 kB
SwapCached:        524 kB
Active:          86104 kB
Inactive:       144700 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        780892 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            17128 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:15:55 (client local time) WITH STATUS 30 IN 776.539 SECONDS
stats: 16991 0 776.539 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 327 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................ssssssssssssssssssssssss
c ---[ 349]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 345]---> Adder-cost: 718   maxlim: 5243515   bits: 24/23
c ---[ 343]---> Sorter-cost: 4443     Base: 2 2 2 2 2 2 3 5 2 2 2 17 2
c ---[ 341]---> BDD-cost:   13
c ---[ 339]---> BDD-cost:   13
c ---[ 337]---> BDD-cost:   13
c ---[ 335]---> BDD-cost:   11
c ---[ 333]---> BDD-cost:   13
c ---[ 331]---> BDD-cost:   13
c ---[ 329]---> BDD-cost:   13
c ---[ 200]---> Sorter-cost:  118     Base:
c ---[ 198]---> Sorter-cost:  127     Base:
c ---[ 196]---> Sorter-cost:  126     Base:
c ---[ 194]---> Sorter-cost:  119     Base:
c ---[ 192]---> Sorter-cost:  126     Base:
c ---[ 190]---> Sorter-cost:  123     Base:
c ---[ 188]---> Sorter-cost:  126     Base:
c ---[ 186]---> Sorter-cost:  127     Base:
c ---[ 184]---> Sorter-cost:  127     Base:
c ---[ 182]---> Adder-cost: 371   maxlim: 235002   bits: 19/18
c ---[ 180]---> Adder-cost: 414   maxlim: 398330   bits: 20/19
c ---[ 178]---> Adder-cost: 414   maxlim: 418810   bits: 20/19
c ---[ 176]---> Adder-cost: 371   maxlim: 195835   bits: 19/18
c ---[ 174]---> Adder-cost: 414   maxlim: 400890   bits: 20/19
c ---[ 172]---> Adder-cost: 414   maxlim: 397050   bits: 20/19
c ---[ 170]---> Adder-cost: 414   maxlim: 416250   bits: 20/19
c ---[ 168]---> BDD-cost:   72
c ---[ 166]---> BDD-cost:   72
c ---[ 165]---> Sorter-cost: 1614     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1614     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> BDD-cost:   98
c ---[ 134]---> BDD-cost:   20
c ---[ 133]---> BDD-cost:   20
c ---[ 132]---> BDD-cost:   20
c ---[ 131]---> BDD-cost:   20
c ---[ 130]---> BDD-cost:   20
c ---[ 129]---> BDD-cost:   20
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:   23
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   23
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:   23
c ---[ 117]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   22
c ---[ 114]---> BDD-cost:   22
c ---[ 113]---> BDD-cost:   22
c ---[ 112]---> BDD-cost:   22
c ---[ 111]---> BDD-cost:   22
c ---[ 110]---> BDD-cost:   22
c ---[ 109]---> BDD-cost:   22
c ---[ 108]---> BDD-cost:   22
c ---[ 107]---> BDD-cost:   22
c ---[ 106]---> BDD-cost:   22
c ---[ 105]---> BDD-cost:   22
c ---[ 104]---> BDD-cost:   24
c ---[ 103]---> BDD-cost:   24
c ---[ 102]---> BDD-cost:   24
c ---[ 101]---> BDD-cost:   24
c ---[ 100]---> BDD-cost:   24
c ---[  99]---> BDD-cost:   24
c ---[  98]---> BDD-cost:   19
c ---[  97]---> BDD-cost:   19
c ---[  96]---> BDD-cost:   19
c ---[  95]---> BDD-cost:   19
c ---[  94]---> BDD-cost:   19
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   23
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   23
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   23
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   23
c ---[  82]---> BDD-cost:   23
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   23
c ---[  77]---> BDD-cost:    5
c ---[  76]---> BDD-cost:    7
c ---[  73]---> BDD-cost:    6
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    6
c ---[  70]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    8
c ---[  61]---> BDD-cost:    7
c ---[  59]---> BDD-cost:    5
c ---[  56]---> BDD-cost:    6
c ---[  55]---> BDD-cost:    7
c ---[  53]---> BDD-cost:    6
c ---[  52]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    7
c ---[  49]---> BDD-cost:    7
c ---[  47]---> BDD-cost:    6
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    7
c ---[  43]---> BDD-cost:    7
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    7
c ---[  35]---> BDD-cost:    6
c ---[  34]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    7
c ---[  30]---> BDD-cost:    7
c ---[  28]---> BDD-cost:    6
c ---[  27]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    7
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    4
c ---[  21]---> BDD-cost:    4
c ---[  20]---> BDD-cost:    4
c ---[  19]---> BDD-cost:    4
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    4
c ---[  16]---> BDD-cost:    4
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    4
c ---[  13]---> BDD-cost:    4
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    4
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    4
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    4
c ---[   6]---> BDD-cost:    4
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    4
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   50790   151605 |   16930       0        0     nan |  0.000 % |
c |       101 |   50668   151333 |   18623      98     1896    19.3 |  7.499 % |
c |       251 |   50129   149847 |   20485     232     5573    24.0 |  8.280 % |
c |       477 |   49918   149131 |   22533     456    11214    24.6 |  8.480 % |
c |       815 |   49549   148135 |   24787     791    21555    27.3 |  9.047 % |
c |      1322 |   49541   148109 |   27265    1297    45960    35.4 |  9.055 % |
c |      2081 |   49391   147677 |   29992    2035    68311    33.6 |  9.276 % |
c |      3220 |   49329   147507 |   32991    3165    96394    30.5 |  9.372 % |
c |      4928 |   49046   146782 |   36290    4865   156211    32.1 |  9.881 % |
c ==============================================================================
c [1mFound solution: 1458112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7358 |   48464   145245 |   16154    7097   231356    32.6 |  9.881 % |
c |      7459 |   48464   145245 |   17769    7198   237830    33.0 | 10.975 % |
c |      7609 |   48464   145245 |   19546    7348   249118    33.9 | 10.975 % |
c |      7835 |   48446   145189 |   21500    7546   266322    35.3 | 11.049 % |
c |      8172 |   48418   145112 |   23651    7880   275220    34.9 | 11.056 % |
c |      8684 |   48418   145112 |   26016    8392   292586    34.9 | 11.056 % |
c ==============================================================================
c [1mFound solution: 1456768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8763 |   48445   145179 |   16148    8471   294523    34.8 | 11.056 % |
c |      8864 |   48445   145179 |   17762    8572   297021    34.7 | 11.057 % |
c ==============================================================================
c [1mFound solution: 1448960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8998 |   48463   145225 |   16154    8706   304885    35.0 | 11.057 % |
c |      9098 |   48463   145225 |   17769    8806   308941    35.1 | 11.060 % |
c ==============================================================================
c [1mFound solution: 1448512[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9141 |   48438   145175 |   16146    8848   313475    35.4 | 11.060 % |
c |      9242 |   48429   145144 |   17760    8947   315611    35.3 | 11.179 % |
c |      9395 |   48410   145094 |   19536    9098   320586    35.2 | 11.208 % |
c |      9624 |   48383   145034 |   21490    9322   333154    35.7 | 11.267 % |
c |      9961 |   48367   144982 |   23639    9657   347486    36.0 | 11.282 % |
c |     10468 |   48352   144949 |   26003   10162   371458    36.6 | 11.311 % |
c ==============================================================================
c [1mFound solution: 1447808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11131 |   48364   144983 |   16121   10815   401493    37.1 | 11.311 % |
c |     11233 |   48355   144952 |   17733   10916   409288    37.5 | 11.350 % |
c |     11383 |   48355   144952 |   19506   11066   412895    37.3 | 11.350 % |
c |     11612 |   48355   144952 |   21457   11295   416570    36.9 | 11.350 % |
c |     11950 |   48355   144952 |   23602   11633   430385    37.0 | 11.350 % |
c ==============================================================================
c [1mFound solution: 1447296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12007 |   48384   145023 |   16128   11690   437448    37.4 | 11.350 % |
c |     12109 |   48384   145023 |   17740   11792   439297    37.3 | 11.350 % |
c |     12259 |   48384   145023 |   19514   11942   442581    37.1 | 11.350 % |
c |     12486 |   48384   145023 |   21466   12169   449667    37.0 | 11.350 % |
c |     12824 |   48328   144837 |   23613   12498   471700    37.7 | 11.401 % |
c |     13330 |   48127   144355 |   25974   12990   483905    37.3 | 11.820 % |
c ==============================================================================
c [1mFound solution: 1444928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13475 |   48140   144380 |   16046   13132   488125    37.2 | 11.820 % |
c |     13575 |   48140   144380 |   17650   13232   495166    37.4 | 11.830 % |
c |     13726 |   48140   144380 |   19415   13383   507223    37.9 | 11.830 % |
c |     13952 |   48140   144380 |   21357   13609   509922    37.5 | 11.830 % |
c |     14291 |   48131   144349 |   23492   13946   517410    37.1 | 11.837 % |
c |     14798 |   48077   144163 |   25842   14444   541210    37.5 | 11.881 % |
c |     15558 |   48077   144163 |   28426   15204   586176    38.6 | 11.881 % |
c ==============================================================================
c [1mFound solution: 1444864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16159 |   48077   144147 |   16025   15799   628031    39.8 | 11.881 % |
c |     16260 |   48068   144116 |   17627   15899   634611    39.9 | 11.906 % |
c |     16410 |   48068   144116 |   19390   16049   636257    39.6 | 11.906 % |
c |     16638 |   48059   144085 |   21329   16276   641762    39.4 | 11.913 % |
c |     16975 |   47976   143837 |   23462   16605   680478    41.0 | 12.024 % |
c |     17482 |   47967   143806 |   25808   17111   702501    41.1 | 12.031 % |
c ==============================================================================
c [1mFound solution: 1444288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17565 |   47993   143872 |   15997   17194   715664    41.6 | 12.031 % |
c |     17668 |   47980   143842 |   17596   17288   718863    41.6 | 12.069 % |
c |     17818 |   47980   143842 |   19356   17438   722799    41.4 | 12.069 % |
c ==============================================================================
c [1mFound solution: 1434624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17892 |   48000   143892 |   16000   17512   732864    41.8 | 12.069 % |
c |     17993 |   47701   143212 |   17600   17607   735952    41.8 | 12.687 % |
c |     18143 |   47701   143212 |   19360   17757   760245    42.8 | 12.687 % |
c |     18368 |   47701   143212 |   21296   17982   776115    43.2 | 12.687 % |
c |     18706 |   47568   142897 |   23425   18313   798216    43.6 | 12.973 % |
c |     19215 |   47550   142835 |   25768   18818   833764    44.3 | 12.988 % |
c |     19975 |   47514   142754 |   28344   19569   897864    45.9 | 13.076 % |
c |     21114 |   47398   142382 |   31179   20665   932210    45.1 | 13.223 % |
c |     22827 |   47241   141856 |   34297   22334  1069951    47.9 | 13.399 % |
c |     25390 |   47196   141701 |   37727   24890  1342854    54.0 | 13.436 % |
c ==============================================================================
c [1mFound solution: 1434304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25484 |   47226   141775 |   15742   24984  1352481    54.1 | 13.436 % |
c |     25586 |   47226   141775 |   17316   12594   745899    59.2 | 13.434 % |
c |     25739 |   47226   141775 |   19047   12747   750096    58.8 | 13.434 % |
c |     25968 |   47226   141775 |   20952   12976   755346    58.2 | 13.434 % |
c |     26306 |   47226   141775 |   23047   13314   783433    58.8 | 13.434 % |
c |     26812 |   47226   141775 |   25352   13820   858652    62.1 | 13.434 % |
c |     27571 |   47226   141775 |   27887   14579   957839    65.7 | 13.434 % |
c ==============================================================================
c [1mFound solution: 1430464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28429 |   47254   141843 |   15751   15437  1055558    68.4 | 13.434 % |
c |     28530 |   47254   141843 |   17326   15538  1064460    68.5 | 13.433 % |
c |     28681 |   47254   141843 |   19058   15689  1069113    68.1 | 13.433 % |
c |     28908 |   47254   141843 |   20964   15916  1077085    67.7 | 13.433 % |
c |     29246 |   47254   141843 |   23061   16254  1133268    69.7 | 13.433 % |
c |     29752 |   47254   141843 |   25367   16760  1202188    71.7 | 13.433 % |
c |     30511 |   47254   141843 |   27903   17519  1224601    69.9 | 13.433 % |
c |     31650 |   47188   141624 |   30694   18649  1284348    68.9 | 13.498 % |
c |     33358 |   47155   141511 |   33763   20350  1480043    72.7 | 13.542 % |
c |     35921 |   47120   141405 |   37140   22910  1661643    72.5 | 13.572 % |
c |     39765 |   47111   141374 |   40854   26752  1931091    72.2 | 13.579 % |
c |     45535 |   46978   141015 |   44939   32509  2570793    79.1 | 13.821 % |
c |     54184 |   46951   140922 |   49433   41152  4009198    97.4 | 13.843 % |
c |     67159 |   46921   140833 |   54376   22797  2786071   122.2 | 13.887 % |
c |     86623 |   46858   140648 |   59814   42250  5757599   136.3 | 13.968 % |
c |    115816 |   46609   140004 |   65795   33140  3322314   100.3 | 14.429 % |
c ==============================================================================
c [1mOptimal solution: 1430464[0m
s OPTIMUM FOUND
v -COL133_bit_7 -COL133_bit_6 -COL133_bit_5 -COL133_bit_4 -COL133_bit_3 -COL133_bit_2 COL133_bit_1 COL133_bit0 COL133_bit1 COL133_bit2 -COL133_bit3 -COL133_bit4 COL133_bit5 -COL133_bit6 COL133_bit7 COL133_bit8 COL133_bit9 -COL133_bit10 COL133_bit11 -COL133_bit12 COL133_bit13 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 -COL006_bit0 COL007_bit0 -COL008_bit0 COL009_bit0 -COL010_bit0 -COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 -COL018_bit0 -COL019_bit0 -COL020_bit0 -COL021_bit0 -COL022_bit0 COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 -COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 -COL031_bit0 COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 -COL036_bit0 COL037_bit0 -COL038_bit0 -COL039_bit0 -COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 -COL045_bit0 -COL046_bit0 COL047_bit0 -COL048_bit0 -COL049_bit0 -COL050_bit0 -COL051_bit0 -COL052_bit0 COL053_bit0 -COL054_bit0 -COL055_bit0 -COL056_bit0 -COL057_bit0 COL058_bit0 COL059_bit0 COL060_bit0 -COL061_bit0 -COL062_bit0 -COL063_bit0 -COL064_bit0 -COL065_bit0 -COL066_bit0 -COL067_bit0 -COL068_bit0 -COL069_bit0 -COL070_bit0 COL071_bit0 -COL072_bit0 COL129_bit0 COL130_bit0 -COL134_bit_7 -COL134_bit_6 -COL134_bit_5 -COL134_bit_4 -COL134_bit_3 -COL134_bit_2 -COL134_bit_1 COL134_bit0 COL134_bit1 -COL134_bit2 -COL134_bit3 -COL134_bit4 COL134_bit5 -COL134_bit6 COL134_bit7 -COL134_bit8 COL134_bit9 COL134_bit10 -COL134_bit11 -COL134_bit12 COL134_bit13 -COL135_bit_7 -COL135_bit_6 -COL135_bit_5 -COL135_bit_4 -COL135_bit_3 -COL135_bit_2 -COL135_bit_1 COL135_bit0 -COL135_bit1 COL135_bit2 -COL135_bit3 -COL135_bit4 -COL135_bit5 -COL135_bit6 COL135_bit7 COL135_bit8 COL135_bit9 -COL135_bit10 -COL135_bit11 -COL135_bit12 COL135_bit13 -COL136_bit_7 -COL136_bit_6 -COL136_bit_5 -COL136_bit_4 -COL136_bit_3 -COL136_bit_2 COL136_bit_1 COL136_bit0 -COL136_bit1 COL136_bit2 COL136_bit3 COL136_bit4 COL136_bit5 COL136_bit6 -COL136_bit7 COL136_bit8 -COL136_bit9 -COL136_bit10 -COL136_bit11 -COL136_bit12 COL136_bit13 -COL115_bit_7 -COL115_bit_6 -COL115_bit_5 -COL115_bit_4 -COL115_bit_3 -COL115_bit_2 -COL115_bit_1 -COL115_bit0 -COL115_bit1 -COL115_bit2 -COL115_bit3 -COL115_bit4 -COL115_bit5 -COL115_bit6 -COL115_bit7 -COL115_bit8 -COL115_bit9 -COL115_bit10 -COL115_bit11 -COL115_bit12 -COL116_bit_7 -COL116_bit_6 -COL116_bit_5 -COL116_bit_4 -COL116_bit_3 -COL116_bit_2 -COL116_bit_1 -COL116_bit0 -COL116_bit1 COL116_bit2 -COL116_bit3 COL116_bit4 -COL116_bit5 COL116_bit6 -COL116_bit7 COL116_bit8 -COL116_bit9 -COL116_bit10 -COL116_bit11 -COL116_bit12 -COL117_bit_7 -COL117_bit_6 -COL117_bit_5 -COL117_bit_4 -COL117_bit_3 -COL117_bit_2 -COL117_bit_1 -COL117_bit0 -COL117_bit1 -COL117_bit2 COL117_bit3 -COL117_bit4 -COL117_bit5 COL117_bit6 COL117_bit7 -COL117_bit8 -COL117_bit9 -COL117_bit10 -COL117_bit11 -COL117_bit12 -COL118_bit_7 -COL118_bit_6 -COL118_bit_5 -COL118_bit_4 -COL118_bit_3 -COL118_bit_2 -COL118_bit_1 -COL118_bit0 COL118_bit1 -COL118_bit2 COL118_bit3 COL118_bit4 COL118_bit5 COL118_bit6 COL118_bit7 -COL118_bit8 -COL118_bit9 -COL118_bit10 -COL118_bit11 -COL118_bit12 -COL119_bit_7 -COL119_bit_6 -COL119_bit_5 -COL119_bit_4 -COL119_bit_3 -COL119_bit_2 -COL119_bit_1 -COL119_bit0 -COL119_bit1 -COL119_bit2 -COL119_bit3 -COL119_bit4 -COL119_bit5 -COL119_bit6 -COL119_bit7 -COL119_bit8 -COL119_bit9 -COL119_bit10 -COL119_bit11 -COL119_bit12 -COL120_bit_7 -COL120_bit_6 -COL120_bit_5 -COL120_bit_4 -COL120_bit_3 -COL120_bit_2 -COL120_bit_1 -COL120_bit0 -COL120_bit1 -COL120_bit2 -COL120_bit3 -COL120_bit4 -COL120_bit5 -COL120_bit6 -COL120_bit7 -COL120_bit8 -COL120_bit9 -COL120_bit10 -COL120_bit11 -COL120_bit12 -COL121_bit_7 -COL121_bit_6 -COL121_bit_5 -COL121_bit_4 -COL121_bit_3 -COL121_bit_2 -COL121_bit_1 -COL121_bit0 -COL121_bit1 -COL121_bit2 -COL121_bit3 -COL121_bit4 -COL121_bit5 -COL121_bit6 -COL121_bit7 -COL121_bit8 -COL121_bit9 -COL121_bit10 -COL121_bit11 -COL121_bit12 -COL122_bit_7 -COL122_bit_6 -COL122_bit_5 -COL122_bit_4 -COL122_bit_3 -COL122_bit_2 -COL122_bit_1 -COL122_bit0 -COL122_bit1 -COL122_bit2 -COL122_bit3 -COL122_bit4 -COL122_bit5 -COL122_bit6 -COL122_bit7 -COL122_bit8 -COL122_bit9 -COL122_bit10 -COL122_bit11 -COL122_bit12 -COL123_bit_7 -COL123_bit_6 -COL123_bit_5 -COL123_bit_4 -COL123_bit_3 -COL123_bit_2 -COL123_bit_1 -COL123_bit0 -COL123_bit1 -COL123_bit2 -COL123_bit3 -COL123_bit4 -COL123_bit5 -COL123_bit6 -COL123_bit7 -COL123_bit8 -COL123_bit9 -COL123_bit10 -COL123_bit11 -COL123_bit12 -COL124_bit_7 -COL124_bit_6 -COL124_bit_5 -COL124_bit_4 -COL124_bit_3 -COL124_bit_2 -COL124_bit_1 -COL124_bit0 -COL124_bit1 -COL124_bit2 -COL124_bit3 -COL124_bit4 -COL124_bit5 -COL124_bit6 -COL124_bit7 -COL124_bit8 -COL124_bit9 -COL124_bit10 -COL124_bit11 -COL124_bit12 -COL125_bit_7 -COL125_bit_6 -COL125_bit_5 -COL125_bit_4 -COL125_bit_3 -COL125_bit_2 -COL125_bit_1 -COL125_bit0 -COL125_bit1 -COL125_bit2 -COL125_bit3 -COL125_bit4 -COL125_bit5 -COL125_bit6 -COL125_bit7 -COL125_bit8 -COL125_bit9 -COL125_bit10 -COL125_bit11 -COL125_bit12 -COL126_bit_7 -COL126_bit_6 -COL126_bit_5 -COL126_bit_4 -COL126_bit_3 -COL126_bit_2 -COL126_bit_1 -COL126_bit0 -COL126_bit1 -COL126_bit2 -COL126_bit3 -COL126_bit4 -COL126_bit5 -COL126_bit6 -COL126_bit7 -COL126_bit8 -COL126_bit9 -COL126_bit10 -COL126_bit11 -COL126_bit12 -COL127_bit_7 -COL127_bit_6 -COL127_bit_5 -COL127_bit_4 -COL127_bit_3 -COL127_bit_2 -COL127_bit_1 -COL127_bit0 -COL127_bit1 -COL127_bit2 -COL127_bit3 -COL127_bit4 -COL127_bit5 -COL127_bit6 -COL127_bit7 -COL127_bit8 -COL127_bit9 -COL127_bit10 -COL127_bit11 -COL127_bit12 -COL128_bit_7 -COL128_bit_6 -COL128_bit_5 -COL128_bit_4 -COL128_bit_3 -COL128_bit_2 -COL128_bit_1 -COL128_bit0 COL128_bit1 COL128_bit2 COL128_bit3 -COL128_bit4 -COL128_bit5 -COL128_bit6 -COL128_bit7 COL128_bit8 -COL128_bit9 -COL128_bit10 -COL128_bit11 -COL128_bit12 -COL073_bit_7 -COL073_bit_6 -COL073_bit_5 -COL073_bit_4 -COL073_bit_3 -COL073_bit_2 -COL073_bit_1 -COL073_bit0 -COL073_bit1 -COL073_bit2 -COL073_bit3 -COL073_bit4 -COL073_bit5 -COL073_bit6 -COL073_bit7 -COL073_bit8 -COL073_bit9 -COL073_bit10 -COL073_bit11 -COL073_bit12 -COL074_bit_7 -COL074_bit_6 -COL074_bit_5 -COL074_bit_4 -COL074_bit_3 -COL074_bit_2 -COL074_bit_1 -COL074_bit0 -COL074_bit1 -COL074_bit2 -COL074_bit3 -COL074_bit4 -COL074_bit5 -COL074_bit6 -COL074_bit7 -COL074_bit8 -COL074_bit9 -COL074_bit10 -COL074_bit11 -COL074_bit12 -COL075_bit_7 -COL075_bit_6 -COL075_bit_5 -COL075_bit_4 -COL075_bit_3 -COL075_bit_2 -COL075_bit_1 -COL075_bit0 -COL075_bit1 -COL075_bit2 -COL075_bit3 -COL075_bit4 -COL075_bit5 -COL075_bit6 -COL075_bit7 -COL075_bit8 -COL075_bit9 -COL075_bit10 -COL075_bit11 -COL075_bit12 -COL076_bit_7 -COL076_bit_6 -COL076_bit_5 -COL076_bit_4 -COL076_bit_3 -COL076_bit_2 -COL076_bit_1 -COL076_bit0 -COL076_bit1 -COL076_bit2 -COL076_bit3 -COL076_bit4 -COL076_bit5 -COL076_bit6 -COL076_bit7 -COL076_bit8 -COL076_bit9 -COL076_bit10 -COL076_bit11 -COL076_bit12 -COL077_bit_7 -COL077_bit_6 -COL077_bit_5 -COL077_bit_4 -COL077_bit_3 -COL077_bit_2 -COL077_bit_1 -COL077_bit0 -COL077_bit1 -COL077_bit2 -COL077_bit3 -COL077_bit4 -COL077_bit5 -COL077_bit6 -COL077_bit7 -COL077_bit8 -COL077_bit9 -COL077_bit10 -COL077_bit11 -COL077_bit12 -COL078_bit_7 -COL078_bit_6 -COL078_bit_5 -COL078_bit_4 -COL078_bit_3 -COL078_bit_2 -COL078_bit_1 -COL078_bit0 -COL078_bit1 -COL078_bit2 -COL078_bit3 -COL078_bit4 -COL078_bit5 -COL078_bit6 -COL078_bit7 -COL078_bit8 -COL078_bit9 -COL078_bit10 -COL078_bit11 -COL078_bit12 -COL079_bit_7 -COL079_bit_6 -COL079_bit_5 -COL079_bit_4 -COL079_bit_3 -COL079_bit_2 -COL079_bit_1 -COL079_bit0 -COL079_bit1 COL079_bit2 COL079_bit3 -COL079_bit4 COL079_bit5 -COL079_bit6 -COL079_bit7 COL079_bit8 -COL079_bit9 -COL079_bit10 -COL079_bit11 -COL079_bit12 -COL085_bit_7 -COL085_bit_6 -COL085_bit_5 -COL085_bit_4 -COL085_bit_3 -COL085_bit_2 -COL085_bit_1 -COL085_bit0 -COL085_bit1 -COL085_bit2 -COL085_bit3 -COL085_bit4 -COL085_bit5 -COL085_bit6 -COL085_bit7 -COL085_bit8 -COL085_bit9 -COL085_bit10 -COL085_bit11 -COL085_bit12 -COL091_bit_7 -COL091_bit_6 -COL091_bit_5 -COL091_bit_4 -COL091_bit_3 -COL091_bit_2 -COL091_bit_1 -COL091_bit0 -COL091_bit1 -COL091_bit2 -COL091_bit3 -COL091_bit4 -COL091_bit5 -COL091_bit6 -COL091_bit7 -COL091_bit8 -COL091_bit9 -COL091_bit10 -COL091_bit11 -COL091_bit12 -COL097_bit_7 -COL097_bit_6 -COL097_bit_5 -COL097_bit_4 -COL097_bit_3 -COL097_bit_2 -COL097_bit_1 -COL097_bit0 -COL097_bit1 -COL097_bit2 -COL097_bit3 -COL097_bit4 -COL097_bit5 -COL097_bit6 -COL097_bit7 -COL097_bit8 -COL097_bit9 -COL097_bit10 -COL097_bit11 -COL097_bit12 -COL103_bit_7 -COL103_bit_6 -COL103_bit_5 -COL103_bit_4 -COL103_bit_3 -COL103_bit_2 -COL103_bit_1 -COL103_bit0 -COL103_bit1 -COL103_bit2 -COL103_bit3 -COL103_bit4 -COL103_bit5 -COL103_bit6 -COL103_bit7 -COL103_bit8 -COL103_bit9 -COL103_bit10 -COL103_bit11 -COL103_bit12 -COL109_bit_7 -COL109_bit_6 -COL109_bit_5 -COL109_bit_4 -COL109_bit_3 -COL109_bit_2 -COL109_bit_1 -COL109_bit0 -COL109_bit1 -COL109_bit2 -COL109_bit3 -COL109_bit4 -COL109_bit5 -COL109_bit6 -COL109_bit7 -COL109_bit8 -COL109_bit9 -COL109_bit10 -COL109_bit11 -COL109_bit12 -COL080_bit_7 -COL080_bit_6 -COL080_bit_5 -COL080_bit_4 -COL080_bit_3 -COL080_bit_2 -COL080_bit_1 -COL080_bit0 -COL080_bit1 -COL080_bit2 -COL080_bit3 -COL080_bit4 -COL080_bit5 -COL080_bit6 -COL080_bit7 -COL080_bit8 -COL080_bit9 -COL080_bit10 -COL080_bit11 -COL080_bit12 -COL081_bit_7 -COL081_bit_6 -COL081_bit_5 -COL081_bit_4 -COL081_bit_3 -COL081_bit_2 -COL081_bit_1 -COL081_bit0 -COL081_bit1 -COL081_bit2 -COL081_bit3 -COL081_bit4 -COL081_bit5 -COL081_bit6 -COL081_bit7 -COL081_bit8 -COL081_bit9 -COL081_bit10 -COL081_bit11 -COL081_bit12 -COL082_bit_7 -COL082_bit_6 -COL082_bit_5 -COL082_bit_4 -COL082_bit_3 -COL082_bit_2 -COL082_bit_1 -COL082_bit0 -COL082_bit1 -COL082_bit2 -COL082_bit3 -COL082_bit4 -COL082_bit5 -COL082_bit6 -COL082_bit7 -COL082_bit8 -COL082_bit9 -COL082_bit10 -COL082_bit11 -COL082_bit12 -COL083_bit_7 -COL083_bit_6 -COL083_bit_5 -COL083_bit_4 -COL083_bit_3 -COL083_bit_2 -COL083_bit_1 -COL083_bit0 -COL083_bit1 -COL083_bit2 -COL083_bit3 -COL083_bit4 -COL083_bit5 -COL083_bit6 -COL083_bit7 -COL083_bit8 -COL083_bit9 -COL083_bit10 -COL083_bit11 -COL083_bit12 -COL084_bit_7 -COL084_bit_6 -COL084_bit_5 -COL084_bit_4 -COL084_bit_3 -COL084_bit_2 -COL084_bit_1 -COL084_bit0 -COL084_bit1 -COL084_bit2 -COL084_bit3 -COL084_bit4 -COL084_bit5 -COL084_bit6 -COL084_bit7 -COL084_bit8 -COL084_bit9 -COL084_bit10 -COL084_bit11 -COL084_bit12 -COL086_bit_7 -COL086_bit_6 -COL086_bit_5 -COL086_bit_4 -COL086_bit_3 -COL086_bit_2 -COL086_bit_1 -COL086_bit0 -COL086_bit1 -COL086_bit2 -COL086_bit3 -COL086_bit4 -COL086_bit5 -COL086_bit6 -COL086_bit7 -COL086_bit8 -COL086_bit9 -COL086_bit10 -COL086_bit11 -COL086_bit12 -COL092_bit_7 -COL092_bit_6 -COL092_bit_5 -COL092_bit_4 -COL092_bit_3 -COL092_bit_2 -COL092_bit_1 -COL092_bit0 -COL092_bit1 -COL092_bit2 -COL092_bit3 -COL092_bit4 -COL092_bit5 -COL092_bit6 -COL092_bit7 -COL092_bit8 -COL092_bit9 -COL092_bit10 -COL092_bit11 -COL092_bit12 -COL098_bit_7 -COL098_bit_6 -COL098_bit_5 -COL098_bit_4 -COL098_bit_3 -COL098_bit_2 -COL098_bit_1 -COL098_bit0 -COL098_bit1 -COL098_bit2 -COL098_bit3 -COL098_bit4 -COL098_bit5 -COL098_bit6 -COL098_bit7 -COL098_bit8 -COL098_bit9 -COL098_bit10 -COL098_bit11 -COL098_bit12 -COL104_bit_7 -COL104_bit_6 -COL104_bit_5 -COL104_bit_4 -COL104_bit_3 -COL104_bit_2 -COL104_bit_1 -COL104_bit0 -COL104_bit1 -COL104_bit2 -COL104_bit3 -COL104_bit4 -COL104_bit5 -COL104_bit6 -COL104_bit7 -COL104_bit8 -COL104_bit9 -COL104_bit10 -COL104_bit11 -COL104_bit12 -COL110_bit_7 -COL110_bit_6 -COL110_bit_5 -COL110_bit_4 -COL110_bit_3 -COL110_bit_2 -COL110_bit_1 -COL110_bit0 -COL110_bit1 -COL110_bit2 -COL110_bit3 -COL110_bit4 -COL110_bit5 -COL110_bit6 -COL110_bit7 -COL110_bit8 -COL110_bit9 -COL110_bit10 -COL110_bit11 -COL110_bit12 -COL087_bit_7 -COL087_bit_6 -COL087_bit_5 -COL087_bit_4 -COL087_bit_3 -COL087_bit_2 -COL087_bit_1 -COL087_bit0 -COL087_bit1 -COL087_bit2 -COL087_bit3 -COL087_bit4 -COL087_bit5 -COL087_bit6 -COL087_bit7 -COL087_bit8 -COL087_bit9 -COL087_bit10 -COL087_bit11 -COL087_bit12 -COL088_bit_7 -COL088_bit_6 -COL088_bit_5 -COL088_bit_4 -COL088_bit_3 -COL088_bit_2 -COL088_bit_1 -COL088_bit0 -COL088_bit1 -COL088_bit2 -COL088_bit3 -COL088_bit4 -COL088_bit5 -COL088_bit6 -COL088_bit7 -COL088_bit8 -COL088_bit9 -COL088_bit10 -COL088_bit11 -COL088_bit12 -COL089_bit_7 -COL089_bit_6 -COL089_bit_5 -COL089_bit_4 -COL089_bit_3 -COL089_bit_2 -COL089_bit_1 -COL089_bit0 -COL089_bit1 -COL089_bit2 -COL089_bit3 -COL089_bit4 -COL089_bit5 -COL089_bit6 -COL089_bit7 -COL089_bit8 -COL089_bit9 -COL089_bit10 -COL089_bit11 -COL089_bit12 -COL090_bit_7 -COL090_bit_6 -COL090_bit_5 -COL090_bit_4 -COL090_bit_3 -COL090_bit_2 -COL090_bit_1 -COL090_bit0 -COL090_bit1 -COL090_bit2 -COL090_bit3 -COL090_bit4 -COL090_bit5 -COL090_bit6 -COL090_bit7 -COL090_bit8 -COL090_bit9 -COL090_bit10 -COL090_bit11 -COL090_bit12 -COL093_bit_7 -COL093_bit_6 -COL093_bit_5 -COL093_bit_4 -COL093_bit_3 -COL093_bit_2 -COL093_bit_1 -COL093_bit0 -COL093_bit1 -COL093_bit2 -COL093_bit3 -COL093_bit4 -COL093_bit5 -COL093_bit6 -COL093_bit7 -COL093_bit8 -COL093_bit9 -COL093_bit10 -COL093_bit11 -COL093_bit12 -COL099_bit_7 -COL099_bit_6 -COL099_bit_5 -COL099_bit_4 -COL099_bit_3 -COL099_bit_2 -COL099_bit_1 -COL099_bit0 -COL099_bit1 -COL099_bit2 -COL099_bit3 -COL099_bit4 -COL099_bit5 -COL099_bit6 -COL099_bit7 -COL099_bit8 -COL099_bit9 -COL099_bit10 -COL099_bit11 -COL099_bit12 -COL105_bit_7 -COL105_bit_6 -COL105_bit_5 -COL105_bit_4 -COL105_bit_3 -COL105_bit_2 -COL105_bit_1 -COL105_bit0 -COL105_bit1 -COL105_bit2 -COL105_bit3 -COL105_bit4 -COL105_bit5 -COL105_bit6 -COL105_bit7 -COL105_bit8 -COL105_bit9 -COL105_bit10 -COL105_bit11 -COL105_bit12 -COL111_bit_7 -COL111_bit_6 -COL111_bit_5 -COL111_bit_4 -COL111_bit_3 -COL111_bit_2 -COL111_bit_1 -COL111_bit0 -COL111_bit1 -COL111_bit2 -COL111_bit3 -COL111_bit4 -COL111_bit5 -COL111_bit6 -COL111_bit7 -COL111_bit8 -COL111_bit9 -COL111_bit10 -COL111_bit11 -COL111_bit12 -COL094_bit_7 -COL094_bit_6 -COL094_bit_5 -COL094_bit_4 -COL094_bit_3 -COL094_bit_2 -COL094_bit_1 -COL094_bit0 -COL094_bit1 -COL094_bit2 -COL094_bit3 -COL094_bit4 -COL094_bit5 -COL094_bit6 -COL094_bit7 -COL094_bit8 -COL094_bit9 -COL094_bit10 -COL094_bit11 -COL094_bit12 -COL095_bit_7 -COL095_bit_6 -COL095_bit_5 -COL095_bit_4 -COL095_bit_3 -COL095_bit_2 -COL095_bit_1 -COL095_bit0 -COL095_bit1 -COL095_bit2 -COL095_bit3 -COL095_bit4 -COL095_bit5 -COL095_bit6 -COL095_bit7 -COL095_bit8 -COL095_bit9 -COL095_bit10 -COL095_bit11 -COL095_bit12 -COL096_bit_7 -COL096_bit_6 -COL096_bit_5 -COL096_bit_4 -COL096_bit_3 -COL096_bit_2 -COL096_bit_1 -COL096_bit0 -COL096_bit1 -COL096_bit2 -COL096_bit3 -COL096_bit4 -COL096_bit5 -COL096_bit6 -COL096_bit7 -COL096_bit8 -COL096_bit9 -COL096_bit10 -COL096_bit11 -COL096_bit12 -COL100_bit_7 -COL100_bit_6 -COL100_bit_5 -COL100_bit_4 -COL100_bit_3 -COL100_bit_2 -COL100_bit_1 -COL100_bit0 -COL100_bit1 -COL100_bit2 -COL100_bit3 -COL100_bit4 -COL100_bit5 -COL100_bit6 -COL100_bit7 -COL100_bit8 -COL100_bit9 -COL100_bit10 -COL100_bit11 -COL100_bit12 -COL106_bit_7 -COL106_bit_6 -COL106_bit_5 -COL106_bit_4 -COL106_bit_3 -COL106_bit_2 -COL106_bit_1 -COL106_bit0 -COL106_bit1 -COL106_bit2 -COL106_bit3 -COL106_bit4 -COL106_bit5 -COL106_bit6 -COL106_bit7 -COL106_bit8 -COL106_bit9 -COL106_bit10 -COL106_bit11 -COL106_bit12 -COL112_bit_7 -COL112_bit_6 -COL112_bit_5 -COL112_bit_4 -COL112_bit_3 -COL112_bit_2 -COL112_bit_1 -COL112_bit0 -COL112_bit1 -COL112_bit2 -COL112_bit3 -COL112_bit4 -COL112_bit5 -COL112_bit6 -COL112_bit7 -COL112_bit8 -COL112_bit9 -COL112_bit10 -COL112_bit11 -COL112_bit12 -COL101_bit_7 -COL101_bit_6 -COL101_bit_5 -COL101_bit_4 -COL101_bit_3 -COL101_bit_2 -COL101_bit_1 -COL101_bit0 COL101_bit1 COL101_bit2 COL101_bit3 COL101_bit4 -COL101_bit5 -COL101_bit6 -COL101_bit7 -COL101_bit8 -COL101_bit9 -COL101_bit10 -COL101_bit11 -COL101_bit12 -COL102_bit_7 -COL102_bit_6 -COL102_bit_5 -COL102_bit_4 -COL102_bit_3 -COL102_bit_2 -COL102_bit_1 -COL102_bit0 -COL102_bit1 -COL102_bit2 -COL102_bit3 -COL102_bit4 -COL102_bit5 -COL102_bit6 -COL102_bit7 -COL102_bit8 -COL102_bit9 -COL102_bit10 -COL102_bit11 -COL102_bit12 -COL107_bit_7 -COL107_bit_6 -COL107_bit_5 -COL107_bit_4 -COL107_bit_3 -COL107_bit_2 -COL107_bit_1 -COL107_bit0 -COL107_bit1 -COL107_bit2 -COL107_bit3 -COL107_bit4 -COL107_bit5 -COL107_bit6 -COL107_bit7 -COL107_bit8 -COL107_bit9 -COL107_bit10 -COL107_bit11 -COL107_bit12 -COL113_bit_7 -COL113_bit_6 -COL113_bit_5 -COL113_bit_4 -COL113_bit_3 -COL113_bit_2 -COL113_bit_1 -COL113_bit0 COL113_bit1 -COL113_bit2 COL113_bit3 COL113_bit4 -COL113_bit5 COL113_bit6 -COL113_bit7 -COL113_bit8 -COL113_bit9 -COL113_bit10 -COL113_bit11 -COL113_bit12 -COL108_bit_7 -COL108_bit_6 -COL108_bit_5 -COL108_bit_4 -COL108_bit_3 -COL108_bit_2 -COL108_bit_1 -COL108_bit0 -COL108_bit1 -COL108_bit2 -COL108_bit3 -COL108_bit4 -COL108_bit5 -COL108_bit6 -COL108_bit7 -COL108_bit8 -COL108_bit9 -COL108_bit10 -COL108_bit11 -COL108_bit12 -COL114_bit_7 -COL114_bit_6 -COL114_bit_5 -COL114_bit_4 -COL114_bit_3 -COL114_bit_2 -COL114_bit_1 -COL114_bit0 -COL114_bit1 -COL114_bit2 -COL114_bit3 -COL114_bit4 -COL114_bit5 -COL114_bit6 -COL114_bit7 -COL114_bit8 -COL114_bit9 -COL114_bit10 -COL114_bit11 -COL114_bit12 -COL131_bit_7 -COL131_bit_6 -COL131_bit_5 -COL131_bit_4 -COL131_bit_3 -COL131_bit_2 -COL131_bit_1 -COL131_bit0 COL131_bit1 -COL131_bit2 -COL131_bit3 -COL131_bit4 -COL131_bit5 -COL131_bit6 -COL131_bit7 -COL131_bit8 -COL131_bit9 -COL131_bit10 -COL131_bit11 -COL131_bit12 COL131_bit13 -COL132_bit_7 -COL132_bit_6 -COL132_bit_5 -COL132_bit_4 -COL132_bit_3 -COL132_bit_2 -COL132_bit_1 -COL132_bit0 -COL132_bit1 -COL132_bit2 -COL132_bit3 -COL132_bit4 -COL132_bit5 -COL132_bit6 -COL132_bit7 -COL132_bit8 -COL132_bit9 -COL132_bit10 -COL132_bit11 -COL132_bit12 COL132_bit13
c _______________________________________________________________________________
c 
c restarts              : 85
c conflicts             : 136633         (176 /sec)
c decisions             : 243856         (314 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 776.142 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.74 0.92 0.90 2/54 13694
Raw data (stat): 13694 (runsolver) R 13693 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547085158 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.78 0.93 0.90 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 1912 0 0 0 993 5 0 0 25 0 1 0 547085158 9469952 1881 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1881 603 41 0 2271 0
vsize: 9248
[startup+20.0016 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 2139 0 0 0 1992 6 0 0 25 0 1 0 547085158 10665984 2108 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2604 2108 603 41 0 2563 0
vsize: 10416
[startup+30.001 s]
Raw data (loadavg): 0.84 0.93 0.90 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 2366 0 0 0 2990 7 0 0 25 0 1 0 547085158 11599872 2335 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2832 2335 603 41 0 2791 0
vsize: 11328
[startup+40.001 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 2597 0 0 0 3990 8 0 0 25 0 1 0 547085158 12558336 2566 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3066 2566 603 41 0 3025 0
vsize: 12264
[startup+50.0017 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 2912 0 0 0 4989 9 0 0 25 0 1 0 547085158 13889536 2881 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3391 2881 603 41 0 3350 0
vsize: 13564
[startup+60.0021 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3182 0 0 0 5988 10 0 0 25 0 1 0 547085158 14938112 3151 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 3151 603 41 0 3606 0
vsize: 14588
[startup+70.0034 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3199 0 0 0 6987 11 0 0 25 0 1 0 547085158 15073280 3168 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3680 3168 603 41 0 3639 0
vsize: 14720
[startup+80.0038 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3199 0 0 0 7987 11 0 0 25 0 1 0 547085158 15073280 3168 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3680 3168 603 41 0 3639 0
vsize: 14720
[startup+90.0042 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3389 0 0 0 8987 11 0 0 25 0 1 0 547085158 15867904 3358 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3358 603 41 0 3833 0
vsize: 15496
[startup+100.004 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3588 0 0 0 9987 12 0 0 25 0 1 0 547085158 16654336 3557 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4066 3557 603 41 0 4025 0
vsize: 16264
[startup+110.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3789 0 0 0 10987 12 0 0 25 0 1 0 547085158 17444864 3758 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4259 3758 603 41 0 4218 0
vsize: 17036
[startup+120.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 3990 0 0 0 11986 12 0 0 25 0 1 0 547085158 18255872 3959 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4457 3959 603 41 0 4416 0
vsize: 17828
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 4219 0 0 0 12986 13 0 0 25 0 1 0 547085158 19165184 4188 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4679 4188 603 41 0 4638 0
vsize: 18716
[startup+140.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 4510 0 0 0 13986 13 0 0 25 0 1 0 547085158 20471808 4479 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4998 4479 603 41 0 4957 0
vsize: 19992
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 4801 0 0 0 14985 14 0 0 25 0 1 0 547085158 21778432 4770 4294967295 134512640 134672761 3221224544 3221223648 134559802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5317 4770 603 41 0 5276 0
vsize: 21268
[startup+160.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 5078 0 0 0 15985 16 0 0 25 0 1 0 547085158 22827008 5047 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5573 5047 603 41 0 5532 0
vsize: 22292
[startup+170.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 5397 0 0 0 16983 17 0 0 25 0 1 0 547085158 24121344 5366 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5889 5366 603 41 0 5848 0
vsize: 23556
[startup+180.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 5720 0 0 0 17983 17 0 0 25 0 1 0 547085158 25542656 5689 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6236 5689 603 41 0 6195 0
vsize: 24944
[startup+190.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13694
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 5994 0 0 0 18982 18 0 0 25 0 1 0 547085158 26578944 5963 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6489 5963 603 41 0 6448 0
vsize: 25956
[startup+200.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 6224 0 0 0 19981 19 0 0 25 0 1 0 547085158 27500544 6193 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6714 6193 603 41 0 6673 0
vsize: 26856
[startup+210.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 6476 0 0 0 20981 20 0 0 25 0 1 0 547085158 28524544 6445 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6964 6445 603 41 0 6923 0
vsize: 27856
[startup+220.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 6713 0 0 0 21981 21 0 0 25 0 1 0 547085158 29564928 6682 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7218 6682 603 41 0 7177 0
vsize: 28872
[startup+230.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 6942 0 0 0 22980 21 0 0 25 0 1 0 547085158 30461952 6911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7437 6911 603 41 0 7396 0
vsize: 29748
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 7201 0 0 0 23979 22 0 0 25 0 1 0 547085158 31535104 7170 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7699 7170 603 41 0 7658 0
vsize: 30796
[startup+250.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 7425 0 0 0 24979 23 0 0 25 0 1 0 547085158 32460800 7394 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7925 7394 603 41 0 7884 0
vsize: 31700
[startup+260.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 7666 0 0 0 25978 24 0 0 25 0 1 0 547085158 33505280 7635 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8180 7635 603 41 0 8139 0
vsize: 32720
[startup+270.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 7896 0 0 0 26978 25 0 0 25 0 1 0 547085158 34422784 7865 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8404 7865 603 41 0 8363 0
vsize: 33616
[startup+280.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8170 0 0 0 27977 25 0 0 25 0 1 0 547085158 35487744 8139 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8664 8139 603 41 0 8623 0
vsize: 34656
[startup+290.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8300 0 0 0 28977 26 0 0 25 0 1 0 547085158 36012032 8269 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8792 8269 603 41 0 8751 0
vsize: 35168
[startup+300.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8306 0 0 0 29976 26 0 0 25 0 1 0 547085158 36167680 8275 4294967295 134512640 134672761 3221224544 3221223760 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8830 8275 603 41 0 8789 0
vsize: 35320
[startup+310.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8308 0 0 0 30975 27 0 0 25 0 1 0 547085158 36167680 8277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8830 8277 603 41 0 8789 0
vsize: 35320
[startup+320.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8309 0 0 0 31975 27 0 0 25 0 1 0 547085158 36167680 8278 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8830 8278 603 41 0 8789 0
vsize: 35320
[startup+330.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8309 0 0 0 32975 27 0 0 25 0 1 0 547085158 36167680 8278 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8830 8278 603 41 0 8789 0
vsize: 35320
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8312 0 0 0 33976 27 0 0 25 0 1 0 547085158 36167680 8281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8830 8281 603 41 0 8789 0
vsize: 35320
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8334 0 0 0 34976 27 0 0 25 0 1 0 547085158 36331520 8303 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8870 8303 603 41 0 8829 0
vsize: 35480
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8337 0 0 0 35976 27 0 0 25 0 1 0 547085158 36331520 8306 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8870 8306 603 41 0 8829 0
vsize: 35480
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8349 0 0 0 36976 27 0 0 25 0 1 0 547085158 36331520 8318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8870 8318 603 41 0 8829 0
vsize: 35480
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8360 0 0 0 37976 27 0 0 25 0 1 0 547085158 36331520 8329 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8870 8329 603 41 0 8829 0
vsize: 35480
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8374 0 0 0 38976 27 0 0 25 0 1 0 547085158 36528128 8343 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8343 603 41 0 8877 0
vsize: 35672
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8376 0 0 0 39977 27 0 0 25 0 1 0 547085158 36528128 8345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8345 603 41 0 8877 0
vsize: 35672
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8379 0 0 0 40977 27 0 0 25 0 1 0 547085158 36528128 8348 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8348 603 41 0 8877 0
vsize: 35672
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8381 0 0 0 41977 27 0 0 25 0 1 0 547085158 36528128 8350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8918 8350 603 41 0 8877 0
vsize: 35672
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8472 0 0 0 42977 27 0 0 25 0 1 0 547085158 36786176 8441 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8981 8441 603 41 0 8940 0
vsize: 35924
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8726 0 0 0 43977 27 0 0 25 0 1 0 547085158 37834752 8695 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9237 8695 603 41 0 9196 0
vsize: 36948
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 8953 0 0 0 44977 28 0 0 25 0 1 0 547085158 38866944 8922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9489 8922 603 41 0 9448 0
vsize: 37956
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 9209 0 0 0 45975 29 0 0 25 0 1 0 547085158 39895040 9178 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9740 9178 603 41 0 9699 0
vsize: 38960
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 9472 0 0 0 46975 30 0 0 25 0 1 0 547085158 40943616 9441 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9996 9441 603 41 0 9955 0
vsize: 39984
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 9665 0 0 0 47974 31 0 0 25 0 1 0 547085158 41725952 9634 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9634 603 41 0 10146 0
vsize: 40748
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 9903 0 0 0 48974 31 0 0 25 0 1 0 547085158 42762240 9872 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10440 9872 603 41 0 10399 0
vsize: 41760
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 10055 0 0 0 49974 32 0 0 25 0 1 0 547085158 43335680 10024 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10580 10024 603 41 0 10539 0
vsize: 42320
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 10247 0 0 0 50974 32 0 0 25 0 1 0 547085158 44187648 10216 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10788 10216 603 41 0 10747 0
vsize: 43152
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 10395 0 0 0 51974 32 0 0 25 0 1 0 547085158 44834816 10364 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10946 10364 603 41 0 10905 0
vsize: 43784
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 10614 0 0 0 52973 33 0 0 25 0 1 0 547085158 45666304 10583 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11149 10583 603 41 0 11108 0
vsize: 44596
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 10806 0 0 0 53973 33 0 0 25 0 1 0 547085158 46448640 10775 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11340 10775 603 41 0 11299 0
vsize: 45360
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 10950 0 0 0 54973 33 0 0 25 0 1 0 547085158 47144960 10919 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11510 10919 603 41 0 11469 0
vsize: 46040
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11112 0 0 0 55972 34 0 0 25 0 1 0 547085158 47792128 11081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11668 11081 603 41 0 11627 0
vsize: 46672
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11235 0 0 0 56972 34 0 0 25 0 1 0 547085158 48226304 11204 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11774 11204 603 41 0 11733 0
vsize: 47096
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11455 0 0 0 57972 35 0 0 25 0 1 0 547085158 49156096 11424 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12001 11424 603 41 0 11960 0
vsize: 48004
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11586 0 0 0 58972 36 0 0 25 0 1 0 547085158 49668096 11555 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11555 603 41 0 12085 0
vsize: 48504
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11586 0 0 0 59972 36 0 0 25 0 1 0 547085158 49668096 11555 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11555 603 41 0 12085 0
vsize: 48504
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11596 0 0 0 60972 36 0 0 25 0 1 0 547085158 49856512 11565 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11565 603 41 0 12131 0
vsize: 48688
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11597 0 0 0 61972 36 0 0 25 0 1 0 547085158 49856512 11566 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11566 603 41 0 12131 0
vsize: 48688
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11597 0 0 0 62972 36 0 0 25 0 1 0 547085158 49856512 11566 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11566 603 41 0 12131 0
vsize: 48688
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11598 0 0 0 63972 36 0 0 25 0 1 0 547085158 49856512 11567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11567 603 41 0 12131 0
vsize: 48688
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11598 0 0 0 64972 36 0 0 25 0 1 0 547085158 49856512 11567 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11567 603 41 0 12131 0
vsize: 48688
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11598 0 0 0 65972 36 0 0 25 0 1 0 547085158 49856512 11567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11567 603 41 0 12131 0
vsize: 48688
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11598 0 0 0 66972 36 0 0 25 0 1 0 547085158 49856512 11567 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11567 603 41 0 12131 0
vsize: 48688
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11613 0 0 0 67972 36 0 0 25 0 1 0 547085158 49856512 11582 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11582 603 41 0 12131 0
vsize: 48688
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11613 0 0 0 68973 36 0 0 25 0 1 0 547085158 49856512 11582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11582 603 41 0 12131 0
vsize: 48688
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11615 0 0 0 69973 36 0 0 25 0 1 0 547085158 49856512 11584 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11584 603 41 0 12131 0
vsize: 48688
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11617 0 0 0 70973 36 0 0 25 0 1 0 547085158 49856512 11586 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11586 603 41 0 12131 0
vsize: 48688
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11617 0 0 0 71973 36 0 0 25 0 1 0 547085158 49856512 11586 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11586 603 41 0 12131 0
vsize: 48688
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11618 0 0 0 72973 36 0 0 25 0 1 0 547085158 49856512 11587 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11587 603 41 0 12131 0
vsize: 48688
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11618 0 0 0 73973 36 0 0 25 0 1 0 547085158 49856512 11587 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11587 603 41 0 12131 0
vsize: 48688
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11618 0 0 0 74974 36 0 0 25 0 1 0 547085158 49856512 11587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11587 603 41 0 12131 0
vsize: 48688
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11618 0 0 0 75974 36 0 0 25 0 1 0 547085158 49856512 11587 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11587 603 41 0 12131 0
vsize: 48688
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11618 0 0 0 76974 36 0 0 25 0 1 0 547085158 49856512 11587 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11587 603 41 0 12131 0
vsize: 48688
[startup+776.456 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 13696
Raw data (stat): 13694 (minisat+) R 13693 28546 28545 0 -1 0 11618 0 0 0 76974 36 0 0 25 0 1 0 547085158 49856512 11587 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11587 603 41 0 12131 0
vsize: 0

Child status: 30
Real time (s): 776.455
CPU time (s): 776.539
CPU user time (s): 776.147
CPU system time (s): 0.39194
CPU usage (%): 100.011
Max. virtual memory (Kb): 48688
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1430464
#### END VERIFIER DATA ####