Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mod008.opb
MD5SUM581d778a36086562107993896110e0a2
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 361
Optimality of the best value was proved NO
Number of terms in the objective function 319
Biggest coefficient in the objective function 87
Number of bits for the biggest coefficient in the objective function 7
Sum of the numbers in the objective function 23554
Number of bits of the sum of numbers in the objective function 15
Biggest number in a constraint 22000
Number of bits of the biggest number in a constraint 15
Biggest sum of numbers in a constraint 1027256
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.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 4556

Launcher Data

LAUNCH ON wulflinc12 THE 2005-09-19 18:23:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3019 boxname=wulflinc12 idbench=675 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /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: 3019
/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:        921480 kB
Buffers:         37032 kB
Cached:          43888 kB
SwapCached:        544 kB
Active:          59020 kB
Inactive:        24480 kB
HighTotal:      131008 kB
HighFree:        86492 kB
LowTotal:       903652 kB
LowFree:        834988 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            23880 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:43:14 (client local time) WITH STATUS 10 IN 1208.74 SECONDS
stats: 3019 7 1208.74 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/4238/stat): 4238 (minisat+_script) R 4237 4238 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793785736 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/4238/statm): 174 3 169 147 0 27 0
[pid=4238] 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=4239
New process pid=4240
New process pid=4241
One traced child (pid=4240) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=4241) exited with status: 0
One traced child (pid=4239) exited with status: 0
New process pid=4242
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.0039 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 4707 0 0 0 971 15 0 0 25 0 1 0 1793785741 5906432 1286 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 1442 1286 145 145 0 1297 0
[pid=4242] vsize: 5768
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 7892

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9637 0 0 0 1933 34 0 0 25 0 1 0 1793785741 28651520 5748 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 6995 5748 145 145 0 6850 0
[pid=4242] vsize: 27980
Current children cumulated CPU time (s) 19.69
Current children cumulated vsize (Kb) 30104

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9682 0 0 0 2931 35 0 0 25 0 1 0 1793785741 28831744 5793 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 7039 5793 145 145 0 6894 0
[pid=4242] vsize: 28156
Current children cumulated CPU time (s) 29.68
Current children cumulated vsize (Kb) 30280

[startup+40.0065 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9818 0 0 0 3928 36 0 0 25 0 1 0 1793785741 29372416 5929 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 7171 5929 145 145 0 7026 0
[pid=4242] vsize: 28684
Current children cumulated CPU time (s) 39.66
Current children cumulated vsize (Kb) 30808

[startup+50.0083 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9978 0 0 0 4925 38 0 0 25 0 1 0 1793785741 30007296 6089 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 7326 6089 145 145 0 7181 0
[pid=4242] vsize: 29304
Current children cumulated CPU time (s) 49.65
Current children cumulated vsize (Kb) 31428

[startup+60.0092 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10242 0 0 0 5923 39 0 0 25 0 1 0 1793785741 30896128 6311 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 7543 6311 145 145 0 7398 0
[pid=4242] vsize: 30172
Current children cumulated CPU time (s) 59.64
Current children cumulated vsize (Kb) 32296

[startup+70.01 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10265 0 0 0 6922 40 0 0 25 0 1 0 1793785741 30986240 6334 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 7565 6334 145 145 0 7420 0
[pid=4242] vsize: 30260
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 32384

[startup+80.0109 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10309 0 0 0 7921 40 0 0 25 0 1 0 1793785741 31227904 6378 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 7624 6378 145 145 0 7479 0
[pid=4242] vsize: 30496
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 32620

[startup+90.0127 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10426 0 0 0 8919 41 0 0 25 0 1 0 1793785741 31432704 6430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 7674 6430 145 145 0 7529 0
[pid=4242] vsize: 30696
Current children cumulated CPU time (s) 89.62
Current children cumulated vsize (Kb) 32820

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10497 0 0 0 9919 42 0 0 25 0 1 0 1793785741 31727616 6501 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 7746 6501 145 145 0 7601 0
[pid=4242] vsize: 30984
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 33108

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10599 0 0 0 10917 42 0 0 25 0 1 0 1793785741 32141312 6603 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 7847 6603 145 145 0 7702 0
[pid=4242] vsize: 31388
Current children cumulated CPU time (s) 109.61
Current children cumulated vsize (Kb) 33512

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10854 0 0 0 11914 43 0 0 25 0 1 0 1793785741 32653312 6731 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 7972 6731 145 145 0 7827 0
[pid=4242] vsize: 31888
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 34012

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11015 0 0 0 12912 45 0 0 25 0 1 0 1793785741 33361920 6892 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8145 6892 145 145 0 8000 0
[pid=4242] vsize: 32580
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 34704

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11244 0 0 0 13909 47 0 0 25 0 1 0 1793785741 34033664 7057 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8309 7057 145 145 0 8164 0
[pid=4242] vsize: 33236
Current children cumulated CPU time (s) 139.58
Current children cumulated vsize (Kb) 35360

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11312 0 0 0 14908 47 0 0 25 0 1 0 1793785741 34308096 7125 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8376 7125 145 145 0 8231 0
[pid=4242] vsize: 33504
Current children cumulated CPU time (s) 149.57
Current children cumulated vsize (Kb) 35628

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11405 0 0 0 15906 48 0 0 25 0 1 0 1793785741 34684928 7218 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8468 7218 145 145 0 8323 0
[pid=4242] vsize: 33872
Current children cumulated CPU time (s) 159.56
Current children cumulated vsize (Kb) 35996

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11481 0 0 0 16905 48 0 0 25 0 1 0 1793785741 34959360 7294 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8535 7294 145 145 0 8390 0
[pid=4242] vsize: 34140
Current children cumulated CPU time (s) 169.55
Current children cumulated vsize (Kb) 36264

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11521 0 0 0 17905 49 0 0 25 0 1 0 1793785741 35119104 7334 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8574 7334 145 145 0 8429 0
[pid=4242] vsize: 34296
Current children cumulated CPU time (s) 179.56
Current children cumulated vsize (Kb) 36420

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11735 0 0 0 18901 50 0 0 25 0 1 0 1793785741 35991552 7548 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8787 7548 145 145 0 8642 0
[pid=4242] vsize: 35148
Current children cumulated CPU time (s) 189.53
Current children cumulated vsize (Kb) 37272

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11937 0 0 0 19899 52 0 0 25 0 1 0 1793785741 36814848 7750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 8988 7750 145 145 0 8843 0
[pid=4242] vsize: 35952
Current children cumulated CPU time (s) 199.53
Current children cumulated vsize (Kb) 38076

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 12310 0 0 0 20892 55 0 0 25 0 1 0 1793785741 38338560 8123 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 9360 8123 145 145 0 9215 0
[pid=4242] vsize: 37440
Current children cumulated CPU time (s) 209.49
Current children cumulated vsize (Kb) 39564

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 12691 0 0 0 21888 57 0 0 25 0 1 0 1793785741 39895040 8504 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 9740 8504 145 145 0 9595 0
[pid=4242] vsize: 38960
Current children cumulated CPU time (s) 219.47
Current children cumulated vsize (Kb) 41084

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 12955 0 0 0 22884 59 0 0 25 0 1 0 1793785741 40972288 8768 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 10003 8768 145 145 0 9858 0
[pid=4242] vsize: 40012
Current children cumulated CPU time (s) 229.45
Current children cumulated vsize (Kb) 42136

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13306 0 0 0 23878 61 0 0 25 0 1 0 1793785741 42405888 9119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 10353 9119 145 145 0 10208 0
[pid=4242] vsize: 41412
Current children cumulated CPU time (s) 239.41
Current children cumulated vsize (Kb) 43536

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13416 0 0 0 24877 61 0 0 25 0 1 0 1793785741 42983424 9229 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 10494 9229 145 145 0 10349 0
[pid=4242] vsize: 41976
Current children cumulated CPU time (s) 249.4
Current children cumulated vsize (Kb) 44100

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13708 0 0 0 25872 63 0 0 25 0 1 0 1793785741 44175360 9521 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 10785 9521 145 145 0 10640 0
[pid=4242] vsize: 43140
Current children cumulated CPU time (s) 259.37
Current children cumulated vsize (Kb) 45264

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13985 0 0 0 26869 65 0 0 25 0 1 0 1793785741 45301760 9798 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 11060 9798 145 145 0 10915 0
[pid=4242] vsize: 44240
Current children cumulated CPU time (s) 269.36
Current children cumulated vsize (Kb) 46364

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14224 0 0 0 27865 67 0 0 25 0 1 0 1793785741 46280704 10037 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 11299 10037 145 145 0 11154 0
[pid=4242] vsize: 45196
Current children cumulated CPU time (s) 279.34
Current children cumulated vsize (Kb) 47320

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14467 0 0 0 28862 69 0 0 25 0 1 0 1793785741 47271936 10280 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 11541 10280 145 145 0 11396 0
[pid=4242] vsize: 46164
Current children cumulated CPU time (s) 289.33
Current children cumulated vsize (Kb) 48288

[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14640 0 0 0 29859 70 0 0 25 0 1 0 1793785741 47972352 10453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 11712 10453 145 145 0 11567 0
[pid=4242] vsize: 46848
Current children cumulated CPU time (s) 299.31
Current children cumulated vsize (Kb) 48972

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14953 0 0 0 30856 71 0 0 25 0 1 0 1793785741 49254400 10766 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 12025 10766 145 145 0 11880 0
[pid=4242] vsize: 48100
Current children cumulated CPU time (s) 309.29
Current children cumulated vsize (Kb) 50224

[startup+320.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15146 0 0 0 31854 73 0 0 25 0 1 0 1793785741 50036736 10959 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 12216 10959 145 145 0 12071 0
[pid=4242] vsize: 48864
Current children cumulated CPU time (s) 319.29
Current children cumulated vsize (Kb) 50988

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15347 0 0 0 32849 76 0 0 25 0 1 0 1793785741 50855936 11160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 12416 11160 145 145 0 12271 0
[pid=4242] vsize: 49664
Current children cumulated CPU time (s) 329.27
Current children cumulated vsize (Kb) 51788

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15582 0 0 0 33844 78 0 0 25 0 1 0 1793785741 51810304 11395 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 12649 11395 145 145 0 12504 0
[pid=4242] vsize: 50596
Current children cumulated CPU time (s) 339.24
Current children cumulated vsize (Kb) 52720

[startup+350.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15802 0 0 0 34840 80 0 0 25 0 1 0 1793785741 52707328 11615 4294967295 134512640 135094434 3221224432 3221223056 134557645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 12868 11615 145 145 0 12723 0
[pid=4242] vsize: 51472
Current children cumulated CPU time (s) 349.22
Current children cumulated vsize (Kb) 53596

[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15983 0 0 0 35837 82 0 0 25 0 1 0 1793785741 53440512 11796 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 13047 11796 145 145 0 12902 0
[pid=4242] vsize: 52188
Current children cumulated CPU time (s) 359.21
Current children cumulated vsize (Kb) 54312

[startup+370.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16179 0 0 0 36834 84 0 0 25 0 1 0 1793785741 54239232 11992 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 13242 11992 145 145 0 13097 0
[pid=4242] vsize: 52968
Current children cumulated CPU time (s) 369.2
Current children cumulated vsize (Kb) 55092

[startup+380.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16367 0 0 0 37832 84 0 0 25 0 1 0 1793785741 55013376 12180 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 13431 12180 145 145 0 13286 0
[pid=4242] vsize: 53724
Current children cumulated CPU time (s) 379.18
Current children cumulated vsize (Kb) 55848

[startup+390.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16551 0 0 0 38829 86 0 0 25 0 1 0 1793785741 55758848 12364 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 13613 12364 145 145 0 13468 0
[pid=4242] vsize: 54452
Current children cumulated CPU time (s) 389.17
Current children cumulated vsize (Kb) 56576

[startup+400.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16810 0 0 0 39824 88 0 0 25 0 1 0 1793785741 56811520 12623 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 13870 12623 145 145 0 13725 0
[pid=4242] vsize: 55480
Current children cumulated CPU time (s) 399.14
Current children cumulated vsize (Kb) 57604

[startup+410.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17042 0 0 0 40821 90 0 0 25 0 1 0 1793785741 57757696 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 14101 12855 145 145 0 13956 0
[pid=4242] vsize: 56404
Current children cumulated CPU time (s) 409.13
Current children cumulated vsize (Kb) 58528

[startup+420.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17175 0 0 0 41819 91 0 0 25 0 1 0 1793785741 58298368 12988 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 14233 12988 145 145 0 14088 0
[pid=4242] vsize: 56932
Current children cumulated CPU time (s) 419.12
Current children cumulated vsize (Kb) 59056

[startup+430.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17267 0 0 0 42817 92 0 0 25 0 1 0 1793785741 58671104 13080 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 14324 13080 145 145 0 14179 0
[pid=4242] vsize: 57296
Current children cumulated CPU time (s) 429.11
Current children cumulated vsize (Kb) 59420

[startup+440.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17525 0 0 0 43812 94 0 0 25 0 1 0 1793785741 59719680 13338 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 14580 13338 145 145 0 14435 0
[pid=4242] vsize: 58320
Current children cumulated CPU time (s) 439.08
Current children cumulated vsize (Kb) 60444

[startup+450.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17753 0 0 0 44808 96 0 0 25 0 1 0 1793785741 60645376 13566 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 14806 13566 145 145 0 14661 0
[pid=4242] vsize: 59224
Current children cumulated CPU time (s) 449.06
Current children cumulated vsize (Kb) 61348

[startup+460.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18057 0 0 0 45803 98 0 0 25 0 1 0 1793785741 61882368 13870 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 15108 13870 145 145 0 14963 0
[pid=4242] vsize: 60432
Current children cumulated CPU time (s) 459.03
Current children cumulated vsize (Kb) 62556

[startup+470.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18380 0 0 0 46796 101 0 0 25 0 1 0 1793785741 63205376 14193 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 15431 14193 145 145 0 15286 0
[pid=4242] vsize: 61724
Current children cumulated CPU time (s) 468.99
Current children cumulated vsize (Kb) 63848

[startup+480.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18496 0 0 0 47795 101 0 0 25 0 1 0 1793785741 63676416 14309 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 15546 14309 145 145 0 15401 0
[pid=4242] vsize: 62184
Current children cumulated CPU time (s) 478.98
Current children cumulated vsize (Kb) 64308

[startup+490.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18612 0 0 0 48793 102 0 0 25 0 1 0 1793785741 64147456 14425 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 15661 14425 145 145 0 15516 0
[pid=4242] vsize: 62644
Current children cumulated CPU time (s) 488.97
Current children cumulated vsize (Kb) 64768

[startup+500.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18819 0 0 0 49790 103 0 0 25 0 1 0 1793785741 64987136 14632 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 15866 14632 145 145 0 15721 0
[pid=4242] vsize: 63464
Current children cumulated CPU time (s) 498.95
Current children cumulated vsize (Kb) 65588

[startup+510.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19019 0 0 0 50787 104 0 0 25 0 1 0 1793785741 65806336 14832 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16066 14832 145 145 0 15921 0
[pid=4242] vsize: 64264
Current children cumulated CPU time (s) 508.93
Current children cumulated vsize (Kb) 66388

[startup+520.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19146 0 0 0 51786 105 0 0 25 0 1 0 1793785741 66322432 14959 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16192 14959 145 145 0 16047 0
[pid=4242] vsize: 64768
Current children cumulated CPU time (s) 518.93
Current children cumulated vsize (Kb) 66892

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19247 0 0 0 52785 106 0 0 25 0 1 0 1793785741 67108864 15060 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16384 15060 145 145 0 16239 0
[pid=4242] vsize: 65536
Current children cumulated CPU time (s) 528.93
Current children cumulated vsize (Kb) 67660

[startup+540.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19361 0 0 0 53783 106 0 0 25 0 1 0 1793785741 67571712 15174 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16497 15174 145 145 0 16352 0
[pid=4242] vsize: 65988
Current children cumulated CPU time (s) 538.91
Current children cumulated vsize (Kb) 68112

[startup+550.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19484 0 0 0 54781 107 0 0 25 0 1 0 1793785741 68067328 15297 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16618 15297 145 145 0 16473 0
[pid=4242] vsize: 66472
Current children cumulated CPU time (s) 548.9
Current children cumulated vsize (Kb) 68596

[startup+560.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19594 0 0 0 55779 108 0 0 25 0 1 0 1793785741 68517888 15407 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16728 15407 145 145 0 16583 0
[pid=4242] vsize: 66912
Current children cumulated CPU time (s) 558.89
Current children cumulated vsize (Kb) 69036

[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19649 0 0 0 56779 109 0 0 25 0 1 0 1793785741 68739072 15462 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16782 15462 145 145 0 16637 0
[pid=4242] vsize: 67128
Current children cumulated CPU time (s) 568.9
Current children cumulated vsize (Kb) 69252

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19691 0 0 0 57778 109 0 0 25 0 1 0 1793785741 68911104 15504 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16824 15504 145 145 0 16679 0
[pid=4242] vsize: 67296
Current children cumulated CPU time (s) 578.89
Current children cumulated vsize (Kb) 69420

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19735 0 0 0 58777 109 0 0 25 0 1 0 1793785741 69091328 15548 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16868 15548 145 145 0 16723 0
[pid=4242] vsize: 67472
Current children cumulated CPU time (s) 588.88
Current children cumulated vsize (Kb) 69596

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19860 0 0 0 59775 111 0 0 25 0 1 0 1793785741 69599232 15673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 16992 15673 145 145 0 16847 0
[pid=4242] vsize: 67968
Current children cumulated CPU time (s) 598.88
Current children cumulated vsize (Kb) 70092

[startup+610.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19972 0 0 0 60773 111 0 0 25 0 1 0 1793785741 70057984 15785 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17104 15785 145 145 0 16959 0
[pid=4242] vsize: 68416
Current children cumulated CPU time (s) 608.86
Current children cumulated vsize (Kb) 70540

[startup+620.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20079 0 0 0 61772 112 0 0 25 0 1 0 1793785741 70492160 15892 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17210 15892 145 145 0 17065 0
[pid=4242] vsize: 68840
Current children cumulated CPU time (s) 618.86
Current children cumulated vsize (Kb) 70964

[startup+630.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20169 0 0 0 62771 113 0 0 25 0 1 0 1793785741 70868992 15982 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17302 15982 145 145 0 17157 0
[pid=4242] vsize: 69208
Current children cumulated CPU time (s) 628.86
Current children cumulated vsize (Kb) 71332

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20272 0 0 0 63771 113 0 0 25 0 1 0 1793785741 71278592 16085 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17402 16085 145 145 0 17257 0
[pid=4242] vsize: 69608
Current children cumulated CPU time (s) 638.86
Current children cumulated vsize (Kb) 71732

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) T 4238 4238 8263 0 -1 0 20406 0 0 0 64768 114 0 0 25 0 1 0 1793785741 71823360 16219 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17535 16219 145 145 0 17390 0
[pid=4242] vsize: 70140
Current children cumulated CPU time (s) 648.84
Current children cumulated vsize (Kb) 72264

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20498 0 0 0 65767 115 0 0 25 0 1 0 1793785741 72208384 16311 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17629 16311 145 145 0 17484 0
[pid=4242] vsize: 70516
Current children cumulated CPU time (s) 658.84
Current children cumulated vsize (Kb) 72640

[startup+670.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20605 0 0 0 66765 116 0 0 25 0 1 0 1793785741 72634368 16418 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17733 16418 145 145 0 17588 0
[pid=4242] vsize: 70932
Current children cumulated CPU time (s) 668.83
Current children cumulated vsize (Kb) 73056

[startup+680.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20697 0 0 0 67764 117 0 0 25 0 1 0 1793785741 73011200 16510 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17825 16510 145 145 0 17680 0
[pid=4242] vsize: 71300
Current children cumulated CPU time (s) 678.83
Current children cumulated vsize (Kb) 73424

[startup+690.069 s]
Raw data (loadavg): 0.99 0.97 0.91 4/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20738 0 0 0 68764 117 0 0 25 0 1 0 1793785741 73179136 16551 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17866 16551 145 145 0 17721 0
[pid=4242] vsize: 71464
Current children cumulated CPU time (s) 688.83
Current children cumulated vsize (Kb) 73588

[startup+700.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20807 0 0 0 69763 118 0 0 25 0 1 0 1793785741 73453568 16620 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 17933 16620 145 145 0 17788 0
[pid=4242] vsize: 71732
Current children cumulated CPU time (s) 698.83
Current children cumulated vsize (Kb) 73856

[startup+710.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20896 0 0 0 70762 118 0 0 25 0 1 0 1793785741 73818112 16709 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18022 16709 145 145 0 17877 0
[pid=4242] vsize: 72088
Current children cumulated CPU time (s) 708.82
Current children cumulated vsize (Kb) 74212

[startup+720.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21016 0 0 0 71760 119 0 0 25 0 1 0 1793785741 74305536 16829 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18141 16829 145 145 0 17996 0
[pid=4242] vsize: 72564
Current children cumulated CPU time (s) 718.81
Current children cumulated vsize (Kb) 74688

[startup+730.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21106 0 0 0 72758 120 0 0 25 0 1 0 1793785741 74670080 16919 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18230 16919 145 145 0 18085 0
[pid=4242] vsize: 72920
Current children cumulated CPU time (s) 728.8
Current children cumulated vsize (Kb) 75044

[startup+740.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21233 0 0 0 73756 121 0 0 25 0 1 0 1793785741 75190272 17046 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18357 17046 145 145 0 18212 0
[pid=4242] vsize: 73428
Current children cumulated CPU time (s) 738.79
Current children cumulated vsize (Kb) 75552

[startup+750.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21300 0 0 0 74755 122 0 0 25 0 1 0 1793785741 75468800 17113 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18425 17113 145 145 0 18280 0
[pid=4242] vsize: 73700
Current children cumulated CPU time (s) 748.79
Current children cumulated vsize (Kb) 75824

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21414 0 0 0 75753 122 0 0 25 0 1 0 1793785741 75931648 17227 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18538 17227 145 145 0 18393 0
[pid=4242] vsize: 74152
Current children cumulated CPU time (s) 758.77
Current children cumulated vsize (Kb) 76276

[startup+770.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21509 0 0 0 76752 123 0 0 25 0 1 0 1793785741 76333056 17322 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 18636 17322 145 145 0 18491 0
[pid=4242] vsize: 74544
Current children cumulated CPU time (s) 768.77
Current children cumulated vsize (Kb) 76668

[startup+780.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21550 0 0 0 77751 123 0 0 25 0 1 0 1793785741 76509184 17363 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18679 17363 145 145 0 18534 0
[pid=4242] vsize: 74716
Current children cumulated CPU time (s) 778.76
Current children cumulated vsize (Kb) 76840

[startup+790.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21587 0 0 0 78751 123 0 0 25 0 1 0 1793785741 76656640 17400 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18715 17400 145 145 0 18570 0
[pid=4242] vsize: 74860
Current children cumulated CPU time (s) 788.76
Current children cumulated vsize (Kb) 76984

[startup+800.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21634 0 0 0 79750 124 0 0 25 0 1 0 1793785741 76845056 17447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18761 17447 145 145 0 18616 0
[pid=4242] vsize: 75044
Current children cumulated CPU time (s) 798.76
Current children cumulated vsize (Kb) 77168

[startup+810.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21660 0 0 0 80750 125 0 0 25 0 1 0 1793785741 76951552 17473 4294967295 134512640 135094434 3221224432 3221223104 134556437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18787 17473 145 145 0 18642 0
[pid=4242] vsize: 75148
Current children cumulated CPU time (s) 808.77
Current children cumulated vsize (Kb) 77272

[startup+820.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21681 0 0 0 81750 125 0 0 25 0 1 0 1793785741 77037568 17494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18808 17494 145 145 0 18663 0
[pid=4242] vsize: 75232
Current children cumulated CPU time (s) 818.77
Current children cumulated vsize (Kb) 77356

[startup+830.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21698 0 0 0 82750 125 0 0 25 0 1 0 1793785741 77103104 17511 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18824 17511 145 145 0 18679 0
[pid=4242] vsize: 75296
Current children cumulated CPU time (s) 828.77
Current children cumulated vsize (Kb) 77420

[startup+840.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21719 0 0 0 83750 125 0 0 25 0 1 0 1793785741 77189120 17532 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18845 17532 145 145 0 18700 0
[pid=4242] vsize: 75380
Current children cumulated CPU time (s) 838.77
Current children cumulated vsize (Kb) 77504

[startup+850.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21747 0 0 0 84750 125 0 0 25 0 1 0 1793785741 77303808 17560 4294967295 134512640 135094434 3221224432 3221223056 134562128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18873 17560 145 145 0 18728 0
[pid=4242] vsize: 75492
Current children cumulated CPU time (s) 848.77
Current children cumulated vsize (Kb) 77616

[startup+860.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21770 0 0 0 85750 125 0 0 25 0 1 0 1793785741 77393920 17583 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18895 17583 145 145 0 18750 0
[pid=4242] vsize: 75580
Current children cumulated CPU time (s) 858.77
Current children cumulated vsize (Kb) 77704

[startup+870.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21786 0 0 0 86750 126 0 0 25 0 1 0 1793785741 77459456 17599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18911 17599 145 145 0 18766 0
[pid=4242] vsize: 75644
Current children cumulated CPU time (s) 868.78
Current children cumulated vsize (Kb) 77768

[startup+880.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21806 0 0 0 87749 126 0 0 25 0 1 0 1793785741 77541376 17619 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18931 17619 145 145 0 18786 0
[pid=4242] vsize: 75724
Current children cumulated CPU time (s) 878.77
Current children cumulated vsize (Kb) 77848

[startup+890.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21845 0 0 0 88749 126 0 0 25 0 1 0 1793785741 77705216 17658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18971 17658 145 145 0 18826 0
[pid=4242] vsize: 75884
Current children cumulated CPU time (s) 888.77
Current children cumulated vsize (Kb) 78008

[startup+900.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21860 0 0 0 89748 126 0 0 25 0 1 0 1793785741 77762560 17673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 18985 17673 145 145 0 18840 0
[pid=4242] vsize: 75940
Current children cumulated CPU time (s) 898.76
Current children cumulated vsize (Kb) 78064

[startup+910.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21879 0 0 0 90748 127 0 0 25 0 1 0 1793785741 77840384 17692 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19004 17692 145 145 0 18859 0
[pid=4242] vsize: 76016
Current children cumulated CPU time (s) 908.77
Current children cumulated vsize (Kb) 78140

[startup+920.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21911 0 0 0 91747 128 0 0 25 0 1 0 1793785741 77967360 17724 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19035 17724 145 145 0 18890 0
[pid=4242] vsize: 76140
Current children cumulated CPU time (s) 918.77
Current children cumulated vsize (Kb) 78264

[startup+930.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21953 0 0 0 92746 129 0 0 25 0 1 0 1793785741 78143488 17766 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 19078 17766 145 145 0 18933 0
[pid=4242] vsize: 76312
Current children cumulated CPU time (s) 928.77
Current children cumulated vsize (Kb) 78436

[startup+940.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21982 0 0 0 93744 129 0 0 25 0 1 0 1793785741 78262272 17795 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19107 17795 145 145 0 18962 0
[pid=4242] vsize: 76428
Current children cumulated CPU time (s) 938.75
Current children cumulated vsize (Kb) 78552

[startup+950.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22017 0 0 0 94744 130 0 0 25 0 1 0 1793785741 78401536 17830 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19141 17830 145 145 0 18996 0
[pid=4242] vsize: 76564
Current children cumulated CPU time (s) 948.76
Current children cumulated vsize (Kb) 78688

[startup+960.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22045 0 0 0 95743 130 0 0 25 0 1 0 1793785741 78516224 17858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19169 17858 145 145 0 19024 0
[pid=4242] vsize: 76676
Current children cumulated CPU time (s) 958.75
Current children cumulated vsize (Kb) 78800

[startup+970.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22068 0 0 0 96743 131 0 0 25 0 1 0 1793785741 78606336 17881 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19191 17881 145 145 0 19046 0
[pid=4242] vsize: 76764
Current children cumulated CPU time (s) 968.76
Current children cumulated vsize (Kb) 78888

[startup+980.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22092 0 0 0 97742 131 0 0 25 0 1 0 1793785741 78704640 17905 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19215 17905 145 145 0 19070 0
[pid=4242] vsize: 76860
Current children cumulated CPU time (s) 978.75
Current children cumulated vsize (Kb) 78984

[startup+990.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22115 0 0 0 98742 131 0 0 25 0 1 0 1793785741 78794752 17928 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19237 17928 145 145 0 19092 0
[pid=4242] vsize: 76948
Current children cumulated CPU time (s) 988.75
Current children cumulated vsize (Kb) 79072

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22134 0 0 0 99742 131 0 0 25 0 1 0 1793785741 78876672 17947 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19257 17947 145 145 0 19112 0
[pid=4242] vsize: 77028
Current children cumulated CPU time (s) 998.75
Current children cumulated vsize (Kb) 79152

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22162 0 0 0 100742 132 0 0 25 0 1 0 1793785741 78991360 17975 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19285 17975 145 145 0 19140 0
[pid=4242] vsize: 77140
Current children cumulated CPU time (s) 1008.76
Current children cumulated vsize (Kb) 79264

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22256 0 0 0 101741 132 0 0 25 0 1 0 1793785741 79368192 18069 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19377 18069 145 145 0 19232 0
[pid=4242] vsize: 77508
Current children cumulated CPU time (s) 1018.75
Current children cumulated vsize (Kb) 79632

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22390 0 0 0 102740 133 0 0 25 0 1 0 1793785741 79921152 18203 4294967295 134512640 135094434 3221224432 3221223104 134555260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19512 18203 145 145 0 19367 0
[pid=4242] vsize: 78048
Current children cumulated CPU time (s) 1028.75
Current children cumulated vsize (Kb) 80172

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22478 0 0 0 103739 133 0 0 25 0 1 0 1793785741 80273408 18291 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19598 18291 145 145 0 19453 0
[pid=4242] vsize: 78392
Current children cumulated CPU time (s) 1038.74
Current children cumulated vsize (Kb) 80516

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22553 0 0 0 104738 134 0 0 25 0 1 0 1793785741 80584704 18366 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19674 18366 145 145 0 19529 0
[pid=4242] vsize: 78696
Current children cumulated CPU time (s) 1048.74
Current children cumulated vsize (Kb) 80820

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22665 0 0 0 105737 134 0 0 25 0 1 0 1793785741 81047552 18478 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19787 18478 145 145 0 19642 0
[pid=4242] vsize: 79148
Current children cumulated CPU time (s) 1058.73
Current children cumulated vsize (Kb) 81272

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22721 0 0 0 106736 135 0 0 25 0 1 0 1793785741 81268736 18534 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19841 18534 145 145 0 19696 0
[pid=4242] vsize: 79364
Current children cumulated CPU time (s) 1068.73
Current children cumulated vsize (Kb) 81488

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22797 0 0 0 107735 136 0 0 25 0 1 0 1793785741 81592320 18610 4294967295 134512640 135094434 3221224432 3221223024 134557013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 19920 18610 145 145 0 19775 0
[pid=4242] vsize: 79680
Current children cumulated CPU time (s) 1078.73
Current children cumulated vsize (Kb) 81804

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22886 0 0 0 108735 136 0 0 25 0 1 0 1793785741 81965056 18699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 20011 18699 145 145 0 19866 0
[pid=4242] vsize: 80044
Current children cumulated CPU time (s) 1088.73
Current children cumulated vsize (Kb) 82168

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22947 0 0 0 109735 136 0 0 25 0 1 0 1793785741 82198528 18760 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4242/statm): 20068 18760 145 145 0 19923 0
[pid=4242] vsize: 80272
Current children cumulated CPU time (s) 1098.73
Current children cumulated vsize (Kb) 82396

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 110732 137 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1108.71
Current children cumulated vsize (Kb) 82748

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 111732 138 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1118.72
Current children cumulated vsize (Kb) 82748

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 112731 138 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1128.71
Current children cumulated vsize (Kb) 82748

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 113731 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1138.72
Current children cumulated vsize (Kb) 82748

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 114731 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1148.72
Current children cumulated vsize (Kb) 82748

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 115730 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1158.71
Current children cumulated vsize (Kb) 82748

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 116730 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1168.71
Current children cumulated vsize (Kb) 82748

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 117730 140 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1178.72
Current children cumulated vsize (Kb) 82748

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 118729 140 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1188.71
Current children cumulated vsize (Kb) 82748

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 119729 141 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1198.72
Current children cumulated vsize (Kb) 82748

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 120729 141 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] 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): 0.99 0.97 0.91 2/57 4242
Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4238/statm): 531 226 485 147 0 384 0
[pid=4238] vsize: 2124
Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 120729 141 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0
[pid=4242] vsize: 80624
Current children cumulated CPU time (s) 1208.72
Current children cumulated vsize (Kb) 82748

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1208.74
CPU user time (s): 1207.29
CPU system time (s): 1.44778
CPU usage (%): 99.8829
Max. virtual memory (cumulated for all children) (Kb): 82748

Verifier Data

ERROR: no interpretation found !