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/miplib3/normalized-mps-v2-20-10-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.01784
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 16352

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 07:01:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13629 boxname=wulflinc11 idbench=1049 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 13629
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        767960 kB
Buffers:         28368 kB
Cached:         217452 kB
SwapCached:          0 kB
Active:          90552 kB
Inactive:       158092 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        767708 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              56 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12324 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:21:47 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 13629 7 1200.22 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.79 0.96 0.96 2/54 30219
Raw data (stat): 30219 (runsolver) R 30218 32461 32460 0 -1 64 2 0 0 0 0 0 0 0 19 0 1 0 484896782 1052672 97 4294967295 134512640 135381576 3221224512 3221219872 134891116 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.82 0.96 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 9697 0 0 0 977 21 0 0 25 0 1 0 484896782 30670848 5914 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7488 5914 603 41 0 7447 0
vsize: 29952
[startup+20.0004 s]
Raw data (loadavg): 0.85 0.96 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 9748 0 0 0 1977 21 0 0 25 0 1 0 484896782 30806016 5965 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.0013 s]
Raw data (loadavg): 0.87 0.96 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 9896 0 0 0 2976 22 0 0 25 0 1 0 484896782 31346688 6113 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7653 6113 603 41 0 7612 0
vsize: 30612
[startup+40.0013 s]
Raw data (loadavg): 0.89 0.96 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10064 0 0 0 3975 23 0 0 25 0 1 0 484896782 32022528 6281 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7818 6281 603 41 0 7777 0
vsize: 31272
[startup+50.0017 s]
Raw data (loadavg): 0.91 0.96 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10309 0 0 0 4975 24 0 0 25 0 1 0 484896782 32821248 6484 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.92 0.96 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10335 0 0 0 5975 24 0 0 25 0 1 0 484896782 32952320 6510 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8045 6510 603 41 0 8004 0
vsize: 32180
[startup+70.0019 s]
Raw data (loadavg): 0.93 0.97 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10373 0 0 0 6974 24 0 0 25 0 1 0 484896782 33243136 6548 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8116 6548 603 41 0 8075 0
vsize: 32464
[startup+80.0023 s]
Raw data (loadavg): 0.94 0.97 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10458 0 0 0 7973 24 0 0 25 0 1 0 484896782 33435648 6606 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 6606 603 41 0 8122 0
vsize: 32652
[startup+90.0019 s]
Raw data (loadavg): 1.02 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10580 0 0 0 8973 24 0 0 25 0 1 0 484896782 33976320 6728 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8295 6728 603 41 0 8254 0
vsize: 33180
[startup+100.003 s]
Raw data (loadavg): 1.02 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10635 0 0 0 9973 25 0 0 25 0 1 0 484896782 34107392 6783 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 6783 603 41 0 8286 0
vsize: 33308
[startup+110.003 s]
Raw data (loadavg): 1.02 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 10924 0 0 0 10972 25 0 0 25 0 1 0 484896782 34996224 6991 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8544 6991 603 41 0 8503 0
vsize: 34176
[startup+120.003 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11127 0 0 0 11972 26 0 0 25 0 1 0 484896782 35700736 7169 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8716 7169 603 41 0 8675 0
vsize: 34864
[startup+130.003 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11202 0 0 0 12972 26 0 0 25 0 1 0 484896782 36089856 7244 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8811 7244 603 41 0 8770 0
vsize: 35244
[startup+140.003 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11318 0 0 0 13971 27 0 0 25 0 1 0 484896782 36491264 7360 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8909 7360 603 41 0 8868 0
vsize: 35636
[startup+150.004 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11381 0 0 0 14972 27 0 0 25 0 1 0 484896782 36761600 7423 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8975 7423 603 41 0 8934 0
vsize: 35900
[startup+160.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11439 0 0 0 15971 27 0 0 25 0 1 0 484896782 37023744 7481 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9039 7481 603 41 0 8998 0
vsize: 36156
[startup+170.003 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11569 0 0 0 16971 28 0 0 25 0 1 0 484896782 37548032 7611 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9167 7611 603 41 0 9126 0
vsize: 36668
[startup+180.003 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 11774 0 0 0 17971 28 0 0 25 0 1 0 484896782 38350848 7816 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9363 7816 603 41 0 9322 0
vsize: 37452
[startup+190.003 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 12033 0 0 0 18970 29 0 0 25 0 1 0 484896782 39419904 8075 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9624 8075 603 41 0 9583 0
vsize: 38496
[startup+200.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 12597 0 0 0 19969 30 0 0 25 0 1 0 484896782 41672704 8639 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10174 8639 603 41 0 10133 0
vsize: 40696
[startup+210.003 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 12795 0 0 0 20968 31 0 0 25 0 1 0 484896782 42471424 8837 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 8837 603 41 0 10328 0
vsize: 41476
[startup+220.003 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 13159 0 0 0 21968 32 0 0 25 0 1 0 484896782 43941888 9201 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10728 9201 603 41 0 10687 0
vsize: 42912
[startup+230.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30219
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 13331 0 0 0 22967 32 0 0 25 0 1 0 484896782 44867584 9373 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10954 9373 603 41 0 10913 0
vsize: 43816
[startup+240.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 13544 0 0 0 23967 33 0 0 25 0 1 0 484896782 45678592 9586 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11152 9586 603 41 0 11111 0
vsize: 44608
[startup+250.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 13854 0 0 0 24967 34 0 0 25 0 1 0 484896782 47013888 9896 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11478 9896 603 41 0 11437 0
vsize: 45912
[startup+260.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 14104 0 0 0 25966 34 0 0 25 0 1 0 484896782 47951872 10146 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 10146 603 41 0 11666 0
vsize: 46828
[startup+270.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 14389 0 0 0 26966 34 0 0 25 0 1 0 484896782 49156096 10431 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12001 10431 603 41 0 11960 0
vsize: 48004
[startup+280.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 14550 0 0 0 27966 34 0 0 25 0 1 0 484896782 49799168 10592 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12158 10592 603 41 0 12117 0
vsize: 48632
[startup+290.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 14859 0 0 0 28966 35 0 0 25 0 1 0 484896782 51122176 10901 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12481 10901 603 41 0 12440 0
vsize: 49924
[startup+300.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 15075 0 0 0 29966 35 0 0 25 0 1 0 484896782 51916800 11117 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12675 11117 603 41 0 12634 0
vsize: 50700
[startup+310.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 15273 0 0 0 30965 36 0 0 25 0 1 0 484896782 52711424 11315 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12869 11315 603 41 0 12828 0
vsize: 51476
[startup+320.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 15498 0 0 0 31964 37 0 0 25 0 1 0 484896782 53645312 11540 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13097 11540 603 41 0 13056 0
vsize: 52388
[startup+330.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 15735 0 0 0 32964 38 0 0 25 0 1 0 484896782 54575104 11777 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13324 11777 603 41 0 13283 0
vsize: 53296
[startup+340.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 15919 0 0 0 33964 38 0 0 25 0 1 0 484896782 55369728 11961 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13518 11961 603 41 0 13477 0
vsize: 54072
[startup+350.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 16119 0 0 0 34963 39 0 0 25 0 1 0 484896782 56168448 12161 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13713 12161 603 41 0 13672 0
vsize: 54852
[startup+360.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 16308 0 0 0 35962 40 0 0 25 0 1 0 484896782 56963072 12350 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13907 12350 603 41 0 13866 0
vsize: 55628
[startup+370.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 16503 0 0 0 36962 40 0 0 25 0 1 0 484896782 57765888 12545 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14103 12545 603 41 0 14062 0
vsize: 56412
[startup+380.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 16768 0 0 0 37962 41 0 0 25 0 1 0 484896782 58843136 12810 4294967295 134512640 134672761 3221224624 3221223808 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14366 12810 603 41 0 14325 0
vsize: 57464
[startup+390.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 17003 0 0 0 38961 41 0 0 25 0 1 0 484896782 59772928 13045 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14593 13045 603 41 0 14552 0
vsize: 58372
[startup+400.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 17120 0 0 0 39961 41 0 0 25 0 1 0 484896782 60309504 13162 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14724 13162 603 41 0 14683 0
vsize: 58896
[startup+410.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 17246 0 0 0 40961 42 0 0 25 0 1 0 484896782 60846080 13288 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14855 13288 603 41 0 14814 0
vsize: 59420
[startup+420.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 17517 0 0 0 41960 44 0 0 25 0 1 0 484896782 61911040 13559 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15115 13559 603 41 0 15074 0
vsize: 60460
[startup+430.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 17766 0 0 0 42959 44 0 0 25 0 1 0 484896782 62849024 13808 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15344 13808 603 41 0 15303 0
vsize: 61376
[startup+440.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 18052 0 0 0 43959 45 0 0 25 0 1 0 484896782 64049152 14094 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15637 14094 603 41 0 15596 0
vsize: 62548
[startup+450.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 18395 0 0 0 44958 46 0 0 25 0 1 0 484896782 65503232 14437 4294967295 134512640 134672761 3221224624 3221223760 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15992 14437 603 41 0 15951 0
vsize: 63968
[startup+460.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 18448 0 0 0 45958 46 0 0 25 0 1 0 484896782 65638400 14490 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16025 14490 603 41 0 15984 0
vsize: 64100
[startup+470.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 18610 0 0 0 46957 47 0 0 25 0 1 0 484896782 66301952 14652 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16187 14652 603 41 0 16146 0
vsize: 64748
[startup+480.009 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 18811 0 0 0 47957 47 0 0 25 0 1 0 484896782 67104768 14853 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16383 14853 603 41 0 16342 0
vsize: 65532
[startup+490.009 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 18993 0 0 0 48956 48 0 0 25 0 1 0 484896782 67895296 15035 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16576 15035 603 41 0 16535 0
vsize: 66304
[startup+500.009 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19163 0 0 0 49956 49 0 0 25 0 1 0 484896782 68956160 15205 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16835 15205 603 41 0 16794 0
vsize: 67340
[startup+510.01 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19214 0 0 0 50956 49 0 0 25 0 1 0 484896782 69214208 15256 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16898 15256 603 41 0 16857 0
vsize: 67592
[startup+520.01 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19331 0 0 0 51956 49 0 0 25 0 1 0 484896782 69611520 15373 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16995 15373 603 41 0 16954 0
vsize: 67980
[startup+530.01 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19470 0 0 0 52956 50 0 0 25 0 1 0 484896782 70144000 15512 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17125 15512 603 41 0 17084 0
vsize: 68500
[startup+540.01 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19569 0 0 0 53956 50 0 0 25 0 1 0 484896782 70541312 15611 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17222 15611 603 41 0 17181 0
vsize: 68888
[startup+550.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19612 0 0 0 54956 50 0 0 25 0 1 0 484896782 70799360 15654 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 15654 603 41 0 17244 0
vsize: 69140
[startup+560.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19652 0 0 0 55956 50 0 0 25 0 1 0 484896782 70934528 15694 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17318 15694 603 41 0 17277 0
vsize: 69272
[startup+570.01 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19746 0 0 0 56956 51 0 0 25 0 1 0 484896782 71331840 15788 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17415 15788 603 41 0 17374 0
vsize: 69660
[startup+580.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19867 0 0 0 57955 51 0 0 25 0 1 0 484896782 71872512 15909 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17547 15909 603 41 0 17506 0
vsize: 70188
[startup+590.01 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 19963 0 0 0 58955 51 0 0 25 0 1 0 484896782 72261632 16005 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17642 16005 603 41 0 17601 0
vsize: 70568
[startup+600.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20071 0 0 0 59955 51 0 0 25 0 1 0 484896782 72654848 16113 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17738 16113 603 41 0 17697 0
vsize: 70952
[startup+610.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20181 0 0 0 60955 52 0 0 25 0 1 0 484896782 73056256 16223 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17836 16223 603 41 0 17795 0
vsize: 71344
[startup+620.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20309 0 0 0 61955 52 0 0 25 0 1 0 484896782 73572352 16351 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17962 16351 603 41 0 17921 0
vsize: 71848
[startup+630.011 s]
Raw data (loadavg): 1.00 0.98 0.96 3/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20397 0 0 0 62955 53 0 0 25 0 1 0 484896782 73981952 16439 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18062 16439 603 41 0 18021 0
vsize: 72248
[startup+640.011 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20507 0 0 0 63955 53 0 0 25 0 1 0 484896782 74493952 16549 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18187 16549 603 41 0 18146 0
vsize: 72748
[startup+650.012 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20618 0 0 0 64955 53 0 0 25 0 1 0 484896782 74878976 16660 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18281 16660 603 41 0 18240 0
vsize: 73124
[startup+660.013 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20672 0 0 0 65955 53 0 0 25 0 1 0 484896782 75137024 16714 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18344 16714 603 41 0 18303 0
vsize: 73376
[startup+670.013 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20731 0 0 0 66955 53 0 0 25 0 1 0 484896782 75390976 16773 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18406 16773 603 41 0 18365 0
vsize: 73624
[startup+680.014 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20802 0 0 0 67955 53 0 0 25 0 1 0 484896782 75644928 16844 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18468 16844 603 41 0 18427 0
vsize: 73872
[startup+690.014 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 20936 0 0 0 68955 53 0 0 25 0 1 0 484896782 76177408 16978 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18598 16978 603 41 0 18557 0
vsize: 74392
[startup+700.015 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21033 0 0 0 69955 54 0 0 25 0 1 0 484896782 76578816 17075 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18696 17075 603 41 0 18655 0
vsize: 74784
[startup+710.015 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21162 0 0 0 70955 54 0 0 25 0 1 0 484896782 77119488 17204 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18828 17204 603 41 0 18787 0
vsize: 75312
[startup+720.015 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21230 0 0 0 71955 54 0 0 25 0 1 0 484896782 77381632 17272 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18892 17272 603 41 0 18851 0
vsize: 75568
[startup+730.015 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21332 0 0 0 72955 55 0 0 25 0 1 0 484896782 77758464 17374 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18984 17374 603 41 0 18943 0
vsize: 75936
[startup+740.015 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21440 0 0 0 73954 55 0 0 25 0 1 0 484896782 78184448 17482 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19088 17482 603 41 0 19047 0
vsize: 76352
[startup+750.016 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21482 0 0 0 74954 55 0 0 25 0 1 0 484896782 78446592 17524 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 17524 603 41 0 19111 0
vsize: 76608
[startup+760.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21524 0 0 0 75954 56 0 0 25 0 1 0 484896782 78573568 17566 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19183 17566 603 41 0 19142 0
vsize: 76732
[startup+770.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21571 0 0 0 76954 56 0 0 25 0 1 0 484896782 78839808 17613 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 17613 603 41 0 19207 0
vsize: 76992
[startup+780.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21599 0 0 0 77954 56 0 0 25 0 1 0 484896782 78839808 17641 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 17641 603 41 0 19207 0
vsize: 76992
[startup+790.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21620 0 0 0 78954 56 0 0 25 0 1 0 484896782 78970880 17662 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19280 17662 603 41 0 19239 0
vsize: 77120
[startup+800.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21637 0 0 0 79954 56 0 0 25 0 1 0 484896782 79106048 17679 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 17679 603 41 0 19272 0
vsize: 77252
[startup+810.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21658 0 0 0 80954 56 0 0 25 0 1 0 484896782 79106048 17700 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19313 17700 603 41 0 19272 0
vsize: 77252
[startup+820.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21687 0 0 0 81954 56 0 0 25 0 1 0 484896782 79237120 17729 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19345 17729 603 41 0 19304 0
vsize: 77380
[startup+830.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21712 0 0 0 82955 56 0 0 25 0 1 0 484896782 79372288 17754 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19378 17754 603 41 0 19337 0
vsize: 77512
[startup+840.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21726 0 0 0 83955 56 0 0 25 0 1 0 484896782 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+850.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21752 0 0 0 84955 56 0 0 25 0 1 0 484896782 79507456 17794 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19411 17794 603 41 0 19370 0
vsize: 77644
[startup+860.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21788 0 0 0 85955 56 0 0 25 0 1 0 484896782 79642624 17830 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19444 17830 603 41 0 19403 0
vsize: 77776
[startup+870.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21801 0 0 0 86955 56 0 0 25 0 1 0 484896782 79773696 17843 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 17843 603 41 0 19435 0
vsize: 77904
[startup+880.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21825 0 0 0 87955 56 0 0 25 0 1 0 484896782 79773696 17867 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 17867 603 41 0 19435 0
vsize: 77904
[startup+890.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21868 0 0 0 88955 56 0 0 25 0 1 0 484896782 80039936 17910 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19541 17910 603 41 0 19500 0
vsize: 78164
[startup+900.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21905 0 0 0 89956 56 0 0 25 0 1 0 484896782 80175104 17947 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 17947 603 41 0 19533 0
vsize: 78296
[startup+910.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21930 0 0 0 90955 56 0 0 25 0 1 0 484896782 80310272 17972 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19607 17972 603 41 0 19566 0
vsize: 78428
[startup+920.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21967 0 0 0 91955 57 0 0 25 0 1 0 484896782 80445440 18009 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19640 18009 603 41 0 19599 0
vsize: 78560
[startup+930.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 21990 0 0 0 92956 57 0 0 25 0 1 0 484896782 80445440 18032 4294967295 134512640 134672761 3221224624 3221223780 134565154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19640 18032 603 41 0 19599 0
vsize: 78560
[startup+940.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22018 0 0 0 93956 57 0 0 25 0 1 0 484896782 80580608 18060 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19673 18060 603 41 0 19632 0
vsize: 78692
[startup+950.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22043 0 0 0 94956 57 0 0 25 0 1 0 484896782 80715776 18085 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19706 18085 603 41 0 19665 0
vsize: 78824
[startup+960.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22064 0 0 0 95956 57 0 0 25 0 1 0 484896782 80855040 18106 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 18106 603 41 0 19699 0
vsize: 78960
[startup+970.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22086 0 0 0 96956 57 0 0 25 0 1 0 484896782 80855040 18128 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19740 18128 603 41 0 19699 0
vsize: 78960
[startup+980.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22155 0 0 0 97956 58 0 0 25 0 1 0 484896782 81117184 18197 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19804 18197 603 41 0 19763 0
vsize: 79216
[startup+990.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22276 0 0 0 98956 58 0 0 25 0 1 0 484896782 81641472 18318 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19932 18318 603 41 0 19891 0
vsize: 79728
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22381 0 0 0 99956 58 0 0 25 0 1 0 484896782 82038784 18423 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20029 18423 603 41 0 19988 0
vsize: 80116
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22473 0 0 0 100955 58 0 0 25 0 1 0 484896782 82440192 18515 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20127 18515 603 41 0 20086 0
vsize: 80508
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22559 0 0 0 101956 58 0 0 25 0 1 0 484896782 82821120 18601 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20220 18601 603 41 0 20179 0
vsize: 80880
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22639 0 0 0 102956 59 0 0 25 0 1 0 484896782 83075072 18681 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20282 18681 603 41 0 20241 0
vsize: 81128
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22715 0 0 0 103956 59 0 0 25 0 1 0 484896782 83492864 18757 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 18757 603 41 0 20343 0
vsize: 81536
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22811 0 0 0 104956 59 0 0 25 0 1 0 484896782 83902464 18853 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20484 18853 603 41 0 20443 0
vsize: 81936
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22874 0 0 0 105956 59 0 0 25 0 1 0 484896782 84037632 18916 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20517 18916 603 41 0 20476 0
vsize: 82068
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 22957 0 0 0 106956 59 0 0 25 0 1 0 484896782 84418560 18999 4294967295 134512640 134672761 3221224624 3221223748 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20610 18999 603 41 0 20569 0
vsize: 82440
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 107955 60 0 0 25 0 1 0 484896782 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+1090.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 108955 60 0 0 25 0 1 0 484896782 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+1100.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 109955 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134561229 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): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 110955 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560246 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): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 111955 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 112955 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 113956 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 114956 60 0 0 25 0 1 0 484896782 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+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 115956 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 116956 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 117957 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 118957 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 30221
Raw data (stat): 30219 (minisat+) R 30218 32461 32460 0 -1 0 23013 0 0 0 119957 60 0 0 25 0 1 0 484896782 84504576 19031 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19031 603 41 0 20590 0
vsize: 82524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.98 0.96 1/54 30221
Raw data (stat): 30219 (minisat+) Z 30218 32461 32460 0 -1 12 23016 0 0 0 119957 64 0 0 25 0 1 0 484896782 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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