Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod008.opb
MD5SUMfbdb3cf321a85412feefcaac30780520
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.06
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 3872

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        881536 kB
Buffers:         39604 kB
Cached:          73616 kB
SwapCached:        544 kB
Active:          70608 kB
Inactive:        54860 kB
HighTotal:      131008 kB
HighFree:        57372 kB
LowTotal:       903652 kB
LowFree:        824164 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22192 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:33:16 (client local time) WITH STATUS 10 IN 1208.76 SECONDS
stats: 2868 7 1208.76 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/29309/stat): 29309 (minisat+_script) R 29308 29309 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788325283 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/29309/statm): 174 3 169 147 0 27 0
[pid=29309] 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=29310
New process pid=29311
New process pid=29312
execve syscall for /bin/sed executable
One traced child (pid=29311) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=29312) exited with status: 0
One traced child (pid=29310) exited with status: 0
New process pid=29313
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-mod008.opb

[startup+10.0036 s]
Raw data (loadavg): 0.96 1.08 1.05 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 4707 0 0 0 970 14 0 0 25 0 1 0 1788325288 5906432 1286 4294967295 134512640 135094434 3221224432 3221221728 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 1442 1286 145 145 0 1297 0
[pid=29313] vsize: 5768
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 7892

[startup+20.0045 s]
Raw data (loadavg): 0.97 1.08 1.05 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9625 0 0 0 1934 33 0 0 25 0 1 0 1788325288 28651520 5736 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 6995 5736 145 145 0 6850 0
[pid=29313] vsize: 27980
Current children cumulated CPU time (s) 19.68
Current children cumulated vsize (Kb) 30104

[startup+30.0053 s]
Raw data (loadavg): 0.97 1.07 1.05 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9682 0 0 0 2932 33 0 0 25 0 1 0 1788325288 28831744 5793 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7039 5793 145 145 0 6894 0
[pid=29313] vsize: 28156
Current children cumulated CPU time (s) 29.66
Current children cumulated vsize (Kb) 30280

[startup+40.0072 s]
Raw data (loadavg): 0.98 1.07 1.05 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9818 0 0 0 3929 35 0 0 25 0 1 0 1788325288 29372416 5929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7171 5929 145 145 0 7026 0
[pid=29313] vsize: 28684
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 30808

[startup+50.008 s]
Raw data (loadavg): 0.98 1.07 1.05 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9976 0 0 0 4926 36 0 0 25 0 1 0 1788325288 29999104 6087 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7324 6087 145 145 0 7179 0
[pid=29313] vsize: 29296
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 31420

[startup+60.0088 s]
Raw data (loadavg): 0.98 1.06 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10242 0 0 0 5924 36 0 0 25 0 1 0 1788325288 30896128 6311 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7543 6311 145 145 0 7398 0
[pid=29313] vsize: 30172
Current children cumulated CPU time (s) 59.61
Current children cumulated vsize (Kb) 32296

[startup+70.0107 s]
Raw data (loadavg): 0.98 1.06 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10264 0 0 0 6925 36 0 0 25 0 1 0 1788325288 30982144 6333 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7564 6333 145 145 0 7419 0
[pid=29313] vsize: 30256
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 32380

[startup+80.0115 s]
Raw data (loadavg): 0.99 1.06 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10309 0 0 0 7924 37 0 0 25 0 1 0 1788325288 31227904 6378 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 7624 6378 145 145 0 7479 0
[pid=29313] vsize: 30496
Current children cumulated CPU time (s) 79.62
Current children cumulated vsize (Kb) 32620

[startup+90.0134 s]
Raw data (loadavg): 0.99 1.06 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10424 0 0 0 8923 38 0 0 25 0 1 0 1788325288 31424512 6428 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7672 6428 145 145 0 7527 0
[pid=29313] vsize: 30688
Current children cumulated CPU time (s) 89.62
Current children cumulated vsize (Kb) 32812

[startup+100.014 s]
Raw data (loadavg): 0.99 1.05 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10496 0 0 0 9922 38 0 0 25 0 1 0 1788325288 31723520 6500 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7745 6500 145 145 0 7600 0
[pid=29313] vsize: 30980
Current children cumulated CPU time (s) 99.61
Current children cumulated vsize (Kb) 33104

[startup+110.015 s]
Raw data (loadavg): 0.99 1.05 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10587 0 0 0 10920 39 0 0 25 0 1 0 1788325288 32092160 6591 4294967295 134512640 135094434 3221224432 3221222976 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7835 6591 145 145 0 7690 0
[pid=29313] vsize: 31340
Current children cumulated CPU time (s) 109.6
Current children cumulated vsize (Kb) 33464

[startup+120.017 s]
Raw data (loadavg): 0.99 1.05 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10849 0 0 0 11917 40 0 0 25 0 1 0 1788325288 32632832 6726 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 7967 6726 145 145 0 7822 0
[pid=29313] vsize: 31868
Current children cumulated CPU time (s) 119.58
Current children cumulated vsize (Kb) 33992

[startup+130.018 s]
Raw data (loadavg): 0.99 1.05 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11015 0 0 0 12915 42 0 0 25 0 1 0 1788325288 33361920 6892 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8145 6892 145 145 0 8000 0
[pid=29313] vsize: 32580
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 34704

[startup+140.019 s]
Raw data (loadavg): 0.99 1.05 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11238 0 0 0 13912 43 0 0 25 0 1 0 1788325288 34009088 7051 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8303 7051 145 145 0 8158 0
[pid=29313] vsize: 33212
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 35336

[startup+150.019 s]
Raw data (loadavg): 0.99 1.04 1.04 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11293 0 0 0 14911 43 0 0 25 0 1 0 1788325288 34230272 7106 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8357 7106 145 145 0 8212 0
[pid=29313] vsize: 33428
Current children cumulated CPU time (s) 149.55
Current children cumulated vsize (Kb) 35552

[startup+160.02 s]
Raw data (loadavg): 0.99 1.04 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11400 0 0 0 15910 44 0 0 25 0 1 0 1788325288 34664448 7213 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8463 7213 145 145 0 8318 0
[pid=29313] vsize: 33852
Current children cumulated CPU time (s) 159.55
Current children cumulated vsize (Kb) 35976

[startup+170.021 s]
Raw data (loadavg): 0.99 1.04 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11465 0 0 0 16909 45 0 0 25 0 1 0 1788325288 34934784 7278 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8529 7278 145 145 0 8384 0
[pid=29313] vsize: 34116
Current children cumulated CPU time (s) 169.55
Current children cumulated vsize (Kb) 36240

[startup+180.022 s]
Raw data (loadavg): 0.99 1.04 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11517 0 0 0 17908 45 0 0 25 0 1 0 1788325288 35106816 7330 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8571 7330 145 145 0 8426 0
[pid=29313] vsize: 34284
Current children cumulated CPU time (s) 179.54
Current children cumulated vsize (Kb) 36408

[startup+190.024 s]
Raw data (loadavg): 0.99 1.04 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11687 0 0 0 18906 46 0 0 25 0 1 0 1788325288 35794944 7500 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8739 7500 145 145 0 8594 0
[pid=29313] vsize: 34956
Current children cumulated CPU time (s) 189.53
Current children cumulated vsize (Kb) 37080

[startup+200.025 s]
Raw data (loadavg): 0.99 1.04 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11898 0 0 0 19903 48 0 0 25 0 1 0 1788325288 36655104 7711 4294967295 134512640 135094434 3221224432 3221223104 134556523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 8949 7711 145 145 0 8804 0
[pid=29313] vsize: 35796
Current children cumulated CPU time (s) 199.52
Current children cumulated vsize (Kb) 37920

[startup+210.025 s]
Raw data (loadavg): 0.99 1.03 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 12196 0 0 0 20898 50 0 0 25 0 1 0 1788325288 37871616 8009 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 9246 8009 145 145 0 9101 0
[pid=29313] vsize: 36984
Current children cumulated CPU time (s) 209.49
Current children cumulated vsize (Kb) 39108

[startup+220.027 s]
Raw data (loadavg): 0.99 1.03 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 12680 0 0 0 21892 52 0 0 25 0 1 0 1788325288 39849984 8493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 9729 8493 145 145 0 9584 0
[pid=29313] vsize: 38916
Current children cumulated CPU time (s) 219.45
Current children cumulated vsize (Kb) 41040

[startup+230.028 s]
Raw data (loadavg): 0.99 1.03 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 12881 0 0 0 22889 54 0 0 25 0 1 0 1788325288 40669184 8694 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 9929 8694 145 145 0 9784 0
[pid=29313] vsize: 39716
Current children cumulated CPU time (s) 229.44
Current children cumulated vsize (Kb) 41840

[startup+240.029 s]
Raw data (loadavg): 0.99 1.03 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 13250 0 0 0 23883 57 0 0 25 0 1 0 1788325288 42176512 9063 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 10297 9063 145 145 0 10152 0
[pid=29313] vsize: 41188
Current children cumulated CPU time (s) 239.41
Current children cumulated vsize (Kb) 43312

[startup+250.03 s]
Raw data (loadavg): 0.99 1.03 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 13391 0 0 0 24882 58 0 0 25 0 1 0 1788325288 42881024 9204 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 10469 9204 145 145 0 10324 0
[pid=29313] vsize: 41876
Current children cumulated CPU time (s) 249.41
Current children cumulated vsize (Kb) 44000

[startup+260.031 s]
Raw data (loadavg): 0.99 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) T 29309 29309 8263 0 -1 0 13606 0 0 0 25878 59 0 0 25 0 1 0 1788325288 43757568 9419 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/29313/statm): 10683 9419 145 145 0 10538 0
[pid=29313] vsize: 42732
Current children cumulated CPU time (s) 259.38
Current children cumulated vsize (Kb) 44856

[startup+270.031 s]
Raw data (loadavg): 0.99 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 13907 0 0 0 26875 61 0 0 25 0 1 0 1788325288 44986368 9720 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 10983 9720 145 145 0 10838 0
[pid=29313] vsize: 43932
Current children cumulated CPU time (s) 269.37
Current children cumulated vsize (Kb) 46056

[startup+280.032 s]
Raw data (loadavg): 0.99 1.02 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14134 0 0 0 27872 62 0 0 25 0 1 0 1788325288 45912064 9947 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 11209 9947 145 145 0 11064 0
[pid=29313] vsize: 44836
Current children cumulated CPU time (s) 279.35
Current children cumulated vsize (Kb) 46960

[startup+290.034 s]
Raw data (loadavg): 0.99 1.02 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14427 0 0 0 28868 64 0 0 25 0 1 0 1788325288 47108096 10240 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 11501 10240 145 145 0 11356 0
[pid=29313] vsize: 46004
Current children cumulated CPU time (s) 289.33
Current children cumulated vsize (Kb) 48128

[startup+300.035 s]
Raw data (loadavg): 0.99 1.02 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14584 0 0 0 29867 65 0 0 25 0 1 0 1788325288 47751168 10397 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 11658 10397 145 145 0 11513 0
[pid=29313] vsize: 46632
Current children cumulated CPU time (s) 299.33
Current children cumulated vsize (Kb) 48756

[startup+310.036 s]
Raw data (loadavg): 1.07 1.04 1.03 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14876 0 0 0 30863 66 0 0 25 0 1 0 1788325288 48934912 10689 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 11947 10689 145 145 0 11802 0
[pid=29313] vsize: 47788
Current children cumulated CPU time (s) 309.3
Current children cumulated vsize (Kb) 49912

[startup+320.037 s]
Raw data (loadavg): 1.06 1.04 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15077 0 0 0 31861 67 0 0 25 0 1 0 1788325288 49762304 10890 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 12149 10890 145 145 0 12004 0
[pid=29313] vsize: 48596
Current children cumulated CPU time (s) 319.29
Current children cumulated vsize (Kb) 50720

[startup+330.037 s]
Raw data (loadavg): 1.05 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15277 0 0 0 32857 68 0 0 25 0 1 0 1788325288 50573312 11090 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 12347 11090 145 145 0 12202 0
[pid=29313] vsize: 49388
Current children cumulated CPU time (s) 329.26
Current children cumulated vsize (Kb) 51512

[startup+340.038 s]
Raw data (loadavg): 1.04 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15493 0 0 0 33853 70 0 0 25 0 1 0 1788325288 51449856 11306 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 12561 11306 145 145 0 12416 0
[pid=29313] vsize: 50244
Current children cumulated CPU time (s) 339.24
Current children cumulated vsize (Kb) 52368

[startup+350.039 s]
Raw data (loadavg): 1.03 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15732 0 0 0 34850 71 0 0 25 0 1 0 1788325288 52420608 11545 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 12798 11545 145 145 0 12653 0
[pid=29313] vsize: 51192
Current children cumulated CPU time (s) 349.22
Current children cumulated vsize (Kb) 53316

[startup+360.04 s]
Raw data (loadavg): 1.03 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15893 0 0 0 35847 73 0 0 25 0 1 0 1788325288 53075968 11706 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 12958 11706 145 145 0 12813 0
[pid=29313] vsize: 51832
Current children cumulated CPU time (s) 359.21
Current children cumulated vsize (Kb) 53956

[startup+370.042 s]
Raw data (loadavg): 1.02 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16099 0 0 0 36844 74 0 0 25 0 1 0 1788325288 53915648 11912 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 13163 11912 145 145 0 13018 0
[pid=29313] vsize: 52652
Current children cumulated CPU time (s) 369.19
Current children cumulated vsize (Kb) 54776

[startup+380.043 s]
Raw data (loadavg): 1.02 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16309 0 0 0 37841 76 0 0 25 0 1 0 1788325288 54771712 12122 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 13372 12122 145 145 0 13227 0
[pid=29313] vsize: 53488
Current children cumulated CPU time (s) 379.18
Current children cumulated vsize (Kb) 55612

[startup+390.045 s]
Raw data (loadavg): 1.02 1.03 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16457 0 0 0 38840 76 0 0 25 0 1 0 1788325288 55377920 12270 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 13520 12270 145 145 0 13375 0
[pid=29313] vsize: 54080
Current children cumulated CPU time (s) 389.17
Current children cumulated vsize (Kb) 56204

[startup+400.045 s]
Raw data (loadavg): 1.01 1.02 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16700 0 0 0 39836 78 0 0 25 0 1 0 1788325288 56365056 12513 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 13761 12513 145 145 0 13616 0
[pid=29313] vsize: 55044
Current children cumulated CPU time (s) 399.15
Current children cumulated vsize (Kb) 57168

[startup+410.045 s]
Raw data (loadavg): 1.01 1.02 1.02 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16931 0 0 0 40830 80 0 0 25 0 1 0 1788325288 57307136 12744 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 13991 12744 145 145 0 13846 0
[pid=29313] vsize: 55964
Current children cumulated CPU time (s) 409.11
Current children cumulated vsize (Kb) 58088

[startup+420.046 s]
Raw data (loadavg): 1.01 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17128 0 0 0 41827 82 0 0 25 0 1 0 1788325288 58105856 12941 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 14186 12941 145 145 0 14041 0
[pid=29313] vsize: 56744
Current children cumulated CPU time (s) 419.1
Current children cumulated vsize (Kb) 58868

[startup+430.047 s]
Raw data (loadavg): 1.01 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17191 0 0 0 42825 83 0 0 25 0 1 0 1788325288 58359808 13004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 14248 13004 145 145 0 14103 0
[pid=29313] vsize: 56992
Current children cumulated CPU time (s) 429.09
Current children cumulated vsize (Kb) 59116

[startup+440.048 s]
Raw data (loadavg): 1.00 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17386 0 0 0 43822 84 0 0 25 0 1 0 1788325288 59154432 13199 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 14442 13199 145 145 0 14297 0
[pid=29313] vsize: 57768
Current children cumulated CPU time (s) 439.07
Current children cumulated vsize (Kb) 59892

[startup+450.049 s]
Raw data (loadavg): 1.00 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17623 0 0 0 44818 86 0 0 25 0 1 0 1788325288 60116992 13436 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 14677 13436 145 145 0 14532 0
[pid=29313] vsize: 58708
Current children cumulated CPU time (s) 449.05
Current children cumulated vsize (Kb) 60832

[startup+460.049 s]
Raw data (loadavg): 1.00 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17927 0 0 0 45813 88 0 0 25 0 1 0 1788325288 61353984 13740 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 14979 13740 145 145 0 14834 0
[pid=29313] vsize: 59916
Current children cumulated CPU time (s) 459.02
Current children cumulated vsize (Kb) 62040

[startup+470.05 s]
Raw data (loadavg): 1.00 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18186 0 0 0 46809 91 0 0 25 0 1 0 1788325288 62410752 13999 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 15237 13999 145 145 0 15092 0
[pid=29313] vsize: 60948
Current children cumulated CPU time (s) 469.01
Current children cumulated vsize (Kb) 63072

[startup+480.051 s]
Raw data (loadavg): 1.00 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18471 0 0 0 47805 93 0 0 25 0 1 0 1788325288 63574016 14284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 15521 14284 145 145 0 15376 0
[pid=29313] vsize: 62084
Current children cumulated CPU time (s) 478.99
Current children cumulated vsize (Kb) 64208

[startup+490.053 s]
Raw data (loadavg): 1.00 1.02 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18512 0 0 0 48805 93 0 0 25 0 1 0 1788325288 63737856 14325 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 15561 14325 145 145 0 15416 0
[pid=29313] vsize: 62244
Current children cumulated CPU time (s) 488.99
Current children cumulated vsize (Kb) 64368

[startup+500.054 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18685 0 0 0 49802 94 0 0 25 0 1 0 1788325288 64442368 14498 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 15733 14498 145 145 0 15588 0
[pid=29313] vsize: 62932
Current children cumulated CPU time (s) 498.97
Current children cumulated vsize (Kb) 65056

[startup+510.055 s]
Raw data (loadavg): 1.00 1.01 1.01 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18896 0 0 0 50799 96 0 0 25 0 1 0 1788325288 65302528 14709 4294967295 134512640 135094434 3221224432 3221223024 134556793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 15943 14709 145 145 0 15798 0
[pid=29313] vsize: 63772
Current children cumulated CPU time (s) 508.96
Current children cumulated vsize (Kb) 65896

[startup+520.055 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19062 0 0 0 51796 96 0 0 25 0 1 0 1788325288 65978368 14875 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16108 14875 145 145 0 15963 0
[pid=29313] vsize: 64432
Current children cumulated CPU time (s) 518.93
Current children cumulated vsize (Kb) 66556

[startup+530.056 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19223 0 0 0 52794 97 0 0 25 0 1 0 1788325288 67006464 15036 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16359 15036 145 145 0 16214 0
[pid=29313] vsize: 65436
Current children cumulated CPU time (s) 528.92
Current children cumulated vsize (Kb) 67560

[startup+540.057 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19274 0 0 0 53793 98 0 0 25 0 1 0 1788325288 67223552 15087 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16412 15087 145 145 0 16267 0
[pid=29313] vsize: 65648
Current children cumulated CPU time (s) 538.92
Current children cumulated vsize (Kb) 67772

[startup+550.058 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19386 0 0 0 54792 98 0 0 25 0 1 0 1788325288 67674112 15199 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16522 15199 145 145 0 16377 0
[pid=29313] vsize: 66088
Current children cumulated CPU time (s) 548.91
Current children cumulated vsize (Kb) 68212

[startup+560.059 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19512 0 0 0 55790 99 0 0 25 0 1 0 1788325288 68182016 15325 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16646 15325 145 145 0 16501 0
[pid=29313] vsize: 66584
Current children cumulated CPU time (s) 558.9
Current children cumulated vsize (Kb) 68708

[startup+570.06 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19612 0 0 0 56789 99 0 0 25 0 1 0 1788325288 68591616 15425 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16746 15425 145 145 0 16601 0
[pid=29313] vsize: 66984
Current children cumulated CPU time (s) 568.89
Current children cumulated vsize (Kb) 69108

[startup+580.06 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19660 0 0 0 57789 99 0 0 25 0 1 0 1788325288 68784128 15473 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16793 15473 145 145 0 16648 0
[pid=29313] vsize: 67172
Current children cumulated CPU time (s) 578.89
Current children cumulated vsize (Kb) 69296

[startup+590.061 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19704 0 0 0 58789 99 0 0 25 0 1 0 1788325288 68964352 15517 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16837 15517 145 145 0 16692 0
[pid=29313] vsize: 67348
Current children cumulated CPU time (s) 588.89
Current children cumulated vsize (Kb) 69472

[startup+600.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19768 0 0 0 59788 100 0 0 25 0 1 0 1788325288 69226496 15581 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 16901 15581 145 145 0 16756 0
[pid=29313] vsize: 67604
Current children cumulated CPU time (s) 598.89
Current children cumulated vsize (Kb) 69728

[startup+610.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19898 0 0 0 60787 100 0 0 25 0 1 0 1788325288 69754880 15711 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17030 15711 145 145 0 16885 0
[pid=29313] vsize: 68120
Current children cumulated CPU time (s) 608.88
Current children cumulated vsize (Kb) 70244

[startup+620.064 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19992 0 0 0 61786 101 0 0 25 0 1 0 1788325288 70139904 15805 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17124 15805 145 145 0 16979 0
[pid=29313] vsize: 68496
Current children cumulated CPU time (s) 618.88
Current children cumulated vsize (Kb) 70620

[startup+630.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20110 0 0 0 62784 102 0 0 25 0 1 0 1788325288 70619136 15923 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17241 15923 145 145 0 17096 0
[pid=29313] vsize: 68964
Current children cumulated CPU time (s) 628.87
Current children cumulated vsize (Kb) 71088

[startup+640.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20197 0 0 0 63783 102 0 0 25 0 1 0 1788325288 70971392 16010 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17327 16010 145 145 0 17182 0
[pid=29313] vsize: 69308
Current children cumulated CPU time (s) 638.86
Current children cumulated vsize (Kb) 71432

[startup+650.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20311 0 0 0 64781 103 0 0 25 0 1 0 1788325288 71438336 16124 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17441 16124 145 145 0 17296 0
[pid=29313] vsize: 69764
Current children cumulated CPU time (s) 648.85
Current children cumulated vsize (Kb) 71888

[startup+660.068 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20435 0 0 0 65780 104 0 0 25 0 1 0 1788325288 71942144 16248 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17564 16248 145 145 0 17419 0
[pid=29313] vsize: 70256
Current children cumulated CPU time (s) 658.85
Current children cumulated vsize (Kb) 72380

[startup+670.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20520 0 0 0 66780 104 0 0 25 0 1 0 1788325288 72290304 16333 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17649 16333 145 145 0 17504 0
[pid=29313] vsize: 70596
Current children cumulated CPU time (s) 668.85
Current children cumulated vsize (Kb) 72720

[startup+680.071 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20631 0 0 0 67779 104 0 0 25 0 1 0 1788325288 72740864 16444 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17759 16444 145 145 0 17614 0
[pid=29313] vsize: 71036
Current children cumulated CPU time (s) 678.84
Current children cumulated vsize (Kb) 73160

[startup+690.073 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20710 0 0 0 68778 105 0 0 25 0 1 0 1788325288 73072640 16523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17840 16523 145 145 0 17695 0
[pid=29313] vsize: 71360
Current children cumulated CPU time (s) 688.84
Current children cumulated vsize (Kb) 73484

[startup+700.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20745 0 0 0 69778 105 0 0 25 0 1 0 1788325288 73207808 16558 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17873 16558 145 145 0 17728 0
[pid=29313] vsize: 71492
Current children cumulated CPU time (s) 698.84
Current children cumulated vsize (Kb) 73616

[startup+710.074 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20815 0 0 0 70777 105 0 0 25 0 1 0 1788325288 73494528 16628 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 17943 16628 145 145 0 17798 0
[pid=29313] vsize: 71772
Current children cumulated CPU time (s) 708.83
Current children cumulated vsize (Kb) 73896

[startup+720.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20910 0 0 0 71776 106 0 0 25 0 1 0 1788325288 73875456 16723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18036 16723 145 145 0 17891 0
[pid=29313] vsize: 72144
Current children cumulated CPU time (s) 718.83
Current children cumulated vsize (Kb) 74268

[startup+730.076 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21022 0 0 0 72775 107 0 0 25 0 1 0 1788325288 74330112 16835 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18147 16835 145 145 0 18002 0
[pid=29313] vsize: 72588
Current children cumulated CPU time (s) 728.83
Current children cumulated vsize (Kb) 74712

[startup+740.078 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21121 0 0 0 73773 107 0 0 25 0 1 0 1788325288 74731520 16934 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18245 16934 145 145 0 18100 0
[pid=29313] vsize: 72980
Current children cumulated CPU time (s) 738.81
Current children cumulated vsize (Kb) 75104

[startup+750.079 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21240 0 0 0 74772 108 0 0 25 0 1 0 1788325288 75218944 17053 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18364 17053 145 145 0 18219 0
[pid=29313] vsize: 73456
Current children cumulated CPU time (s) 748.81
Current children cumulated vsize (Kb) 75580

[startup+760.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21309 0 0 0 75771 108 0 0 25 0 1 0 1788325288 75509760 17122 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18435 17122 145 145 0 18290 0
[pid=29313] vsize: 73740
Current children cumulated CPU time (s) 758.8
Current children cumulated vsize (Kb) 75864

[startup+770.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21429 0 0 0 76769 109 0 0 25 0 1 0 1788325288 76005376 17242 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18556 17242 145 145 0 18411 0
[pid=29313] vsize: 74224
Current children cumulated CPU time (s) 768.79
Current children cumulated vsize (Kb) 76348

[startup+780.081 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21514 0 0 0 77769 109 0 0 25 0 1 0 1788325288 76353536 17327 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18641 17327 145 145 0 18496 0
[pid=29313] vsize: 74564
Current children cumulated CPU time (s) 778.79
Current children cumulated vsize (Kb) 76688

[startup+790.083 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21558 0 0 0 78768 109 0 0 25 0 1 0 1788325288 76537856 17371 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18686 17371 145 145 0 18541 0
[pid=29313] vsize: 74744
Current children cumulated CPU time (s) 788.78
Current children cumulated vsize (Kb) 76868

[startup+800.084 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21593 0 0 0 79768 110 0 0 25 0 1 0 1788325288 76681216 17406 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18721 17406 145 145 0 18576 0
[pid=29313] vsize: 74884
Current children cumulated CPU time (s) 798.79
Current children cumulated vsize (Kb) 77008

[startup+810.085 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21637 0 0 0 80767 110 0 0 25 0 1 0 1788325288 76857344 17450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18764 17450 145 145 0 18619 0
[pid=29313] vsize: 75056
Current children cumulated CPU time (s) 808.78
Current children cumulated vsize (Kb) 77180

[startup+820.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21663 0 0 0 81766 111 0 0 25 0 1 0 1788325288 76963840 17476 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18790 17476 145 145 0 18645 0
[pid=29313] vsize: 75160
Current children cumulated CPU time (s) 818.78
Current children cumulated vsize (Kb) 77284

[startup+830.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21682 0 0 0 82766 111 0 0 25 0 1 0 1788325288 77041664 17495 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18809 17495 145 145 0 18664 0
[pid=29313] vsize: 75236
Current children cumulated CPU time (s) 828.78
Current children cumulated vsize (Kb) 77360

[startup+840.088 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21698 0 0 0 83766 111 0 0 25 0 1 0 1788325288 77103104 17511 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18824 17511 145 145 0 18679 0
[pid=29313] vsize: 75296
Current children cumulated CPU time (s) 838.78
Current children cumulated vsize (Kb) 77420

[startup+850.089 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21719 0 0 0 84766 111 0 0 25 0 1 0 1788325288 77189120 17532 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 18845 17532 145 145 0 18700 0
[pid=29313] vsize: 75380
Current children cumulated CPU time (s) 848.78
Current children cumulated vsize (Kb) 77504

[startup+860.089 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21749 0 0 0 85765 112 0 0 25 0 1 0 1788325288 77312000 17562 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18875 17562 145 145 0 18730 0
[pid=29313] vsize: 75500
Current children cumulated CPU time (s) 858.78
Current children cumulated vsize (Kb) 77624

[startup+870.091 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21774 0 0 0 86765 112 0 0 25 0 1 0 1788325288 77410304 17587 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18899 17587 145 145 0 18754 0
[pid=29313] vsize: 75596
Current children cumulated CPU time (s) 868.78
Current children cumulated vsize (Kb) 77720

[startup+880.093 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21787 0 0 0 87764 112 0 0 25 0 1 0 1788325288 77463552 17600 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18912 17600 145 145 0 18767 0
[pid=29313] vsize: 75648
Current children cumulated CPU time (s) 878.77
Current children cumulated vsize (Kb) 77772

[startup+890.093 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21806 0 0 0 88764 113 0 0 25 0 1 0 1788325288 77541376 17619 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18931 17619 145 145 0 18786 0
[pid=29313] vsize: 75724
Current children cumulated CPU time (s) 888.78
Current children cumulated vsize (Kb) 77848

[startup+900.094 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21846 0 0 0 89763 114 0 0 25 0 1 0 1788325288 77709312 17659 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18972 17659 145 145 0 18827 0
[pid=29313] vsize: 75888
Current children cumulated CPU time (s) 898.78
Current children cumulated vsize (Kb) 78012

[startup+910.096 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21860 0 0 0 90762 115 0 0 25 0 1 0 1788325288 77762560 17673 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 18985 17673 145 145 0 18840 0
[pid=29313] vsize: 75940
Current children cumulated CPU time (s) 908.78
Current children cumulated vsize (Kb) 78064

[startup+920.097 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21882 0 0 0 91761 115 0 0 25 0 1 0 1788325288 77852672 17695 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 19007 17695 145 145 0 18862 0
[pid=29313] vsize: 76028
Current children cumulated CPU time (s) 918.77
Current children cumulated vsize (Kb) 78152

[startup+930.098 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21914 0 0 0 92760 116 0 0 25 0 1 0 1788325288 77979648 17727 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 19038 17727 145 145 0 18893 0
[pid=29313] vsize: 76152
Current children cumulated CPU time (s) 928.77
Current children cumulated vsize (Kb) 78276

[startup+940.099 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21958 0 0 0 93757 118 0 0 25 0 1 0 1788325288 78163968 17771 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 19083 17771 145 145 0 18938 0
[pid=29313] vsize: 76332
Current children cumulated CPU time (s) 938.76
Current children cumulated vsize (Kb) 78456

[startup+950.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21984 0 0 0 94756 119 0 0 25 0 1 0 1788325288 78270464 17797 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 19109 17797 145 145 0 18964 0
[pid=29313] vsize: 76436
Current children cumulated CPU time (s) 948.76
Current children cumulated vsize (Kb) 78560

[startup+960.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22019 0 0 0 95756 119 0 0 25 0 1 0 1788325288 78409728 17832 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19143 17832 145 145 0 18998 0
[pid=29313] vsize: 76572
Current children cumulated CPU time (s) 958.76
Current children cumulated vsize (Kb) 78696

[startup+970.102 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22046 0 0 0 96755 119 0 0 25 0 1 0 1788325288 78520320 17859 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19170 17859 145 145 0 19025 0
[pid=29313] vsize: 76680
Current children cumulated CPU time (s) 968.75
Current children cumulated vsize (Kb) 78804

[startup+980.103 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22069 0 0 0 97755 120 0 0 25 0 1 0 1788325288 78610432 17882 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19192 17882 145 145 0 19047 0
[pid=29313] vsize: 76768
Current children cumulated CPU time (s) 978.76
Current children cumulated vsize (Kb) 78892

[startup+990.104 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22093 0 0 0 98755 120 0 0 25 0 1 0 1788325288 78708736 17906 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19216 17906 145 145 0 19071 0
[pid=29313] vsize: 76864
Current children cumulated CPU time (s) 988.76
Current children cumulated vsize (Kb) 78988

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22116 0 0 0 99755 120 0 0 25 0 1 0 1788325288 78798848 17929 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19238 17929 145 145 0 19093 0
[pid=29313] vsize: 76952
Current children cumulated CPU time (s) 998.76
Current children cumulated vsize (Kb) 79076

[startup+1010.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22135 0 0 0 100755 120 0 0 25 0 1 0 1788325288 78880768 17948 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19258 17948 145 145 0 19113 0
[pid=29313] vsize: 77032
Current children cumulated CPU time (s) 1008.76
Current children cumulated vsize (Kb) 79156

[startup+1020.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22162 0 0 0 101755 120 0 0 25 0 1 0 1788325288 78991360 17975 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19285 17975 145 145 0 19140 0
[pid=29313] vsize: 77140
Current children cumulated CPU time (s) 1018.76
Current children cumulated vsize (Kb) 79264

[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22260 0 0 0 102753 121 0 0 25 0 1 0 1788325288 79384576 18073 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19381 18073 145 145 0 19236 0
[pid=29313] vsize: 77524
Current children cumulated CPU time (s) 1028.75
Current children cumulated vsize (Kb) 79648

[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22392 0 0 0 103752 121 0 0 25 0 1 0 1788325288 79925248 18205 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19513 18205 145 145 0 19368 0
[pid=29313] vsize: 78052
Current children cumulated CPU time (s) 1038.74
Current children cumulated vsize (Kb) 80176

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22478 0 0 0 104751 122 0 0 25 0 1 0 1788325288 80273408 18291 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19598 18291 145 145 0 19453 0
[pid=29313] vsize: 78392
Current children cumulated CPU time (s) 1048.74
Current children cumulated vsize (Kb) 80516

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22553 0 0 0 105751 122 0 0 25 0 1 0 1788325288 80584704 18366 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19674 18366 145 145 0 19529 0
[pid=29313] vsize: 78696
Current children cumulated CPU time (s) 1058.74
Current children cumulated vsize (Kb) 80820

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22660 0 0 0 106750 123 0 0 25 0 1 0 1788325288 81022976 18473 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19781 18473 145 145 0 19636 0
[pid=29313] vsize: 79124
Current children cumulated CPU time (s) 1068.74
Current children cumulated vsize (Kb) 81248

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22721 0 0 0 107748 123 0 0 25 0 1 0 1788325288 81268736 18534 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29313/statm): 19841 18534 145 145 0 19696 0
[pid=29313] vsize: 79364
Current children cumulated CPU time (s) 1078.72
Current children cumulated vsize (Kb) 81488

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22796 0 0 0 108746 124 0 0 25 0 1 0 1788325288 81588224 18609 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 19919 18609 145 145 0 19774 0
[pid=29313] vsize: 79676
Current children cumulated CPU time (s) 1088.71
Current children cumulated vsize (Kb) 81800

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22882 0 0 0 109746 125 0 0 25 0 1 0 1788325288 81940480 18695 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20005 18695 145 145 0 19860 0
[pid=29313] vsize: 80020
Current children cumulated CPU time (s) 1098.72
Current children cumulated vsize (Kb) 82144

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22946 0 0 0 110746 125 0 0 25 0 1 0 1788325288 82198528 18759 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20068 18759 145 145 0 19923 0
[pid=29313] vsize: 80272
Current children cumulated CPU time (s) 1108.72
Current children cumulated vsize (Kb) 82396

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 111743 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1118.7
Current children cumulated vsize (Kb) 82748

[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 112743 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1128.7
Current children cumulated vsize (Kb) 82748

[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 113744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1138.71
Current children cumulated vsize (Kb) 82748

[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 114744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1148.71
Current children cumulated vsize (Kb) 82748

[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 115744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1158.71
Current children cumulated vsize (Kb) 82748

[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 116744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1168.71
Current children cumulated vsize (Kb) 82748

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 117744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1178.71
Current children cumulated vsize (Kb) 82748

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 118745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1188.72
Current children cumulated vsize (Kb) 82748

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 119745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1198.72
Current children cumulated vsize (Kb) 82748

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 120745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1208.72
Current children cumulated vsize (Kb) 82748



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 29313
Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/29309/statm): 531 226 485 147 0 384 0
[pid=29309] vsize: 2124
Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 120745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134562161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0
[pid=29313] vsize: 80624
Current children cumulated CPU time (s) 1208.72
Current children cumulated vsize (Kb) 82748

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1208.76
CPU user time (s): 1207.46
CPU system time (s): 1.2978
CPU usage (%): 99.8838
Max. virtual memory (cumulated for all children) (Kb): 82748

Verifier Data

ERROR: no interpretation found !