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 19110

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 18:04:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16983 boxname=wulflinc18 idbench=1307 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4f7891bf040f9fa135208e1a9808a8bc  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-misc05.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-misc05.opb
IDLAUNCH: 16983
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        824252 kB
Buffers:         10220 kB
Cached:         177376 kB
SwapCached:        764 kB
Active:          61972 kB
Inactive:       127656 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        824000 kB
SwapTotal:     2097892 kB
SwapFree:      2096152 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15120 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:15:53 (client local time) WITH STATUS 30 IN 713.169 SECONDS
stats: 16983 0 713.169 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 |   48852   145668 |   16284       0        0     nan |  0.000 % |
c |       100 |   48473   144802 |   17912      87     1032    11.9 |  8.008 % |
c |       251 |   47837   142882 |   19703     230     6649    28.9 |  8.745 % |
c |       477 |   47804   142769 |   21674     445    26007    58.4 |  8.775 % |
c |       815 |   47804   142769 |   23841     783    42781    54.6 |  8.775 % |
c |      1321 |   47772   142680 |   26225    1286    66877    52.0 |  8.834 % |
c |      2080 |   47677   142376 |   28848    2030    80669    39.7 |  8.929 % |
c |      3222 |   47616   142192 |   31732    3087   108083    35.0 |  9.010 % |
c ==============================================================================
c [1mFound solution: 1470400[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 |      3488 |   47576   142078 |   15858    3335   113031    33.9 |  9.010 % |
c |      3591 |   46795   140275 |   17443    3425   115323    33.7 | 10.767 % |
c |      3742 |   46758   140146 |   19188    3551   119339    33.6 | 10.797 % |
c |      3970 |   46754   140137 |   21106    3777   132020    35.0 | 10.804 % |
c |      4308 |   46710   140025 |   23217    4111   145836    35.5 | 10.892 % |
c |      4815 |   46693   139987 |   25539    4617   164554    35.6 | 10.929 % |
c ==============================================================================
c [1mFound solution: 1458688[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 |      4858 |   46706   140017 |   15568    4660   166088    35.6 | 10.929 % |
c |      4959 |   46516   139580 |   17124    4757   167153    35.1 | 11.381 % |
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 |      5050 |   46530   139615 |   15510    4848   177143    36.5 | 11.381 % |
c |      5152 |   46502   139552 |   17061    4947   180533    36.5 | 11.448 % |
c |      5303 |   46229   138776 |   18767    5081   189065    37.2 | 11.890 % |
c |      5528 |   46229   138776 |   20643    5306   201209    37.9 | 11.890 % |
c |      5865 |   46229   138776 |   22708    5643   210452    37.3 | 11.890 % |
c |      6372 |   46196   138669 |   24979    6140   227294    37.0 | 11.927 % |
c ==============================================================================
c [1mFound solution: 1455040[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 |      6942 |   46160   138579 |   15386    6663   259144    38.9 | 11.927 % |
c |      7044 |   46160   138579 |   16924    6765   261439    38.6 | 12.016 % |
c |      7194 |   46115   138416 |   18617    6818   262748    38.5 | 12.053 % |
c |      7419 |   46086   138309 |   20478    7003   277196    39.6 | 12.075 % |
c |      7757 |   46029   138147 |   22526    7332   281611    38.4 | 12.149 % |
c |      8263 |   46003   138059 |   24779    7831   288770    36.9 | 12.171 % |
c |      9026 |   45977   138002 |   27257    8592   319033    37.1 | 12.222 % |
c |     10165 |   45968   137971 |   29982    9729   349309    35.9 | 12.230 % |
c ==============================================================================
c [1mFound solution: 1446784[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 |     10942 |   45918   137796 |   15306   10470   397748    38.0 | 12.230 % |
c |     11043 |   45890   137710 |   16836   10567   403950    38.2 | 12.341 % |
c |     11194 |   45881   137679 |   18520   10715   410467    38.3 | 12.348 % |
c |     11420 |   45852   137572 |   20372   10919   421384    38.6 | 12.370 % |
c |     11758 |   45843   137541 |   22409   11255   427376    38.0 | 12.378 % |
c |     12270 |   45684   137105 |   24650   11748   455268    38.8 | 12.635 % |
c ==============================================================================
c [1mFound solution: 1441472[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 |     12697 |   45686   137118 |   15228   12171   509452    41.9 | 12.635 % |
c |     12798 |   45686   137118 |   16750   12272   516863    42.1 | 12.658 % |
c |     12951 |   45671   137067 |   18425   12422   525957    42.3 | 12.673 % |
c |     13176 |   45671   137067 |   20268   12647   537122    42.5 | 12.673 % |
c |     13516 |   45671   137067 |   22295   12987   554389    42.7 | 12.673 % |
c |     14026 |   45558   136781 |   24524   13473   591617    43.9 | 12.937 % |
c |     14785 |   45545   136738 |   26977   14226   635502    44.7 | 12.952 % |
c |     15925 |   45530   136705 |   29675   15365   690407    44.9 | 12.981 % |
c ==============================================================================
c [1mFound solution: 1440384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17569 |   45528   136693 |   15176   17003   849380    50.0 | 12.981 % |
c |     17670 |   45488   136578 |   16693    8592   448924    52.2 | 13.050 % |
c |     17820 |   45098   135674 |   18362    8733   451605    51.7 | 13.969 % |
c |     18046 |   44637   134612 |   20199    8927   453832    50.8 | 15.005 % |
c |     18386 |   44637   134612 |   22219    9267   502383    54.2 | 15.005 % |
c |     18894 |   44610   134519 |   24441    9764   534712    54.8 | 15.027 % |
c ==============================================================================
c [1mFound solution: 1438208[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 |     19030 |   44611   134515 |   14870    9899   550805    55.6 | 15.027 % |
c |     19131 |   44611   134515 |   16357   10000   555167    55.5 | 15.035 % |
c |     19282 |   44611   134515 |   17992   10151   564804    55.6 | 15.035 % |
c |     19508 |   44593   134476 |   19791   10374   578005    55.7 | 15.072 % |
c |     19846 |   44584   134445 |   21771   10710   621262    58.0 | 15.079 % |
c |     20354 |   44576   134427 |   23948   11217   672228    59.9 | 15.094 % |
c |     21113 |   44576   134427 |   26343   11976   712430    59.5 | 15.094 % |
c ==============================================================================
c [1mFound solution: 1434304[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 |     22239 |   44588   134458 |   14862   13102   776357    59.3 | 15.094 % |
c |     22340 |   44588   134458 |   16348   13203   781276    59.2 | 15.093 % |
c |     22491 |   44588   134458 |   17983   13354   786424    58.9 | 15.093 % |
c |     22717 |   44579   134427 |   19781   13579   809699    59.6 | 15.101 % |
c |     23054 |   44579   134427 |   21759   13916   824214    59.2 | 15.101 % |
c |     23563 |   44441   133965 |   23935   14360   898500    62.6 | 15.233 % |
c |     24324 |   44441   133965 |   26328   15121   999624    66.1 | 15.233 % |
c |     25463 |   44413   133891 |   28961   16254  1136548    69.9 | 15.284 % |
c |     27171 |   44402   133867 |   31858   17961  1235245    68.8 | 15.306 % |
c |     29734 |   44247   133490 |   35043   20516  1574498    76.7 | 15.644 % |
c ==============================================================================
c [1mFound solution: 1433088[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 |     31403 |   44257   133518 |   14752   22185  1831642    82.6 | 15.644 % |
c |     31504 |   44257   133518 |   16227   11194   863873    77.2 | 15.643 % |
c |     31656 |   44257   133518 |   17849   11346   869893    76.7 | 15.643 % |
c |     31887 |   44257   133518 |   19634   11577   878494    75.9 | 15.643 % |
c |     32224 |   44242   133485 |   21598   11913   895491    75.2 | 15.672 % |
c |     32730 |   44242   133485 |   23758   12419   922137    74.3 | 15.672 % |
c ==============================================================================
c [1mFound solution: 1430464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33388 |   44252   133511 |   14750   13077   975217    74.6 | 15.672 % |
c |     33488 |   44252   133511 |   16225   13177   979563    74.3 | 15.672 % |
c |     33640 |   44252   133511 |   17847   13329   989384    74.2 | 15.672 % |
c |     33865 |   44244   133485 |   19632   13553  1020532    75.3 | 15.679 % |
c |     34202 |   44229   133451 |   21595   13888  1051046    75.7 | 15.716 % |
c |     34708 |   44229   133451 |   23755   14394  1069655    74.3 | 15.716 % |
c |     35469 |   44229   133451 |   26130   15155  1102706    72.8 | 15.716 % |
c |     36610 |   44220   133420 |   28743   16295  1262426    77.5 | 15.723 % |
c |     38318 |   44212   133394 |   31617   18002  1472027    81.8 | 15.730 % |
c |     40881 |   44212   133394 |   34779   20565  1934457    94.1 | 15.730 % |
c |     44725 |   44204   133376 |   38257   24408  2577841   105.6 | 15.745 % |
c |     50491 |   44102   133110 |   42083   30162  3370113   111.7 | 15.936 % |
c |     59141 |   43677   132136 |   46291   38801  4147664   106.9 | 16.867 % |
c |     72118 |   43641   132012 |   50921   23997  2736454   114.0 | 16.896 % |
c |     91580 |   43632   131981 |   56013   43457  5676244   130.6 | 16.904 % |
c |    120774 |   43598   131882 |   61614   38799  4358121   112.3 | 16.962 % |
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              : 89
c conflicts             : 141412         (198 /sec)
c decisions             : 270076         (379 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 712.718 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.66 0.88 0.88 2/55 4188
Raw data (stat): 4188 (runsolver) R 4187 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547085951 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.99955 s]
Raw data (loadavg): 0.71 0.88 0.88 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 1898 0 0 0 994 4 0 0 25 0 1 0 547085951 9490432 1865 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2317 1865 603 41 0 2276 0
vsize: 9268
[startup+20.0008 s]
Raw data (loadavg): 0.76 0.89 0.88 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 2255 0 0 0 1993 5 0 0 25 0 1 0 547085951 10964992 2222 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2677 2222 603 41 0 2636 0
vsize: 10708
[startup+30.0018 s]
Raw data (loadavg): 0.79 0.89 0.88 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 2521 0 0 0 2992 7 0 0 25 0 1 0 547085951 12075008 2488 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2948 2488 603 41 0 2907 0
vsize: 11792
[startup+40.0023 s]
Raw data (loadavg): 0.83 0.89 0.89 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 2587 0 0 0 3991 8 0 0 25 0 1 0 547085951 12541952 2554 4294967295 134512640 134672761 3221224624 3221223792 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3062 2554 603 41 0 3021 0
vsize: 12248
[startup+50.0036 s]
Raw data (loadavg): 0.85 0.90 0.89 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 2745 0 0 0 4990 8 0 0 25 0 1 0 547085951 13189120 2712 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3220 2712 603 41 0 3179 0
vsize: 12880
[startup+60.0036 s]
Raw data (loadavg): 0.87 0.90 0.89 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 3040 0 0 0 5989 10 0 0 25 0 1 0 547085951 14503936 3007 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3541 3007 603 41 0 3500 0
vsize: 14164
[startup+70.004 s]
Raw data (loadavg): 0.89 0.90 0.89 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 3391 0 0 0 6988 11 0 0 25 0 1 0 547085951 15945728 3358 4294967295 134512640 134672761 3221224624 3221223808 134558943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3893 3358 603 41 0 3852 0
vsize: 15572
[startup+80.0045 s]
Raw data (loadavg): 0.91 0.90 0.89 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 3692 0 0 0 7987 12 0 0 25 0 1 0 547085951 17113088 3659 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3659 603 41 0 4137 0
vsize: 16712
[startup+90.0079 s]
Raw data (loadavg): 0.92 0.91 0.89 2/55 4188
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 3692 0 0 0 8987 12 0 0 25 0 1 0 547085951 17113088 3659 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3659 603 41 0 4137 0
vsize: 16712
[startup+100.008 s]
Raw data (loadavg): 0.93 0.91 0.89 2/55 4190
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 3692 0 0 0 9986 13 0 0 25 0 1 0 547085951 17113088 3659 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4178 3659 603 41 0 4137 0
vsize: 16712
[startup+110.008 s]
Raw data (loadavg): 0.94 0.91 0.89 2/55 4190
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 3774 0 0 0 10986 13 0 0 25 0 1 0 547085951 17375232 3741 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4242 3741 603 41 0 4201 0
vsize: 16968
[startup+120.009 s]
Raw data (loadavg): 0.95 0.91 0.89 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 4096 0 0 0 11985 15 0 0 25 0 1 0 547085951 18804736 4063 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4591 4063 603 41 0 4550 0
vsize: 18364
[startup+130.009 s]
Raw data (loadavg): 0.96 0.92 0.89 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 4424 0 0 0 12983 16 0 0 25 0 1 0 547085951 20107264 4391 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4909 4391 603 41 0 4868 0
vsize: 19636
[startup+140.01 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 4756 0 0 0 13982 18 0 0 25 0 1 0 547085951 21417984 4723 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5229 4723 603 41 0 5188 0
vsize: 20916
[startup+150.011 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 5112 0 0 0 14981 20 0 0 25 0 1 0 547085951 22859776 5079 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 5079 603 41 0 5540 0
vsize: 22324
[startup+160.01 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 5301 0 0 0 15980 20 0 0 25 0 1 0 547085951 23646208 5268 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5773 5268 603 41 0 5732 0
vsize: 23092
[startup+170.011 s]
Raw data (loadavg): 0.98 0.92 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 5491 0 0 0 16979 21 0 0 25 0 1 0 547085951 24453120 5458 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5970 5458 603 41 0 5929 0
vsize: 23880
[startup+180.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 5687 0 0 0 17978 22 0 0 25 0 1 0 547085951 25399296 5654 4294967295 134512640 134672761 3221224624 3221223808 134558658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6201 5654 603 41 0 6160 0
vsize: 24804
[startup+190.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 5937 0 0 0 18977 23 0 0 25 0 1 0 547085951 26472448 5904 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6463 5904 603 41 0 6422 0
vsize: 25852
[startup+200.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 6233 0 0 0 19976 24 0 0 25 0 1 0 547085951 27652096 6200 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6751 6200 603 41 0 6710 0
vsize: 27004
[startup+210.012 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 6530 0 0 0 20976 25 0 0 25 0 1 0 547085951 28864512 6497 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7047 6497 603 41 0 7006 0
vsize: 28188
[startup+220.013 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 6776 0 0 0 21975 26 0 0 25 0 1 0 547085951 29900800 6743 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6743 603 41 0 7259 0
vsize: 29200
[startup+230.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 7114 0 0 0 22974 27 0 0 25 0 1 0 547085951 31211520 7081 4294967295 134512640 134672761 3221224624 3221223808 134558754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7620 7081 603 41 0 7579 0
vsize: 30480
[startup+240.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 7401 0 0 0 23973 28 0 0 25 0 1 0 547085951 32391168 7368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7908 7368 603 41 0 7867 0
vsize: 31632
[startup+250.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 7663 0 0 0 24972 29 0 0 25 0 1 0 547085951 33566720 7630 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8195 7630 603 41 0 8154 0
vsize: 32780
[startup+260.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 7948 0 0 0 25972 30 0 0 25 0 1 0 547085951 34729984 7915 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8479 7915 603 41 0 8438 0
vsize: 33916
[startup+270.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8205 0 0 0 26971 31 0 0 25 0 1 0 547085951 35774464 8172 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8734 8172 603 41 0 8693 0
vsize: 34936
[startup+280.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8366 0 0 0 27970 32 0 0 25 0 1 0 547085951 36421632 8333 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8892 8333 603 41 0 8851 0
vsize: 35568
[startup+290.018 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8370 0 0 0 28970 32 0 0 25 0 1 0 547085951 36421632 8337 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8892 8337 603 41 0 8851 0
vsize: 35568
[startup+300.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8376 0 0 0 29970 32 0 0 25 0 1 0 547085951 36569088 8343 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8343 603 41 0 8887 0
vsize: 35712
[startup+310.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8376 0 0 0 30970 32 0 0 25 0 1 0 547085951 36569088 8343 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8343 603 41 0 8887 0
vsize: 35712
[startup+320.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8376 0 0 0 31970 32 0 0 25 0 1 0 547085951 36569088 8343 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8343 603 41 0 8887 0
vsize: 35712
[startup+330.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8376 0 0 0 32969 33 0 0 25 0 1 0 547085951 36569088 8343 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8343 603 41 0 8887 0
vsize: 35712
[startup+340.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8385 0 0 0 33969 33 0 0 25 0 1 0 547085951 36569088 8352 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8352 603 41 0 8887 0
vsize: 35712
[startup+350.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8387 0 0 0 34969 33 0 0 25 0 1 0 547085951 36569088 8354 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8354 603 41 0 8887 0
vsize: 35712
[startup+360.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8397 0 0 0 35969 33 0 0 25 0 1 0 547085951 36569088 8364 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8364 603 41 0 8887 0
vsize: 35712
[startup+370.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8411 0 0 0 36969 34 0 0 25 0 1 0 547085951 36732928 8378 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8968 8378 603 41 0 8927 0
vsize: 35872
[startup+380.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8411 0 0 0 37969 34 0 0 25 0 1 0 547085951 36732928 8378 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8968 8378 603 41 0 8927 0
vsize: 35872
[startup+390.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4192
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8412 0 0 0 38969 34 0 0 25 0 1 0 547085951 36732928 8379 4294967295 134512640 134672761 3221224624 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8968 8379 603 41 0 8927 0
vsize: 35872
[startup+400.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8426 0 0 0 39968 35 0 0 25 0 1 0 547085951 36732928 8393 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8968 8393 603 41 0 8927 0
vsize: 35872
[startup+410.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8436 0 0 0 40968 35 0 0 25 0 1 0 547085951 36732928 8403 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8968 8403 603 41 0 8927 0
vsize: 35872
[startup+420.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8693 0 0 0 41968 36 0 0 25 0 1 0 547085951 37892096 8660 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9251 8660 603 41 0 9210 0
vsize: 37004
[startup+430.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 8936 0 0 0 42967 36 0 0 25 0 1 0 547085951 38817792 8903 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9477 8903 603 41 0 9436 0
vsize: 37908
[startup+440.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 9194 0 0 0 43967 37 0 0 25 0 1 0 547085951 39878656 9161 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9736 9161 603 41 0 9695 0
vsize: 38944
[startup+450.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 9459 0 0 0 44967 37 0 0 25 0 1 0 547085951 40931328 9426 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9993 9426 603 41 0 9952 0
vsize: 39972
[startup+460.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 9689 0 0 0 45966 38 0 0 25 0 1 0 547085951 41963520 9656 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10245 9656 603 41 0 10204 0
vsize: 40980
[startup+470.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 9925 0 0 0 46966 39 0 0 25 0 1 0 547085951 42864640 9892 4294967295 134512640 134672761 3221224624 3221223808 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10465 9893 603 41 0 10424 0
vsize: 41860
[startup+480.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10153 0 0 0 47965 40 0 0 25 0 1 0 547085951 43790336 10120 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10691 10120 603 41 0 10650 0
vsize: 42764
[startup+490.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10397 0 0 0 48964 40 0 0 25 0 1 0 547085951 44818432 10364 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10942 10364 603 41 0 10901 0
vsize: 43768
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10597 0 0 0 49964 41 0 0 25 0 1 0 547085951 45588480 10564 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11130 10564 603 41 0 11089 0
vsize: 44520
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10718 0 0 0 50964 41 0 0 25 0 1 0 547085951 46125056 10685 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11261 10685 603 41 0 11220 0
vsize: 45044
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10718 0 0 0 51964 41 0 0 25 0 1 0 547085951 46125056 10685 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11261 10685 603 41 0 11220 0
vsize: 45044
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10718 0 0 0 52964 41 0 0 25 0 1 0 547085951 46125056 10685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11261 10685 603 41 0 11220 0
vsize: 45044
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10718 0 0 0 53964 41 0 0 25 0 1 0 547085951 46125056 10685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11261 10685 603 41 0 11220 0
vsize: 45044
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10719 0 0 0 54964 41 0 0 25 0 1 0 547085951 46125056 10686 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11261 10686 603 41 0 11220 0
vsize: 45044
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10729 0 0 0 55964 42 0 0 25 0 1 0 547085951 46313472 10696 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10696 603 41 0 11266 0
vsize: 45228
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10730 0 0 0 56965 42 0 0 25 0 1 0 547085951 46313472 10697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10697 603 41 0 11266 0
vsize: 45228
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10730 0 0 0 57965 42 0 0 25 0 1 0 547085951 46313472 10697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10697 603 41 0 11266 0
vsize: 45228
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10731 0 0 0 58964 42 0 0 25 0 1 0 547085951 46313472 10698 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11307 10698 603 41 0 11266 0
vsize: 45228
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10742 0 0 0 59964 42 0 0 25 0 1 0 547085951 46313472 10709 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10709 603 41 0 11266 0
vsize: 45228
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10745 0 0 0 60964 42 0 0 25 0 1 0 547085951 46313472 10712 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10712 603 41 0 11266 0
vsize: 45228
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10746 0 0 0 61964 42 0 0 25 0 1 0 547085951 46313472 10713 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10713 603 41 0 11266 0
vsize: 45228
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10746 0 0 0 62965 42 0 0 25 0 1 0 547085951 46313472 10713 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10713 603 41 0 11266 0
vsize: 45228
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10746 0 0 0 63965 42 0 0 25 0 1 0 547085951 46313472 10713 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10713 603 41 0 11266 0
vsize: 45228
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 64965 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 65965 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 66965 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 67965 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4194
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 68966 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4196
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 69966 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4196
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 70966 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 45228
[startup+713.115 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4196
Raw data (stat): 4188 (minisat+) R 4187 20024 20023 0 -1 0 10749 0 0 0 70966 42 0 0 25 0 1 0 547085951 46313472 10716 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11307 10716 603 41 0 11266 0
vsize: 0

Child status: 30
Real time (s): 713.114
CPU time (s): 713.169
CPU user time (s): 712.722
CPU system time (s): 0.446932
CPU usage (%): 100.008
Max. virtual memory (Kb): 45228
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1430464
#### END VERIFIER DATA ####