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 31082

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-25 22:00:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22491 boxname=wulflinc23 idbench=1307 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  4f7891bf040f9fa135208e1a9808a8bc  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-misc05.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-misc05.opb
IDLAUNCH: 22491
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        608612 kB
Buffers:         33492 kB
Cached:         370848 kB
SwapCached:        532 kB
Active:          24920 kB
Inactive:       381828 kB
HighTotal:      131008 kB
HighFree:         4340 kB
LowTotal:       903652 kB
LowFree:        604272 kB
SwapTotal:     2097136 kB
SwapFree:      2096016 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5628 kB
Slab:            13576 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:12:24 (client local time) WITH STATUS 30 IN 733.298 SECONDS
stats: 22491 0 733.298 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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         (193 /sec)
c decisions             : 270076         (369 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 732.799 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.84 0.96 0.92 2/54 20931
Raw data (stat): 20931 (runsolver) R 20930 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842313564 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0007 s]
Raw data (loadavg): 0.87 0.96 0.92 2/55 20935
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.96 0.92 2/55 20935
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0006 s]
Raw data (loadavg): 0.90 0.97 0.92 2/55 20935
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.97 0.92 2/55 20935
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 20935
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0011 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0014 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20937
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+733.208 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 20939
Raw data (stat): 20931 (minisat+_script) S 20930 5562 5561 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842313564 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 733.208
CPU time (s): 733.298
CPU user time (s): 732.809
CPU system time (s): 0.489925
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1430464
#### END VERIFIER DATA ####