PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
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 numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01684
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 15647

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 05:21:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17022 boxname=wulflinc29 idbench=1310 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 17022
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        841920 kB
Buffers:         20892 kB
Cached:         143816 kB
SwapCached:        464 kB
Active:          44596 kB
Inactive:       122296 kB
HighTotal:      131008 kB
HighFree:          336 kB
LowTotal:       903652 kB
LowFree:        841584 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            19972 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:41:13 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 17022 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: 1989[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 1974[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 814[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 574[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 573[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 548[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 525[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 389[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: 385[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.97 2/54 22673
Raw data (stat): 22673 (runsolver) R 22672 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542514245 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.87 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 9693 0 0 0 978 20 0 0 25 0 1 0 542514245 30670848 5910 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7488 5910 603 41 0 7447 0
vsize: 29952
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 9748 0 0 0 1976 21 0 0 25 0 1 0 542514245 30806016 5965 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7521 5965 603 41 0 7480 0
vsize: 30084
[startup+30.001 s]
Raw data (loadavg): 0.91 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 9895 0 0 0 2975 21 0 0 25 0 1 0 542514245 31346688 6112 4294967295 134512640 134672761 3221224624 3221223760 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7653 6113 603 41 0 7612 0
vsize: 30612
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10062 0 0 0 3974 22 0 0 25 0 1 0 542514245 32022528 6279 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7818 6279 603 41 0 7777 0
vsize: 31272
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10309 0 0 0 4974 22 0 0 25 0 1 0 542514245 32821248 6484 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8013 6484 603 41 0 7972 0
vsize: 32052
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10334 0 0 0 5974 23 0 0 25 0 1 0 542514245 32952320 6509 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8045 6509 603 41 0 8004 0
vsize: 32180
[startup+70.0018 s]
Raw data (loadavg): 0.95 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10373 0 0 0 6974 23 0 0 25 0 1 0 542514245 33243136 6548 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8116 6548 603 41 0 8075 0
vsize: 32464
[startup+80.002 s]
Raw data (loadavg): 0.96 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10457 0 0 0 7973 23 0 0 25 0 1 0 542514245 33435648 6605 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 6605 603 41 0 8122 0
vsize: 32652
[startup+90.0019 s]
Raw data (loadavg): 0.96 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10573 0 0 0 8971 24 0 0 25 0 1 0 542514245 33841152 6721 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8262 6721 603 41 0 8221 0
vsize: 33048
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10630 0 0 0 9971 25 0 0 25 0 1 0 542514245 34107392 6778 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 6778 603 41 0 8286 0
vsize: 33308
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 10902 0 0 0 10970 26 0 0 25 0 1 0 542514245 34856960 6969 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8510 6969 603 41 0 8469 0
vsize: 34040
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11086 0 0 0 11969 27 0 0 25 0 1 0 542514245 35569664 7128 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8684 7128 603 41 0 8643 0
vsize: 34736
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11201 0 0 0 12969 27 0 0 25 0 1 0 542514245 36089856 7243 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8811 7243 603 41 0 8770 0
vsize: 35244
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11296 0 0 0 13968 28 0 0 25 0 1 0 542514245 36491264 7338 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8909 7338 603 41 0 8868 0
vsize: 35636
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11368 0 0 0 14967 29 0 0 25 0 1 0 542514245 36761600 7410 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8975 7410 603 41 0 8934 0
vsize: 35900
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11436 0 0 0 15967 29 0 0 25 0 1 0 542514245 37023744 7478 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9039 7478 603 41 0 8998 0
vsize: 36156
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11503 0 0 0 16967 30 0 0 25 0 1 0 542514245 37281792 7545 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9102 7545 603 41 0 9061 0
vsize: 36408
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11759 0 0 0 17965 31 0 0 25 0 1 0 542514245 38215680 7801 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9330 7801 603 41 0 9289 0
vsize: 37320
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 11961 0 0 0 18965 32 0 0 25 0 1 0 542514245 39157760 8003 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9560 8003 603 41 0 9519 0
vsize: 38240
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 12452 0 0 0 19963 34 0 0 25 0 1 0 542514245 41136128 8494 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10043 8494 603 41 0 10002 0
vsize: 40172
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 12746 0 0 0 20962 35 0 0 25 0 1 0 542514245 42340352 8788 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10337 8788 603 41 0 10296 0
vsize: 41348
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 13046 0 0 0 21961 36 0 0 25 0 1 0 542514245 43540480 9088 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10630 9088 603 41 0 10589 0
vsize: 42520
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 13317 0 0 0 22960 37 0 0 25 0 1 0 542514245 44732416 9359 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10921 9359 603 41 0 10880 0
vsize: 43684
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 13402 0 0 0 23960 38 0 0 25 0 1 0 542514245 45137920 9444 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11020 9444 603 41 0 10979 0
vsize: 44080
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 13738 0 0 0 24959 39 0 0 25 0 1 0 542514245 46481408 9780 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11348 9780 603 41 0 11307 0
vsize: 45392
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 14003 0 0 0 25958 40 0 0 25 0 1 0 542514245 47550464 10045 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11609 10045 603 41 0 11568 0
vsize: 46436
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 14274 0 0 0 26956 41 0 0 25 0 1 0 542514245 48615424 10316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11869 10316 603 41 0 11828 0
vsize: 47476
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 14467 0 0 0 27955 43 0 0 25 0 1 0 542514245 49418240 10509 4294967295 134512640 134672761 3221224624 3221223728 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12065 10509 603 41 0 12024 0
vsize: 48260
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 14760 0 0 0 28955 43 0 0 25 0 1 0 542514245 50589696 10802 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12351 10802 603 41 0 12310 0
vsize: 49404
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 14985 0 0 0 29953 45 0 0 25 0 1 0 542514245 51511296 11027 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12576 11027 603 41 0 12535 0
vsize: 50304
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 15174 0 0 0 30953 46 0 0 25 0 1 0 542514245 52314112 11216 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12772 11216 603 41 0 12731 0
vsize: 51088
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 15407 0 0 0 31951 47 0 0 25 0 1 0 542514245 53239808 11449 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12998 11449 603 41 0 12957 0
vsize: 51992
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 15633 0 0 0 32950 48 0 0 25 0 1 0 542514245 54173696 11675 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 11675 603 41 0 13185 0
vsize: 52904
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 15816 0 0 0 33950 49 0 0 25 0 1 0 542514245 54968320 11858 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13420 11858 603 41 0 13379 0
vsize: 53680
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 16007 0 0 0 34949 50 0 0 25 0 1 0 542514245 55771136 12049 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13616 12049 603 41 0 13575 0
vsize: 54464
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 16221 0 0 0 35949 50 0 0 25 0 1 0 542514245 56569856 12263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13811 12263 603 41 0 13770 0
vsize: 55244
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 16374 0 0 0 36948 51 0 0 25 0 1 0 542514245 57229312 12416 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13972 12416 603 41 0 13931 0
vsize: 55888
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 16625 0 0 0 37947 52 0 0 25 0 1 0 542514245 58302464 12667 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14234 12667 603 41 0 14193 0
vsize: 56936
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 16867 0 0 0 38947 53 0 0 25 0 1 0 542514245 59240448 12909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14463 12909 603 41 0 14422 0
vsize: 57852
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 17068 0 0 0 39945 54 0 0 25 0 1 0 542514245 60043264 13110 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14659 13110 603 41 0 14618 0
vsize: 58636
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 17134 0 0 0 40945 55 0 0 25 0 1 0 542514245 60309504 13176 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14724 13176 603 41 0 14683 0
vsize: 58896
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 17335 0 0 0 41944 56 0 0 25 0 1 0 542514245 61116416 13377 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14921 13377 603 41 0 14880 0
vsize: 59684
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 17572 0 0 0 42942 57 0 0 25 0 1 0 542514245 62042112 13614 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15147 13614 603 41 0 15106 0
vsize: 60588
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 17889 0 0 0 43941 58 0 0 25 0 1 0 542514245 63377408 13931 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15473 13931 603 41 0 15432 0
vsize: 61892
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 18168 0 0 0 44940 59 0 0 25 0 1 0 542514245 64581632 14210 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 14210 603 41 0 15726 0
vsize: 63068
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 18414 0 0 0 45940 60 0 0 25 0 1 0 542514245 65503232 14456 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15992 14456 603 41 0 15951 0
vsize: 63968
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 18469 0 0 0 46940 60 0 0 25 0 1 0 542514245 65773568 14511 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16058 14511 603 41 0 16017 0
vsize: 64232
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 18648 0 0 0 47939 61 0 0 25 0 1 0 542514245 66437120 14690 4294967295 134512640 134672761 3221224624 3221223792 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16220 14690 603 41 0 16179 0
vsize: 64880
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 18900 0 0 0 48938 62 0 0 25 0 1 0 542514245 67502080 14942 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16480 14942 603 41 0 16439 0
vsize: 65920
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19040 0 0 0 49937 63 0 0 25 0 1 0 542514245 68030464 15082 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16609 15082 603 41 0 16568 0
vsize: 66436
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19163 0 0 0 50937 64 0 0 25 0 1 0 542514245 68956160 15205 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16835 15205 603 41 0 16794 0
vsize: 67340
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19229 0 0 0 51937 64 0 0 25 0 1 0 542514245 69214208 15271 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16898 15271 603 41 0 16857 0
vsize: 67592
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19354 0 0 0 52936 65 0 0 25 0 1 0 542514245 69746688 15396 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17028 15396 603 41 0 16987 0
vsize: 68112
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19517 0 0 0 53936 66 0 0 25 0 1 0 542514245 70406144 15559 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17189 15559 603 41 0 17148 0
vsize: 68756
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19577 0 0 0 54935 66 0 0 25 0 1 0 542514245 70672384 15619 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17254 15619 603 41 0 17213 0
vsize: 69016
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19620 0 0 0 55935 67 0 0 25 0 1 0 542514245 70799360 15662 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17285 15662 603 41 0 17244 0
vsize: 69140
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19656 0 0 0 56935 67 0 0 25 0 1 0 542514245 70934528 15698 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17318 15698 603 41 0 17277 0
vsize: 69272
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19762 0 0 0 57934 68 0 0 25 0 1 0 542514245 71331840 15804 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17415 15804 603 41 0 17374 0
vsize: 69660
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19880 0 0 0 58933 68 0 0 25 0 1 0 542514245 71872512 15922 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17547 15922 603 41 0 17506 0
vsize: 70188
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 19981 0 0 0 59933 69 0 0 25 0 1 0 542514245 72261632 16023 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17642 16023 603 41 0 17601 0
vsize: 70568
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20085 0 0 0 60933 70 0 0 25 0 1 0 542514245 72654848 16127 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16127 603 41 0 17697 0
vsize: 70952
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20186 0 0 0 61932 70 0 0 25 0 1 0 542514245 73191424 16228 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17869 16228 603 41 0 17828 0
vsize: 71476
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20310 0 0 0 62931 71 0 0 25 0 1 0 542514245 73572352 16352 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17962 16352 603 41 0 17921 0
vsize: 71848
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20401 0 0 0 63931 72 0 0 25 0 1 0 542514245 73981952 16443 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18062 16443 603 41 0 18021 0
vsize: 72248
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20509 0 0 0 64931 72 0 0 25 0 1 0 542514245 74493952 16551 4294967295 134512640 134672761 3221224624 3221223760 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18187 16551 603 41 0 18146 0
vsize: 72748
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20618 0 0 0 65930 72 0 0 25 0 1 0 542514245 74878976 16660 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18281 16660 603 41 0 18240 0
vsize: 73124
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20672 0 0 0 66930 72 0 0 25 0 1 0 542514245 75137024 16714 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18344 16714 603 41 0 18303 0
vsize: 73376
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20730 0 0 0 67930 73 0 0 25 0 1 0 542514245 75390976 16772 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18406 16772 603 41 0 18365 0
vsize: 73624
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20800 0 0 0 68930 73 0 0 25 0 1 0 542514245 75644928 16842 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18468 16842 603 41 0 18427 0
vsize: 73872
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 20927 0 0 0 69930 74 0 0 25 0 1 0 542514245 76177408 16969 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18598 16969 603 41 0 18557 0
vsize: 74392
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21026 0 0 0 70929 74 0 0 25 0 1 0 542514245 76578816 17068 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18696 17068 603 41 0 18655 0
vsize: 74784
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21160 0 0 0 71929 75 0 0 25 0 1 0 542514245 77119488 17202 4294967295 134512640 134672761 3221224624 3221223728 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18828 17202 603 41 0 18787 0
vsize: 75312
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21222 0 0 0 72929 75 0 0 25 0 1 0 542514245 77381632 17264 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18892 17264 603 41 0 18851 0
vsize: 75568
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21311 0 0 0 73929 75 0 0 25 0 1 0 542514245 77758464 17353 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18984 17353 603 41 0 18943 0
vsize: 75936
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21424 0 0 0 74928 76 0 0 25 0 1 0 542514245 78184448 17466 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19088 17466 603 41 0 19047 0
vsize: 76352
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21477 0 0 0 75928 77 0 0 25 0 1 0 542514245 78446592 17519 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19152 17519 603 41 0 19111 0
vsize: 76608
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21516 0 0 0 76928 77 0 0 25 0 1 0 542514245 78573568 17558 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19183 17558 603 41 0 19142 0
vsize: 76732
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21567 0 0 0 77927 78 0 0 25 0 1 0 542514245 78839808 17609 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19248 17609 603 41 0 19207 0
vsize: 76992
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21593 0 0 0 78927 78 0 0 25 0 1 0 542514245 78839808 17635 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19248 17635 603 41 0 19207 0
vsize: 76992
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21617 0 0 0 79927 78 0 0 25 0 1 0 542514245 78970880 17659 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19280 17659 603 41 0 19239 0
vsize: 77120
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21634 0 0 0 80926 78 0 0 25 0 1 0 542514245 79106048 17676 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19313 17676 603 41 0 19272 0
vsize: 77252
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21652 0 0 0 81926 79 0 0 25 0 1 0 542514245 79106048 17694 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19313 17694 603 41 0 19272 0
vsize: 77252
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21682 0 0 0 82926 79 0 0 25 0 1 0 542514245 79237120 17724 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19345 17724 603 41 0 19304 0
vsize: 77380
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21704 0 0 0 83926 79 0 0 25 0 1 0 542514245 79372288 17746 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19378 17746 603 41 0 19337 0
vsize: 77512
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21721 0 0 0 84926 79 0 0 25 0 1 0 542514245 79372288 17763 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19378 17763 603 41 0 19337 0
vsize: 77512
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21741 0 0 0 85926 80 0 0 25 0 1 0 542514245 79507456 17783 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19411 17783 603 41 0 19370 0
vsize: 77644
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21783 0 0 0 86925 80 0 0 25 0 1 0 542514245 79642624 17825 4294967295 134512640 134672761 3221224624 3221223728 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19444 17825 603 41 0 19403 0
vsize: 77776
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21799 0 0 0 87925 81 0 0 25 0 1 0 542514245 79773696 17841 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19476 17841 603 41 0 19435 0
vsize: 77904
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21815 0 0 0 88925 81 0 0 25 0 1 0 542514245 79773696 17857 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19476 17857 603 41 0 19435 0
vsize: 77904
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21847 0 0 0 89924 82 0 0 25 0 1 0 542514245 79904768 17889 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19508 17889 603 41 0 19467 0
vsize: 78032
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21892 0 0 0 90924 82 0 0 25 0 1 0 542514245 80039936 17934 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19541 17934 603 41 0 19500 0
vsize: 78164
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21920 0 0 0 91924 82 0 0 25 0 1 0 542514245 80175104 17962 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 17962 603 41 0 19533 0
vsize: 78296
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21955 0 0 0 92924 82 0 0 25 0 1 0 542514245 80310272 17997 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19607 17997 603 41 0 19566 0
vsize: 78428
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 21984 0 0 0 93924 83 0 0 25 0 1 0 542514245 80445440 18026 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19640 18026 603 41 0 19599 0
vsize: 78560
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22007 0 0 0 94924 83 0 0 25 0 1 0 542514245 80580608 18049 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19673 18049 603 41 0 19632 0
vsize: 78692
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22031 0 0 0 95925 83 0 0 25 0 1 0 542514245 80715776 18073 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18073 603 41 0 19665 0
vsize: 78824
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22055 0 0 0 96925 83 0 0 25 0 1 0 542514245 80715776 18097 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18097 603 41 0 19665 0
vsize: 78824
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22074 0 0 0 97925 83 0 0 25 0 1 0 542514245 80855040 18116 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 18116 603 41 0 19699 0
vsize: 78960
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22111 0 0 0 98925 83 0 0 25 0 1 0 542514245 80986112 18153 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19772 18153 603 41 0 19731 0
vsize: 79088
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22222 0 0 0 99925 83 0 0 25 0 1 0 542514245 81375232 18264 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19867 18264 603 41 0 19826 0
vsize: 79468
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22341 0 0 0 100925 84 0 0 25 0 1 0 542514245 81911808 18383 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19998 18383 603 41 0 19957 0
vsize: 79992
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22428 0 0 0 101924 84 0 0 25 0 1 0 542514245 82305024 18470 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 18470 603 41 0 20053 0
vsize: 80376
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22508 0 0 0 102924 84 0 0 25 0 1 0 542514245 82567168 18550 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20158 18550 603 41 0 20117 0
vsize: 80632
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22610 0 0 0 103924 84 0 0 25 0 1 0 542514245 83075072 18652 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20282 18652 603 41 0 20241 0
vsize: 81128
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22678 0 0 0 104924 84 0 0 25 0 1 0 542514245 83357696 18720 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20351 18720 603 41 0 20310 0
vsize: 81404
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22759 0 0 0 105924 85 0 0 25 0 1 0 542514245 83628032 18801 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20417 18801 603 41 0 20376 0
vsize: 81668
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22839 0 0 0 106924 85 0 0 25 0 1 0 542514245 83902464 18881 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20484 18881 603 41 0 20443 0
vsize: 81936
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 22902 0 0 0 107924 85 0 0 25 0 1 0 542514245 84164608 18944 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20548 18944 603 41 0 20507 0
vsize: 82192
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 108923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223808 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 109923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 110923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 111923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 112923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 113923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 114923 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 115924 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 116924 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 117924 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 118924 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 22673
Raw data (stat): 22673 (minisat+) R 22672 27222 27221 0 -1 0 23013 0 0 0 119924 86 0 0 25 0 1 0 542514245 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.97 1/54 22673
Raw data (stat): 22673 (minisat+) Z 22672 27222 27221 0 -1 12 23016 0 0 0 119924 90 0 0 25 0 1 0 542514245 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.15
CPU user time (s): 1199.25
CPU system time (s): 0.905862
CPU usage (%): 100.007
Max. virtual memory (Kb): 82524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####