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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.01584
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 22157

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        244720 kB
Buffers:         24368 kB
Cached:         743420 kB
SwapCached:          0 kB
Active:          58120 kB
Inactive:       712468 kB
HighTotal:      131008 kB
HighFree:        29540 kB
LowTotal:       903652 kB
LowFree:        215180 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            13552 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:41:27 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 12030 7 1200.21 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.92 0.98 0.93 2/54 535
Raw data (stat): 535 (runsolver) R 534 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491858277 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0005 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 9693 0 0 0 975 22 0 0 25 0 1 0 491858277 30670848 5910 4294967295 134512640 134672761 3221224624 3221223792 134561188 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.0011 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 9748 0 0 0 1975 22 0 0 25 0 1 0 491858277 30806016 5965 4294967295 134512640 134672761 3221224624 3221223824 134557828 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.0015 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 9888 0 0 0 2974 23 0 0 25 0 1 0 491858277 31346688 6105 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7653 6105 603 41 0 7612 0
vsize: 30612
[startup+40.0008 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10053 0 0 0 3973 24 0 0 25 0 1 0 491858277 32022528 6270 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7818 6270 603 41 0 7777 0
vsize: 31272
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10309 0 0 0 4972 25 0 0 25 0 1 0 491858277 32821248 6484 4294967295 134512640 134672761 3221224624 3221223788 134561235 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.0015 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10332 0 0 0 5972 25 0 0 25 0 1 0 491858277 32952320 6507 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8045 6507 603 41 0 8004 0
vsize: 32180
[startup+70.002 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10373 0 0 0 6971 26 0 0 25 0 1 0 491858277 33243136 6548 4294967295 134512640 134672761 3221224624 3221223792 134560839 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.0028 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10455 0 0 0 7971 26 0 0 25 0 1 0 491858277 33435648 6603 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8163 6603 603 41 0 8122 0
vsize: 32652
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10547 0 0 0 8971 26 0 0 25 0 1 0 491858277 33841152 6695 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8262 6695 603 41 0 8221 0
vsize: 33048
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10628 0 0 0 9971 26 0 0 25 0 1 0 491858277 34107392 6776 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 6776 603 41 0 8286 0
vsize: 33308
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 10891 0 0 0 10971 27 0 0 25 0 1 0 491858277 34856960 6958 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8510 6958 603 41 0 8469 0
vsize: 34040
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11074 0 0 0 11970 28 0 0 25 0 1 0 491858277 35569664 7116 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8684 7116 603 41 0 8643 0
vsize: 34736
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11199 0 0 0 12970 28 0 0 25 0 1 0 491858277 36089856 7241 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8811 7241 603 41 0 8770 0
vsize: 35244
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11283 0 0 0 13969 28 0 0 25 0 1 0 491858277 36356096 7325 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8876 7325 603 41 0 8835 0
vsize: 35504
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11360 0 0 0 14969 29 0 0 25 0 1 0 491858277 36626432 7402 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 7402 603 41 0 8901 0
vsize: 35768
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11432 0 0 0 15969 29 0 0 25 0 1 0 491858277 36896768 7474 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9008 7474 603 41 0 8967 0
vsize: 36032
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11482 0 0 0 16969 29 0 0 25 0 1 0 491858277 37150720 7524 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9070 7524 603 41 0 9029 0
vsize: 36280
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11735 0 0 0 17969 30 0 0 25 0 1 0 491858277 38215680 7777 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9330 7777 603 41 0 9289 0
vsize: 37320
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 11938 0 0 0 18968 30 0 0 25 0 1 0 491858277 39022592 7980 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9527 7980 603 41 0 9486 0
vsize: 38108
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 12394 0 0 0 19967 32 0 0 25 0 1 0 491858277 40873984 8436 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9979 8436 603 41 0 9938 0
vsize: 39916
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 12722 0 0 0 20967 32 0 0 25 0 1 0 491858277 42205184 8764 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10304 8764 603 41 0 10263 0
vsize: 41216
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 13003 0 0 0 21967 33 0 0 25 0 1 0 491858277 43405312 9045 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10597 9045 603 41 0 10556 0
vsize: 42388
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 13275 0 0 0 22966 33 0 0 25 0 1 0 491858277 44470272 9317 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10857 9317 603 41 0 10816 0
vsize: 43428
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 13385 0 0 0 23966 34 0 0 25 0 1 0 491858277 45002752 9427 4294967295 134512640 134672761 3221224624 3221223760 134560613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10987 9427 603 41 0 10946 0
vsize: 43948
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 13718 0 0 0 24965 35 0 0 25 0 1 0 491858277 46346240 9760 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11315 9760 603 41 0 11274 0
vsize: 45260
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 13998 0 0 0 25965 35 0 0 25 0 1 0 491858277 47550464 10040 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11609 10040 603 41 0 11568 0
vsize: 46436
[startup+270.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 14256 0 0 0 26964 36 0 0 25 0 1 0 491858277 48615424 10298 4294967295 134512640 134672761 3221224624 3221223728 134560364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11869 10298 603 41 0 11828 0
vsize: 47476
[startup+280.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 14455 0 0 0 27964 36 0 0 25 0 1 0 491858277 49418240 10497 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12065 10497 603 41 0 12024 0
vsize: 48260
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 14747 0 0 0 28964 37 0 0 25 0 1 0 491858277 50589696 10789 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12351 10789 603 41 0 12310 0
vsize: 49404
[startup+300.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 14977 0 0 0 29963 38 0 0 25 0 1 0 491858277 51511296 11019 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12576 11019 603 41 0 12535 0
vsize: 50304
[startup+310.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 15162 0 0 0 30963 38 0 0 25 0 1 0 491858277 52314112 11204 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12772 11204 603 41 0 12731 0
vsize: 51088
[startup+320.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 15395 0 0 0 31962 39 0 0 25 0 1 0 491858277 53239808 11437 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12998 11437 603 41 0 12957 0
vsize: 51992
[startup+330.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 15628 0 0 0 32962 39 0 0 25 0 1 0 491858277 54173696 11670 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13226 11670 603 41 0 13185 0
vsize: 52904
[startup+340.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 15813 0 0 0 33961 40 0 0 25 0 1 0 491858277 54968320 11855 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13420 11855 603 41 0 13379 0
vsize: 53680
[startup+350.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 16002 0 0 0 34961 41 0 0 25 0 1 0 491858277 55771136 12044 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13616 12044 603 41 0 13575 0
vsize: 54464
[startup+360.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 16218 0 0 0 35961 41 0 0 25 0 1 0 491858277 56569856 12260 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13811 12260 603 41 0 13770 0
vsize: 55244
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 16374 0 0 0 36960 42 0 0 25 0 1 0 491858277 57229312 12416 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13972 12416 603 41 0 13931 0
vsize: 55888
[startup+380.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 16627 0 0 0 37959 43 0 0 25 0 1 0 491858277 58302464 12669 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14234 12669 603 41 0 14193 0
vsize: 56936
[startup+390.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 16870 0 0 0 38959 44 0 0 25 0 1 0 491858277 59240448 12912 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14463 12912 603 41 0 14422 0
vsize: 57852
[startup+400.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 17072 0 0 0 39958 44 0 0 25 0 1 0 491858277 60043264 13114 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14659 13114 603 41 0 14618 0
vsize: 58636
[startup+410.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 17134 0 0 0 40959 44 0 0 25 0 1 0 491858277 60309504 13176 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14724 13176 603 41 0 14683 0
vsize: 58896
[startup+420.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 17341 0 0 0 41958 45 0 0 25 0 1 0 491858277 61116416 13383 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14921 13383 603 41 0 14880 0
vsize: 59684
[startup+430.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 17572 0 0 0 42957 46 0 0 25 0 1 0 491858277 62042112 13614 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15147 13614 603 41 0 15106 0
vsize: 60588
[startup+440.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 17898 0 0 0 43957 47 0 0 25 0 1 0 491858277 63377408 13940 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15473 13940 603 41 0 15432 0
vsize: 61892
[startup+450.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 18187 0 0 0 44956 47 0 0 25 0 1 0 491858277 64581632 14229 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 14229 603 41 0 15726 0
vsize: 63068
[startup+460.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 18417 0 0 0 45956 48 0 0 25 0 1 0 491858277 65503232 14459 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15992 14459 603 41 0 15951 0
vsize: 63968
[startup+470.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 18476 0 0 0 46956 48 0 0 25 0 1 0 491858277 65773568 14518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 14518 603 41 0 16017 0
vsize: 64232
[startup+480.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 18651 0 0 0 47956 48 0 0 25 0 1 0 491858277 66437120 14693 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16220 14693 603 41 0 16179 0
vsize: 64880
[startup+490.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 18912 0 0 0 48955 49 0 0 25 0 1 0 491858277 67502080 14954 4294967295 134512640 134672761 3221224624 3221223760 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16480 14954 603 41 0 16439 0
vsize: 65920
[startup+500.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19048 0 0 0 49955 49 0 0 25 0 1 0 491858277 68161536 15090 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16641 15090 603 41 0 16600 0
vsize: 66564
[startup+510.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19165 0 0 0 50955 49 0 0 25 0 1 0 491858277 68956160 15207 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16835 15207 603 41 0 16794 0
vsize: 67340
[startup+520.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19240 0 0 0 51955 50 0 0 25 0 1 0 491858277 69214208 15282 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16898 15282 603 41 0 16857 0
vsize: 67592
[startup+530.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19376 0 0 0 52955 50 0 0 25 0 1 0 491858277 69877760 15418 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17060 15418 603 41 0 17019 0
vsize: 68240
[startup+540.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19526 0 0 0 53955 50 0 0 25 0 1 0 491858277 70406144 15568 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17189 15568 603 41 0 17148 0
vsize: 68756
[startup+550.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19581 0 0 0 54955 51 0 0 25 0 1 0 491858277 70672384 15623 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17254 15623 603 41 0 17213 0
vsize: 69016
[startup+560.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19622 0 0 0 55955 51 0 0 25 0 1 0 491858277 70799360 15664 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 15664 603 41 0 17244 0
vsize: 69140
[startup+570.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19659 0 0 0 56955 51 0 0 25 0 1 0 491858277 70934528 15701 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17318 15701 603 41 0 17277 0
vsize: 69272
[startup+580.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19771 0 0 0 57954 52 0 0 25 0 1 0 491858277 71467008 15813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17448 15813 603 41 0 17407 0
vsize: 69792
[startup+590.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19885 0 0 0 58954 52 0 0 25 0 1 0 491858277 71872512 15927 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17547 15927 603 41 0 17506 0
vsize: 70188
[startup+600.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 19988 0 0 0 59954 52 0 0 25 0 1 0 491858277 72261632 16030 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17642 16030 603 41 0 17601 0
vsize: 70568
[startup+610.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20093 0 0 0 60954 52 0 0 25 0 1 0 491858277 72790016 16135 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17771 16135 603 41 0 17730 0
vsize: 71084
[startup+620.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20205 0 0 0 61954 52 0 0 25 0 1 0 491858277 73191424 16247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17869 16247 603 41 0 17828 0
vsize: 71476
[startup+630.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20325 0 0 0 62954 53 0 0 25 0 1 0 491858277 73711616 16367 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17996 16367 603 41 0 17955 0
vsize: 71984
[startup+640.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20417 0 0 0 63954 53 0 0 25 0 1 0 491858277 74117120 16459 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 16459 603 41 0 18054 0
vsize: 72380
[startup+650.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20515 0 0 0 64953 54 0 0 25 0 1 0 491858277 74493952 16557 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18187 16557 603 41 0 18146 0
vsize: 72748
[startup+660.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20628 0 0 0 65953 54 0 0 25 0 1 0 491858277 74878976 16670 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18281 16670 603 41 0 18240 0
vsize: 73124
[startup+670.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20675 0 0 0 66953 54 0 0 25 0 1 0 491858277 75137024 16717 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18344 16717 603 41 0 18303 0
vsize: 73376
[startup+680.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20739 0 0 0 67953 55 0 0 25 0 1 0 491858277 75390976 16781 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18406 16781 603 41 0 18365 0
vsize: 73624
[startup+690.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20820 0 0 0 68953 55 0 0 25 0 1 0 491858277 75644928 16862 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18468 16862 603 41 0 18427 0
vsize: 73872
[startup+700.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 20943 0 0 0 69952 56 0 0 25 0 1 0 491858277 76177408 16985 4294967295 134512640 134672761 3221224624 3221223728 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18598 16985 603 41 0 18557 0
vsize: 74392
[startup+710.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21043 0 0 0 70952 56 0 0 25 0 1 0 491858277 76578816 17085 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18696 17085 603 41 0 18655 0
vsize: 74784
[startup+720.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21169 0 0 0 71952 56 0 0 25 0 1 0 491858277 77119488 17211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18828 17211 603 41 0 18787 0
vsize: 75312
[startup+730.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21236 0 0 0 72952 56 0 0 25 0 1 0 491858277 77381632 17278 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18892 17278 603 41 0 18851 0
vsize: 75568
[startup+740.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21345 0 0 0 73952 57 0 0 25 0 1 0 491858277 77893632 17387 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19017 17387 603 41 0 18976 0
vsize: 76068
[startup+750.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21446 0 0 0 74952 57 0 0 25 0 1 0 491858277 78319616 17488 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19121 17488 603 41 0 19080 0
vsize: 76484
[startup+760.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21487 0 0 0 75951 57 0 0 25 0 1 0 491858277 78446592 17529 4294967295 134512640 134672761 3221224624 3221223760 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 17529 603 41 0 19111 0
vsize: 76608
[startup+770.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21526 0 0 0 76951 58 0 0 25 0 1 0 491858277 78573568 17568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19183 17568 603 41 0 19142 0
vsize: 76732
[startup+780.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21573 0 0 0 77952 58 0 0 25 0 1 0 491858277 78839808 17615 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 17615 603 41 0 19207 0
vsize: 76992
[startup+790.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21599 0 0 0 78952 58 0 0 25 0 1 0 491858277 78839808 17641 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 17641 603 41 0 19207 0
vsize: 76992
[startup+800.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21620 0 0 0 79952 58 0 0 25 0 1 0 491858277 78970880 17662 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19280 17662 603 41 0 19239 0
vsize: 77120
[startup+810.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21637 0 0 0 80952 58 0 0 25 0 1 0 491858277 79106048 17679 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 17679 603 41 0 19272 0
vsize: 77252
[startup+820.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21657 0 0 0 81952 58 0 0 25 0 1 0 491858277 79106048 17699 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 17699 603 41 0 19272 0
vsize: 77252
[startup+830.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21687 0 0 0 82952 58 0 0 25 0 1 0 491858277 79237120 17729 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19345 17729 603 41 0 19304 0
vsize: 77380
[startup+840.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21710 0 0 0 83952 58 0 0 25 0 1 0 491858277 79372288 17752 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19378 17752 603 41 0 19337 0
vsize: 77512
[startup+850.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21726 0 0 0 84953 58 0 0 25 0 1 0 491858277 79372288 17768 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19378 17768 603 41 0 19337 0
vsize: 77512
[startup+860.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21744 0 0 0 85953 58 0 0 25 0 1 0 491858277 79507456 17786 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19411 17786 603 41 0 19370 0
vsize: 77644
[startup+870.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21785 0 0 0 86953 58 0 0 25 0 1 0 491858277 79642624 17827 4294967295 134512640 134672761 3221224624 3221223808 134558671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19444 17827 603 41 0 19403 0
vsize: 77776
[startup+880.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21799 0 0 0 87953 58 0 0 25 0 1 0 491858277 79773696 17841 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 17841 603 41 0 19435 0
vsize: 77904
[startup+890.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21822 0 0 0 88953 58 0 0 25 0 1 0 491858277 79773696 17864 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 17864 603 41 0 19435 0
vsize: 77904
[startup+900.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21853 0 0 0 89953 59 0 0 25 0 1 0 491858277 79904768 17895 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19508 17895 603 41 0 19467 0
vsize: 78032
[startup+910.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21898 0 0 0 90953 59 0 0 25 0 1 0 491858277 80175104 17940 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 17940 603 41 0 19533 0
vsize: 78296
[startup+920.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21925 0 0 0 91953 59 0 0 25 0 1 0 491858277 80175104 17967 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 17967 603 41 0 19533 0
vsize: 78296
[startup+930.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21961 0 0 0 92953 59 0 0 25 0 1 0 491858277 80310272 18003 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19607 18003 603 41 0 19566 0
vsize: 78428
[startup+940.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 21986 0 0 0 93953 59 0 0 25 0 1 0 491858277 80445440 18028 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19640 18028 603 41 0 19599 0
vsize: 78560
[startup+950.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22012 0 0 0 94953 60 0 0 25 0 1 0 491858277 80580608 18054 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19673 18054 603 41 0 19632 0
vsize: 78692
[startup+960.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22043 0 0 0 95953 60 0 0 25 0 1 0 491858277 80715776 18085 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18085 603 41 0 19665 0
vsize: 78824
[startup+970.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22057 0 0 0 96953 60 0 0 25 0 1 0 491858277 80715776 18099 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18099 603 41 0 19665 0
vsize: 78824
[startup+980.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22078 0 0 0 97953 60 0 0 25 0 1 0 491858277 80855040 18120 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 18120 603 41 0 19699 0
vsize: 78960
[startup+990.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22122 0 0 0 98953 60 0 0 25 0 1 0 491858277 80986112 18164 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19772 18164 603 41 0 19731 0
vsize: 79088
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22246 0 0 0 99953 60 0 0 25 0 1 0 491858277 81510400 18288 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19900 18288 603 41 0 19859 0
vsize: 79600
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22350 0 0 0 100953 61 0 0 25 0 1 0 491858277 81911808 18392 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19998 18392 603 41 0 19957 0
vsize: 79992
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22437 0 0 0 101953 61 0 0 25 0 1 0 491858277 82305024 18479 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 18479 603 41 0 20053 0
vsize: 80376
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22523 0 0 0 102953 61 0 0 25 0 1 0 491858277 82698240 18565 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20190 18565 603 41 0 20149 0
vsize: 80760
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22620 0 0 0 103953 61 0 0 25 0 1 0 491858277 83075072 18662 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20282 18662 603 41 0 20241 0
vsize: 81128
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22685 0 0 0 104953 61 0 0 25 0 1 0 491858277 83357696 18727 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20351 18727 603 41 0 20310 0
vsize: 81404
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22781 0 0 0 105952 62 0 0 25 0 1 0 491858277 83767296 18823 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20451 18823 603 41 0 20410 0
vsize: 81804
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22845 0 0 0 106952 62 0 0 25 0 1 0 491858277 84037632 18887 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20517 18887 603 41 0 20476 0
vsize: 82068
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 22919 0 0 0 107952 62 0 0 25 0 1 0 491858277 84287488 18961 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20578 18961 603 41 0 20537 0
vsize: 82312
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 108952 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 109952 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134559875 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.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 110952 63 0 0 25 0 1 0 491858277 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+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 111952 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 112952 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560529 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.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 113952 63 0 0 25 0 1 0 491858277 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+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 114953 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560885 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.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 115953 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560198 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.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 116953 63 0 0 25 0 1 0 491858277 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
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 117953 63 0 0 25 0 1 0 491858277 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+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 118953 63 0 0 25 0 1 0 491858277 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 535
Raw data (stat): 535 (minisat+) R 534 30854 30853 0 -1 0 23013 0 0 0 119954 63 0 0 25 0 1 0 491858277 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 535
Raw data (stat): 535 (minisat+) Z 534 30854 30853 0 -1 12 23016 0 0 0 119954 67 0 0 25 0 1 0 491858277 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.54
CPU system time (s): 0.672897
CPU usage (%): 100.013
Max. virtual memory (Kb): 82524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####