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 30716

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-05-25 18:48:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22110 boxname=wulflinc21 idbench=926 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 22110
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        525728 kB
Buffers:         34784 kB
Cached:         446376 kB
SwapCached:        960 kB
Active:          16820 kB
Inactive:       466476 kB
HighTotal:      131008 kB
HighFree:        34076 kB
LowTotal:       903652 kB
LowFree:        491652 kB
SwapTotal:     2097892 kB
SwapFree:      2096008 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            19824 kB
Committed_AS:    63916 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 19:09:04 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22110 7 1229.87 152
#### 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 17155 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.95 0.90 2/55 17151
Raw data (stat): 17151 (runsolver) R 17150 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 718426868 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.99952 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+29.9999 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0008 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 17155
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.103 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 17208
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.103 s]
Raw data (loadavg): 1.06 0.99 0.91 2/56 17208
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.103 s]
Raw data (loadavg): 1.05 0.99 0.91 2/56 17208
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.103 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 17208
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.102 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 17208
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.103 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 17208
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.104 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 17210
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.103 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.104 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.104 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.104 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.105 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.105 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.104 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.107 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17212
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 17214
Raw data (stat): 17151 (minisat+_script) S 17150 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 718426868 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.87
CPU user time (s): 1229.1
CPU system time (s): 0.770882
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####