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/miplib3/normalized-mps-v2-13-7-mod008.opb
MD5SUM	581d778a36086562107993896110e0a2
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.02084
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 18079

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        607944 kB
Buffers:         34092 kB
Cached:         365004 kB
SwapCached:        540 kB
Active:         130700 kB
Inactive:       270412 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        607692 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20016 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:44:44 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 18621 7 1200.23 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.91 0.96 0.98 2/54 26410
Raw data (stat): 26410 (runsolver) R 26409 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545404583 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.001 s]
Raw data (loadavg): 0.93 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 9693 0 0 0 977 21 0 0 25 0 1 0 545404583 30670848 5910 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7488 5910 603 41 0 7447 0
vsize: 29952
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 9748 0 0 0 1976 21 0 0 25 0 1 0 545404583 30806016 5965 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.0024 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 9886 0 0 0 2976 22 0 0 25 0 1 0 545404583 31346688 6103 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7653 6103 603 41 0 7612 0
vsize: 30612
[startup+40.0028 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10049 0 0 0 3975 22 0 0 25 0 1 0 545404583 32022528 6266 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7818 6266 603 41 0 7777 0
vsize: 31272
[startup+50.003 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10309 0 0 0 4974 23 0 0 25 0 1 0 545404583 32821248 6484 4294967295 134512640 134672761 3221224624 3221223760 134560604 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.0042 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10331 0 0 0 5974 23 0 0 25 0 1 0 545404583 32952320 6506 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8045 6506 603 41 0 8004 0
vsize: 32180
[startup+70.0046 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10373 0 0 0 6974 24 0 0 25 0 1 0 545404583 33243136 6548 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8116 6548 603 41 0 8075 0
vsize: 32464
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10453 0 0 0 7974 24 0 0 25 0 1 0 545404583 33435648 6601 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8163 6601 603 41 0 8122 0
vsize: 32652
[startup+90.0057 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10523 0 0 0 8974 24 0 0 25 0 1 0 545404583 33705984 6671 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8229 6671 603 41 0 8188 0
vsize: 32916
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10627 0 0 0 9974 24 0 0 25 0 1 0 545404583 34107392 6775 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 6775 603 41 0 8286 0
vsize: 33308
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10835 0 0 0 10974 25 0 0 25 0 1 0 545404583 34590720 6902 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8445 6902 603 41 0 8404 0
vsize: 33780
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 10996 0 0 0 11973 25 0 0 25 0 1 0 545404583 35377152 7063 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8637 7063 603 41 0 8596 0
vsize: 34548
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11186 0 0 0 12973 26 0 0 25 0 1 0 545404583 35962880 7228 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8780 7228 603 41 0 8739 0
vsize: 35120
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11257 0 0 0 13973 26 0 0 25 0 1 0 545404583 36225024 7299 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8844 7299 603 41 0 8803 0
vsize: 35376
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11346 0 0 0 14972 27 0 0 25 0 1 0 545404583 36626432 7388 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 7388 603 41 0 8901 0
vsize: 35768
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11422 0 0 0 15972 27 0 0 25 0 1 0 545404583 36896768 7464 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9008 7464 603 41 0 8967 0
vsize: 36032
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11461 0 0 0 16972 28 0 0 25 0 1 0 545404583 37023744 7503 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9039 7503 603 41 0 8998 0
vsize: 36156
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11664 0 0 0 17971 28 0 0 25 0 1 0 545404583 37953536 7706 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9266 7706 603 41 0 9225 0
vsize: 37064
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 11871 0 0 0 18971 29 0 0 25 0 1 0 545404583 38752256 7913 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9461 7913 603 41 0 9420 0
vsize: 37844
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 12215 0 0 0 19970 30 0 0 25 0 1 0 545404583 40087552 8257 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9787 8257 603 41 0 9746 0
vsize: 39148
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 12628 0 0 0 20970 31 0 0 25 0 1 0 545404583 41807872 8670 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10207 8670 603 41 0 10166 0
vsize: 40828
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 12877 0 0 0 21969 31 0 0 25 0 1 0 545404583 42868736 8919 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10466 8919 603 41 0 10425 0
vsize: 41864
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 13230 0 0 0 22968 32 0 0 25 0 1 0 545404583 44335104 9272 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10824 9272 603 41 0 10783 0
vsize: 43296
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 13349 0 0 0 23968 33 0 0 25 0 1 0 545404583 44867584 9391 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10954 9391 603 41 0 10913 0
vsize: 43816
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 13611 0 0 0 24968 33 0 0 25 0 1 0 545404583 45948928 9653 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11218 9653 603 41 0 11177 0
vsize: 44872
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 13895 0 0 0 25967 34 0 0 25 0 1 0 545404583 47149056 9937 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11511 9937 603 41 0 11470 0
vsize: 46044
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 14130 0 0 0 26966 35 0 0 25 0 1 0 545404583 48087040 10172 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11740 10172 603 41 0 11699 0
vsize: 46960
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 14399 0 0 0 27965 36 0 0 25 0 1 0 545404583 49156096 10441 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12001 10441 603 41 0 11960 0
vsize: 48004
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 14557 0 0 0 28965 37 0 0 25 0 1 0 545404583 49799168 10599 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12158 10599 603 41 0 12117 0
vsize: 48632
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 14862 0 0 0 29964 37 0 0 25 0 1 0 545404583 51122176 10904 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12481 10904 603 41 0 12440 0
vsize: 49924
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 15069 0 0 0 30964 38 0 0 25 0 1 0 545404583 51916800 11111 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12675 11111 603 41 0 12634 0
vsize: 50700
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 15258 0 0 0 31964 38 0 0 25 0 1 0 545404583 52711424 11300 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12869 11300 603 41 0 12828 0
vsize: 51476
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 15473 0 0 0 32964 39 0 0 25 0 1 0 545404583 53510144 11515 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13064 11515 603 41 0 13023 0
vsize: 52256
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 15710 0 0 0 33963 39 0 0 25 0 1 0 545404583 54575104 11752 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13324 11752 603 41 0 13283 0
vsize: 53296
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 15872 0 0 0 34963 40 0 0 25 0 1 0 545404583 55234560 11914 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13485 11914 603 41 0 13444 0
vsize: 53940
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 16069 0 0 0 35962 41 0 0 25 0 1 0 545404583 56037376 12111 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13681 12111 603 41 0 13640 0
vsize: 54724
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 16277 0 0 0 36962 41 0 0 25 0 1 0 545404583 56832000 12319 4294967295 134512640 134672761 3221224624 3221223808 134559588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13875 12319 603 41 0 13834 0
vsize: 55500
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 16434 0 0 0 37962 41 0 0 25 0 1 0 545404583 57499648 12476 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14038 12476 603 41 0 13997 0
vsize: 56152
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 16688 0 0 0 38962 42 0 0 25 0 1 0 545404583 58572800 12730 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14300 12730 603 41 0 14259 0
vsize: 57200
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 16919 0 0 0 39961 43 0 0 25 0 1 0 545404583 59506688 12961 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14528 12961 603 41 0 14487 0
vsize: 58112
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 17109 0 0 0 40960 44 0 0 25 0 1 0 545404583 60178432 13151 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14692 13151 603 41 0 14651 0
vsize: 58768
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 17149 0 0 0 41960 44 0 0 25 0 1 0 545404583 60440576 13191 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14756 13191 603 41 0 14715 0
vsize: 59024
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 17363 0 0 0 42959 45 0 0 25 0 1 0 545404583 61251584 13405 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14954 13405 603 41 0 14913 0
vsize: 59816
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 17585 0 0 0 43959 46 0 0 25 0 1 0 545404583 62177280 13627 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15180 13627 603 41 0 15139 0
vsize: 60720
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 17905 0 0 0 44958 47 0 0 25 0 1 0 545404583 63512576 13947 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15506 13947 603 41 0 15465 0
vsize: 62024
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 18190 0 0 0 45956 49 0 0 25 0 1 0 545404583 64581632 14232 4294967295 134512640 134672761 3221224624 3221223728 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 14232 603 41 0 15726 0
vsize: 63068
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 18417 0 0 0 46956 49 0 0 25 0 1 0 545404583 65503232 14459 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15992 14459 603 41 0 15951 0
vsize: 63968
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 18473 0 0 0 47956 49 0 0 25 0 1 0 545404583 65773568 14515 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 14515 603 41 0 16017 0
vsize: 64232
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 18648 0 0 0 48955 50 0 0 25 0 1 0 545404583 66437120 14690 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16220 14690 603 41 0 16179 0
vsize: 64880
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 18895 0 0 0 49955 51 0 0 25 0 1 0 545404583 67502080 14937 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16480 14937 603 41 0 16439 0
vsize: 65920
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19033 0 0 0 50955 51 0 0 25 0 1 0 545404583 68030464 15075 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16609 15075 603 41 0 16568 0
vsize: 66436
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19163 0 0 0 51955 51 0 0 25 0 1 0 545404583 68956160 15205 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16835 15205 603 41 0 16794 0
vsize: 67340
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19229 0 0 0 52955 52 0 0 25 0 1 0 545404583 69214208 15271 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16898 15271 603 41 0 16857 0
vsize: 67592
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19339 0 0 0 53954 52 0 0 25 0 1 0 545404583 69611520 15381 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16995 15381 603 41 0 16954 0
vsize: 67980
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19483 0 0 0 54954 53 0 0 25 0 1 0 545404583 70275072 15525 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17157 15525 603 41 0 17116 0
vsize: 68628
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19569 0 0 0 55954 53 0 0 25 0 1 0 545404583 70541312 15611 4294967295 134512640 134672761 3221224624 3221223728 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17222 15611 603 41 0 17181 0
vsize: 68888
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19612 0 0 0 56954 53 0 0 25 0 1 0 545404583 70799360 15654 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 15654 603 41 0 17244 0
vsize: 69140
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19652 0 0 0 57954 53 0 0 25 0 1 0 545404583 70934528 15694 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17318 15694 603 41 0 17277 0
vsize: 69272
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19745 0 0 0 58954 53 0 0 25 0 1 0 545404583 71331840 15787 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17415 15787 603 41 0 17374 0
vsize: 69660
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19862 0 0 0 59954 54 0 0 25 0 1 0 545404583 71737344 15904 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17514 15904 603 41 0 17473 0
vsize: 70056
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 19954 0 0 0 60954 54 0 0 25 0 1 0 545404583 72134656 15996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17611 15996 603 41 0 17570 0
vsize: 70444
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20067 0 0 0 61954 54 0 0 25 0 1 0 545404583 72654848 16109 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17738 16109 603 41 0 17697 0
vsize: 70952
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20167 0 0 0 62954 54 0 0 25 0 1 0 545404583 73056256 16209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17836 16209 603 41 0 17795 0
vsize: 71344
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20274 0 0 0 63954 55 0 0 25 0 1 0 545404583 73453568 16316 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17933 16316 603 41 0 17892 0
vsize: 71732
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20389 0 0 0 64953 55 0 0 25 0 1 0 545404583 73981952 16431 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18062 16431 603 41 0 18021 0
vsize: 72248
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20482 0 0 0 65953 56 0 0 25 0 1 0 545404583 74362880 16524 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18155 16524 603 41 0 18114 0
vsize: 72620
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20592 0 0 0 66953 56 0 0 25 0 1 0 545404583 74743808 16634 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18248 16634 603 41 0 18207 0
vsize: 72992
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20653 0 0 0 67953 56 0 0 25 0 1 0 545404583 75001856 16695 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18311 16695 603 41 0 18270 0
vsize: 73244
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20696 0 0 0 68953 56 0 0 25 0 1 0 545404583 75137024 16738 4294967295 134512640 134672761 3221224624 3221223808 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18344 16738 603 41 0 18303 0
vsize: 73376
[startup+700.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20762 0 0 0 69953 56 0 0 25 0 1 0 545404583 75513856 16804 4294967295 134512640 134672761 3221224624 3221223728 134559939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18436 16804 603 41 0 18395 0
vsize: 73744
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20870 0 0 0 70953 57 0 0 25 0 1 0 545404583 75911168 16912 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18533 16912 603 41 0 18492 0
vsize: 74132
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 20975 0 0 0 71953 57 0 0 25 0 1 0 545404583 76312576 17017 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18631 17017 603 41 0 18590 0
vsize: 74524
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21102 0 0 0 72953 58 0 0 25 0 1 0 545404583 76845056 17144 4294967295 134512640 134672761 3221224624 3221223808 134559318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18761 17144 603 41 0 18720 0
vsize: 75044
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21200 0 0 0 73953 58 0 0 25 0 1 0 545404583 77250560 17242 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18860 17242 603 41 0 18819 0
vsize: 75440
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21258 0 0 0 74953 58 0 0 25 0 1 0 545404583 77504512 17300 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18922 17300 603 41 0 18881 0
vsize: 75688
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21374 0 0 0 75953 58 0 0 25 0 1 0 545404583 78024704 17416 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19049 17416 603 41 0 19008 0
vsize: 76196
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21460 0 0 0 76953 59 0 0 25 0 1 0 545404583 78319616 17502 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19121 17502 603 41 0 19080 0
vsize: 76484
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21501 0 0 0 77952 59 0 0 25 0 1 0 545404583 78446592 17543 4294967295 134512640 134672761 3221224624 3221223808 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 17543 603 41 0 19111 0
vsize: 76608
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21535 0 0 0 78952 59 0 0 25 0 1 0 545404583 78700544 17577 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19214 17577 603 41 0 19173 0
vsize: 76856
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21577 0 0 0 79952 59 0 0 25 0 1 0 545404583 78839808 17619 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 17619 603 41 0 19207 0
vsize: 76992
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21603 0 0 0 80952 59 0 0 25 0 1 0 545404583 78970880 17645 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19280 17645 603 41 0 19239 0
vsize: 77120
[startup+820.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21623 0 0 0 81952 59 0 0 25 0 1 0 545404583 78970880 17665 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19280 17665 603 41 0 19239 0
vsize: 77120
[startup+830.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21638 0 0 0 82952 59 0 0 25 0 1 0 545404583 79106048 17680 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 17680 603 41 0 19272 0
vsize: 77252
[startup+840.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21659 0 0 0 83953 59 0 0 25 0 1 0 545404583 79106048 17701 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 17701 603 41 0 19272 0
vsize: 77252
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21689 0 0 0 84953 59 0 0 25 0 1 0 545404583 79237120 17731 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19345 17731 603 41 0 19304 0
vsize: 77380
[startup+860.039 s]
Raw data (loadavg): 1.07 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21712 0 0 0 85953 59 0 0 25 0 1 0 545404583 79372288 17754 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19378 17754 603 41 0 19337 0
vsize: 77512
[startup+870.04 s]
Raw data (loadavg): 1.06 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21726 0 0 0 86953 59 0 0 25 0 1 0 545404583 79372288 17768 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19378 17768 603 41 0 19337 0
vsize: 77512
[startup+880.039 s]
Raw data (loadavg): 1.05 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21750 0 0 0 87953 59 0 0 25 0 1 0 545404583 79507456 17792 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19411 17792 603 41 0 19370 0
vsize: 77644
[startup+890.04 s]
Raw data (loadavg): 1.04 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21785 0 0 0 88953 60 0 0 25 0 1 0 545404583 79642624 17827 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19444 17827 603 41 0 19403 0
vsize: 77776
[startup+900.04 s]
Raw data (loadavg): 1.04 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21799 0 0 0 89953 60 0 0 25 0 1 0 545404583 79773696 17841 4294967295 134512640 134672761 3221224624 3221223824 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 17841 603 41 0 19435 0
vsize: 77904
[startup+910.04 s]
Raw data (loadavg): 1.03 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21821 0 0 0 90953 60 0 0 25 0 1 0 545404583 79773696 17863 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 17863 603 41 0 19435 0
vsize: 77904
[startup+920.04 s]
Raw data (loadavg): 1.03 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21852 0 0 0 91953 60 0 0 25 0 1 0 545404583 79904768 17894 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19508 17894 603 41 0 19467 0
vsize: 78032
[startup+930.04 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21895 0 0 0 92953 60 0 0 25 0 1 0 545404583 80039936 17937 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19541 17937 603 41 0 19500 0
vsize: 78164
[startup+940.041 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21922 0 0 0 93953 60 0 0 25 0 1 0 545404583 80175104 17964 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 17964 603 41 0 19533 0
vsize: 78296
[startup+950.041 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21956 0 0 0 94953 60 0 0 25 0 1 0 545404583 80310272 17998 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19607 17998 603 41 0 19566 0
vsize: 78428
[startup+960.042 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 21984 0 0 0 95954 60 0 0 25 0 1 0 545404583 80445440 18026 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19640 18026 603 41 0 19599 0
vsize: 78560
[startup+970.043 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22007 0 0 0 96954 61 0 0 25 0 1 0 545404583 80580608 18049 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19673 18049 603 41 0 19632 0
vsize: 78692
[startup+980.043 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22031 0 0 0 97954 61 0 0 25 0 1 0 545404583 80715776 18073 4294967295 134512640 134672761 3221224624 3221223792 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18073 603 41 0 19665 0
vsize: 78824
[startup+990.044 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22053 0 0 0 98954 61 0 0 25 0 1 0 545404583 80715776 18095 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18095 603 41 0 19665 0
vsize: 78824
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22072 0 0 0 99954 61 0 0 25 0 1 0 545404583 80855040 18114 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 18114 603 41 0 19699 0
vsize: 78960
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22095 0 0 0 100954 61 0 0 25 0 1 0 545404583 80855040 18137 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 18137 603 41 0 19699 0
vsize: 78960
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22193 0 0 0 101954 61 0 0 25 0 1 0 545404583 81244160 18235 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19835 18235 603 41 0 19794 0
vsize: 79340
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22319 0 0 0 102953 62 0 0 25 0 1 0 545404583 81776640 18361 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19965 18361 603 41 0 19924 0
vsize: 79860
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22405 0 0 0 103953 62 0 0 25 0 1 0 545404583 82169856 18447 4294967295 134512640 134672761 3221224624 3221223792 134561136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20061 18447 603 41 0 20020 0
vsize: 80244
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22489 0 0 0 104953 62 0 0 25 0 1 0 545404583 82567168 18531 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20158 18531 603 41 0 20117 0
vsize: 80632
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22585 0 0 0 105954 62 0 0 25 0 1 0 545404583 82944000 18627 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20250 18627 603 41 0 20209 0
vsize: 81000
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22652 0 0 0 106954 62 0 0 25 0 1 0 545404583 83202048 18694 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20313 18694 603 41 0 20272 0
vsize: 81252
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22731 0 0 0 107954 63 0 0 25 0 1 0 545404583 83492864 18773 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 18773 603 41 0 20343 0
vsize: 81536
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22815 0 0 0 108954 63 0 0 25 0 1 0 545404583 83902464 18857 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20484 18857 603 41 0 20443 0
vsize: 81936
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 22881 0 0 0 109954 63 0 0 25 0 1 0 545404583 84164608 18923 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20548 18923 603 41 0 20507 0
vsize: 82192
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 110954 63 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223924 134556688 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 111953 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559925 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 112953 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223760 134560688 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 113953 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223760 134560590 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 114954 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560852 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 115954 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223888 134562492 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 116954 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560218 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 117954 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559925 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 118954 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560008 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.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 26410
Raw data (stat): 26410 (minisat+) R 26409 23176 23175 0 -1 0 23013 0 0 0 119954 64 0 0 25 0 1 0 545404583 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.09 s]
Raw data (loadavg): 1.00 0.99 0.99 1/54 26410
Raw data (stat): 26410 (minisat+) Z 26409 23176 23175 0 -1 12 23016 0 0 0 119954 68 0 0 25 0 1 0 545404583 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.09
CPU time (s): 1200.23
CPU user time (s): 1199.54
CPU system time (s): 0.683896
CPU usage (%): 100.011
Max. virtual memory (Kb): 82524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####