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/miplib3/normalized-mps-v2-20-10-egout.opb
MD5SUM99bcb41cf234e24f89287b787fc4273a
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 benchmark1108.66
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 4497

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-19 17:46:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2968 boxname=wulflinc26 idbench=624 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  99bcb41cf234e24f89287b787fc4273a  /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: 2968
/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:        859224 kB
Buffers:         38280 kB
Cached:         108616 kB
SwapCached:        868 kB
Active:          81020 kB
Inactive:        68528 kB
HighTotal:      131008 kB
HighFree:        26432 kB
LowTotal:       903652 kB
LowFree:        832792 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            20408 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:04:31 (client local time) WITH STATUS 30 IN 1108.66 SECONDS
stats: 2968 0 1108.66 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         (123 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1107.27 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/11520/stat): 11520 (minisat+_script) R 11519 11520 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851813923 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11520/statm): 174 3 169 147 0 27 0
[pid=11520] 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=11521
New process pid=11522
New process pid=11523
execve syscall for /bin/sed executable
One traced child (pid=11522) exited with status: 0
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=11523) exited with status: 0
One traced child (pid=11521) exited with status: 0
New process pid=11524
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.0042 s]
Raw data (loadavg): 0.71 0.89 0.68 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 9744 0 2 0 901 40 0 0 25 0 1 0 1851813928 41115648 9428 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 10038 9428 145 145 0 9893 0
[pid=11524] vsize: 40152
Current children cumulated CPU time (s) 9.42
Current children cumulated vsize (Kb) 42276

[startup+20.0049 s]
Raw data (loadavg): 0.75 0.90 0.69 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 9783 0 2 0 1900 41 0 0 25 0 1 0 1851813928 41209856 9467 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 10061 9467 145 145 0 9916 0
[pid=11524] vsize: 40244
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 42368

[startup+30.0066 s]
Raw data (loadavg): 0.79 0.90 0.69 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 10060 0 2 0 2898 42 0 0 25 0 1 0 1851813928 42332160 9744 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 10335 9744 145 145 0 10190 0
[pid=11524] vsize: 41340
Current children cumulated CPU time (s) 29.41
Current children cumulated vsize (Kb) 43464

[startup+40.0072 s]
Raw data (loadavg): 0.82 0.90 0.69 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14511 0 2 0 3864 59 0 0 25 0 1 0 1851813928 65654784 13827 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 16029 13827 145 145 0 15884 0
[pid=11524] vsize: 64116
Current children cumulated CPU time (s) 39.24
Current children cumulated vsize (Kb) 66240

[startup+50.0089 s]
Raw data (loadavg): 0.85 0.91 0.70 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14595 0 2 0 4864 60 0 0 25 0 1 0 1851813928 65925120 13911 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 16095 13911 145 145 0 15950 0
[pid=11524] vsize: 64380
Current children cumulated CPU time (s) 49.25
Current children cumulated vsize (Kb) 66504

[startup+60.0096 s]
Raw data (loadavg): 0.87 0.91 0.70 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14655 0 2 0 5864 60 0 0 25 0 1 0 1851813928 66101248 13971 4294967295 134512640 135094434 3221224432 3221223104 134555447 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 16138 13971 145 145 0 15993 0
[pid=11524] vsize: 64552
Current children cumulated CPU time (s) 59.25
Current children cumulated vsize (Kb) 66676

[startup+70.0103 s]
Raw data (loadavg): 0.89 0.91 0.70 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14774 0 2 0 6862 61 0 0 25 0 1 0 1851813928 66580480 14090 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 16255 14090 145 145 0 16110 0
[pid=11524] vsize: 65020
Current children cumulated CPU time (s) 69.24
Current children cumulated vsize (Kb) 67144

[startup+80.0119 s]
Raw data (loadavg): 0.91 0.91 0.70 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 14990 0 2 0 7861 62 0 0 25 0 1 0 1851813928 67129344 14306 4294967295 134512640 135094434 3221224432 3221221984 134677333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 16389 14306 145 145 0 16244 0
[pid=11524] vsize: 65556
Current children cumulated CPU time (s) 79.24
Current children cumulated vsize (Kb) 67680

[startup+90.0127 s]
Raw data (loadavg): 0.92 0.92 0.71 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 18996 0 2 0 8826 80 0 0 25 0 1 0 1851813928 80711680 18312 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 19705 18312 145 145 0 19560 0
[pid=11524] vsize: 78820
Current children cumulated CPU time (s) 89.07
Current children cumulated vsize (Kb) 80944

[startup+100.014 s]
Raw data (loadavg): 0.93 0.92 0.71 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19002 0 2 0 9827 80 0 0 25 0 1 0 1851813928 80736256 18318 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 19711 18318 145 145 0 19566 0
[pid=11524] vsize: 78844
Current children cumulated CPU time (s) 99.08
Current children cumulated vsize (Kb) 80968

[startup+110.016 s]
Raw data (loadavg): 0.94 0.92 0.71 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19009 0 2 0 10826 80 0 0 25 0 1 0 1851813928 80764928 18325 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 19718 18325 145 145 0 19573 0
[pid=11524] vsize: 78872
Current children cumulated CPU time (s) 109.07
Current children cumulated vsize (Kb) 80996

[startup+120.017 s]
Raw data (loadavg): 0.95 0.92 0.72 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19030 0 2 0 11825 81 0 0 25 0 1 0 1851813928 80879616 18346 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 19746 18346 145 145 0 19601 0
[pid=11524] vsize: 78984
Current children cumulated CPU time (s) 119.07
Current children cumulated vsize (Kb) 81108

[startup+130.018 s]
Raw data (loadavg): 0.96 0.92 0.72 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19076 0 2 0 12824 81 0 0 25 0 1 0 1851813928 81104896 18392 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 19801 18392 145 145 0 19656 0
[pid=11524] vsize: 79204
Current children cumulated CPU time (s) 129.06
Current children cumulated vsize (Kb) 81328

[startup+140.019 s]
Raw data (loadavg): 0.96 0.93 0.72 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19301 0 2 0 13822 83 0 0 25 0 1 0 1851813928 82276352 18617 4294967295 134512640 135094434 3221224432 3221221632 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20087 18617 145 145 0 19942 0
[pid=11524] vsize: 80348
Current children cumulated CPU time (s) 139.06
Current children cumulated vsize (Kb) 82472

[startup+150.021 s]
Raw data (loadavg): 0.97 0.93 0.72 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19313 0 2 0 14822 83 0 0 25 0 1 0 1851813928 82317312 18629 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20097 18629 145 145 0 19952 0
[pid=11524] vsize: 80388
Current children cumulated CPU time (s) 149.06
Current children cumulated vsize (Kb) 82512

[startup+160.021 s]
Raw data (loadavg): 0.97 0.93 0.73 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19330 0 2 0 15821 84 0 0 25 0 1 0 1851813928 82386944 18646 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20114 18646 145 145 0 19969 0
[pid=11524] vsize: 80456
Current children cumulated CPU time (s) 159.06
Current children cumulated vsize (Kb) 82580

[startup+170.022 s]
Raw data (loadavg): 0.98 0.93 0.73 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19501 0 2 0 16819 85 0 0 25 0 1 0 1851813928 82550784 18687 4294967295 134512640 135094434 3221224432 3221220496 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20154 18687 145 145 0 20009 0
[pid=11524] vsize: 80616
Current children cumulated CPU time (s) 169.05
Current children cumulated vsize (Kb) 82740

[startup+180.023 s]
Raw data (loadavg): 0.98 0.93 0.73 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19622 0 2 0 17817 86 0 0 25 0 1 0 1851813928 82567168 18691 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20158 18691 145 145 0 20013 0
[pid=11524] vsize: 80632
Current children cumulated CPU time (s) 179.04
Current children cumulated vsize (Kb) 82756

[startup+190.024 s]
Raw data (loadavg): 0.98 0.94 0.73 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19706 0 2 0 18816 87 0 0 25 0 1 0 1851813928 82759680 18742 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20205 18742 145 145 0 20060 0
[pid=11524] vsize: 80820
Current children cumulated CPU time (s) 189.04
Current children cumulated vsize (Kb) 82944

[startup+200.026 s]
Raw data (loadavg): 0.98 0.94 0.74 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19772 0 2 0 19815 87 0 0 25 0 1 0 1851813928 82665472 18718 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20182 18718 145 145 0 20037 0
[pid=11524] vsize: 80728
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 82852

[startup+210.027 s]
Raw data (loadavg): 0.99 0.94 0.74 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19865 0 2 0 20814 88 0 0 25 0 1 0 1851813928 82669568 18720 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20183 18720 145 145 0 20038 0
[pid=11524] vsize: 80732
Current children cumulated CPU time (s) 209.03
Current children cumulated vsize (Kb) 82856

[startup+220.028 s]
Raw data (loadavg): 0.99 0.94 0.74 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19883 0 2 0 21813 89 0 0 25 0 1 0 1851813928 82739200 18738 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20200 18738 145 145 0 20055 0
[pid=11524] vsize: 80800
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 82924

[startup+230.029 s]
Raw data (loadavg): 0.99 0.94 0.74 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 19914 0 2 0 22813 89 0 0 25 0 1 0 1851813928 82866176 18769 4294967295 134512640 135094434 3221224432 3221223072 134562063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20231 18769 145 145 0 20086 0
[pid=11524] vsize: 80924
Current children cumulated CPU time (s) 229.03
Current children cumulated vsize (Kb) 83048

[startup+240.03 s]
Raw data (loadavg): 0.99 0.94 0.74 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20026 0 2 0 23811 90 0 0 25 0 1 0 1851813928 82956288 18791 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20253 18791 145 145 0 20108 0
[pid=11524] vsize: 81012
Current children cumulated CPU time (s) 239.02
Current children cumulated vsize (Kb) 83136

[startup+250.032 s]
Raw data (loadavg): 0.99 0.94 0.75 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20045 0 2 0 24810 91 0 0 25 0 1 0 1851813928 83030016 18810 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20271 18810 145 145 0 20126 0
[pid=11524] vsize: 81084
Current children cumulated CPU time (s) 249.02
Current children cumulated vsize (Kb) 83208

[startup+260.033 s]
Raw data (loadavg): 0.99 0.95 0.75 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20057 0 2 0 25809 92 0 0 25 0 1 0 1851813928 83079168 18822 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20283 18822 145 145 0 20138 0
[pid=11524] vsize: 81132
Current children cumulated CPU time (s) 259.02
Current children cumulated vsize (Kb) 83256

[startup+270.034 s]
Raw data (loadavg): 0.99 0.95 0.75 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20062 0 2 0 26809 92 0 0 25 0 1 0 1851813928 83099648 18827 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20288 18827 145 145 0 20143 0
[pid=11524] vsize: 81152
Current children cumulated CPU time (s) 269.02
Current children cumulated vsize (Kb) 83276

[startup+280.036 s]
Raw data (loadavg): 0.99 0.95 0.75 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20097 0 2 0 27808 92 0 0 25 0 1 0 1851813928 83238912 18862 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20322 18862 145 145 0 20177 0
[pid=11524] vsize: 81288
Current children cumulated CPU time (s) 279.01
Current children cumulated vsize (Kb) 83412

[startup+290.037 s]
Raw data (loadavg): 0.99 0.95 0.75 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20111 0 2 0 28808 93 0 0 25 0 1 0 1851813928 83296256 18876 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20336 18876 145 145 0 20191 0
[pid=11524] vsize: 81344
Current children cumulated CPU time (s) 289.02
Current children cumulated vsize (Kb) 83468

[startup+300.038 s]
Raw data (loadavg): 0.99 0.95 0.75 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20133 0 2 0 29807 93 0 0 25 0 1 0 1851813928 83390464 18898 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20359 18898 145 145 0 20214 0
[pid=11524] vsize: 81436
Current children cumulated CPU time (s) 299.01
Current children cumulated vsize (Kb) 83560

[startup+310.039 s]
Raw data (loadavg): 0.99 0.95 0.76 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20184 0 2 0 30807 94 0 0 25 0 1 0 1851813928 83697664 18949 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20434 18949 145 145 0 20289 0
[pid=11524] vsize: 81736
Current children cumulated CPU time (s) 309.02
Current children cumulated vsize (Kb) 83860

[startup+320.039 s]
Raw data (loadavg): 0.99 0.95 0.76 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20188 0 2 0 31807 94 0 0 25 0 1 0 1851813928 83697664 18953 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20434 18953 145 145 0 20289 0
[pid=11524] vsize: 81736
Current children cumulated CPU time (s) 319.02
Current children cumulated vsize (Kb) 83860

[startup+330.041 s]
Raw data (loadavg): 0.99 0.95 0.76 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20204 0 2 0 32806 94 0 0 25 0 1 0 1851813928 83750912 18969 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20447 18969 145 145 0 20302 0
[pid=11524] vsize: 81788
Current children cumulated CPU time (s) 329.01
Current children cumulated vsize (Kb) 83912

[startup+340.042 s]
Raw data (loadavg): 0.99 0.95 0.76 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20221 0 2 0 33806 95 0 0 25 0 1 0 1851813928 83877888 18986 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20478 18986 145 145 0 20333 0
[pid=11524] vsize: 81912
Current children cumulated CPU time (s) 339.02
Current children cumulated vsize (Kb) 84036

[startup+350.043 s]
Raw data (loadavg): 0.99 0.95 0.76 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20245 0 2 0 34805 96 0 0 25 0 1 0 1851813928 83976192 19010 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20502 19010 145 145 0 20357 0
[pid=11524] vsize: 82008
Current children cumulated CPU time (s) 349.02
Current children cumulated vsize (Kb) 84132

[startup+360.044 s]
Raw data (loadavg): 0.99 0.95 0.77 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20288 0 2 0 35805 96 0 0 25 0 1 0 1851813928 84123648 19053 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20538 19053 145 145 0 20393 0
[pid=11524] vsize: 82152
Current children cumulated CPU time (s) 359.02
Current children cumulated vsize (Kb) 84276

[startup+370.045 s]
Raw data (loadavg): 0.99 0.96 0.77 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20374 0 2 0 36804 97 0 0 25 0 1 0 1851813928 84316160 19100 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20585 19100 145 145 0 20440 0
[pid=11524] vsize: 82340
Current children cumulated CPU time (s) 369.02
Current children cumulated vsize (Kb) 84464

[startup+380.046 s]
Raw data (loadavg): 0.99 0.96 0.77 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20419 0 2 0 37803 97 0 0 25 0 1 0 1851813928 84283392 19093 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20577 19093 145 145 0 20432 0
[pid=11524] vsize: 82308
Current children cumulated CPU time (s) 379.01
Current children cumulated vsize (Kb) 84432

[startup+390.047 s]
Raw data (loadavg): 0.99 0.96 0.77 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20435 0 2 0 38802 98 0 0 25 0 1 0 1851813928 84348928 19109 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20593 19109 145 145 0 20448 0
[pid=11524] vsize: 82372
Current children cumulated CPU time (s) 389.01
Current children cumulated vsize (Kb) 84496

[startup+400.049 s]
Raw data (loadavg): 0.99 0.96 0.77 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20528 0 2 0 39801 99 0 0 25 0 1 0 1851813928 84463616 19137 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20621 19137 145 145 0 20476 0
[pid=11524] vsize: 82484
Current children cumulated CPU time (s) 399.01
Current children cumulated vsize (Kb) 84608

[startup+410.049 s]
Raw data (loadavg): 0.99 0.96 0.78 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20528 0 2 0 40800 99 0 0 25 0 1 0 1851813928 84463616 19137 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20621 19137 145 145 0 20476 0
[pid=11524] vsize: 82484
Current children cumulated CPU time (s) 409
Current children cumulated vsize (Kb) 84608

[startup+420.05 s]
Raw data (loadavg): 0.99 0.96 0.78 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20533 0 2 0 41800 100 0 0 25 0 1 0 1851813928 84480000 19142 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20625 19142 145 145 0 20480 0
[pid=11524] vsize: 82500
Current children cumulated CPU time (s) 419.01
Current children cumulated vsize (Kb) 84624

[startup+430.052 s]
Raw data (loadavg): 0.99 0.96 0.78 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20541 0 2 0 42799 100 0 0 25 0 1 0 1851813928 84512768 19150 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20633 19150 145 145 0 20488 0
[pid=11524] vsize: 82532
Current children cumulated CPU time (s) 429
Current children cumulated vsize (Kb) 84656

[startup+440.052 s]
Raw data (loadavg): 0.99 0.96 0.78 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20557 0 2 0 43798 101 0 0 25 0 1 0 1851813928 84578304 19166 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20649 19166 145 145 0 20504 0
[pid=11524] vsize: 82596
Current children cumulated CPU time (s) 439
Current children cumulated vsize (Kb) 84720

[startup+450.053 s]
Raw data (loadavg): 0.99 0.96 0.78 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20567 0 2 0 44798 101 0 0 25 0 1 0 1851813928 84627456 19176 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20661 19176 145 145 0 20516 0
[pid=11524] vsize: 82644
Current children cumulated CPU time (s) 449
Current children cumulated vsize (Kb) 84768

[startup+460.054 s]
Raw data (loadavg): 0.99 0.96 0.79 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20635 0 2 0 45797 102 0 0 25 0 1 0 1851813928 84738048 19205 4294967295 134512640 135094434 3221224432 3221219944 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20688 19205 145 145 0 20543 0
[pid=11524] vsize: 82752
Current children cumulated CPU time (s) 459
Current children cumulated vsize (Kb) 84876

[startup+470.055 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20668 0 2 0 46796 103 0 0 25 0 1 0 1851813928 84668416 19187 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20671 19187 145 145 0 20526 0
[pid=11524] vsize: 82684
Current children cumulated CPU time (s) 469
Current children cumulated vsize (Kb) 84808

[startup+480.055 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20676 0 2 0 47796 103 0 0 25 0 1 0 1851813928 84697088 19195 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20678 19195 145 145 0 20533 0
[pid=11524] vsize: 82712
Current children cumulated CPU time (s) 479
Current children cumulated vsize (Kb) 84836

[startup+490.056 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20690 0 2 0 48796 103 0 0 25 0 1 0 1851813928 84758528 19209 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20693 19209 145 145 0 20548 0
[pid=11524] vsize: 82772
Current children cumulated CPU time (s) 489
Current children cumulated vsize (Kb) 84896

[startup+500.058 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20707 0 2 0 49795 104 0 0 25 0 1 0 1851813928 84819968 19226 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20708 19226 145 145 0 20563 0
[pid=11524] vsize: 82832
Current children cumulated CPU time (s) 499
Current children cumulated vsize (Kb) 84956

[startup+510.058 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20739 0 2 0 50795 105 0 0 25 0 1 0 1851813928 84951040 19258 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20740 19258 145 145 0 20595 0
[pid=11524] vsize: 82960
Current children cumulated CPU time (s) 509.01
Current children cumulated vsize (Kb) 85084

[startup+520.059 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20762 0 2 0 51794 105 0 0 25 0 1 0 1851813928 85049344 19281 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20764 19281 145 145 0 20619 0
[pid=11524] vsize: 83056
Current children cumulated CPU time (s) 519
Current children cumulated vsize (Kb) 85180

[startup+530.061 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20767 0 2 0 52794 106 0 0 25 0 1 0 1851813928 85065728 19286 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20768 19286 145 145 0 20623 0
[pid=11524] vsize: 83072
Current children cumulated CPU time (s) 529.01
Current children cumulated vsize (Kb) 85196

[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20791 0 2 0 53793 106 0 0 25 0 1 0 1851813928 85164032 19310 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20792 19310 145 145 0 20647 0
[pid=11524] vsize: 83168
Current children cumulated CPU time (s) 539
Current children cumulated vsize (Kb) 85292

[startup+550.063 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20900 0 2 0 54792 107 0 0 25 0 1 0 1851813928 85233664 19328 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20809 19328 145 145 0 20664 0
[pid=11524] vsize: 83236
Current children cumulated CPU time (s) 549
Current children cumulated vsize (Kb) 85360

[startup+560.065 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 20976 0 2 0 55791 108 0 0 25 0 1 0 1851813928 85381120 19364 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20845 19364 145 145 0 20700 0
[pid=11524] vsize: 83380
Current children cumulated CPU time (s) 559
Current children cumulated vsize (Kb) 85504

[startup+570.065 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21017 0 2 0 56790 108 0 0 25 0 1 0 1851813928 85336064 19353 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20834 19353 145 145 0 20689 0
[pid=11524] vsize: 83336
Current children cumulated CPU time (s) 568.99
Current children cumulated vsize (Kb) 85460

[startup+580.067 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21035 0 2 0 57790 109 0 0 25 0 1 0 1851813928 85409792 19371 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20852 19371 145 145 0 20707 0
[pid=11524] vsize: 83408
Current children cumulated CPU time (s) 579
Current children cumulated vsize (Kb) 85532

[startup+590.068 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21049 0 2 0 58790 110 0 0 25 0 1 0 1851813928 85463040 19385 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20865 19385 145 145 0 20720 0
[pid=11524] vsize: 83460
Current children cumulated CPU time (s) 589.01
Current children cumulated vsize (Kb) 85584

[startup+600.068 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21082 0 2 0 59789 110 0 0 25 0 1 0 1851813928 85602304 19418 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11524/statm): 20899 19418 145 145 0 20754 0
[pid=11524] vsize: 83596
Current children cumulated CPU time (s) 599
Current children cumulated vsize (Kb) 85720

[startup+610.07 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21115 0 2 0 60788 111 0 0 25 0 1 0 1851813928 85745664 19451 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 20934 19451 145 145 0 20789 0
[pid=11524] vsize: 83736
Current children cumulated CPU time (s) 609
Current children cumulated vsize (Kb) 85860

[startup+620.071 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21136 0 2 0 61788 111 0 0 25 0 1 0 1851813928 85815296 19472 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 20951 19472 145 145 0 20806 0
[pid=11524] vsize: 83804
Current children cumulated CPU time (s) 619
Current children cumulated vsize (Kb) 85928

[startup+630.071 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21155 0 2 0 62788 111 0 0 25 0 1 0 1851813928 85893120 19491 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 20970 19491 145 145 0 20825 0
[pid=11524] vsize: 83880
Current children cumulated CPU time (s) 629
Current children cumulated vsize (Kb) 86004

[startup+640.072 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21169 0 2 0 63788 112 0 0 25 0 1 0 1851813928 85954560 19505 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 20985 19505 145 145 0 20840 0
[pid=11524] vsize: 83940
Current children cumulated CPU time (s) 639.01
Current children cumulated vsize (Kb) 86064

[startup+650.073 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21177 0 2 0 64787 112 0 0 25 0 1 0 1851813928 85983232 19513 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 20992 19513 145 145 0 20847 0
[pid=11524] vsize: 83968
Current children cumulated CPU time (s) 649
Current children cumulated vsize (Kb) 86092

[startup+660.073 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21199 0 2 0 65787 112 0 0 25 0 1 0 1851813928 86089728 19535 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21018 19535 145 145 0 20873 0
[pid=11524] vsize: 84072
Current children cumulated CPU time (s) 659
Current children cumulated vsize (Kb) 86196

[startup+670.074 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21296 0 2 0 66787 112 0 0 25 0 1 0 1851813928 86102016 19541 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21021 19541 145 145 0 20876 0
[pid=11524] vsize: 84084
Current children cumulated CPU time (s) 669
Current children cumulated vsize (Kb) 86208

[startup+680.076 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21310 0 2 0 67787 112 0 0 25 0 1 0 1851813928 86155264 19555 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21034 19555 145 145 0 20889 0
[pid=11524] vsize: 84136
Current children cumulated CPU time (s) 679
Current children cumulated vsize (Kb) 86260

[startup+690.076 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21322 0 2 0 68787 112 0 0 25 0 1 0 1851813928 86200320 19567 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21045 19567 145 145 0 20900 0
[pid=11524] vsize: 84180
Current children cumulated CPU time (s) 689
Current children cumulated vsize (Kb) 86304

[startup+700.078 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21350 0 2 0 69788 112 0 0 25 0 1 0 1851813928 86310912 19595 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21072 19595 145 145 0 20927 0
[pid=11524] vsize: 84288
Current children cumulated CPU time (s) 699.01
Current children cumulated vsize (Kb) 86412

[startup+710.079 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21365 0 2 0 70788 112 0 0 25 0 1 0 1851813928 86376448 19610 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21088 19610 145 145 0 20943 0
[pid=11524] vsize: 84352
Current children cumulated CPU time (s) 709.01
Current children cumulated vsize (Kb) 86476

[startup+720.078 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21442 0 2 0 71787 113 0 0 25 0 1 0 1851813928 86528000 19648 4294967295 134512640 135094434 3221224432 3221220224 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21125 19648 145 145 0 20980 0
[pid=11524] vsize: 84500
Current children cumulated CPU time (s) 719.01
Current children cumulated vsize (Kb) 86624

[startup+730.079 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21483 0 2 0 72786 114 0 0 25 0 1 0 1851813928 86487040 19638 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21115 19638 145 145 0 20970 0
[pid=11524] vsize: 84460
Current children cumulated CPU time (s) 729.01
Current children cumulated vsize (Kb) 86584

[startup+740.08 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21492 0 2 0 73787 114 0 0 25 0 1 0 1851813928 86519808 19647 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21123 19647 145 145 0 20978 0
[pid=11524] vsize: 84492
Current children cumulated CPU time (s) 739.02
Current children cumulated vsize (Kb) 86616

[startup+750.082 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21504 0 2 0 74787 114 0 0 25 0 1 0 1851813928 86564864 19659 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21134 19659 145 145 0 20989 0
[pid=11524] vsize: 84536
Current children cumulated CPU time (s) 749.02
Current children cumulated vsize (Kb) 86660

[startup+760.082 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21515 0 2 0 75785 115 0 0 25 0 1 0 1851813928 86609920 19670 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21145 19670 145 145 0 21000 0
[pid=11524] vsize: 84580
Current children cumulated CPU time (s) 759.01
Current children cumulated vsize (Kb) 86704

[startup+770.083 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21526 0 2 0 76785 116 0 0 25 0 1 0 1851813928 86654976 19681 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21156 19681 145 145 0 21011 0
[pid=11524] vsize: 84624
Current children cumulated CPU time (s) 769.02
Current children cumulated vsize (Kb) 86748

[startup+780.084 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21543 0 2 0 77785 116 0 0 25 0 1 0 1851813928 86724608 19698 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21173 19698 145 145 0 21028 0
[pid=11524] vsize: 84692
Current children cumulated CPU time (s) 779.02
Current children cumulated vsize (Kb) 86816

[startup+790.084 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21645 0 2 0 78784 117 0 0 25 0 1 0 1851813928 86765568 19709 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21183 19709 145 145 0 21038 0
[pid=11524] vsize: 84732
Current children cumulated CPU time (s) 789.02
Current children cumulated vsize (Kb) 86856

[startup+800.086 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21667 0 2 0 79783 118 0 0 25 0 1 0 1851813928 86855680 19731 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21205 19731 145 145 0 21060 0
[pid=11524] vsize: 84820
Current children cumulated CPU time (s) 799.02
Current children cumulated vsize (Kb) 86944

[startup+810.087 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21680 0 2 0 80784 118 0 0 25 0 1 0 1851813928 86904832 19744 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21217 19744 145 145 0 21072 0
[pid=11524] vsize: 84868
Current children cumulated CPU time (s) 809.03
Current children cumulated vsize (Kb) 86992

[startup+820.087 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21699 0 2 0 81783 118 0 0 25 0 1 0 1851813928 86986752 19763 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21237 19763 145 145 0 21092 0
[pid=11524] vsize: 84948
Current children cumulated CPU time (s) 819.02
Current children cumulated vsize (Kb) 87072

[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21800 0 2 0 82783 119 0 0 25 0 1 0 1851813928 87011328 19772 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21243 19772 145 145 0 21098 0
[pid=11524] vsize: 84972
Current children cumulated CPU time (s) 829.03
Current children cumulated vsize (Kb) 87096

[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21891 0 2 0 83781 119 0 0 25 0 1 0 1851813928 87248896 19830 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21301 19830 145 145 0 21156 0
[pid=11524] vsize: 85204
Current children cumulated CPU time (s) 839.01
Current children cumulated vsize (Kb) 87328

[startup+850.089 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21908 0 2 0 84782 119 0 0 25 0 1 0 1851813928 87318528 19847 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19847 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 849.02
Current children cumulated vsize (Kb) 87396

[startup+860.09 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 85782 119 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 859.02
Current children cumulated vsize (Kb) 87396

[startup+870.09 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 86782 120 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 869.03
Current children cumulated vsize (Kb) 87396

[startup+880.091 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 87782 120 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223056 134562142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 879.03
Current children cumulated vsize (Kb) 87396

[startup+890.091 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21909 0 2 0 88782 120 0 0 25 0 1 0 1851813928 87318528 19848 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19848 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 889.03
Current children cumulated vsize (Kb) 87396

[startup+900.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21910 0 2 0 89782 120 0 0 25 0 1 0 1851813928 87318528 19849 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19849 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 899.03
Current children cumulated vsize (Kb) 87396

[startup+910.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21910 0 2 0 90782 120 0 0 25 0 1 0 1851813928 87318528 19849 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19849 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 909.03
Current children cumulated vsize (Kb) 87396

[startup+920.092 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21910 0 2 0 91782 120 0 0 25 0 1 0 1851813928 87318528 19849 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21318 19849 145 145 0 21173 0
[pid=11524] vsize: 85272
Current children cumulated CPU time (s) 919.03
Current children cumulated vsize (Kb) 87396

[startup+930.093 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21918 0 2 0 92782 120 0 0 25 0 1 0 1851813928 87351296 19857 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21326 19857 145 145 0 21181 0
[pid=11524] vsize: 85304
Current children cumulated CPU time (s) 929.03
Current children cumulated vsize (Kb) 87428

[startup+940.094 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21935 0 2 0 93782 121 0 0 25 0 1 0 1851813928 87416832 19874 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21342 19874 145 145 0 21197 0
[pid=11524] vsize: 85368
Current children cumulated CPU time (s) 939.04
Current children cumulated vsize (Kb) 87492

[startup+950.094 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 21950 0 2 0 94782 121 0 0 25 0 1 0 1851813928 87482368 19889 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21358 19889 145 145 0 21213 0
[pid=11524] vsize: 85432
Current children cumulated CPU time (s) 949.04
Current children cumulated vsize (Kb) 87556

[startup+960.095 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22021 0 2 0 95782 121 0 0 25 0 1 0 1851813928 87609344 19921 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21389 19921 145 145 0 21244 0
[pid=11524] vsize: 85556
Current children cumulated CPU time (s) 959.04
Current children cumulated vsize (Kb) 87680

[startup+970.096 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22054 0 2 0 96781 121 0 0 25 0 1 0 1851813928 87535616 19903 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21371 19903 145 145 0 21226 0
[pid=11524] vsize: 85484
Current children cumulated CPU time (s) 969.03
Current children cumulated vsize (Kb) 87608

[startup+980.097 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22155 0 2 0 97780 122 0 0 25 0 1 0 1851813928 87576576 19913 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21381 19913 145 145 0 21236 0
[pid=11524] vsize: 85524
Current children cumulated CPU time (s) 979.03
Current children cumulated vsize (Kb) 87648

[startup+990.098 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22165 0 2 0 98780 122 0 0 25 0 1 0 1851813928 87613440 19923 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21390 19923 145 145 0 21245 0
[pid=11524] vsize: 85560
Current children cumulated CPU time (s) 989.03
Current children cumulated vsize (Kb) 87684

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22180 0 2 0 99780 122 0 0 25 0 1 0 1851813928 87678976 19938 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21406 19938 145 145 0 21261 0
[pid=11524] vsize: 85624
Current children cumulated CPU time (s) 999.03
Current children cumulated vsize (Kb) 87748

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22194 0 2 0 100780 122 0 0 25 0 1 0 1851813928 87732224 19952 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21419 19952 145 145 0 21274 0
[pid=11524] vsize: 85676
Current children cumulated CPU time (s) 1009.03
Current children cumulated vsize (Kb) 87800

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22209 0 2 0 101780 122 0 0 25 0 1 0 1851813928 87789568 19967 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21433 19967 145 145 0 21288 0
[pid=11524] vsize: 85732
Current children cumulated CPU time (s) 1019.03
Current children cumulated vsize (Kb) 87856

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22222 0 2 0 102780 122 0 0 25 0 1 0 1851813928 87842816 19980 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21446 19980 145 145 0 21301 0
[pid=11524] vsize: 85784
Current children cumulated CPU time (s) 1029.03
Current children cumulated vsize (Kb) 87908

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22236 0 2 0 103780 123 0 0 25 0 1 0 1851813928 87900160 19994 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21460 19994 145 145 0 21315 0
[pid=11524] vsize: 85840
Current children cumulated CPU time (s) 1039.04
Current children cumulated vsize (Kb) 87964

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22251 0 2 0 104780 123 0 0 25 0 1 0 1851813928 87961600 20009 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21475 20009 145 145 0 21330 0
[pid=11524] vsize: 85900
Current children cumulated CPU time (s) 1049.04
Current children cumulated vsize (Kb) 88024

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22295 0 2 0 105780 123 0 0 25 0 1 0 1851813928 88272896 20053 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21551 20053 145 145 0 21406 0
[pid=11524] vsize: 86204
Current children cumulated CPU time (s) 1059.04
Current children cumulated vsize (Kb) 88328

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22295 0 2 0 106781 123 0 0 25 0 1 0 1851813928 88272896 20053 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21551 20053 145 145 0 21406 0
[pid=11524] vsize: 86204
Current children cumulated CPU time (s) 1069.05
Current children cumulated vsize (Kb) 88328

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22295 0 2 0 107781 123 0 0 25 0 1 0 1851813928 88272896 20053 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21551 20053 145 145 0 21406 0
[pid=11524] vsize: 86204
Current children cumulated CPU time (s) 1079.05
Current children cumulated vsize (Kb) 88328

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22300 0 2 0 108781 123 0 0 25 0 1 0 1851813928 88289280 20058 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21555 20058 145 145 0 21410 0
[pid=11524] vsize: 86220
Current children cumulated CPU time (s) 1089.05
Current children cumulated vsize (Kb) 88344

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 11524
Raw data (/proc/11520/stat): 11520 (minisat+_script) S 11519 11520 16528 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1851813923 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11520/statm): 531 226 485 147 0 384 0
[pid=11520] vsize: 2124
Raw data (/proc/11524/stat): 11524 (minisat+_64-bit) R 11520 11520 16528 0 -1 0 22315 0 2 0 109781 123 0 0 25 0 1 0 1851813928 88346624 20073 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11524/statm): 21569 20073 145 145 0 21424 0
[pid=11524] vsize: 86276
Current children cumulated CPU time (s) 1099.05
Current children cumulated vsize (Kb) 88400
One traced child (pid=11524) exited with status: 30
One traced child (pid=11520) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 1109.69
CPU time (s): 1108.66
CPU user time (s): 1107.36
CPU system time (s): 1.3028
CPU usage (%): 99.9071
Max. virtual memory (cumulated for all children) (Kb): 88400

Verifier Data

Verifier:	OK	471047168