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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mod008.opb
MD5SUM581d778a36086562107993896110e0a2
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 361
Optimality of the best value was proved NO
Number of terms in the objective function 319
Biggest coefficient in the objective function 87
Number of bits for the biggest coefficient in the objective function 7
Sum of the numbers in the objective function 23554
Number of bits of the sum of numbers in the objective function 15
Biggest number in a constraint 22000
Number of bits of the biggest number in a constraint 15
Biggest sum of numbers in a constraint 1027256
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.05
Number of variables319
Total number of constraints325
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)319
Number of constraints which are nor clauses,nor cardinality constraints6
Minimum length of a constraint1
Maximum length of a constraint231

Trace number 6236

Launcher Data

LAUNCH ON wulflinc7 THE 2005-09-20 04:43:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3402 boxname=wulflinc7 idbench=1058 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 3402
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906384 kB
Buffers:          8508 kB
Cached:          94584 kB
SwapCached:        744 kB
Active:          26332 kB
Inactive:        79412 kB
HighTotal:      131008 kB
HighFree:        32228 kB
LowTotal:       903652 kB
LowFree:        874156 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            16644 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:03:37 (client local time) WITH STATUS 10 IN 1208.75 SECONDS
stats: 3402 7 1208.75 10

Solver Data

c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> Adder-cost: 2481   maxlim: 21999   bits: 16/15
c ---[   5]---> Adder-cost: 2052   maxlim: 4999   bits: 14/13
c ---[   4]---> Adder-cost: 2306   maxlim: 11999   bits: 15/14
c ---[   2]---> BDD-cost:  478
c ---[   1]---> BDD-cost: 2553
c ---[   0]---> Adder-cost: 1803   maxlim: 3999   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   62010   221290 |   20670       0        0     nan |  0.000 % |
c |       100 |   62010   221290 |   22737     100      343     3.4 |  0.272 % |
c |       251 |   62010   221290 |   25010     251      940     3.7 |  0.272 % |
c |       477 |   62010   221290 |   27511     477     2129     4.5 |  0.272 % |
c |       816 |   62010   221290 |   30262     816    14323    17.6 |  0.272 % |
c |      1323 |   62010   221290 |   33289    1323    19211    14.5 |  0.272 % |
c ==============================================================================
c Found solution: 1989
c ---[   0]---> Sorter-cost:61666     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2068 |  212587   572921 |   70862    2068    31161    15.1 |  0.272 % |
c |      2168 |  212587   572921 |   77948    2168    31706    14.6 |  0.044 % |
c |      2318 |  212587   572921 |   85743    2318    33024    14.2 |  0.044 % |
c |      2544 |  212587   572921 |   94317    2544    44942    17.7 |  0.044 % |
c |      2881 |  212587   572921 |  103749    2881    48764    16.9 |  0.044 % |
c |      3387 |  212587   572921 |  114123    3387    58430    17.3 |  0.044 % |
c |      4146 |  212587   572921 |  125536    4146    66243    16.0 |  0.044 % |
c |      5285 |  212587   572921 |  138089    5285    84457    16.0 |  0.044 % |
c |      6993 |  212587   572921 |  151898    6993   111949    16.0 |  0.044 % |
c |      9555 |  212587   572921 |  167088    9555   195934    20.5 |  0.044 % |
c |     13401 |  212587   572921 |  183797   13401   357669    26.7 |  0.044 % |
c ==============================================================================
c Found solution: 1974
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13769 |  212607   573161 |   70869   13769   383633    27.9 |  0.044 % |
c |     13869 |  212607   573161 |   77955   13869   384775    27.7 |  0.046 % |
c |     14021 |  212607   573161 |   85751   14021   385869    27.5 |  0.046 % |
c |     14246 |  212607   573161 |   94326   14246   394337    27.7 |  0.046 % |
c ==============================================================================
c Found solution: 814
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14260 |  212681   573330 |   70893   14260   394825    27.7 |  0.046 % |
c ==============================================================================
c Found solution: 574
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14279 |  212709   573397 |   70903   14279   395338    27.7 |  0.046 % |
c ==============================================================================
c Found solution: 573
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14286 |  213333   575013 |   71111   14286   396113    27.7 |  0.046 % |
c |     14391 |  213333   575013 |   78222   14391   410775    28.5 |  0.050 % |
c |     14541 |  213333   575013 |   86044   14541   418766    28.8 |  0.050 % |
c |     14767 |  213333   575013 |   94648   14767   425049    28.8 |  0.050 % |
c |     15104 |  213250   574823 |  104113   15041   440754    29.3 |  0.082 % |
c |     15610 |  213250   574823 |  114524   15547   456423    29.4 |  0.082 % |
c |     16371 |  213250   574823 |  125977   16308   475439    29.2 |  0.082 % |
c ==============================================================================
c Found solution: 548
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16771 |  213076   574533 |   71025   16590   503647    30.4 |  0.082 % |
c |     16873 |  213076   574533 |   78127   16692   520097    31.2 |  0.158 % |
c |     17023 |  213076   574533 |   85940   16842   530977    31.5 |  0.158 % |
c |     17248 |  213076   574533 |   94534   17067   535357    31.4 |  0.158 % |
c |     17585 |  212948   574238 |  103987   17398   545681    31.4 |  0.217 % |
c |     18092 |  212758   573802 |  114386   17829   590918    33.1 |  0.297 % |
c |     18851 |  212367   572913 |  125825   18400   651840    35.4 |  0.464 % |
c |     19991 |  212090   572277 |  138407   19470   687672    35.3 |  0.589 % |
c ==============================================================================
c Found solution: 525
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20564 |  212094   572286 |   70698   20043   725393    36.2 |  0.589 % |
c |     20664 |  212094   572286 |   77767   20143   730456    36.3 |  0.591 % |
c |     20815 |  212094   572286 |   85544   20294   776161    38.2 |  0.591 % |
c |     21040 |  212094   572286 |   94099   20519   805956    39.3 |  0.591 % |
c |     21381 |  212074   572241 |  103508   20858   857655    41.1 |  0.598 % |
c |     21887 |  212074   572241 |  113859   21364   927987    43.4 |  0.598 % |
c ==============================================================================
c Found solution: 389
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22374 |  212090   572280 |   70696   21851   967074    44.3 |  0.598 % |
c |     22476 |  212090   572280 |   77765   21953   972904    44.3 |  0.600 % |
c |     22627 |  212090   572280 |   85542   22104  1012989    45.8 |  0.600 % |
c |     22852 |  212090   572280 |   94096   22329  1051720    47.1 |  0.600 % |
c |     23190 |  212090   572280 |  103506   22667  1072607    47.3 |  0.600 % |
c |     23696 |  212090   572280 |  113856   23173  1121981    48.4 |  0.600 % |
c |     24455 |  212090   572280 |  125242   23932  1188663    49.7 |  0.600 % |
c |     25596 |  212090   572280 |  137766   25073  1311227    52.3 |  0.600 % |
c |     27308 |  211704   571405 |  151543   26765  1500814    56.1 |  0.759 % |
c |     29871 |  211704   571405 |  166697   29328  2469277    84.2 |  0.759 % |
c |     33716 |  211704   571405 |  183367   33173  3164018    95.4 |  0.759 % |
c |     39483 |  211084   569990 |  201703   38873  4866988   125.2 |  1.036 % |
c |     48135 |  210928   569631 |  221874   47496  6207615   130.7 |  1.110 % |
c |     61110 |  210871   569502 |  244061   60467  7966433   131.7 |  1.134 % |
c |     80574 |  210871   569502 |  268467   79931 10789561   135.0 |  1.134 % |
c ==============================================================================
c Found solution: 385
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93507 |  210875   569512 |   70291   92864 12122456   130.5 |  1.134 % |
c |     93607 |  210875   569512 |   77320   26188  1518346    58.0 |  1.136 % |
c |     93758 |  210875   569512 |   85052   26339  1522964    57.8 |  1.136 % |
c |     93983 |  210875   569512 |   93557   26564  1531296    57.6 |  1.136 % |
c |     94320 |  210875   569512 |  102913   26901  1590344    59.1 |  1.136 % |
c |     94826 |  210875   569512 |  113204   27407  1653992    60.3 |  1.136 % |
c |     95589 |  210813   569370 |  124524   28168  1742947    61.9 |  1.163 % |
c |     96733 |  210813   569370 |  136977   29312  1979284    67.5 |  1.163 % |
c |     98441 |  210813   569370 |  150675   31020  2403707    77.5 |  1.163 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 -C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 -C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 -C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 -C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 -C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 -C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 -C189_0x2e__bit0 -C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 -C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -

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/10556/stat): 10556 (minisat+_script) R 10555 10556 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797544617 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/10556/statm): 174 3 169 147 0 27 0
[pid=10556] 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=10557
New process pid=10558
New process pid=10559
One traced child (pid=10558) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=10559) exited with status: 0
One traced child (pid=10557) exited with status: 0
New process pid=10560
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-mod008.opb

[startup+10.0036 s]
Raw data (loadavg): 0.87 0.94 0.90 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 4707 0 0 0 971 14 0 0 25 0 1 0 1797544622 5906432 1286 4294967295 134512640 135094434 3221224432 3221221280 134676552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 1442 1286 145 145 0 1297 0
[pid=10560] vsize: 5768
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 7892

[startup+20.0043 s]
Raw data (loadavg): 0.89 0.94 0.90 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9625 0 0 0 1932 32 0 0 25 0 1 0 1797544622 28651520 5736 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 6995 5736 145 145 0 6850 0
[pid=10560] vsize: 27980
Current children cumulated CPU time (s) 19.64
Current children cumulated vsize (Kb) 30104

[startup+30.0059 s]
Raw data (loadavg): 0.91 0.94 0.90 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9680 0 0 0 2930 33 0 0 25 0 1 0 1797544622 28823552 5791 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7037 5791 145 145 0 6892 0
[pid=10560] vsize: 28148
Current children cumulated CPU time (s) 29.63
Current children cumulated vsize (Kb) 30272

[startup+40.0065 s]
Raw data (loadavg): 0.92 0.94 0.90 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9815 0 0 0 3927 34 0 0 25 0 1 0 1797544622 29360128 5926 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7168 5926 145 145 0 7023 0
[pid=10560] vsize: 28672
Current children cumulated CPU time (s) 39.61
Current children cumulated vsize (Kb) 30796

[startup+50.0081 s]
Raw data (loadavg): 0.93 0.94 0.90 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9969 0 0 0 4924 35 0 0 25 0 1 0 1797544622 29970432 6080 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7317 6080 145 145 0 7172 0
[pid=10560] vsize: 29268
Current children cumulated CPU time (s) 49.59
Current children cumulated vsize (Kb) 31392

[startup+60.0088 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10242 0 0 0 5921 37 0 0 25 0 1 0 1797544622 30896128 6311 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7543 6311 145 145 0 7398 0
[pid=10560] vsize: 30172
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 32296

[startup+70.0094 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10263 0 0 0 6921 38 0 0 25 0 1 0 1797544622 30978048 6332 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7563 6332 145 145 0 7418 0
[pid=10560] vsize: 30252
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 32376

[startup+80.011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10309 0 0 0 7920 38 0 0 25 0 1 0 1797544622 31227904 6378 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7624 6378 145 145 0 7479 0
[pid=10560] vsize: 30496
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 32620

[startup+90.0117 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10424 0 0 0 8918 39 0 0 25 0 1 0 1797544622 31424512 6428 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7672 6428 145 145 0 7527 0
[pid=10560] vsize: 30688
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 32812

[startup+100.012 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10494 0 0 0 9917 40 0 0 25 0 1 0 1797544622 31715328 6498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 7743 6498 145 145 0 7598 0
[pid=10560] vsize: 30972
Current children cumulated CPU time (s) 99.57
Current children cumulated vsize (Kb) 33096

[startup+110.014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10584 0 0 0 10915 41 0 0 25 0 1 0 1797544622 32079872 6588 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 7832 6588 145 145 0 7687 0
[pid=10560] vsize: 31328
Current children cumulated CPU time (s) 109.56
Current children cumulated vsize (Kb) 33452

[startup+120.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10849 0 0 0 11912 43 0 0 25 0 1 0 1797544622 32632832 6726 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 7967 6726 145 145 0 7822 0
[pid=10560] vsize: 31868
Current children cumulated CPU time (s) 119.55
Current children cumulated vsize (Kb) 33992

[startup+130.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11014 0 0 0 12909 44 0 0 25 0 1 0 1797544622 33361920 6891 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 8145 6891 145 145 0 8000 0
[pid=10560] vsize: 32580
Current children cumulated CPU time (s) 129.53
Current children cumulated vsize (Kb) 34704

[startup+140.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11236 0 0 0 13906 46 0 0 25 0 1 0 1797544622 34000896 7049 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 8301 7049 145 145 0 8156 0
[pid=10560] vsize: 33204
Current children cumulated CPU time (s) 139.52
Current children cumulated vsize (Kb) 35328

[startup+150.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11292 0 0 0 14905 47 0 0 25 0 1 0 1797544622 34226176 7105 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 8356 7105 145 145 0 8211 0
[pid=10560] vsize: 33424
Current children cumulated CPU time (s) 149.52
Current children cumulated vsize (Kb) 35548

[startup+160.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11399 0 0 0 15903 47 0 0 25 0 1 0 1797544622 34660352 7212 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 8462 7212 145 145 0 8317 0
[pid=10560] vsize: 33848
Current children cumulated CPU time (s) 159.5
Current children cumulated vsize (Kb) 35972

[startup+170.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11463 0 0 0 16902 48 0 0 25 0 1 0 1797544622 34922496 7276 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 8526 7276 145 145 0 8381 0
[pid=10560] vsize: 34104
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 36228

[startup+180.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11514 0 0 0 17902 48 0 0 25 0 1 0 1797544622 35090432 7327 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 8567 7327 145 145 0 8422 0
[pid=10560] vsize: 34268
Current children cumulated CPU time (s) 179.5
Current children cumulated vsize (Kb) 36392

[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11685 0 0 0 18900 49 0 0 25 0 1 0 1797544622 35786752 7498 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 8737 7498 145 145 0 8592 0
[pid=10560] vsize: 34948
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 37072

[startup+200.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11888 0 0 0 19897 51 0 0 25 0 1 0 1797544622 36614144 7701 4294967295 134512640 135094434 3221224432 3221223024 134557044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 8939 7701 145 145 0 8794 0
[pid=10560] vsize: 35756
Current children cumulated CPU time (s) 199.48
Current children cumulated vsize (Kb) 37880

[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 12190 0 0 0 20892 53 0 0 25 0 1 0 1797544622 37847040 8003 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 9240 8003 145 145 0 9095 0
[pid=10560] vsize: 36960
Current children cumulated CPU time (s) 209.45
Current children cumulated vsize (Kb) 39084

[startup+220.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 12679 0 0 0 21885 56 0 0 25 0 1 0 1797544622 39845888 8492 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 9728 8492 145 145 0 9583 0
[pid=10560] vsize: 38912
Current children cumulated CPU time (s) 219.41
Current children cumulated vsize (Kb) 41036

[startup+230.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 12869 0 0 0 22882 57 0 0 25 0 1 0 1797544622 40620032 8682 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10560/statm): 9917 8682 145 145 0 9772 0
[pid=10560] vsize: 39668
Current children cumulated CPU time (s) 229.39
Current children cumulated vsize (Kb) 41792

[startup+240.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13238 0 0 0 23874 60 0 0 25 0 1 0 1797544622 42127360 9051 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 10285 9051 145 145 0 10140 0
[pid=10560] vsize: 41140
Current children cumulated CPU time (s) 239.34
Current children cumulated vsize (Kb) 43264

[startup+250.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13391 0 0 0 24873 61 0 0 25 0 1 0 1797544622 42881024 9204 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 10469 9204 145 145 0 10324 0
[pid=10560] vsize: 41876
Current children cumulated CPU time (s) 249.34
Current children cumulated vsize (Kb) 44000

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13600 0 0 0 25869 62 0 0 25 0 1 0 1797544622 43732992 9413 4294967295 134512640 135094434 3221224432 3221223128 134784927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 10677 9413 145 145 0 10532 0
[pid=10560] vsize: 42708
Current children cumulated CPU time (s) 259.31
Current children cumulated vsize (Kb) 44832

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13903 0 0 0 26865 64 0 0 25 0 1 0 1797544622 44969984 9716 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 10979 9716 145 145 0 10834 0
[pid=10560] vsize: 43916
Current children cumulated CPU time (s) 269.29
Current children cumulated vsize (Kb) 46040

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14134 0 0 0 27863 66 0 0 25 0 1 0 1797544622 45912064 9947 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 11209 9947 145 145 0 11064 0
[pid=10560] vsize: 44836
Current children cumulated CPU time (s) 279.29
Current children cumulated vsize (Kb) 46960

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14427 0 0 0 28859 68 0 0 25 0 1 0 1797544622 47108096 10240 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 11501 10240 145 145 0 11356 0
[pid=10560] vsize: 46004
Current children cumulated CPU time (s) 289.27
Current children cumulated vsize (Kb) 48128

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14585 0 0 0 29857 68 0 0 25 0 1 0 1797544622 47755264 10398 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 11659 10398 145 145 0 11514 0
[pid=10560] vsize: 46636
Current children cumulated CPU time (s) 299.25
Current children cumulated vsize (Kb) 48760

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14880 0 0 0 30853 70 0 0 25 0 1 0 1797544622 48951296 10693 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 11951 10693 145 145 0 11806 0
[pid=10560] vsize: 47804
Current children cumulated CPU time (s) 309.23
Current children cumulated vsize (Kb) 49928

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15085 0 0 0 31851 71 0 0 25 0 1 0 1797544622 49790976 10898 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 12156 10898 145 145 0 12011 0
[pid=10560] vsize: 48624
Current children cumulated CPU time (s) 319.22
Current children cumulated vsize (Kb) 50748

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15287 0 0 0 32847 72 0 0 25 0 1 0 1797544622 50610176 11100 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 12356 11100 145 145 0 12211 0
[pid=10560] vsize: 49424
Current children cumulated CPU time (s) 329.19
Current children cumulated vsize (Kb) 51548

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15499 0 0 0 33845 73 0 0 25 0 1 0 1797544622 51474432 11312 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 12567 11312 145 145 0 12422 0
[pid=10560] vsize: 50268
Current children cumulated CPU time (s) 339.18
Current children cumulated vsize (Kb) 52392

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15746 0 0 0 34840 75 0 0 25 0 1 0 1797544622 52477952 11559 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 12812 11559 145 145 0 12667 0
[pid=10560] vsize: 51248
Current children cumulated CPU time (s) 349.15
Current children cumulated vsize (Kb) 53372

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15900 0 0 0 35836 77 0 0 25 0 1 0 1797544622 53104640 11713 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 12965 11713 145 145 0 12820 0
[pid=10560] vsize: 51860
Current children cumulated CPU time (s) 359.13
Current children cumulated vsize (Kb) 53984

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16107 0 0 0 36833 79 0 0 25 0 1 0 1797544622 53948416 11920 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 13171 11920 145 145 0 13026 0
[pid=10560] vsize: 52684
Current children cumulated CPU time (s) 369.12
Current children cumulated vsize (Kb) 54808

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16320 0 0 0 37831 80 0 0 25 0 1 0 1797544622 54816768 12133 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 13383 12133 145 145 0 13238 0
[pid=10560] vsize: 53532
Current children cumulated CPU time (s) 379.11
Current children cumulated vsize (Kb) 55656

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16474 0 0 0 38829 81 0 0 25 0 1 0 1797544622 55447552 12287 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 13537 12287 145 145 0 13392 0
[pid=10560] vsize: 54148
Current children cumulated CPU time (s) 389.1
Current children cumulated vsize (Kb) 56272

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16720 0 0 0 39826 83 0 0 25 0 1 0 1797544622 56446976 12533 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 13781 12533 145 145 0 13636 0
[pid=10560] vsize: 55124
Current children cumulated CPU time (s) 399.09
Current children cumulated vsize (Kb) 57248

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16962 0 0 0 40821 85 0 0 25 0 1 0 1797544622 57434112 12775 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 14022 12775 145 145 0 13877 0
[pid=10560] vsize: 56088
Current children cumulated CPU time (s) 409.06
Current children cumulated vsize (Kb) 58212

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17153 0 0 0 41818 86 0 0 25 0 1 0 1797544622 58208256 12966 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 14211 12966 145 145 0 14066 0
[pid=10560] vsize: 56844
Current children cumulated CPU time (s) 419.04
Current children cumulated vsize (Kb) 58968

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) T 10556 10556 15400 0 -1 0 17195 0 0 0 42818 86 0 0 25 0 1 0 1797544622 58376192 13008 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/10560/statm): 14252 13008 145 145 0 14107 0
[pid=10560] vsize: 57008
Current children cumulated CPU time (s) 429.04
Current children cumulated vsize (Kb) 59132

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17412 0 0 0 43815 87 0 0 25 0 1 0 1797544622 59260928 13225 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 14468 13225 145 145 0 14323 0
[pid=10560] vsize: 57872
Current children cumulated CPU time (s) 439.02
Current children cumulated vsize (Kb) 59996

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17634 0 0 0 44810 89 0 0 25 0 1 0 1797544622 60162048 13447 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 14688 13447 145 145 0 14543 0
[pid=10560] vsize: 58752
Current children cumulated CPU time (s) 448.99
Current children cumulated vsize (Kb) 60876

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17959 0 0 0 45806 90 0 0 25 0 1 0 1797544622 61485056 13772 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 15011 13772 145 145 0 14866 0
[pid=10560] vsize: 60044
Current children cumulated CPU time (s) 458.96
Current children cumulated vsize (Kb) 62168

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18242 0 0 0 46801 92 0 0 25 0 1 0 1797544622 62640128 14055 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 15293 14055 145 145 0 15148 0
[pid=10560] vsize: 61172
Current children cumulated CPU time (s) 468.93
Current children cumulated vsize (Kb) 63296

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18477 0 0 0 47797 94 0 0 25 0 1 0 1797544622 63598592 14290 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 15527 14290 145 145 0 15382 0
[pid=10560] vsize: 62108
Current children cumulated CPU time (s) 478.91
Current children cumulated vsize (Kb) 64232

[startup+490.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18532 0 0 0 48796 95 0 0 25 0 1 0 1797544622 63819776 14345 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 15581 14345 145 145 0 15436 0
[pid=10560] vsize: 62324
Current children cumulated CPU time (s) 488.91
Current children cumulated vsize (Kb) 64448

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18708 0 0 0 49794 96 0 0 25 0 1 0 1797544622 64536576 14521 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 15756 14521 145 145 0 15611 0
[pid=10560] vsize: 63024
Current children cumulated CPU time (s) 498.9
Current children cumulated vsize (Kb) 65148

[startup+510.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18958 0 0 0 50790 97 0 0 25 0 1 0 1797544622 65556480 14771 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16005 14771 145 145 0 15860 0
[pid=10560] vsize: 64020
Current children cumulated CPU time (s) 508.87
Current children cumulated vsize (Kb) 66144

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19096 0 0 0 51787 99 0 0 25 0 1 0 1797544622 66117632 14909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16142 14909 145 145 0 15997 0
[pid=10560] vsize: 64568
Current children cumulated CPU time (s) 518.86
Current children cumulated vsize (Kb) 66692

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19223 0 0 0 52785 101 0 0 25 0 1 0 1797544622 67006464 15036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16359 15036 145 145 0 16214 0
[pid=10560] vsize: 65436
Current children cumulated CPU time (s) 528.86
Current children cumulated vsize (Kb) 67560

[startup+540.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19290 0 0 0 53785 101 0 0 25 0 1 0 1797544622 67289088 15103 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16428 15103 145 145 0 16283 0
[pid=10560] vsize: 65712
Current children cumulated CPU time (s) 538.86
Current children cumulated vsize (Kb) 67836

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19407 0 0 0 54784 102 0 0 25 0 1 0 1797544622 67760128 15220 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16543 15220 145 145 0 16398 0
[pid=10560] vsize: 66172
Current children cumulated CPU time (s) 548.86
Current children cumulated vsize (Kb) 68296

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19560 0 0 0 55783 102 0 0 25 0 1 0 1797544622 68378624 15373 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16694 15373 145 145 0 16549 0
[pid=10560] vsize: 66776
Current children cumulated CPU time (s) 558.85
Current children cumulated vsize (Kb) 68900

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19633 0 0 0 56781 103 0 0 25 0 1 0 1797544622 68673536 15446 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16766 15446 145 145 0 16621 0
[pid=10560] vsize: 67064
Current children cumulated CPU time (s) 568.84
Current children cumulated vsize (Kb) 69188

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19675 0 0 0 57781 103 0 0 25 0 1 0 1797544622 68845568 15488 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16808 15488 145 145 0 16663 0
[pid=10560] vsize: 67232
Current children cumulated CPU time (s) 578.84
Current children cumulated vsize (Kb) 69356

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19713 0 0 0 58781 103 0 0 25 0 1 0 1797544622 69001216 15526 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16846 15526 145 145 0 16701 0
[pid=10560] vsize: 67384
Current children cumulated CPU time (s) 588.84
Current children cumulated vsize (Kb) 69508

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19809 0 0 0 59780 104 0 0 25 0 1 0 1797544622 69394432 15622 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 16942 15622 145 145 0 16797 0
[pid=10560] vsize: 67768
Current children cumulated CPU time (s) 598.84
Current children cumulated vsize (Kb) 69892

[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19930 0 0 0 60778 104 0 0 25 0 1 0 1797544622 69885952 15743 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17062 15743 145 145 0 16917 0
[pid=10560] vsize: 68248
Current children cumulated CPU time (s) 608.82
Current children cumulated vsize (Kb) 70372

[startup+620.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20024 0 0 0 61777 105 0 0 25 0 1 0 1797544622 70275072 15837 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17157 15837 145 145 0 17012 0
[pid=10560] vsize: 68628
Current children cumulated CPU time (s) 618.82
Current children cumulated vsize (Kb) 70752

[startup+630.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20130 0 0 0 62776 105 0 0 25 0 1 0 1797544622 70701056 15943 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17261 15943 145 145 0 17116 0
[pid=10560] vsize: 69044
Current children cumulated CPU time (s) 628.81
Current children cumulated vsize (Kb) 71168

[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20237 0 0 0 63774 106 0 0 25 0 1 0 1797544622 71135232 16050 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17367 16050 145 145 0 17222 0
[pid=10560] vsize: 69468
Current children cumulated CPU time (s) 638.8
Current children cumulated vsize (Kb) 71592

[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20344 0 0 0 64773 107 0 0 25 0 1 0 1797544622 71581696 16157 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17476 16157 145 145 0 17331 0
[pid=10560] vsize: 69904
Current children cumulated CPU time (s) 648.8
Current children cumulated vsize (Kb) 72028

[startup+660.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20454 0 0 0 65771 107 0 0 25 0 1 0 1797544622 72019968 16267 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17583 16267 145 145 0 17438 0
[pid=10560] vsize: 70332
Current children cumulated CPU time (s) 658.78
Current children cumulated vsize (Kb) 72456

[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20551 0 0 0 66770 108 0 0 25 0 1 0 1797544622 72417280 16364 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17680 16364 145 145 0 17535 0
[pid=10560] vsize: 70720
Current children cumulated CPU time (s) 668.78
Current children cumulated vsize (Kb) 72844

[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20666 0 0 0 67768 109 0 0 25 0 1 0 1797544622 72884224 16479 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17794 16479 145 145 0 17649 0
[pid=10560] vsize: 71176
Current children cumulated CPU time (s) 678.77
Current children cumulated vsize (Kb) 73300

[startup+690.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20715 0 0 0 68768 109 0 0 25 0 1 0 1797544622 73084928 16528 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17843 16528 145 145 0 17698 0
[pid=10560] vsize: 71372
Current children cumulated CPU time (s) 688.77
Current children cumulated vsize (Kb) 73496

[startup+700.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20767 0 0 0 69768 109 0 0 25 0 1 0 1797544622 73297920 16580 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17895 16580 145 145 0 17750 0
[pid=10560] vsize: 71580
Current children cumulated CPU time (s) 698.77
Current children cumulated vsize (Kb) 73704

[startup+710.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20836 0 0 0 70767 109 0 0 25 0 1 0 1797544622 73572352 16649 4294967295 134512640 135094434 3221224432 3221223024 134557345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 17962 16649 145 145 0 17817 0
[pid=10560] vsize: 71848
Current children cumulated CPU time (s) 708.76
Current children cumulated vsize (Kb) 73972

[startup+720.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20957 0 0 0 71765 110 0 0 25 0 1 0 1797544622 74063872 16770 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18082 16770 145 145 0 17937 0
[pid=10560] vsize: 72328
Current children cumulated CPU time (s) 718.75
Current children cumulated vsize (Kb) 74452

[startup+730.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21063 0 0 0 72763 111 0 0 25 0 1 0 1797544622 74498048 16876 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18188 16876 145 145 0 18043 0
[pid=10560] vsize: 72752
Current children cumulated CPU time (s) 728.74
Current children cumulated vsize (Kb) 74876

[startup+740.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21187 0 0 0 73761 112 0 0 25 0 1 0 1797544622 75001856 17000 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18311 17000 145 145 0 18166 0
[pid=10560] vsize: 73244
Current children cumulated CPU time (s) 738.73
Current children cumulated vsize (Kb) 75368

[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21267 0 0 0 74759 113 0 0 25 0 1 0 1797544622 75329536 17080 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18391 17080 145 145 0 18246 0
[pid=10560] vsize: 73564
Current children cumulated CPU time (s) 748.72
Current children cumulated vsize (Kb) 75688

[startup+760.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21333 0 0 0 75759 113 0 0 25 0 1 0 1797544622 75603968 17146 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18458 17146 145 145 0 18313 0
[pid=10560] vsize: 73832
Current children cumulated CPU time (s) 758.72
Current children cumulated vsize (Kb) 75956

[startup+770.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21459 0 0 0 76758 114 0 0 25 0 1 0 1797544622 76124160 17272 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18585 17272 145 145 0 18440 0
[pid=10560] vsize: 74340
Current children cumulated CPU time (s) 768.72
Current children cumulated vsize (Kb) 76464

[startup+780.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21528 0 0 0 77756 114 0 0 25 0 1 0 1797544622 76414976 17341 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18656 17341 145 145 0 18511 0
[pid=10560] vsize: 74624
Current children cumulated CPU time (s) 778.7
Current children cumulated vsize (Kb) 76748

[startup+790.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21569 0 0 0 78756 114 0 0 25 0 1 0 1797544622 76582912 17382 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18697 17382 145 145 0 18552 0
[pid=10560] vsize: 74788
Current children cumulated CPU time (s) 788.7
Current children cumulated vsize (Kb) 76912

[startup+800.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21615 0 0 0 79756 115 0 0 25 0 1 0 1797544622 76771328 17428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18743 17428 145 145 0 18598 0
[pid=10560] vsize: 74972
Current children cumulated CPU time (s) 798.71
Current children cumulated vsize (Kb) 77096

[startup+810.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21644 0 0 0 80755 115 0 0 25 0 1 0 1797544622 76886016 17457 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18771 17457 145 145 0 18626 0
[pid=10560] vsize: 75084
Current children cumulated CPU time (s) 808.7
Current children cumulated vsize (Kb) 77208

[startup+820.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21675 0 0 0 81755 115 0 0 25 0 1 0 1797544622 77017088 17488 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18803 17488 145 145 0 18658 0
[pid=10560] vsize: 75212
Current children cumulated CPU time (s) 818.7
Current children cumulated vsize (Kb) 77336

[startup+830.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21689 0 0 0 82755 115 0 0 25 0 1 0 1797544622 77070336 17502 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18816 17502 145 145 0 18671 0
[pid=10560] vsize: 75264
Current children cumulated CPU time (s) 828.7
Current children cumulated vsize (Kb) 77388

[startup+840.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21704 0 0 0 83755 115 0 0 25 0 1 0 1797544622 77127680 17517 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18830 17517 145 145 0 18685 0
[pid=10560] vsize: 75320
Current children cumulated CPU time (s) 838.7
Current children cumulated vsize (Kb) 77444

[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21731 0 0 0 84755 116 0 0 25 0 1 0 1797544622 77238272 17544 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18857 17544 145 145 0 18712 0
[pid=10560] vsize: 75428
Current children cumulated CPU time (s) 848.71
Current children cumulated vsize (Kb) 77552

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21756 0 0 0 85755 116 0 0 25 0 1 0 1797544622 77336576 17569 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18881 17569 145 145 0 18736 0
[pid=10560] vsize: 75524
Current children cumulated CPU time (s) 858.71
Current children cumulated vsize (Kb) 77648

[startup+870.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21774 0 0 0 86755 116 0 0 25 0 1 0 1797544622 77410304 17587 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18899 17587 145 145 0 18754 0
[pid=10560] vsize: 75596
Current children cumulated CPU time (s) 868.71
Current children cumulated vsize (Kb) 77720

[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21795 0 0 0 87756 116 0 0 25 0 1 0 1797544622 77496320 17608 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18920 17608 145 145 0 18775 0
[pid=10560] vsize: 75680
Current children cumulated CPU time (s) 878.72
Current children cumulated vsize (Kb) 77804

[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21825 0 0 0 88755 116 0 0 25 0 1 0 1797544622 77623296 17638 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18951 17638 145 145 0 18806 0
[pid=10560] vsize: 75804
Current children cumulated CPU time (s) 888.71
Current children cumulated vsize (Kb) 77928

[startup+900.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21854 0 0 0 89755 116 0 0 25 0 1 0 1797544622 77737984 17667 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18979 17667 145 145 0 18834 0
[pid=10560] vsize: 75916
Current children cumulated CPU time (s) 898.71
Current children cumulated vsize (Kb) 78040

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21871 0 0 0 90755 116 0 0 25 0 1 0 1797544622 77807616 17684 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 18996 17684 145 145 0 18851 0
[pid=10560] vsize: 75984
Current children cumulated CPU time (s) 908.71
Current children cumulated vsize (Kb) 78108

[startup+920.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21893 0 0 0 91754 116 0 0 25 0 1 0 1797544622 77897728 17706 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19018 17706 145 145 0 18873 0
[pid=10560] vsize: 76072
Current children cumulated CPU time (s) 918.7
Current children cumulated vsize (Kb) 78196

[startup+930.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21938 0 0 0 92754 117 0 0 25 0 1 0 1797544622 78077952 17751 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19062 17751 145 145 0 18917 0
[pid=10560] vsize: 76248
Current children cumulated CPU time (s) 928.71
Current children cumulated vsize (Kb) 78372

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21970 0 0 0 93754 117 0 0 25 0 1 0 1797544622 78213120 17783 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19095 17783 145 145 0 18950 0
[pid=10560] vsize: 76380
Current children cumulated CPU time (s) 938.71
Current children cumulated vsize (Kb) 78504

[startup+950.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21997 0 0 0 94753 117 0 0 25 0 1 0 1797544622 78323712 17810 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19122 17810 145 145 0 18977 0
[pid=10560] vsize: 76488
Current children cumulated CPU time (s) 948.7
Current children cumulated vsize (Kb) 78612

[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22032 0 0 0 95753 117 0 0 25 0 1 0 1797544622 78462976 17845 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19156 17845 145 145 0 19011 0
[pid=10560] vsize: 76624
Current children cumulated CPU time (s) 958.7
Current children cumulated vsize (Kb) 78748

[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22053 0 0 0 96753 117 0 0 25 0 1 0 1797544622 78548992 17866 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19177 17866 145 145 0 19032 0
[pid=10560] vsize: 76708
Current children cumulated CPU time (s) 968.7
Current children cumulated vsize (Kb) 78832

[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22079 0 0 0 97753 117 0 0 25 0 1 0 1797544622 78651392 17892 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19202 17892 145 145 0 19057 0
[pid=10560] vsize: 76808
Current children cumulated CPU time (s) 978.7
Current children cumulated vsize (Kb) 78932

[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22105 0 0 0 98753 118 0 0 25 0 1 0 1797544622 78757888 17918 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19228 17918 145 145 0 19083 0
[pid=10560] vsize: 76912
Current children cumulated CPU time (s) 988.71
Current children cumulated vsize (Kb) 79036

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22125 0 0 0 99753 118 0 0 25 0 1 0 1797544622 78839808 17938 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19248 17938 145 145 0 19103 0
[pid=10560] vsize: 76992
Current children cumulated CPU time (s) 998.71
Current children cumulated vsize (Kb) 79116

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22145 0 0 0 100753 118 0 0 25 0 1 0 1797544622 78921728 17958 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19268 17958 145 145 0 19123 0
[pid=10560] vsize: 77072
Current children cumulated CPU time (s) 1008.71
Current children cumulated vsize (Kb) 79196

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22207 0 0 0 101752 118 0 0 25 0 1 0 1797544622 79167488 18020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19328 18020 145 145 0 19183 0
[pid=10560] vsize: 77312
Current children cumulated CPU time (s) 1018.7
Current children cumulated vsize (Kb) 79436

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22329 0 0 0 102751 120 0 0 25 0 1 0 1797544622 79667200 18142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19450 18142 145 145 0 19305 0
[pid=10560] vsize: 77800
Current children cumulated CPU time (s) 1028.71
Current children cumulated vsize (Kb) 79924

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22426 0 0 0 103750 120 0 0 25 0 1 0 1797544622 80064512 18239 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19547 18239 145 145 0 19402 0
[pid=10560] vsize: 78188
Current children cumulated CPU time (s) 1038.7
Current children cumulated vsize (Kb) 80312

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22513 0 0 0 104749 121 0 0 25 0 1 0 1797544622 80416768 18326 4294967295 134512640 135094434 3221224432 3221223024 134557018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19633 18326 145 145 0 19488 0
[pid=10560] vsize: 78532
Current children cumulated CPU time (s) 1048.7
Current children cumulated vsize (Kb) 80656

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22601 0 0 0 105749 121 0 0 25 0 1 0 1797544622 80785408 18414 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19723 18414 145 145 0 19578 0
[pid=10560] vsize: 78892
Current children cumulated CPU time (s) 1058.7
Current children cumulated vsize (Kb) 81016

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22692 0 0 0 106747 122 0 0 25 0 1 0 1797544622 81149952 18505 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19812 18505 145 145 0 19667 0
[pid=10560] vsize: 79248
Current children cumulated CPU time (s) 1068.69
Current children cumulated vsize (Kb) 81372

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22764 0 0 0 107747 122 0 0 25 0 1 0 1797544622 81457152 18577 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19887 18577 145 145 0 19742 0
[pid=10560] vsize: 79548
Current children cumulated CPU time (s) 1078.69
Current children cumulated vsize (Kb) 81672

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22853 0 0 0 108746 123 0 0 25 0 1 0 1797544622 81829888 18666 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 19978 18666 145 145 0 19833 0
[pid=10560] vsize: 79912
Current children cumulated CPU time (s) 1088.69
Current children cumulated vsize (Kb) 82036

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22913 0 0 0 109746 123 0 0 25 0 1 0 1797544622 82063360 18726 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20035 18726 145 145 0 19890 0
[pid=10560] vsize: 80140
Current children cumulated CPU time (s) 1098.69
Current children cumulated vsize (Kb) 82264

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23003 0 0 0 110745 124 0 0 25 0 1 0 1797544622 82427904 18816 4294967295 134512640 135094434 3221224432 3221223104 134555547 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20124 18816 145 145 0 19979 0
[pid=10560] vsize: 80496
Current children cumulated CPU time (s) 1108.69
Current children cumulated vsize (Kb) 82620

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 111743 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1118.68
Current children cumulated vsize (Kb) 82748

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 112744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1128.69
Current children cumulated vsize (Kb) 82748

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 113744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1138.69
Current children cumulated vsize (Kb) 82748

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 114744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1148.69
Current children cumulated vsize (Kb) 82748

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 115744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1158.69
Current children cumulated vsize (Kb) 82748

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 116745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1168.7
Current children cumulated vsize (Kb) 82748

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 117745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1178.7
Current children cumulated vsize (Kb) 82748

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 118745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1188.7
Current children cumulated vsize (Kb) 82748

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 119745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1198.7
Current children cumulated vsize (Kb) 82748

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 120745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1208.7
Current children cumulated vsize (Kb) 82748



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 10560
Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/10556/statm): 531 226 485 147 0 384 0
[pid=10556] vsize: 2124
Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 120746 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0
[pid=10560] vsize: 80624
Current children cumulated CPU time (s) 1208.71
Current children cumulated vsize (Kb) 82748

Sending SIGTERM to -10556
Sleeping 2 seconds
One traced child (pid=10556) ended because it received signal 15 (SIGTERM)
One traced child (pid=10560) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.75
CPU user time (s): 1207.46
CPU system time (s): 1.2898
CPU usage (%): 99.8851
Max. virtual memory (cumulated for all children) (Kb): 82748

Verifier Data

ERROR: no interpretation found !