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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-egout.opb
MD5SUM9f6abccf92594d7ee18b1409c45097d3
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 471047168
Optimality of the best value was proved YES
Number of terms in the objective function 1615
Biggest coefficient in the objective function 545997717504
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 15186728411329
Number of bits of the sum of numbers in the objective function 44
Biggest number in a constraint 545997717504
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 15186728411329
Number of bits of the biggest sum of numbers44
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark1118.41
Number of variables1705
Total number of constraints153
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)55
Number of constraints which are nor clauses,nor cardinality constraints98
Minimum length of a constraint1
Maximum length of a constraint420

Trace number 3846

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-19 03:05:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2851 boxname=wulflinc26 idbench=507 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9f6abccf92594d7ee18b1409c45097d3  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-egout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-egout.opb
IDLAUNCH: 2851
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890384 kB
Buffers:         37936 kB
Cached:          78020 kB
SwapCached:        868 kB
Active:          69384 kB
Inactive:        49244 kB
HighTotal:      131008 kB
HighFree:        50232 kB
LowTotal:       903652 kB
LowFree:        840152 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            20164 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:24:19 (client local time) WITH STATUS 30 IN 1118.41 SECONDS
stats: 2851 0 1118.41 30

Solver Data

c Parsing PB file...
c Converting 115 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 113]---> Adder-cost: 339   maxlim: 107520   bits: 18/17
c ---[ 111]---> BDD-cost:   55
c ---[ 109]---> BDD-cost:   34
c ---[ 107]---> BDD-cost:   60
c ---[ 105]---> BDD-cost:  110
c ---[ 101]---> BDD-cost:   48
c ---[  99]---> BDD-cost:  127
c ---[  97]---> BDD-cost:   43
c ---[  91]---> BDD-cost:   70
c ---[  89]---> BDD-cost:   49
c ---[  85]---> BDD-cost:  155
c ---[  83]---> BDD-cost:   49
c ---[  81]---> BDD-cost:  139
c ---[  79]---> BDD-cost:   58
c ---[  75]---> BDD-cost:   60
c ---[  73]---> BDD-cost:   37
c ---[  71]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> BDD-cost:   70
c ---[  67]---> Sorter-cost:  363     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:  145
c ---[  59]---> BDD-cost:   60
c ---[  57]---> BDD-cost:   49
c ---[  55]---> BDD-cost:   49
c ---[  53]---> BDD-cost:   60
c ---[  49]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   12
c ---[  42]---> BDD-cost:   12
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   16
c ---[  27]---> BDD-cost:   31
c ---[  26]---> BDD-cost:   31
c ---[  25]---> BDD-cost:   31
c ---[  24]---> BDD-cost:   31
c ---[  23]---> BDD-cost:   31
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   31
c ---[  17]---> BDD-cost:   31
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   31
c ---[  13]---> BDD-cost:   31
c ---[  12]---> BDD-cost:   31
c ---[   9]---> BDD-cost:   31
c ---[   8]---> BDD-cost:   31
c ---[   7]---> BDD-cost:   31
c ---[   6]---> BDD-cost:   31
c ---[   4]---> BDD-cost:   31
c ---[   3]---> BDD-cost:   31
c ---[   2]---> BDD-cost:   31
c ---[   1]---> BDD-cost:   31
c ---[   0]---> BDD-cost:   31
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11092    29500 |    3697       0        0     nan |  0.000 % |
c |       100 |   10818    28827 |    4066      63      280     4.4 | 27.106 % |
c |       250 |   10461    28046 |    4473     152      576     3.8 | 29.335 % |
c |       475 |   10435    27992 |    4920     367     2302     6.3 | 29.543 % |
c ==============================================================================
c Found solution: 790136183
c ---[   0]---> Sorter-cost:116869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       551 |  342702   803652 |  114234     434     2916     6.7 | 29.543 % |
c |       651 |  342649   803542 |  125657     517     3370     6.5 |  1.374 % |
c |       801 |  342492   803212 |  138223     614     4825     7.9 |  1.429 % |
c |      1026 |  342462   803152 |  152045     824     6926     8.4 |  1.442 % |
c |      1365 |  342462   803152 |  167249    1163    10178     8.8 |  1.442 % |
c |      1871 |  342448   803121 |  183974    1667    14953     9.0 |  1.445 % |
c ==============================================================================
c Found solution: 787836070
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2031 |  343541   806548 |  114513    1821    20102    11.0 |  1.445 % |
c |      2131 |  342381   803940 |  125964    1912    21570    11.3 |  1.712 % |
c ==============================================================================
c Found solution: 641849380
c ---[   0]---> Sorter-cost:54320     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2200 |  491103  1151289 |  163701    1978    22839    11.5 |  1.712 % |
c |      2300 |  491051  1151173 |  180071    2076    23686    11.4 |  1.239 % |
c |      2450 |  485688  1139024 |  198078    2186    25750    11.8 |  2.142 % |
c |      2675 |  484954  1137363 |  217886    2402    33244    13.8 |  2.268 % |
c |      3013 |  479071  1123907 |  239674    2728    63648    23.3 |  3.322 % |
c |      3519 |  479036  1123826 |  263642    3233    70618    21.8 |  3.330 % |
c |      4278 |  477156  1119563 |  290006    3971    97970    24.7 |  3.632 % |
c |      5417 |  476951  1119096 |  319006    5103   229500    45.0 |  3.670 % |
c |      7125 |  475968  1116840 |  350907    6802   281414    41.4 |  3.841 % |
c ==============================================================================
c Found solution: 641510112
c ---[   0]---> Sorter-cost:57305     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7236 |  635245  1488680 |  211748    6913   282937    40.9 |  3.841 % |
c |      7337 |  635245  1488680 |  232922    7014   296309    42.2 |  3.021 % |
c |      7488 |  635176  1488526 |  256215    7160   304834    42.6 |  3.034 % |
c |      7713 |  635176  1488526 |  281836    7385   311292    42.2 |  3.034 % |
c |      8050 |  634959  1488029 |  310020    7721   317236    41.1 |  3.064 % |
c |      8558 |  634959  1488029 |  341022    8229   326912    39.7 |  3.064 % |
c |      9317 |  634959  1488029 |  375124    8988   385949    42.9 |  3.064 % |
c ==============================================================================
c Found solution: 631308145
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9517 |  634993  1488681 |  211664    9188   397359    43.2 |  3.064 % |
c |      9617 |  634993  1488681 |  232830    9288   398829    42.9 |  3.064 % |
c |      9767 |  634993  1488681 |  256113    9438   399924    42.4 |  3.064 % |
c |      9992 |  634993  1488681 |  281724    9663   402008    41.6 |  3.064 % |
c |     10329 |  634993  1488681 |  309897   10000   405040    40.5 |  3.064 % |
c |     10835 |  634976  1488644 |  340886   10505   408311    38.9 |  3.067 % |
c |     11594 |  634976  1488644 |  374975   11264   440595    39.1 |  3.067 % |
c ==============================================================================
c Found solution: 629990536
c ---[   0]---> Sorter-cost:   22     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12067 |  635197  1489236 |  211732   11733   462718    39.4 |  3.067 % |
c ==============================================================================
c Found solution: 629989990
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12068 |  635217  1489286 |  211739   11734   462725    39.4 |  3.067 % |
c ==============================================================================
c Found solution: 629987824
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12071 |  635242  1489346 |  211747   11737   463826    39.5 |  3.067 % |
c |     12171 |  634779  1488310 |  232921   11816   466306    39.5 |  3.149 % |
c |     12321 |  634711  1488158 |  256213   11965   467610    39.1 |  3.157 % |
c ==============================================================================
c Found solution: 625743872
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12524 |  635128  1489179 |  211709   12166   476578    39.2 |  3.157 % |
c |     12626 |  634997  1488887 |  232879   12267   477513    38.9 |  3.172 % |
c |     12776 |  634932  1488741 |  256167   12415   479453    38.6 |  3.181 % |
c |     13003 |  634932  1488741 |  281784   12642   481401    38.1 |  3.181 % |
c ==============================================================================
c Found solution: 527555584
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13127 |  634757  1488439 |  211585   12765   482939    37.8 |  3.181 % |
c |     13227 |  634757  1488439 |  232743   12865   489477    38.0 |  3.217 % |
c ==============================================================================
c Found solution: 519630848
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13261 |  634750  1488429 |  211583   12897   489902    38.0 |  3.217 % |
c |     13361 |  634750  1488429 |  232741   12997   493944    38.0 |  3.221 % |
c |     13513 |  634746  1488420 |  256015   13146   495485    37.7 |  3.222 % |
c |     13738 |  634619  1488130 |  281616   13369   526009    39.3 |  3.237 % |
c ==============================================================================
c Found solution: 516612560
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13936 |  634646  1488191 |  211548   13567   537238    39.6 |  3.237 % |
c |     14039 |  634646  1488191 |  232702   13670   543759    39.8 |  3.237 % |
c |     14189 |  634646  1488191 |  255973   13820   555383    40.2 |  3.237 % |
c |     14419 |  634469  1487800 |  281570   14042   560233    39.9 |  3.263 % |
c |     14756 |  634469  1487800 |  309727   14379   581027    40.4 |  3.263 % |
c |     15263 |  634399  1487640 |  340700   14881   597600    40.2 |  3.273 % |
c |     16022 |  634210  1487217 |  374770   15639   649030    41.5 |  3.296 % |
c |     17162 |  632880  1484200 |  412247   16715   728206    43.6 |  3.473 % |
c ==============================================================================
c Found solution: 515807136
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17646 |  632902  1484251 |  210967   17199   796539    46.3 |  3.473 % |
c |     17748 |  632902  1484251 |  232063   17301   805371    46.6 |  3.473 % |
c |     17898 |  632902  1484251 |  255270   17451   808224    46.3 |  3.473 % |
c |     18123 |  632902  1484251 |  280797   17676   820943    46.4 |  3.473 % |
c ==============================================================================
c Found solution: 515620864
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18234 |  632917  1484284 |  210972   17787   827395    46.5 |  3.473 % |
c |     18336 |  632917  1484284 |  232069   17889   829065    46.3 |  3.473 % |
c |     18487 |  632917  1484284 |  255276   18040   832126    46.1 |  3.474 % |
c |     18712 |  632917  1484284 |  280803   18265   835541    45.7 |  3.473 % |
c |     19049 |  632917  1484284 |  308884   18602   843674    45.4 |  3.474 % |
c |     19555 |  632831  1484093 |  339772   18339   866385    47.2 |  3.486 % |
c ==============================================================================
c Found solution: 512361472
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19977 |  632764  1483950 |  210921   18757   880688    47.0 |  3.486 % |
c |     20078 |  632743  1483903 |  232013   18852   882296    46.8 |  3.504 % |
c |     20229 |  632743  1483903 |  255214   19003   886606    46.7 |  3.504 % |
c |     20454 |  632743  1483903 |  280735   19228   896523    46.6 |  3.504 % |
c |     20791 |  632462  1483267 |  308809   19558   915667    46.8 |  3.539 % |
c |     21300 |  632462  1483267 |  339690   20067   967402    48.2 |  3.539 % |
c ==============================================================================
c Found solution: 494220288
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21941 |  632461  1483270 |  210820   20703  1008230    48.7 |  3.539 % |
c |     22041 |  632461  1483270 |  231902   20803  1020378    49.0 |  3.543 % |
c ==============================================================================
c Found solution: 493697024
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22104 |  632479  1483316 |  210826   20866  1021877    49.0 |  3.543 % |
c |     22204 |  632479  1483316 |  231908   20966  1024945    48.9 |  3.544 % |
c |     22355 |  632479  1483316 |  255099   21117  1034835    49.0 |  3.544 % |
c |     22580 |  632479  1483316 |  280609   21342  1041324    48.8 |  3.544 % |
c |     22918 |  632479  1483316 |  308670   21680  1055245    48.7 |  3.544 % |
c |     23424 |  632479  1483316 |  339537   22186  1098345    49.5 |  3.544 % |
c |     24186 |  632479  1483316 |  373491   22948  1155521    50.4 |  3.544 % |
c ==============================================================================
c Found solution: 493501312
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24928 |  632501  1483368 |  210833   23690  1189701    50.2 |  3.544 % |
c |     25028 |  632501  1483368 |  231916   23790  1196652    50.3 |  3.544 % |
c |     25180 |  632501  1483368 |  255107   23942  1205144    50.3 |  3.544 % |
c |     25407 |  632501  1483368 |  280618   24169  1211295    50.1 |  3.544 % |
c |     25745 |  632501  1483368 |  308680   24507  1240119    50.6 |  3.544 % |
c ==============================================================================
c Found solution: 489304064
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26109 |  632517  1483405 |  210839   24871  1267828    51.0 |  3.544 % |
c |     26209 |  632517  1483405 |  231922   24971  1276605    51.1 |  3.544 % |
c |     26359 |  632517  1483405 |  255115   25121  1282518    51.1 |  3.544 % |
c |     26586 |  632517  1483405 |  280626   25348  1292110    51.0 |  3.544 % |
c |     26923 |  632517  1483405 |  308689   25685  1303287    50.7 |  3.544 % |
c |     27430 |  632517  1483405 |  339558   26192  1325978    50.6 |  3.544 % |
c ==============================================================================
c Found solution: 488373248
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27516 |  632532  1483441 |  210844   26278  1329979    50.6 |  3.544 % |
c |     27616 |  632532  1483441 |  231928   26378  1334243    50.6 |  3.545 % |
c |     27766 |  632381  1483099 |  255121   26527  1347432    50.8 |  3.563 % |
c |     27991 |  632381  1483099 |  280633   26752  1359555    50.8 |  3.563 % |
c ==============================================================================
c Found solution: 482404352
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28296 |  632403  1483154 |  210801   27057  1382197    51.1 |  3.563 % |
c |     28396 |  632403  1483154 |  231881   27157  1384666    51.0 |  3.563 % |
c ==============================================================================
c Found solution: 480050176
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28404 |  632412  1483180 |  210804   27165  1384862    51.0 |  3.563 % |
c |     28507 |  632412  1483180 |  231884   27268  1387112    50.9 |  3.563 % |
c |     28658 |  632412  1483180 |  255072   27419  1390731    50.7 |  3.563 % |
c ==============================================================================
c Found solution: 474212352
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28663 |  632424  1483207 |  210808   27424  1390964    50.7 |  3.563 % |
c |     28763 |  632424  1483207 |  231888   27524  1393092    50.6 |  3.563 % |
c |     28913 |  632424  1483207 |  255077   27674  1397868    50.5 |  3.563 % |
c |     29138 |  632424  1483207 |  280585   27899  1402701    50.3 |  3.563 % |
c |     29475 |  632424  1483207 |  308643   28236  1410024    49.9 |  3.563 % |
c |     29981 |  632424  1483207 |  339508   28742  1424166    49.5 |  3.563 % |
c |     30740 |  632424  1483207 |  373459   29501  1443029    48.9 |  3.563 % |
c ==============================================================================
c Found solution: 473361408
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31450 |  632442  1483249 |  210814   30211  1472693    48.7 |  3.563 % |
c |     31552 |  632442  1483249 |  231895   30313  1475203    48.7 |  3.564 % |
c ==============================================================================
c Found solution: 471047168
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31617 |  632454  1483278 |  210818   30378  1477273    48.6 |  3.564 % |
c |     31720 |  632454  1483278 |  231899   30481  1482311    48.6 |  3.564 % |
c |     31870 |  632454  1483278 |  255089   30631  1487267    48.6 |  3.564 % |
c |     32097 |  632454  1483278 |  280598   30858  1495234    48.5 |  3.564 % |
c |     32435 |  632454  1483278 |  308658   31196  1507843    48.3 |  3.564 % |
c |     32942 |  632454  1483278 |  339524   31703  1527516    48.2 |  3.564 % |
c |     33701 |  632454  1483278 |  373476   32462  1558062    48.0 |  3.564 % |
c |     34841 |  632454  1483278 |  410824   33602  1594606    47.5 |  3.564 % |
c ==============================================================================
c Optimal solution: 471047168
s OPTIMUM FOUND
v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 I_0x2e_008_0x2e__0x2e__0x2e__bit0 -I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 I_0x2e_016_0x2e__0x2e__0x2e__bit0 -I_0x2e_016017_bit0 -I_0x2e_017018_bit0 -I_0x2e_009018_bit0 -I_0x2e_018019_bit0 I_0x2e_019024_bit0 -I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 -I_0x2e_027_0x2e__0x2e__0x2e__bit0 I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 -I_0x2e_036037_bit0 -I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_10 -F_0x2e_001_0x2e__0x2e__0x2e__bit_9 -F_0x2e_001_0x2e__0x2e__0x2e__bit_8 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001_0x2e__0x2e__0x2e__bit13 -F_0x2e_001_0x2e__0x2e__0x2e__bit14 -F_0x2e_001_0x2e__0x2e__0x2e__bit15 -F_0x2e_001_0x2e__0x2e__0x2e__bit16 -F_0x2e_001_0x2e__0x2e__0x2e__bit17 -F_0x2e_001_0x2e__0x2e__0x2e__bit18 -F_0x2e_001_0x2e__0x2e__0x2e__bit19 -F_0x2e_001003_bit_10 -F_0x2e_001003_bit_9 -F_0x2e_001003_bit_8 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_001003_bit13 -F_0x2e_001003_bit14 -F_0x2e_001003_bit15 -F_0x2e_001003_bit16 -F_0x2e_001003_bit17 -F_0x2e_001003_bit18 -F_0x2e_001003_bit19 -F_0x2e_002003_bit_10 -F_0x2e_002003_bit_9 -F_0x2e_002003_bit_8 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002003_bit13 -F_0x2e_002003_bit14 -F_0x2e_002003_bit15 -F_0x2e_002003_bit16 -F_0x2e_002003_bit17 -F_0x2e_002003_bit18 -F_0x2e_002003_bit19 -F_0x2e_002_0x2e__0x2e__0x2e__bit_10 -F_0x2e_002_0x2e__0x2e__0x2e__bit_9 -F_0x2e_002_0x2e__0x2e__0x2e__bit_8 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit13 -F_0x2e_002_0x2e__0x2e__0x2e__bit14 -F_0x2e_002_0x2e__0x2e__0x2e__bit15 -F_0x2e_002_0x2e__0x2e__0x2e__bit16 -F_0x2e_002_0x2e__0x2e__0x2e__bit17 -F_0x2e_002_0x2e__0x2e__0x2e__bit18 -F_0x2e_002_0x2e__0x2e__0x2e__bit19 -F_0x2e_003005_bit_10 -F_0x2e_003005_bit_9 -F_0x2e_003005_bit_8 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_003005_bit13 -F_0x2e_003005_bit14 -F_0x2e_003005_bit15 -F_0x2e_003005_bit16 -F_0x2e_003005_bit17 -F_0x2e_003005_bit18 -F_0x2e_003005_bit19 -F_0x2e_004005_bit_10 -F_0x2e_004005_bit_9 -F_0x2e_004005_bit_8 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004005_bit13 -F_0x2e_004005_bit14 -F_0x2e_004005_bit15 -F_0x2e_004005_bit16 -F_0x2e_004005_bit17 -F_0x2e_004005_bit18 -F_0x2e_004005_bit19 -F_0x2e_004_0x2e__0x2e__0x2e__bit_10 -F_0x2e_004_0x2e__0x2e__0x2e__bit_9 -F_0x2e_004_0x2e__0x2e__0x2e__bit_8 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit13 -F_0x2e_004_0x2e__0x2e__0x2e__bit14 -F_0x2e_004_0x2e__0x2e__0x2e__bit15 -F_0x2e_004_0x2e__0x2e__0x2e__bit16 -F_0x2e_004_0x2e__0x2e__0x2e__bit17 -F_0x2e_004_0x2e__0x2e__0x2e__bit18 -F_0x2e_004_0x2e__0x2e__0x2e__bit19 -F_0x2e_005007_bit_10 -F_0x2e_005007_bit_9 -F_0x2e_005007_bit_8 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_005007_bit13 -F_0x2e_005007_bit14 -F_0x2e_005007_bit15 -F_0x2e_005007_bit16 -F_0x2e_005007_bit17 -F_0x2e_005007_bit18 -F_0x2e_005007_bit19 -F_0x2e_006007_bit_10 -F_0x2e_006007_bit_9 -F_0x2e_006007_bit_8 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_006007_bit13 -F_0x2e_006007_bit14 -F_0x2e_006007_bit15 -F_0x2e_006007_bit16 -F_0x2e_006007_bit17 -F_0x2e_006007_bit18 -F_0x2e_006007_bit19 -F_0x2e_007008_bit_10 -F_0x2e_007008_bit_9 -F_0x2e_007008_bit_8 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_007008_bit13 -F_0x2e_007008_bit14 -F_0x2e_007008_bit15 -F_0x2e_007008_bit16 -F_0x2e_007008_bit17 -F_0x2e_007008_bit18 -F_0x2e_007008_bit19 -F_0x2e_008_0x2e__0x2e__0x2e__bit_10 -F_0x2e_008_0x2e__0x2e__0x2e__bit_9 -F_0x2e_008_0x2e__0x2e__0x2e__bit_8 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 F_0x2e_008_0x2e__0x2e__0x2e__bit2 F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit13 -F_0x2e_008_0x2e__0x2e__0x2e__bit14 -F_0x2e_008_0x2e__0x2e__0x2e__bit15 -F_0x2e_008_0x2e__0x2e__0x2e__bit16 -F_0x2e_008_0x2e__0x2e__0x2e__bit17 -F_0x2e_008_0x2e__0x2e__0x2e__bit18 -F_0x2e_008_0x2e__0x2e__0x2e__bit19 -F_0x2e_008009_bit_10 -F_0x2e_008009_bit_9 -F_0x2e_008009_bit_8 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 -F_0x2e_008009_bit2 -F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_008009_bit13 -F_0x2e_008009_bit14 -F_0x2e_008009_bit15 -F_0x2e_008009_bit16 -F_0x2e_008009_bit17 -F_0x2e_008009_bit18 -F_0x2e_008009_bit19 -F_0x2e_010012_bit_10 -F_0x2e_010012_bit_9 -F_0x2e_010012_bit_8 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_010012_bit13 -F_0x2e_010012_bit14 -F_0x2e_010012_bit15 -F_0x2e_010012_bit16 -F_0x2e_010012_bit17 -F_0x2e_010012_bit18 -F_0x2e_010012_bit19 -F_0x2e_012_0x2e__0x2e__0x2e__bit_10 -F_0x2e_012_0x2e__0x2e__0x2e__bit_9 -F_0x2e_012_0x2e__0x2e__0x2e__bit_8 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit13 -F_0x2e_012_0x2e__0x2e__0x2e__bit14 -F_0x2e_012_0x2e__0x2e__0x2e__bit15 -F_0x2e_012_0x2e__0x2e__0x2e__bit16 -F_0x2e_012_0x2e__0x2e__0x2e__bit17 -F_0x2e_012_0x2e__0x2e__0x2e__bit18 -F_0x2e_012_0x2e__0x2e__0x2e__bit19 -F_0x2e_012013_bit_10 -F_0x2e_012013_bit_9 -F_0x2e_012013_bit_8 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_012013_bit13 -F_0x2e_012013_bit14 -F_0x2e_012013_bit15 -F_0x2e_012013_bit16 -F_0x2e_012013_bit17 -F_0x2e_012013_bit18 -F_0x2e_012013_bit19 -F_0x2e_013016_bit_10 -F_0x2e_013016_bit_9 -F_0x2e_013016_bit_8 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_013016_bit13 -F_0x2e_013016_bit14 -F_0x2e_013016_bit15 -F_0x2e_013016_bit16 -F_0x2e_013016_bit17 -F_0x2e_013016_bit18 -F_0x2e_013016_bit19 -F_0x2e_014015_bit_10 -F_0x2e_014015_bit_9 -F_0x2e_014015_bit_8 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_014015_bit13 -F_0x2e_014015_bit14 -F_0x2e_014015_bit15 -F_0x2e_014015_bit16 -F_0x2e_014015_bit17 -F_0x2e_014015_bit18 -F_0x2e_014015_bit19 -F_0x2e_015016_bit_10 -F_0x2e_015016_bit_9 -F_0x2e_015016_bit_8 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_015016_bit13 -F_0x2e_015016_bit14 -F_0x2e_015016_bit15 -F_0x2e_015016_bit16 -F_0x2e_015016_bit17 -F_0x2e_015016_bit18 -F_0x2e_015016_bit19 -F_0x2e_016_0x2e__0x2e__0x2e__bit_10 -F_0x2e_016_0x2e__0x2e__0x2e__bit_9 -F_0x2e_016_0x2e__0x2e__0x2e__bit_8 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 F_0x2e_016_0x2e__0x2e__0x2e__bit0 F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 F_0x2e_016_0x2e__0x2e__0x2e__bit3 F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit13 -F_0x2e_016_0x2e__0x2e__0x2e__bit14 -F_0x2e_016_0x2e__0x2e__0x2e__bit15 -F_0x2e_016_0x2e__0x2e__0x2e__bit16 -F_0x2e_016_0x2e__0x2e__0x2e__bit17 -F_0x2e_016_0x2e__0x2e__0x2e__bit18 -F_0x2e_016_0x2e__0x2e__0x2e__bit19 -F_0x2e_016017_bit_10 -F_0x2e_016017_bit_9 -F_0x2e_016017_bit_8 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 -F_0x2e_016017_bit0 -F_0x2e_016017_bit1 -F_0x2e_016017_bit2 -F_0x2e_016017_bit3 -F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_016017_bit13 -F_0x2e_016017_bit14 -F_0x2e_016017_bit15 -F_0x2e_016017_bit16 -F_0x2e_016017_bit17 -F_0x2e_016017_bit18 -F_0x2e_016017_bit19 -F_0x2e_017018_bit_10 -F_0x2e_017018_bit_9 -F_0x2e_017018_bit_8 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 -F_0x2e_017018_bit0 -F_0x2e_017018_bit1 -F_0x2e_017018_bit2 -F_0x2e_017018_bit3 -F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_017018_bit13 -F_0x2e_017018_bit14 -F_0x2e_017018_bit15 -F_0x2e_017018_bit16 -F_0x2e_017018_bit17 -F_0x2e_017018_bit18 -F_0x2e_017018_bit19 -F_0x2e_009018_bit_10 -F_0x2e_009018_bit_9 -F_0x2e_009018_bit_8 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 -F_0x2e_009018_bit2 -F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_009018_bit13 -F_0x2e_009018_bit14 -F_0x2e_009018_bit15 -F_0x2e_009018_bit16 -F_0x2e_009018_bit17 -F_0x2e_009018_bit18 -F_0x2e_009018_bit19 -F_0x2e_018019_bit_10 -F_0x2e_018019_bit_9 -F_0x2e_018019_bit_8 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 -F_0x2e_018019_bit0 -F_0x2e_018019_bit1 -F_0x2e_018019_bit2 -F_0x2e_018019_bit3 -F_0x2e_018019_bit4 -F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_018019_bit13 -F_0x2e_018019_bit14 -F_0x2e_018019_bit15 -F_0x2e_018019_bit16 -F_0x2e_018019_bit17 -F_0x2e_018019_bit18 -F_0x2e_018019_bit19 -F_0x2e_019024_bit_10 -F_0x2e_019024_bit_9 -F_0x2e_019024_bit_8 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 -F_0x2e_019024_bit0 F_0x2e_019024_bit1 -F_0x2e_019024_bit2 -F_0x2e_019024_bit3 -F_0x2e_019024_bit4 -F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_019024_bit13 -F_0x2e_019024_bit14 -F_0x2e_019024_bit15 -F_0x2e_019024_bit16 -F_0x2e_019024_bit17 -F_0x2e_019024_bit18 -F_0x2e_019024_bit19 -F_0x2e_024_0x2e__0x2e__0x2e__bit_10 -F_0x2e_024_0x2e__0x2e__0x2e__bit_9 -F_0x2e_024_0x2e__0x2e__0x2e__bit_8 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 -F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 -F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 -F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit13 -F_0x2e_024_0x2e__0x2e__0x2e__bit14 -F_0x2e_024_0x2e__0x2e__0x2e__bit15 -F_0x2e_024_0x2e__0x2e__0x2e__bit16 -F_0x2e_024_0x2e__0x2e__0x2e__bit17 -F_0x2e_024_0x2e__0x2e__0x2e__bit18 -F_0x2e_024_0x2e__0x2e__0x2e__bit19 -F_0x2e_023024_bit_10 -F_0x2e_023024_bit_9 -F_0x2e_023024_bit_8 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_023024_bit13 -F_0x2e_023024_bit14 -F_0x2e_023024_bit15 -F_0x2e_023024_bit16 -F_0x2e_023024_bit17 -F_0x2e_023024_bit18 -F_0x2e_023024_bit19 -F_0x2e_022023_bit_10 -F_0x2e_022023_bit_9 -F_0x2e_022023_bit_8 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_022023_bit13 -F_0x2e_022023_bit14 -F_0x2e_022023_bit15 -F_0x2e_022023_bit16 -F_0x2e_022023_bit17 -F_0x2e_022023_bit18 -F_0x2e_022023_bit19 -F_0x2e_020022_bit_10 -F_0x2e_020022_bit_9 -F_0x2e_020022_bit_8 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_020022_bit13 -F_0x2e_020022_bit14 -F_0x2e_020022_bit15 -F_0x2e_020022_bit16 -F_0x2e_020022_bit17 -F_0x2e_020022_bit18 -F_0x2e_020022_bit19 -F_0x2e_021022_bit_10 -F_0x2e_021022_bit_9 -F_0x2e_021022_bit_8 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_021022_bit13 -F_0x2e_021022_bit14 -F_0x2e_021022_bit15 -F_0x2e_021022_bit16 -F_0x2e_021022_bit17 -F_0x2e_021022_bit18 -F_0x2e_021022_bit19 -F_0x2e_022_0x2e__0x2e__0x2e__bit_10 -F_0x2e_022_0x2e__0x2e__0x2e__bit_9 -F_0x2e_022_0x2e__0x2e__0x2e__bit_8 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit13 -F_0x2e_022_0x2e__0x2e__0x2e__bit14 -F_0x2e_022_0x2e__0x2e__0x2e__bit15 -F_0x2e_022_0x2e__0x2e__0x2e__bit16 -F_0x2e_022_0x2e__0x2e__0x2e__bit17 -F_0x2e_022_0x2e__0x2e__0x2e__bit18 -F_0x2e_022_0x2e__0x2e__0x2e__bit19 -F_0x2e_024026_bit_10 -F_0x2e_024026_bit_9 -F_0x2e_024026_bit_8 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 F_0x2e_024026_bit1 -F_0x2e_024026_bit2 -F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_024026_bit13 -F_0x2e_024026_bit14 -F_0x2e_024026_bit15 -F_0x2e_024026_bit16 -F_0x2e_024026_bit17 -F_0x2e_024026_bit18 -F_0x2e_024026_bit19 -F_0x2e_025026_bit_10 -F_0x2e_025026_bit_9 -F_0x2e_025026_bit_8 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025026_bit13 -F_0x2e_025026_bit14 -F_0x2e_025026_bit15 -F_0x2e_025026_bit16 -F_0x2e_025026_bit17 -F_0x2e_025026_bit18 -F_0x2e_025026_bit19 -F_0x2e_025_0x2e__0x2e__0x2e__bit_10 -F_0x2e_025_0x2e__0x2e__0x2e__bit_9 -F_0x2e_025_0x2e__0x2e__0x2e__bit_8 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit13 -F_0x2e_025_0x2e__0x2e__0x2e__bit14 -F_0x2e_025_0x2e__0x2e__0x2e__bit15 -F_0x2e_025_0x2e__0x2e__0x2e__bit16 -F_0x2e_025_0x2e__0x2e__0x2e__bit17 -F_0x2e_025_0x2e__0x2e__0x2e__bit18 -F_0x2e_025_0x2e__0x2e__0x2e__bit19 -F_0x2e_026027_bit_10 -F_0x2e_026027_bit_9 -F_0x2e_026027_bit_8 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 F_0x2e_026027_bit1 F_0x2e_026027_bit2 F_0x2e_026027_bit3 F_0x2e_026027_bit4 -F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_026027_bit13 -F_0x2e_026027_bit14 -F_0x2e_026027_bit15 -F_0x2e_026027_bit16 -F_0x2e_026027_bit17 -F_0x2e_026027_bit18 -F_0x2e_026027_bit19 -F_0x2e_027_0x2e__0x2e__0x2e__bit_10 -F_0x2e_027_0x2e__0x2e__0x2e__bit_9 -F_0x2e_027_0x2e__0x2e__0x2e__bit_8 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 -F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 -F_0x2e_027_0x2e__0x2e__0x2e__bit_1 -F_0x2e_027_0x2e__0x2e__0x2e__bit0 -F_0x2e_027_0x2e__0x2e__0x2e__bit1 -F_0x2e_027_0x2e__0x2e__0x2e__bit2 -F_0x2e_027_0x2e__0x2e__0x2e__bit3 -F_0x2e_027_0x2e__0x2e__0x2e__bit4 -F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit13 -F_0x2e_027_0x2e__0x2e__0x2e__bit14 -F_0x2e_027_0x2e__0x2e__0x2e__bit15 -F_0x2e_027_0x2e__0x2e__0x2e__bit16 -F_0x2e_027_0x2e__0x2e__0x2e__bit17 -F_0x2e_027_0x2e__0x2e__0x2e__bit18 -F_0x2e_027_0x2e__0x2e__0x2e__bit19 -F_0x2e_027032_bit_10 -F_0x2e_027032_bit_9 -F_0x2e_027032_bit_8 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 -F_0x2e_027032_bit_5 -F_0x2e_027032_bit_4 -F_0x2e_027032_bit_3 -F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 F_0x2e_027032_bit0 F_0x2e_027032_bit1 F_0x2e_027032_bit2 F_0x2e_027032_bit3 F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_027032_bit13 -F_0x2e_027032_bit14 -F_0x2e_027032_bit15 -F_0x2e_027032_bit16 -F_0x2e_027032_bit17 -F_0x2e_027032_bit18 -F_0x2e_027032_bit19 -F_0x2e_030031_bit_10 -F_0x2e_030031_bit_9 -F_0x2e_030031_bit_8 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_030031_bit13 -F_0x2e_030031_bit14 -F_0x2e_030031_bit15 -F_0x2e_030031_bit16 -F_0x2e_030031_bit17 -F_0x2e_030031_bit18 -F_0x2e_030031_bit19 -F_0x2e_031032_bit_10 -F_0x2e_031032_bit_9 -F_0x2e_031032_bit_8 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_031032_bit13 -F_0x2e_031032_bit14 -F_0x2e_031032_bit15 -F_0x2e_031032_bit16 -F_0x2e_031032_bit17 -F_0x2e_031032_bit18 -F_0x2e_031032_bit19 -F_0x2e_029031_bit_10 -F_0x2e_029031_bit_9 -F_0x2e_029031_bit_8 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_029031_bit13 -F_0x2e_029031_bit14 -F_0x2e_029031_bit15 -F_0x2e_029031_bit16 -F_0x2e_029031_bit17 -F_0x2e_029031_bit18 -F_0x2e_029031_bit19 -F_0x2e_028029_bit_10 -F_0x2e_028029_bit_9 -F_0x2e_028029_bit_8 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028029_bit13 -F_0x2e_028029_bit14 -F_0x2e_028029_bit15 -F_0x2e_028029_bit16 -F_0x2e_028029_bit17 -F_0x2e_028029_bit18 -F_0x2e_028029_bit19 -F_0x2e_028_0x2e__0x2e__0x2e__bit_10 -F_0x2e_028_0x2e__0x2e__0x2e__bit_9 -F_0x2e_028_0x2e__0x2e__0x2e__bit_8 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit13 -F_0x2e_028_0x2e__0x2e__0x2e__bit14 -F_0x2e_028_0x2e__0x2e__0x2e__bit15 -F_0x2e_028_0x2e__0x2e__0x2e__bit16 -F_0x2e_028_0x2e__0x2e__0x2e__bit17 -F_0x2e_028_0x2e__0x2e__0x2e__bit18 -F_0x2e_028_0x2e__0x2e__0x2e__bit19 -F_0x2e_032033_bit_10 -F_0x2e_032033_bit_9 -F_0x2e_032033_bit_8 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 -F_0x2e_032033_bit_5 -F_0x2e_032033_bit_4 -F_0x2e_032033_bit_3 -F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 -F_0x2e_032033_bit0 -F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_032033_bit13 -F_0x2e_032033_bit14 -F_0x2e_032033_bit15 -F_0x2e_032033_bit16 -F_0x2e_032033_bit17 -F_0x2e_032033_bit18 -F_0x2e_032033_bit19 -F_0x2e_033037_bit_10 -F_0x2e_033037_bit_9 -F_0x2e_033037_bit_8 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 -F_0x2e_033037_bit_5 -F_0x2e_033037_bit_4 -F_0x2e_033037_bit_3 -F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 -F_0x2e_033037_bit0 -F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_033037_bit13 -F_0x2e_033037_bit14 -F_0x2e_033037_bit15 -F_0x2e_033037_bit16 -F_0x2e_033037_bit17 -F_0x2e_033037_bit18 -F_0x2e_033037_bit19 -F_0x2e_034036_bit_10 -F_0x2e_034036_bit_9 -F_0x2e_034036_bit_8 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_034036_bit13 -F_0x2e_034036_bit14 -F_0x2e_034036_bit15 -F_0x2e_034036_bit16 -F_0x2e_034036_bit17 -F_0x2e_034036_bit18 -F_0x2e_034036_bit19 -F_0x2e_035036_bit_10 -F_0x2e_035036_bit_9 -F_0x2e_035036_bit_8 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_035036_bit13 -F_0x2e_035036_bit14 -F_0x2e_035036_bit15 -F_0x2e_035036_bit16 -F_0x2e_035036_bit17 -F_0x2e_035036_bit18 -F_0x2e_035036_bit19 -F_0x2e_037038_bit_10 -F_0x2e_037038_bit_9 -F_0x2e_037038_bit_8 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 -F_0x2e_037038_bit_5 -F_0x2e_037038_bit_4 -F_0x2e_037038_bit_3 -F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 -F_0x2e_037038_bit0 -F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_037038_bit13 -F_0x2e_037038_bit14 -F_0x2e_037038_bit15 -F_0x2e_037038_bit16 -F_0x2e_037038_bit17 -F_0x2e_037038_bit18 -F_0x2e_037038_bit19 -F_0x2e_039040_bit_10 -F_0x2e_039040_bit_9 -F_0x2e_039040_bit_8 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_039040_bit13 -F_0x2e_039040_bit14 -F_0x2e_039040_bit15 -F_0x2e_039040_bit16 -F_0x2e_039040_bit17 -F_0x2e_039040_bit18 -F_0x2e_039040_bit19 -F_0x2e_040_0x2e__0x2e__0x2e__bit_10 -F_0x2e_040_0x2e__0x2e__0x2e__bit_9 -F_0x2e_040_0x2e__0x2e__0x2e__bit_8 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit13 -F_0x2e_040_0x2e__0x2e__0x2e__bit14 -F_0x2e_040_0x2e__0x2e__0x2e__bit15 -F_0x2e_040_0x2e__0x2e__0x2e__bit16 -F_0x2e_040_0x2e__0x2e__0x2e__bit17 -F_0x2e_040_0x2e__0x2e__0x2e__bit18 -F_0x2e_040_0x2e__0x2e__0x2e__bit19 -F_0x2e_041_0x2e__0x2e__0x2e__bit_10 -F_0x2e_041_0x2e__0x2e__0x2e__bit_9 -F_0x2e_041_0x2e__0x2e__0x2e__bit_8 -F_0x2e_041_0x2e__0x2e__0x2e__bit_7 -F_0x2e_041_0x2e__0x2e__0x2e__bit_6 -F_0x2e_041_0x2e__0x2e__0x2e__bit_5 -F_0x2e_041_0x2e__0x2e__0x2e__bit_4 -F_0x2e_041_0x2e__0x2e__0x2e__bit_3 -F_0x2e_041_0x2e__0x2e__0x2e__bit_2 -F_0x2e_041_0x2e__0x2e__0x2e__bit_1 -F_0x2e_041_0x2e__0x2e__0x2e__bit0 -F_0x2e_041_0x2e__0x2e__0x2e__bit1 -F_0x2e_041_0x2e__0x2e__0x2e__bit2 -F_0x2e_041_0x2e__0x2e__0x2e__bit3 -F_0x2e_041_0x2e__0x2e__0x2e__bit4 -F_0x2e_041_0x2e__0x2e__0x2e__bit5 -F_0x2e_041_0x2e__0x2e__0x2e__bit6 -F_0x2e_041_0x2e__0x2e__0x2e__bit7 -F_0x2e_041_0x2e__0x2e__0x2e__bit8 -F_0x2e_041_0x2e__0x2e__0x2e__bit9 -F_0x2e_041_0x2e__0x2e__0x2e__bit10 -F_0x2e_041_0x2e__0x2e__0x2e__bit11 -F_0x2e_041_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bit13 -F_0x2e_041_0x2e__0x2e__0x2e__bit14 -F_0x2e_041_0x2e__0x2e__0x2e__bit15 -F_0x2e_041_0x2e__0x2e__0x2e__bit16 -F_0x2e_041_0x2e__0x2e__0x2e__bit17 -F_0x2e_041_0x2e__0x2e__0x2e__bit18 -F_0x2e_041_0x2e__0x2e__0x2e__bit19 -F_0x2e_040041_bit_10 -F_0x2e_040041_bit_9 -F_0x2e_040041_bit_8 -F_0x2e_040041_bit_7 -F_0x2e_040041_bit_6 -F_0x2e_040041_bit_5 -F_0x2e_040041_bit_4 -F_0x2e_040041_bit_3 -F_0x2e_040041_bit_2 -F_0x2e_040041_bit_1 -F_0x2e_040041_bit0 F_0x2e_040041_bit1 F_0x2e_040041_bit2 F_0x2e_040041_bit3 -F_0x2e_040041_bit4 F_0x2e_040041_bit5 -F_0x2e_040041_bit6 -F_0x2e_040041_bit7 -F_0x2e_040041_bit8 -F_0x2e_040041_bit9 -F_0x2e_040041_bit10 -F_0x2e_040041_bit11 -F_0x2e_040041_bit12 -F_0x2e_040041_bit13 -F_0x2e_040041_bit14 -F_0x2e_040041_bit15 -F_0x2e_040041_bit16 -F_0x2e_040041_bit17 -F_0x2e_040041_bit18 -F_0x2e_040041_bit19 -F_0x2e_041042_bit_10 -F_0x2e_041042_bit_9 -F_0x2e_041042_bit_8 -F_0x2e_041042_bit_7 -F_0x2e_041042_bit_6 -F_0x2e_041042_bit_5 -F_0x2e_041042_bit_4 -F_0x2e_041042_bit_3 -F_0x2e_041042_bit_2 -F_0x2e_041042_bit_1 F_0x2e_041042_bit0 F_0x2e_041042_bit1 -F_0x2e_041042_bit2 -F_0x2e_041042_bit3 F_0x2e_041042_bit4 F_0x2e_041042_bit5 -F_0x2e_041042_bit6 -F_0x2e_041042_bit7 -F_0x2e_041042_bit8 -F_0x2e_041042_bit9 -F_0x2e_041042_bit10 -F_0x2e_041042_bit11 -F_0x2e_041042_bit12 -F_0x2e_041042_bit13 -F_0x2e_041042_bit14 -F_0x2e_041042_bit15 -F_0x2e_041042_bit16 -F_0x2e_041042_bit17 -F_0x2e_041042_bit18 -F_0x2e_041042_bit19 -F_0x2e_042_0x2e__0x2e__0x2e__bit_10 -F_0x2e_042_0x2e__0x2e__0x2e__bit_9 -F_0x2e_042_0x2e__0x2e__0x2e__bit_8 -F_0x2e_042_0x2e__0x2e__0x2e__bit_7 -F_0x2e_042_0x2e__0x2e__0x2e__bit_6 -F_0x2e_042_0x2e__0x2e__0x2e__bit_5 -F_0x2e_042_0x2e__0x2e__0x2e__bit_4 -F_0x2e_042_0x2e__0x2e__0x2e__bit_3 -F_0x2e_042_0x2e__0x2e__0x2e__bit_2 -F_0x2e_042_0x2e__0x2e__0x2e__bit_1 F_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_042_0x2e__0x2e__0x2e__bit1 -F_0x2e_042_0x2e__0x2e__0x2e__bit2 F_0x2e_042_0x2e__0x2e__0x2e__bit3 F_0x2e_042_0x2e__0x2e__0x2e__bit4 F_0x2e_042_0x2e__0x2e__0x2e__bit5 -F_0x2e_042_0x2e__0x2e__0x2e__bit6 -F_0x2e_042_0x2e__0x2e__0x2e__bit7 -F_0x2e_042_0x2e__0x2e__0x2e__bit8 -F_0x2e_042_0x2e__0x2e__0x2e__bit9 -F_0x2e_042_0x2e__0x2e__0x2e__bit10 -F_0x2e_042_0x2e__0x2e__0x2e__bit11 -F_0x2e_042_0x2e__0x2e__0x2e__bit12 -F_0x2e_042_0x2e__0x2e__0x2e__bit13 -F_0x2e_042_0x2e__0x2e__0x2e__bit14 -F_0x2e_042_0x2e__0x2e__0x2e__bit15 -F_0x2e_042_0x2e__0x2e__0x2e__bit16 -F_0x2e_042_0x2e__0x2e__0x2e__bit17 -F_0x2e_042_0x2e__0x2e__0x2e__bit18 -F_0x2e_042_0x2e__0x2e__0x2e__bit19 -F_0x2e_011012_bit_10 -F_0x2e_011012_bit_9 -F_0x2e_011012_bit_8 -F_0x2e_011012_bit_7 -F_0x2e_011012_bit_6 -F_0x2e_011012_bit_5 -F_0x2e_011012_bit_4 -F_0x2e_011012_bit_3 -F_0x2e_011012_bit_2 -F_0x2e_011012_bit_1 F_0x2e_011012_bit0 -F_0x2e_011012_bit1 F_0x2e_011012_bit2 -F_0x2e_011012_bit3 F_0x2e_011012_bit4 -F_0x2e_011012_bit5 -F_0x2e_011012_bit6 -F_0x2e_011012_bit7 -F_0x2e_011012_bit8 -F_0x2e_011012_bit9 -F_0x2e_011012_bit10 -F_0x2e_011012_bit11 -F_0x2e_011012_bit12 -F_0x2e_011012_bit13 -F_0x2e_011012_bit14 -F_0x2e_011012_bit15 -F_0x2e_011012_bit16 -F_0x2e_011012_bit17 -F_0x2e_011012_bit18 -F_0x2e_011012_bit19 -F_0x2e_036037_bit_10 -F_0x2e_036037_bit_9 -F_0x2e_036037_bit_8 -F_0x2e_036037_bit_7 -F_0x2e_036037_bit_6 -F_0x2e_036037_bit_5 -F_0x2e_036037_bit_4 -F_0x2e_036037_bit_3 -F_0x2e_036037_bit_2 -F_0x2e_036037_bit_1 -F_0x2e_036037_bit0 -F_0x2e_036037_bit1 -F_0x2e_036037_bit2 -F_0x2e_036037_bit3 -F_0x2e_036037_bit4 -F_0x2e_036037_bit5 -F_0x2e_036037_bit6 -F_0x2e_036037_bit7 -F_0x2e_036037_bit8 -F_0x2e_036037_bit9 -F_0x2e_036037_bit10 -F_0x2e_036037_bit11 -F_0x2e_036037_bit12 -F_0x2e_036037_bit13 -F_0x2e_036037_bit14 -F_0x2e_036037_bit15 -F_0x2e_036037_bit16 -F_0x2e_036037_bit17 -F_0x2e_036037_bit18 -F_0x2e_036037_bit19 -F_0x2e_038040_bit_10 -F_0x2e_038040_bit_9 -F_0x2e_038040_bit_8 -F_0x2e_038040_bit_7 -F_0x2e_038040_bit_6 -F_0x2e_038040_bit_5 -F_0x2e_038040_bit_4 -F_0x2e_038040_bit_3 -F_0x2e_038040_bit_2 -F_0x2e_038040_bit_1 F_0x2e_038040_bit0 -F_0x2e_038040_bit1 -F_0x2e_038040_bit2 F_0x2e_038040_bit3 -F_0x2e_038040_bit4 F_0x2e_038040_bit5 -F_0x2e_038040_bit6 -F_0x2e_038040_bit7 -F_0x2e_038040_bit8 -F_0x2e_038040_bit9 -F_0x2e_038040_bit10 -F_0x2e_038040_bit11 -F_0x2e_038040_bit12 -F_0x2e_038040_bit13 -F_0x2e_038040_bit14 -F_0x2e_038040_bit15 -F_0x2e_038040_bit16 -F_0x2e_038040_bit17 -F_0x2e_038040_bit18 -F_0x2e_038040_bit19
c _______________________________________________________________________________
c 
c restarts              : 120
c conflicts             : 35629          (32 /sec)
c decisions             : 135746         (122 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1117.2 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/8913/stat): 8913 (minisat+_script) R 8912 8913 16528 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1846531049 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/8913/statm): 174 3 169 147 0 27 0
[pid=8913] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=8914
New process pid=8915
New process pid=8916
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=8916) exited with status: 0
One traced child (pid=8915) exited with status: 0
One traced child (pid=8914) exited with status: 0
New process pid=8917
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-egout.opb

[startup+10.0043 s]
Raw data (loadavg): 0.54 0.84 0.70 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 9747 0 0 0 916 38 0 0 25 0 1 0 1846531055 41119744 9429 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 10039 9429 145 145 0 9894 0
[pid=8917] vsize: 40156
Current children cumulated CPU time (s) 9.55
Current children cumulated vsize (Kb) 42280

[startup+20.005 s]
Raw data (loadavg): 0.61 0.84 0.70 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 9785 0 0 0 1914 39 0 0 25 0 1 0 1846531055 41209856 9467 4294967295 134512640 135094434 3221224432 3221223092 134553517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 10061 9467 145 145 0 9916 0
[pid=8917] vsize: 40244
Current children cumulated CPU time (s) 19.54
Current children cumulated vsize (Kb) 42368

[startup+30.0067 s]
Raw data (loadavg): 0.67 0.85 0.71 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 10062 0 0 0 2913 40 0 0 25 0 1 0 1846531055 42332160 9744 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 10335 9744 145 145 0 10190 0
[pid=8917] vsize: 41340
Current children cumulated CPU time (s) 29.54
Current children cumulated vsize (Kb) 43464

[startup+40.0074 s]
Raw data (loadavg): 0.72 0.85 0.71 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14513 0 0 0 3878 59 0 0 25 0 1 0 1846531055 65654784 13827 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 16029 13827 145 145 0 15884 0
[pid=8917] vsize: 64116
Current children cumulated CPU time (s) 39.38
Current children cumulated vsize (Kb) 66240

[startup+50.0081 s]
Raw data (loadavg): 0.76 0.86 0.71 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14597 0 0 0 4877 59 0 0 25 0 1 0 1846531055 65925120 13911 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 16095 13911 145 145 0 15950 0
[pid=8917] vsize: 64380
Current children cumulated CPU time (s) 49.37
Current children cumulated vsize (Kb) 66504

[startup+60.0087 s]
Raw data (loadavg): 0.80 0.86 0.72 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14657 0 0 0 5876 60 0 0 25 0 1 0 1846531055 66101248 13971 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 16138 13971 145 145 0 15993 0
[pid=8917] vsize: 64552
Current children cumulated CPU time (s) 59.37
Current children cumulated vsize (Kb) 66676

[startup+70.0094 s]
Raw data (loadavg): 0.83 0.86 0.72 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14776 0 0 0 6874 61 0 0 25 0 1 0 1846531055 66580480 14090 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 16255 14090 145 145 0 16110 0
[pid=8917] vsize: 65020
Current children cumulated CPU time (s) 69.36
Current children cumulated vsize (Kb) 67144

[startup+80.0111 s]
Raw data (loadavg): 0.85 0.87 0.72 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 14992 0 0 0 7873 62 0 0 25 0 1 0 1846531055 67129344 14306 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8917/statm): 16389 14306 145 145 0 16244 0
[pid=8917] vsize: 65556
Current children cumulated CPU time (s) 79.36
Current children cumulated vsize (Kb) 67680

[startup+90.0118 s]
Raw data (loadavg): 0.88 0.87 0.72 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 18998 0 0 0 8839 78 0 0 25 0 1 0 1846531055 80711680 18312 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 19705 18312 145 145 0 19560 0
[pid=8917] vsize: 78820
Current children cumulated CPU time (s) 89.18
Current children cumulated vsize (Kb) 80944

[startup+100.011 s]
Raw data (loadavg): 0.89 0.88 0.73 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19004 0 0 0 9839 79 0 0 25 0 1 0 1846531055 80736256 18318 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 19711 18318 145 145 0 19566 0
[pid=8917] vsize: 78844
Current children cumulated CPU time (s) 99.19
Current children cumulated vsize (Kb) 80968

[startup+110.012 s]
Raw data (loadavg): 0.91 0.88 0.73 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19010 0 0 0 10839 79 0 0 25 0 1 0 1846531055 80760832 18324 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 19717 18324 145 145 0 19572 0
[pid=8917] vsize: 78868
Current children cumulated CPU time (s) 109.19
Current children cumulated vsize (Kb) 80992

[startup+120.013 s]
Raw data (loadavg): 0.92 0.88 0.73 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19032 0 0 0 11839 79 0 0 25 0 1 0 1846531055 80879616 18346 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 19746 18346 145 145 0 19601 0
[pid=8917] vsize: 78984
Current children cumulated CPU time (s) 119.19
Current children cumulated vsize (Kb) 81108

[startup+130.013 s]
Raw data (loadavg): 0.93 0.89 0.73 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19078 0 0 0 12839 79 0 0 25 0 1 0 1846531055 81104896 18392 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 19801 18392 145 145 0 19656 0
[pid=8917] vsize: 79204
Current children cumulated CPU time (s) 129.19
Current children cumulated vsize (Kb) 81328

[startup+140.014 s]
Raw data (loadavg): 0.94 0.89 0.74 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19303 0 0 0 13838 80 0 0 25 0 1 0 1846531055 82276352 18617 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20087 18617 145 145 0 19942 0
[pid=8917] vsize: 80348
Current children cumulated CPU time (s) 139.19
Current children cumulated vsize (Kb) 82472

[startup+150.015 s]
Raw data (loadavg): 0.95 0.89 0.74 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19315 0 0 0 14838 80 0 0 25 0 1 0 1846531055 82317312 18629 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20097 18629 145 145 0 19952 0
[pid=8917] vsize: 80388
Current children cumulated CPU time (s) 149.19
Current children cumulated vsize (Kb) 82512

[startup+160.016 s]
Raw data (loadavg): 0.96 0.90 0.74 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19331 0 0 0 15837 80 0 0 25 0 1 0 1846531055 82382848 18645 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20113 18645 145 145 0 19968 0
[pid=8917] vsize: 80452
Current children cumulated CPU time (s) 159.18
Current children cumulated vsize (Kb) 82576

[startup+170.016 s]
Raw data (loadavg): 0.97 0.90 0.74 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19446 0 0 0 16837 80 0 0 25 0 1 0 1846531055 82481152 18669 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20137 18669 145 145 0 19992 0
[pid=8917] vsize: 80548
Current children cumulated CPU time (s) 169.18
Current children cumulated vsize (Kb) 82672

[startup+180.017 s]
Raw data (loadavg): 0.97 0.90 0.74 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19624 0 0 0 17836 81 0 0 25 0 1 0 1846531055 82567168 18691 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20158 18691 145 145 0 20013 0
[pid=8917] vsize: 80632
Current children cumulated CPU time (s) 179.18
Current children cumulated vsize (Kb) 82756

[startup+190.018 s]
Raw data (loadavg): 0.97 0.90 0.75 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19708 0 0 0 18834 83 0 0 25 0 1 0 1846531055 82759680 18742 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20205 18742 145 145 0 20060 0
[pid=8917] vsize: 80820
Current children cumulated CPU time (s) 189.18
Current children cumulated vsize (Kb) 82944

[startup+200.02 s]
Raw data (loadavg): 0.98 0.91 0.75 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19774 0 0 0 19833 84 0 0 25 0 1 0 1846531055 82665472 18718 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20182 18718 145 145 0 20037 0
[pid=8917] vsize: 80728
Current children cumulated CPU time (s) 199.18
Current children cumulated vsize (Kb) 82852

[startup+210.021 s]
Raw data (loadavg): 0.98 0.91 0.75 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19867 0 0 0 20832 85 0 0 25 0 1 0 1846531055 82669568 18720 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20183 18720 145 145 0 20038 0
[pid=8917] vsize: 80732
Current children cumulated CPU time (s) 209.18
Current children cumulated vsize (Kb) 82856

[startup+220.022 s]
Raw data (loadavg): 0.98 0.91 0.75 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19871 0 0 0 21832 85 0 0 25 0 1 0 1846531055 82681856 18724 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20186 18724 145 145 0 20041 0
[pid=8917] vsize: 80744
Current children cumulated CPU time (s) 219.18
Current children cumulated vsize (Kb) 82868

[startup+230.022 s]
Raw data (loadavg): 0.98 0.91 0.75 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 19913 0 0 0 22832 85 0 0 25 0 1 0 1846531055 82853888 18766 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20228 18766 145 145 0 20083 0
[pid=8917] vsize: 80912
Current children cumulated CPU time (s) 229.18
Current children cumulated vsize (Kb) 83036

[startup+240.023 s]
Raw data (loadavg): 0.99 0.92 0.75 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20020 0 0 0 23830 86 0 0 25 0 1 0 1846531055 82923520 18783 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20245 18783 145 145 0 20100 0
[pid=8917] vsize: 80980
Current children cumulated CPU time (s) 239.17
Current children cumulated vsize (Kb) 83104

[startup+250.023 s]
Raw data (loadavg): 0.99 0.92 0.76 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20045 0 0 0 24830 86 0 0 25 0 1 0 1846531055 83021824 18808 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20269 18808 145 145 0 20124 0
[pid=8917] vsize: 81076
Current children cumulated CPU time (s) 249.17
Current children cumulated vsize (Kb) 83200

[startup+260.024 s]
Raw data (loadavg): 0.99 0.92 0.76 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20057 0 0 0 25830 86 0 0 25 0 1 0 1846531055 83070976 18820 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20281 18820 145 145 0 20136 0
[pid=8917] vsize: 81124
Current children cumulated CPU time (s) 259.17
Current children cumulated vsize (Kb) 83248

[startup+270.024 s]
Raw data (loadavg): 0.99 0.92 0.76 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20062 0 0 0 26830 86 0 0 25 0 1 0 1846531055 83091456 18825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20286 18825 145 145 0 20141 0
[pid=8917] vsize: 81144
Current children cumulated CPU time (s) 269.17
Current children cumulated vsize (Kb) 83268

[startup+280.025 s]
Raw data (loadavg): 0.99 0.92 0.76 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20090 0 0 0 27829 87 0 0 25 0 1 0 1846531055 83210240 18853 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20315 18853 145 145 0 20170 0
[pid=8917] vsize: 81260
Current children cumulated CPU time (s) 279.17
Current children cumulated vsize (Kb) 83384

[startup+290.025 s]
Raw data (loadavg): 0.99 0.93 0.76 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20110 0 0 0 28829 87 0 0 25 0 1 0 1846531055 83283968 18873 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20333 18873 145 145 0 20188 0
[pid=8917] vsize: 81332
Current children cumulated CPU time (s) 289.17
Current children cumulated vsize (Kb) 83456

[startup+300.026 s]
Raw data (loadavg): 0.99 0.93 0.77 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20130 0 0 0 29829 87 0 0 25 0 1 0 1846531055 83365888 18893 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20353 18893 145 145 0 20208 0
[pid=8917] vsize: 81412
Current children cumulated CPU time (s) 299.17
Current children cumulated vsize (Kb) 83536

[startup+310.027 s]
Raw data (loadavg): 0.99 0.93 0.77 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20186 0 0 0 30829 88 0 0 25 0 1 0 1846531055 83697664 18949 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20434 18949 145 145 0 20289 0
[pid=8917] vsize: 81736
Current children cumulated CPU time (s) 309.18
Current children cumulated vsize (Kb) 83860

[startup+320.027 s]
Raw data (loadavg): 0.99 0.93 0.77 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20190 0 0 0 31829 88 0 0 25 0 1 0 1846531055 83697664 18953 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20434 18953 145 145 0 20289 0
[pid=8917] vsize: 81736
Current children cumulated CPU time (s) 319.18
Current children cumulated vsize (Kb) 83860

[startup+330.029 s]
Raw data (loadavg): 0.99 0.93 0.77 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20206 0 0 0 32829 88 0 0 25 0 1 0 1846531055 83750912 18969 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20447 18969 145 145 0 20302 0
[pid=8917] vsize: 81788
Current children cumulated CPU time (s) 329.18
Current children cumulated vsize (Kb) 83912

[startup+340.03 s]
Raw data (loadavg): 0.99 0.94 0.77 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20223 0 0 0 33829 88 0 0 25 0 1 0 1846531055 83877888 18986 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20478 18986 145 145 0 20333 0
[pid=8917] vsize: 81912
Current children cumulated CPU time (s) 339.18
Current children cumulated vsize (Kb) 84036

[startup+350.031 s]
Raw data (loadavg): 0.99 0.94 0.78 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20231 0 0 0 34829 88 0 0 25 0 1 0 1846531055 83910656 18994 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20486 18994 145 145 0 20341 0
[pid=8917] vsize: 81944
Current children cumulated CPU time (s) 349.18
Current children cumulated vsize (Kb) 84068

[startup+360.032 s]
Raw data (loadavg): 0.99 0.94 0.78 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20276 0 0 0 35829 89 0 0 25 0 1 0 1846531055 84070400 19039 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20525 19039 145 145 0 20380 0
[pid=8917] vsize: 82100
Current children cumulated CPU time (s) 359.19
Current children cumulated vsize (Kb) 84224

[startup+370.032 s]
Raw data (loadavg): 0.99 0.94 0.78 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20316 0 0 0 36829 89 0 0 25 0 1 0 1846531055 84238336 19079 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20566 19079 145 145 0 20421 0
[pid=8917] vsize: 82264
Current children cumulated CPU time (s) 369.19
Current children cumulated vsize (Kb) 84388

[startup+380.033 s]
Raw data (loadavg): 0.99 0.94 0.78 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20416 0 0 0 37828 90 0 0 25 0 1 0 1846531055 84262912 19088 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20572 19088 145 145 0 20427 0
[pid=8917] vsize: 82288
Current children cumulated CPU time (s) 379.19
Current children cumulated vsize (Kb) 84412

[startup+390.033 s]
Raw data (loadavg): 0.99 0.94 0.78 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20430 0 0 0 38828 90 0 0 25 0 1 0 1846531055 84320256 19102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20586 19102 145 145 0 20441 0
[pid=8917] vsize: 82344
Current children cumulated CPU time (s) 389.19
Current children cumulated vsize (Kb) 84468

[startup+400.034 s]
Raw data (loadavg): 0.99 0.94 0.79 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20499 0 0 0 39828 90 0 0 25 0 1 0 1846531055 84467712 19138 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20622 19138 145 145 0 20477 0
[pid=8917] vsize: 82488
Current children cumulated CPU time (s) 399.19
Current children cumulated vsize (Kb) 84612

[startup+410.035 s]
Raw data (loadavg): 0.99 0.95 0.79 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20530 0 0 0 40828 90 0 0 25 0 1 0 1846531055 84463616 19137 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20621 19137 145 145 0 20476 0
[pid=8917] vsize: 82484
Current children cumulated CPU time (s) 409.19
Current children cumulated vsize (Kb) 84608

[startup+420.035 s]
Raw data (loadavg): 0.99 0.95 0.79 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20531 0 0 0 41828 90 0 0 25 0 1 0 1846531055 84463616 19138 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20621 19138 145 145 0 20476 0
[pid=8917] vsize: 82484
Current children cumulated CPU time (s) 419.19
Current children cumulated vsize (Kb) 84608

[startup+430.036 s]
Raw data (loadavg): 0.99 0.95 0.79 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20535 0 0 0 42828 90 0 0 25 0 1 0 1846531055 84480000 19142 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20625 19142 145 145 0 20480 0
[pid=8917] vsize: 82500
Current children cumulated CPU time (s) 429.19
Current children cumulated vsize (Kb) 84624

[startup+440.037 s]
Raw data (loadavg): 0.99 0.95 0.79 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20553 0 0 0 43828 91 0 0 25 0 1 0 1846531055 84553728 19160 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20643 19160 145 145 0 20498 0
[pid=8917] vsize: 82572
Current children cumulated CPU time (s) 439.2
Current children cumulated vsize (Kb) 84696

[startup+450.037 s]
Raw data (loadavg): 0.99 0.95 0.80 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20564 0 0 0 44828 91 0 0 25 0 1 0 1846531055 84598784 19171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20654 19171 145 145 0 20509 0
[pid=8917] vsize: 82616
Current children cumulated CPU time (s) 449.2
Current children cumulated vsize (Kb) 84740

[startup+460.038 s]
Raw data (loadavg): 0.99 0.95 0.80 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20574 0 0 0 45828 91 0 0 25 0 1 0 1846531055 84643840 19181 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20665 19181 145 145 0 20520 0
[pid=8917] vsize: 82660
Current children cumulated CPU time (s) 459.2
Current children cumulated vsize (Kb) 84784

[startup+470.039 s]
Raw data (loadavg): 0.99 0.95 0.80 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20667 0 0 0 46827 92 0 0 25 0 1 0 1846531055 84652032 19184 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20667 19184 145 145 0 20522 0
[pid=8917] vsize: 82668
Current children cumulated CPU time (s) 469.2
Current children cumulated vsize (Kb) 84792

[startup+480.04 s]
Raw data (loadavg): 0.99 0.95 0.80 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20673 0 0 0 47827 92 0 0 25 0 1 0 1846531055 84676608 19190 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20673 19190 145 145 0 20528 0
[pid=8917] vsize: 82692
Current children cumulated CPU time (s) 479.2
Current children cumulated vsize (Kb) 84816

[startup+490.041 s]
Raw data (loadavg): 0.99 0.95 0.80 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20690 0 0 0 48828 92 0 0 25 0 1 0 1846531055 84758528 19207 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20693 19207 145 145 0 20548 0
[pid=8917] vsize: 82772
Current children cumulated CPU time (s) 489.21
Current children cumulated vsize (Kb) 84896

[startup+500.042 s]
Raw data (loadavg): 0.99 0.95 0.81 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20702 0 0 0 49828 92 0 0 25 0 1 0 1846531055 84795392 19219 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20702 19219 145 145 0 20557 0
[pid=8917] vsize: 82808
Current children cumulated CPU time (s) 499.21
Current children cumulated vsize (Kb) 84932

[startup+510.042 s]
Raw data (loadavg): 0.99 0.96 0.81 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20724 0 0 0 50828 92 0 0 25 0 1 0 1846531055 84881408 19241 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20723 19241 145 145 0 20578 0
[pid=8917] vsize: 82892
Current children cumulated CPU time (s) 509.21
Current children cumulated vsize (Kb) 85016

[startup+520.042 s]
Raw data (loadavg): 0.99 0.96 0.81 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20752 0 0 0 51828 92 0 0 25 0 1 0 1846531055 84996096 19269 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20751 19269 145 145 0 20606 0
[pid=8917] vsize: 83004
Current children cumulated CPU time (s) 519.21
Current children cumulated vsize (Kb) 85128

[startup+530.044 s]
Raw data (loadavg): 0.99 0.96 0.81 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20765 0 0 0 52828 92 0 0 25 0 1 0 1846531055 85049344 19282 4294967295 134512640 135094434 3221224432 3221223056 134557645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20764 19282 145 145 0 20619 0
[pid=8917] vsize: 83056
Current children cumulated CPU time (s) 529.21
Current children cumulated vsize (Kb) 85180

[startup+540.045 s]
Raw data (loadavg): 0.99 0.96 0.81 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20772 0 0 0 53828 92 0 0 25 0 1 0 1846531055 85073920 19289 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20770 19289 145 145 0 20625 0
[pid=8917] vsize: 83080
Current children cumulated CPU time (s) 539.21
Current children cumulated vsize (Kb) 85204

[startup+550.045 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20806 0 0 0 54828 92 0 0 25 0 1 0 1846531055 85213184 19323 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20804 19323 145 145 0 20659 0
[pid=8917] vsize: 83216
Current children cumulated CPU time (s) 549.21
Current children cumulated vsize (Kb) 85340

[startup+560.046 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 20917 0 0 0 55827 93 0 0 25 0 1 0 1846531055 85299200 19343 4294967295 134512640 135094434 3221224432 3221223184 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20825 19343 145 145 0 20680 0
[pid=8917] vsize: 83300
Current children cumulated CPU time (s) 559.21
Current children cumulated vsize (Kb) 85424

[startup+570.047 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21009 0 0 0 56827 93 0 0 25 0 1 0 1846531055 85295104 19343 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20824 19343 145 145 0 20679 0
[pid=8917] vsize: 83296
Current children cumulated CPU time (s) 569.21
Current children cumulated vsize (Kb) 85420

[startup+580.047 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21023 0 0 0 57827 93 0 0 25 0 1 0 1846531055 85352448 19357 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20838 19357 145 145 0 20693 0
[pid=8917] vsize: 83352
Current children cumulated CPU time (s) 579.21
Current children cumulated vsize (Kb) 85476

[startup+590.048 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21038 0 0 0 58827 93 0 0 25 0 1 0 1846531055 85409792 19372 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20852 19372 145 145 0 20707 0
[pid=8917] vsize: 83408
Current children cumulated CPU time (s) 589.21
Current children cumulated vsize (Kb) 85532

[startup+600.049 s]
Raw data (loadavg): 0.99 0.96 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21053 0 0 0 59827 94 0 0 25 0 1 0 1846531055 85471232 19387 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20867 19387 145 145 0 20722 0
[pid=8917] vsize: 83468
Current children cumulated CPU time (s) 599.22
Current children cumulated vsize (Kb) 85592

[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21087 0 0 0 60827 94 0 0 25 0 1 0 1846531055 85614592 19421 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20902 19421 145 145 0 20757 0
[pid=8917] vsize: 83608
Current children cumulated CPU time (s) 609.22
Current children cumulated vsize (Kb) 85732

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21128 0 0 0 61826 94 0 0 25 0 1 0 1846531055 85778432 19462 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20942 19462 145 145 0 20797 0
[pid=8917] vsize: 83768
Current children cumulated CPU time (s) 619.21
Current children cumulated vsize (Kb) 85892

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21142 0 0 0 62826 94 0 0 25 0 1 0 1846531055 85831680 19476 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20955 19476 145 145 0 20810 0
[pid=8917] vsize: 83820
Current children cumulated CPU time (s) 629.21
Current children cumulated vsize (Kb) 85944

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21158 0 0 0 63826 94 0 0 25 0 1 0 1846531055 85897216 19492 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20971 19492 145 145 0 20826 0
[pid=8917] vsize: 83884
Current children cumulated CPU time (s) 639.21
Current children cumulated vsize (Kb) 86008

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21173 0 0 0 64826 95 0 0 25 0 1 0 1846531055 85962752 19507 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20987 19507 145 145 0 20842 0
[pid=8917] vsize: 83948
Current children cumulated CPU time (s) 649.22
Current children cumulated vsize (Kb) 86072

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21185 0 0 0 65826 95 0 0 25 0 1 0 1846531055 86003712 19519 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 20997 19519 145 145 0 20852 0
[pid=8917] vsize: 83988
Current children cumulated CPU time (s) 659.22
Current children cumulated vsize (Kb) 86112

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21201 0 0 0 66826 95 0 0 25 0 1 0 1846531055 86089728 19535 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21018 19535 145 145 0 20873 0
[pid=8917] vsize: 84072
Current children cumulated CPU time (s) 669.22
Current children cumulated vsize (Kb) 86196

[startup+680.054 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21300 0 0 0 67825 95 0 0 25 0 1 0 1846531055 86102016 19543 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21021 19543 145 145 0 20876 0
[pid=8917] vsize: 84084
Current children cumulated CPU time (s) 679.21
Current children cumulated vsize (Kb) 86208

[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21312 0 0 0 68825 95 0 0 25 0 1 0 1846531055 86155264 19555 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21034 19555 145 145 0 20889 0
[pid=8917] vsize: 84136
Current children cumulated CPU time (s) 689.21
Current children cumulated vsize (Kb) 86260

[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21333 0 0 0 69825 96 0 0 25 0 1 0 1846531055 86241280 19576 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21055 19576 145 145 0 20910 0
[pid=8917] vsize: 84220
Current children cumulated CPU time (s) 699.22
Current children cumulated vsize (Kb) 86344

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21357 0 0 0 70825 96 0 0 25 0 1 0 1846531055 86331392 19600 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21077 19600 145 145 0 20932 0
[pid=8917] vsize: 84308
Current children cumulated CPU time (s) 709.22
Current children cumulated vsize (Kb) 86432

[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21376 0 0 0 71825 96 0 0 25 0 1 0 1846531055 86409216 19619 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21096 19619 145 145 0 20951 0
[pid=8917] vsize: 84384
Current children cumulated CPU time (s) 719.22
Current children cumulated vsize (Kb) 86508

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21444 0 0 0 72825 96 0 0 25 0 1 0 1846531055 86528000 19648 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21125 19648 145 145 0 20980 0
[pid=8917] vsize: 84500
Current children cumulated CPU time (s) 729.22
Current children cumulated vsize (Kb) 86624

[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21485 0 0 0 73825 96 0 0 25 0 1 0 1846531055 86487040 19638 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21115 19638 145 145 0 20970 0
[pid=8917] vsize: 84460
Current children cumulated CPU time (s) 739.22
Current children cumulated vsize (Kb) 86584

[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21497 0 0 0 74825 96 0 0 25 0 1 0 1846531055 86536192 19650 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21127 19650 145 145 0 20982 0
[pid=8917] vsize: 84508
Current children cumulated CPU time (s) 749.22
Current children cumulated vsize (Kb) 86632

[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21512 0 0 0 75825 97 0 0 25 0 1 0 1846531055 86593536 19665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21141 19665 145 145 0 20996 0
[pid=8917] vsize: 84564
Current children cumulated CPU time (s) 759.23
Current children cumulated vsize (Kb) 86688

[startup+770.06 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21521 0 0 0 76825 97 0 0 25 0 1 0 1846531055 86626304 19674 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21149 19674 145 145 0 21004 0
[pid=8917] vsize: 84596
Current children cumulated CPU time (s) 769.23
Current children cumulated vsize (Kb) 86720

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21533 0 0 0 77825 97 0 0 25 0 1 0 1846531055 86679552 19686 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21162 19686 145 145 0 21017 0
[pid=8917] vsize: 84648
Current children cumulated CPU time (s) 779.23
Current children cumulated vsize (Kb) 86772

[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21549 0 0 0 78824 98 0 0 25 0 1 0 1846531055 86740992 19702 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21177 19702 145 145 0 21032 0
[pid=8917] vsize: 84708
Current children cumulated CPU time (s) 789.23
Current children cumulated vsize (Kb) 86832

[startup+800.063 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21649 0 0 0 79823 99 0 0 25 0 1 0 1846531055 86777856 19711 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21186 19711 145 145 0 21041 0
[pid=8917] vsize: 84744
Current children cumulated CPU time (s) 799.23
Current children cumulated vsize (Kb) 86868

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21670 0 0 0 80822 100 0 0 25 0 1 0 1846531055 86855680 19732 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21205 19732 145 145 0 21060 0
[pid=8917] vsize: 84820
Current children cumulated CPU time (s) 809.23
Current children cumulated vsize (Kb) 86944

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21685 0 0 0 81822 100 0 0 25 0 1 0 1846531055 86921216 19747 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21221 19747 145 145 0 21076 0
[pid=8917] vsize: 84884
Current children cumulated CPU time (s) 819.23
Current children cumulated vsize (Kb) 87008

[startup+830.066 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21702 0 0 0 82822 100 0 0 25 0 1 0 1846531055 86986752 19764 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21237 19764 145 145 0 21092 0
[pid=8917] vsize: 84948
Current children cumulated CPU time (s) 829.23
Current children cumulated vsize (Kb) 87072

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21810 0 0 0 83821 101 0 0 25 0 1 0 1846531055 87060480 19780 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21255 19780 145 145 0 21110 0
[pid=8917] vsize: 85020
Current children cumulated CPU time (s) 839.23
Current children cumulated vsize (Kb) 87144

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21893 0 0 0 84820 102 0 0 25 0 1 0 1846531055 87248896 19830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21301 19830 145 145 0 21156 0
[pid=8917] vsize: 85204
Current children cumulated CPU time (s) 849.23
Current children cumulated vsize (Kb) 87328

[startup+860.068 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21910 0 0 0 85820 102 0 0 25 0 1 0 1846531055 87318528 19847 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19847 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 859.23
Current children cumulated vsize (Kb) 87396

[startup+870.069 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 86821 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 869.24
Current children cumulated vsize (Kb) 87396

[startup+880.07 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 87820 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 879.23
Current children cumulated vsize (Kb) 87396

[startup+890.07 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 88821 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 889.24
Current children cumulated vsize (Kb) 87396

[startup+900.071 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21911 0 0 0 89820 102 0 0 25 0 1 0 1846531055 87318528 19848 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19848 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 899.23
Current children cumulated vsize (Kb) 87396

[startup+910.072 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21912 0 0 0 90821 102 0 0 25 0 1 0 1846531055 87318528 19849 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19849 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 909.24
Current children cumulated vsize (Kb) 87396

[startup+920.072 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21912 0 0 0 91821 102 0 0 25 0 1 0 1846531055 87318528 19849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19849 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 919.24
Current children cumulated vsize (Kb) 87396

[startup+930.073 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21912 0 0 0 92821 102 0 0 25 0 1 0 1846531055 87318528 19849 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21318 19849 145 145 0 21173 0
[pid=8917] vsize: 85272
Current children cumulated CPU time (s) 929.24
Current children cumulated vsize (Kb) 87396

[startup+940.074 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21921 0 0 0 93821 103 0 0 25 0 1 0 1846531055 87355392 19858 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21327 19858 145 145 0 21182 0
[pid=8917] vsize: 85308
Current children cumulated CPU time (s) 939.25
Current children cumulated vsize (Kb) 87432

[startup+950.074 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21941 0 0 0 94821 103 0 0 25 0 1 0 1846531055 87433216 19878 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21346 19878 145 145 0 21201 0
[pid=8917] vsize: 85384
Current children cumulated CPU time (s) 949.25
Current children cumulated vsize (Kb) 87508

[startup+960.075 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 21952 0 0 0 95821 103 0 0 25 0 1 0 1846531055 87482368 19889 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21358 19889 145 145 0 21213 0
[pid=8917] vsize: 85432
Current children cumulated CPU time (s) 959.25
Current children cumulated vsize (Kb) 87556

[startup+970.076 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22023 0 0 0 96821 103 0 0 25 0 1 0 1846531055 87609344 19921 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21389 19921 145 145 0 21244 0
[pid=8917] vsize: 85556
Current children cumulated CPU time (s) 969.25
Current children cumulated vsize (Kb) 87680

[startup+980.077 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22120 0 0 0 97820 104 0 0 25 0 1 0 1846531055 87638016 19928 4294967295 134512640 135094434 3221224432 3221220284 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21396 19928 145 145 0 21251 0
[pid=8917] vsize: 85584
Current children cumulated CPU time (s) 979.25
Current children cumulated vsize (Kb) 87708

[startup+990.077 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22160 0 0 0 98820 104 0 0 25 0 1 0 1846531055 87584768 19916 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21383 19916 145 145 0 21238 0
[pid=8917] vsize: 85532
Current children cumulated CPU time (s) 989.25
Current children cumulated vsize (Kb) 87656

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22168 0 0 0 99820 105 0 0 25 0 1 0 1846531055 87617536 19924 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21391 19924 145 145 0 21246 0
[pid=8917] vsize: 85564
Current children cumulated CPU time (s) 999.26
Current children cumulated vsize (Kb) 87688

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22182 0 0 0 100820 105 0 0 25 0 1 0 1846531055 87678976 19938 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21406 19938 145 145 0 21261 0
[pid=8917] vsize: 85624
Current children cumulated CPU time (s) 1009.26
Current children cumulated vsize (Kb) 87748

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22200 0 0 0 101819 105 0 0 25 0 1 0 1846531055 87752704 19956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21424 19956 145 145 0 21279 0
[pid=8917] vsize: 85696
Current children cumulated CPU time (s) 1019.25
Current children cumulated vsize (Kb) 87820

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22212 0 0 0 102820 105 0 0 25 0 1 0 1846531055 87793664 19968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21434 19968 145 145 0 21289 0
[pid=8917] vsize: 85736
Current children cumulated CPU time (s) 1029.26
Current children cumulated vsize (Kb) 87860

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22229 0 0 0 103820 105 0 0 25 0 1 0 1846531055 87863296 19985 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21451 19985 145 145 0 21306 0
[pid=8917] vsize: 85804
Current children cumulated CPU time (s) 1039.26
Current children cumulated vsize (Kb) 87928

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22241 0 0 0 104820 105 0 0 25 0 1 0 1846531055 87912448 19997 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21463 19997 145 145 0 21318 0
[pid=8917] vsize: 85852
Current children cumulated CPU time (s) 1049.26
Current children cumulated vsize (Kb) 87976

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22253 0 0 0 105820 105 0 0 25 0 1 0 1846531055 87961600 20009 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21475 20009 145 145 0 21330 0
[pid=8917] vsize: 85900
Current children cumulated CPU time (s) 1059.26
Current children cumulated vsize (Kb) 88024

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22297 0 0 0 106820 105 0 0 25 0 1 0 1846531055 88272896 20053 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21551 20053 145 145 0 21406 0
[pid=8917] vsize: 86204
Current children cumulated CPU time (s) 1069.26
Current children cumulated vsize (Kb) 88328

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22297 0 0 0 107820 105 0 0 25 0 1 0 1846531055 88272896 20053 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21551 20053 145 145 0 21406 0
[pid=8917] vsize: 86204
Current children cumulated CPU time (s) 1079.26
Current children cumulated vsize (Kb) 88328

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22297 0 0 0 108820 105 0 0 25 0 1 0 1846531055 88272896 20053 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21551 20053 145 145 0 21406 0
[pid=8917] vsize: 86204
Current children cumulated CPU time (s) 1089.26
Current children cumulated vsize (Kb) 88328

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22303 0 0 0 109821 105 0 0 25 0 1 0 1846531055 88293376 20059 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21556 20059 145 145 0 21411 0
[pid=8917] vsize: 86224
Current children cumulated CPU time (s) 1099.27
Current children cumulated vsize (Kb) 88348

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 8917
Raw data (/proc/8913/stat): 8913 (minisat+_script) S 8912 8913 16528 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1846531049 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/8913/statm): 531 226 485 147 0 384 0
[pid=8913] vsize: 2124
Raw data (/proc/8917/stat): 8917 (minisat+_64-bit) R 8913 8913 16528 0 -1 0 22317 0 0 0 110820 106 0 0 25 0 1 0 1846531055 88346624 20073 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8917/statm): 21569 20073 145 145 0 21424 0
[pid=8917] vsize: 86276
Current children cumulated CPU time (s) 1109.27
Current children cumulated vsize (Kb) 88400
One traced child (pid=8917) exited with status: 30
One traced child (pid=8913) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 1119.21
CPU time (s): 1118.41
CPU user time (s): 1117.29
CPU system time (s): 1.12183
CPU usage (%): 99.929
Max. virtual memory (cumulated for all children) (Kb): 88400

Verifier Data

Verifier:	OK	471047168