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

Namenormalized-opb/submitted/manquinho/logic-synthesis/normalized-clip.b.opb
MD5SUMcddae768b283c2db142f16fe9d163db1
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 15
Optimality of the best value was proved NO
Number of terms in the objective function 350
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 350
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 350
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.05084
Number of variables349
Total number of constraints715
Number of constraints which are clauses707
Number of constraints which are cardinality constraints (but not clauses)8
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint111

Trace number 34768

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-28 10:30:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23990 boxname=wulflinc1 idbench=64 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cddae768b283c2db142f16fe9d163db1  /oldhome/oroussel/tmp/wulflinc1/normalized-clip.b.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc1/normalized-clip.b.opb
IDLAUNCH: 23990
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        521944 kB
Buffers:         37512 kB
Cached:         450988 kB
SwapCached:        760 kB
Active:          66020 kB
Inactive:       424772 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        521692 kB
SwapTotal:     2097136 kB
SwapFree:      2095368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            16144 kB
Committed_AS:    92716 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 10:41:57 (client local time) WITH STATUS 30 IN 661.758 SECONDS
stats: 23990 0 661.758 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...
c got solution with objective value: 94
c [startup+5.2216 s]  setting bit 8 to 1
c CONFLICT during preprocess 
c [startup+5.42421 s]  setting bit 7 to 0
c got solution with objective value: 30
c [startup+10.9329 s]  setting bit 6 to 1
c CONFLICT during preprocess 
c [startup+11.1312 s]  setting bit 5 to 0

Decision: 58312/62137	Time: 23.9844/86400
Decision: 58520/62137	Time: 29.9484/86400
Decision: 58520/62137	Time: 36.5035/86400
Decision: 58520/62137	Time: 44.0833/86400
Decision: 58520/62137	Time: 53.4689/86400
Decision: 58520/62137	Time: 60.2188/86400
Decision: 58520/62137	Time: 67.3398/86400
Decision: 58706/62137	Time: 74.3787/86400
Decision: 58706/62137	Time: 81.7046/86400
Decision: 58706/62137	Time: 88.7505/86400
Decision: 58706/62137	Time: 96.4313/86400
Decision: 58706/62137	Time: 103.59/86400
Decision: 58944/62137	Time: 113.356/86400
Decision: 58944/62137	Time: 120.91/86400
Decision: 58944/62137	Time: 127.867/86400
Decision: 58944/62137	Time: 134.804/86400
Decision: 58944/62137	Time: 141.43/86400
Decision: 58944/62137	Time: 148.047/86400
Decision: 58944/62137	Time: 156.497/86400
Decision: 58944/62137	Time: 164.328/86400
Decision: 58944/62137	Time: 171.979/86400
Decision: 58944/62137	Time: 179.765/86400
Decision: 58944/62137	Time: 186.302/86400
Decision: 58944/62137	Time: 194.456/86400
Decision: 58944/62137	Time: 200.482/86400
Decision: 58944/62137	Time: 208.204/86400
Decision: 58944/62137	Time: 216.74/86400
Decision: 58944/62137	Time: 225.034/86400
Decision: 58944/62137	Time: 232.451/86400
Decision: 58944/62137	Time: 239.976/86400
Decision: 58944/62137	Time: 247.202/86400
Decision: 58944/62137	Time: 254.497/86400
Decision: 58944/62137	Time: 262.555/86400
Decision: 58944/62137	Time: 269.903/86400
Decision: 58944/62137	Time: 276.052/86400
Decision: 58944/62137	Time: 283.96/86400
Decision: 58944/62137	Time: 290.374/86400
Decision: 58944/62137	Time: 297.518/86400
Decision: 58944/62137	Time: 304.983/86400
Decision: 58944/62137	Time: 312.802/86400
Decision: 58944/62137	Time: 320.215/86400
Decision: 58944/62137	Time: 327.796/86400
Decision: 58944/62137	Time: 335.618/86400
Decision: 58944/62137	Time: 343.059/86400
Decision: 58944/62137	Time: 350.795/86400
Decision: 58944/62137	Time: 358.137/86400
Decision: 58944/62137	Time: 365.063/86400
Decision: 58944/62137	Time: 372.658/86400
Decision: 58944/62137	Time: 381.151/86400
Decision: 58944/62137	Time: 387.489/86400
Decision: 58944/62137	Time: 397.15/86400
Decision: 58944/62137	Time: 405.437/86400
Decision: 58944/62137	Time: 412.467/86400
Decision: 58944/62137	Time: 418.313/86400
Decision: 58944/62137	Time: 425.029/86400
Decision: 58944/62137	Time: 433.328/86400
Decision: 58944/62137	Time: 440.775/86400
Decision: 59132/62137	Time: 452.45/86400
Decision: 59132/62137	Time: 459.669/86400
Decision: 59132/62137	Time: 468.446/86400
Decision: 59132/62137	Time: 476.24/86400
Decision: 59132/62137	Time: 485.082/86400
Decision: 59132/62137	Time: 492.821/86400
Decision: 59510/62137	Time: 516.12/86400c [startup+540.273 s]  setting bit 4 to 0
c got solution with objective value: 22
c [startup+542.924 s]  setting bit 3 to 1
c got solution with objective value: 18
c [startup+547.072 s]  setting bit 2 to 1
c got solution with objective value: 16
c [startup+559.352 s]  setting bit 1 to 1

Decision: 58367/62137	Time: 73.5038/86400
Decision: 58367/62137	Time: 82.4565/86400
Decision: 58367/62137	Time: 91.0822/86400
Decision: 58367/62137	Time: 97.8401/86400c got solution with objective value: 15
c [startup+661.5 s]  setting bit 0 to 1
s OPTIMUM FOUND
v -x1 -x10 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x11 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x12 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x13 -x130 -x131 -x132 -x133 -x134 -x135 -x136 x137 -x138 -x139 -x14 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 x15 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x16 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x17 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x18 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x19 -x190 -x191 -x192 x193 -x194 -x195 -x196 -x197 -x198 -x199 -x2 -x20 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x21 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x22 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x23 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x24 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x25 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x26 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 x269 -x27 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x28 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x29 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x3 -x30 -x300 -x301 x302 -x303 x304 -x305 -x306 -x307 -x308 -x309 -x31 -x310 -x311 -x312 x313 -x314 -x315 -x316 -x317 -x318 -x319 -x32 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x33 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x34 -x340 -x341 x342 -x343 -x344 -x345 -x346 x347 -x348 -x349 -x35 -x350 -x36 -x37 -x38 -x39 -x4 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x5 -x50 -x51 -x52 x53 -x54 -x55 -x56 -x57 -x58 x59 -x6 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 x69 -x7 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x8 -x80 -x81 -x82 x83 -x84 -x85 -x86 -x87 -x88 -x89 -x9 -x90 x91 -x92 -x93 -x94 -x95 x96 -x97 -x98 -x99 
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.92 0.95 0.70 1/55 18319
Raw data (stat): 18319 (runsolver) D 18318 8378 8377 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 749020843 884736 94 4294967295 134512640 135332820 3221224480 3221219660 135092226 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.96 0.70 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 8727 0 0 0 982 17 0 0 25 0 1 0 749020843 25067520 5649 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6120 5649 300 300 0 5820 0
vsize: 24480
[startup+20.008 s]
Raw data (loadavg): 0.94 0.96 0.70 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 9012 0 0 0 1982 18 0 0 25 0 1 0 749020843 25067520 5690 4294967295 134512640 135726644 3221224592 3221223184 134760008 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6120 5690 300 300 0 5820 0
vsize: 24480
[startup+30.0077 s]
Raw data (loadavg): 0.95 0.96 0.71 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 9059 0 0 0 2981 18 0 0 25 0 1 0 749020843 25067520 5737 4294967295 134512640 135726644 3221224592 3221223248 134731248 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6120 5737 300 300 0 5820 0
vsize: 24480
[startup+40.0085 s]
Raw data (loadavg): 0.96 0.96 0.71 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 9203 0 0 0 3981 19 0 0 25 0 1 0 749020843 25067520 5759 4294967295 134512640 135726644 3221224592 3221223088 134743980 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6120 5759 300 300 0 5820 0
vsize: 24480
[startup+50.0093 s]
Raw data (loadavg): 0.96 0.96 0.71 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 9517 0 0 0 4979 20 0 0 25 0 1 0 749020843 25202688 5829 4294967295 134512640 135726644 3221224592 3221223088 134743996 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6153 5829 300 300 0 5853 0
vsize: 24612
[startup+60.009 s]
Raw data (loadavg): 0.97 0.96 0.71 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 9690 0 0 0 5979 21 0 0 25 0 1 0 749020843 29532160 5880 4294967295 134512640 135726644 3221224592 3221223088 134743980 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7210 5880 300 300 0 6910 0
vsize: 28840
[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.72 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 9863 0 0 0 6978 22 0 0 25 0 1 0 749020843 29532160 5931 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7210 5931 300 300 0 6910 0
vsize: 28840
[startup+80.0096 s]
Raw data (loadavg): 0.98 0.96 0.72 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 10129 0 0 0 7978 23 0 0 25 0 1 0 749020843 29532160 5953 4294967295 134512640 135726644 3221224592 3221223088 134744059 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7210 5953 300 300 0 6910 0
vsize: 28840
[startup+90.0103 s]
Raw data (loadavg): 0.98 0.96 0.72 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 10292 0 0 0 8977 24 0 0 25 0 1 0 749020843 29667328 5994 4294967295 134512640 135726644 3221224592 3221223088 134744063 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7243 5994 300 300 0 6943 0
vsize: 28972
[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.73 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 10604 0 0 0 9976 24 0 0 25 0 1 0 749020843 29667328 6062 4294967295 134512640 135726644 3221224592 3221223088 134743982 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7243 6062 300 300 0 6943 0
vsize: 28972
[startup+110.01 s]
Raw data (loadavg): 0.98 0.97 0.73 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 10772 0 0 0 10975 26 0 0 25 0 1 0 749020843 29802496 6108 4294967295 134512640 135726644 3221224592 3221223088 134743953 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7276 6108 300 300 0 6976 0
vsize: 29104
[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 10914 0 0 0 11973 28 0 0 25 0 1 0 749020843 29802496 6128 4294967295 134512640 135726644 3221224592 3221223088 134744147 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7276 6128 300 300 0 6976 0
vsize: 29104
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 11063 0 0 0 12972 29 0 0 25 0 1 0 749020843 29802496 6155 4294967295 134512640 135726644 3221224592 3221223088 134743953 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7276 6155 300 300 0 6976 0
vsize: 29104
[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.73 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 11366 0 0 0 13971 31 0 0 25 0 1 0 749020843 29937664 6214 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7309 6214 300 300 0 7009 0
vsize: 29236
[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 11529 0 0 0 14970 31 0 0 25 0 1 0 749020843 29937664 6255 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7309 6255 300 300 0 7009 0
vsize: 29236
[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 11786 0 0 0 15970 32 0 0 25 0 1 0 749020843 29937664 6268 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7309 6268 300 300 0 7009 0
vsize: 29236
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 13457 0 0 0 16965 36 0 0 25 0 1 0 749020843 36229120 6280 4294967295 134512640 135726644 3221224592 3221223088 134744004 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8845 6280 300 300 0 8545 0
vsize: 35380
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 13592 0 0 0 17965 37 0 0 25 0 1 0 749020843 36364288 6293 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8878 6293 300 300 0 8578 0
vsize: 35512
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.74 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 13737 0 0 0 18964 38 0 0 25 0 1 0 749020843 36364288 6316 4294967295 134512640 135726644 3221224592 3221223088 134744009 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8878 6316 300 300 0 8578 0
vsize: 35512
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 14000 0 0 0 19963 39 0 0 25 0 1 0 749020843 36507648 6335 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8913 6335 300 300 0 8613 0
vsize: 35652
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 14184 0 0 0 20962 40 0 0 25 0 1 0 749020843 36507648 6397 4294967295 134512640 135726644 3221224592 3221223088 134743980 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8913 6397 300 300 0 8613 0
vsize: 35652
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 14483 0 0 0 21961 42 0 0 25 0 1 0 749020843 36507648 6452 4294967295 134512640 135726644 3221224592 3221223088 134743961 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8913 6452 300 300 0 8613 0
vsize: 35652
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 14621 0 0 0 22960 42 0 0 25 0 1 0 749020843 36507648 6468 4294967295 134512640 135726644 3221224592 3221223088 134743999 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8913 6468 300 300 0 8613 0
vsize: 35652
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 14758 0 0 0 23960 43 0 0 25 0 1 0 749020843 36646912 6483 4294967295 134512640 135726644 3221224592 3221223088 134743996 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8947 6483 300 300 0 8647 0
vsize: 35788
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 14952 0 0 0 24958 45 0 0 25 0 1 0 749020843 36646912 6555 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8947 6555 300 300 0 8647 0
vsize: 35788
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 15264 0 0 0 25957 46 0 0 25 0 1 0 749020843 36782080 6623 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8980 6623 300 300 0 8680 0
vsize: 35920
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 15402 0 0 0 26956 47 0 0 25 0 1 0 749020843 36782080 6639 4294967295 134512640 135726644 3221224592 3221223088 134743990 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8980 6639 300 300 0 8680 0
vsize: 35920
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 15572 0 0 0 27955 48 0 0 25 0 1 0 749020843 36782080 6687 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8980 6687 300 300 0 8680 0
vsize: 35920
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 15889 0 0 0 28954 50 0 0 25 0 1 0 749020843 36782080 6760 4294967295 134512640 135726644 3221224592 3221223088 134744014 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8980 6760 300 300 0 8680 0
vsize: 35920
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 16051 0 0 0 29953 51 0 0 25 0 1 0 749020843 36921344 6800 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9014 6800 300 300 0 8714 0
vsize: 36056
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 16313 0 0 0 30952 52 0 0 25 0 1 0 749020843 36921344 6818 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9014 6818 300 300 0 8714 0
vsize: 36056
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 16452 0 0 0 31951 53 0 0 25 0 1 0 749020843 36921344 6835 4294967295 134512640 135726644 3221224592 3221223088 134744063 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9014 6835 300 300 0 8714 0
vsize: 36056
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 16614 0 0 0 32950 54 0 0 25 0 1 0 749020843 37056512 6875 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9047 6875 300 300 0 8747 0
vsize: 36188
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 16876 0 0 0 33950 55 0 0 25 0 1 0 749020843 37056512 6893 4294967295 134512640 135726644 3221224592 3221223088 134744004 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9047 6893 300 300 0 8747 0
vsize: 36188
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 17014 0 0 0 34948 56 0 0 25 0 1 0 749020843 37056512 6909 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9047 6909 300 300 0 8747 0
vsize: 36188
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 17210 0 0 0 35948 57 0 0 25 0 1 0 749020843 37056512 6983 4294967295 134512640 135726644 3221224592 3221223088 134743901 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9047 6983 300 300 0 8747 0
vsize: 36188
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 17542 0 0 0 36947 58 0 0 25 0 1 0 749020843 37195776 7071 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9081 7071 300 300 0 8781 0
vsize: 36324
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 17679 0 0 0 37946 59 0 0 25 0 1 0 749020843 37195776 7086 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 9081 7086 300 300 0 8781 0
vsize: 36324
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 17817 0 0 0 38945 60 0 0 25 0 1 0 749020843 37195776 7102 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9081 7102 300 300 0 8781 0
vsize: 36324
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 18072 0 0 0 39944 61 0 0 25 0 1 0 749020843 37339136 7113 4294967295 134512640 135726644 3221224592 3221223088 134744169 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9116 7113 300 300 0 8816 0
vsize: 36464
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 18233 0 0 0 40944 62 0 0 25 0 1 0 749020843 37339136 7152 4294967295 134512640 135726644 3221224592 3221223088 134743953 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9116 7152 300 300 0 8816 0
vsize: 36464
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 18363 0 0 0 41943 63 0 0 25 0 1 0 749020843 37339136 7160 4294967295 134512640 135726644 3221224592 3221223088 134743980 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9116 7160 300 300 0 8816 0
vsize: 36464
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 18681 0 0 0 42942 64 0 0 25 0 1 0 749020843 37339136 7234 4294967295 134512640 135726644 3221224592 3221223088 134743953 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9116 7234 300 300 0 8816 0
vsize: 36464
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 18904 0 0 0 43942 64 0 0 25 0 1 0 749020843 37339136 7335 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9116 7335 300 300 0 8816 0
vsize: 36464
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 19076 0 0 0 44941 65 0 0 25 0 1 0 749020843 37474304 7385 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9149 7385 300 300 0 8849 0
vsize: 36596
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 19225 0 0 0 45941 66 0 0 25 0 1 0 749020843 37474304 7412 4294967295 134512640 135726644 3221224592 3221223088 134743961 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9149 7412 300 300 0 8849 0
vsize: 36596
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 19408 0 0 0 46939 68 0 0 25 0 1 0 749020843 37474304 7473 4294967295 134512640 135726644 3221224592 3221223088 134744150 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 9149 7473 300 300 0 8849 0
vsize: 36596
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 19726 0 0 0 47939 68 0 0 25 0 1 0 749020843 45862912 7547 4294967295 134512640 135726644 3221224592 3221223088 134744147 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11197 7547 300 300 0 10897 0
vsize: 44788
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 19798 0 0 0 48938 69 0 0 25 0 1 0 749020843 45998080 7619 4294967295 134512640 135726644 3221224592 3221222912 134729216 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7619 300 300 0 10930 0
vsize: 44920
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 19928 0 0 0 49938 70 0 0 25 0 1 0 749020843 45998080 7627 4294967295 134512640 135726644 3221224592 3221223088 134744220 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7627 300 300 0 10930 0
vsize: 44920
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20056 0 0 0 50937 70 0 0 25 0 1 0 749020843 45998080 7633 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7633 300 300 0 10930 0
vsize: 44920
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20062 0 0 0 51937 71 0 0 25 0 1 0 749020843 45998080 7639 4294967295 134512640 135726644 3221224592 3221223088 134744163 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7639 300 300 0 10930 0
vsize: 44920
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20190 0 0 0 52937 71 0 0 25 0 1 0 749020843 45998080 7645 4294967295 134512640 135726644 3221224592 3221223088 134744041 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7645 300 300 0 10930 0
vsize: 44920
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20197 0 0 0 53936 72 0 0 25 0 1 0 749020843 45998080 7652 4294967295 134512640 135726644 3221224592 3221223088 134744004 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7652 300 300 0 10930 0
vsize: 44920
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20585 0 0 0 54936 73 0 0 25 0 1 0 749020843 45998080 7674 4294967295 134512640 135726644 3221224592 3221223088 134744063 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7674 300 300 0 10930 0
vsize: 44920
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20723 0 0 0 55935 73 0 0 25 0 1 0 749020843 45998080 7690 4294967295 134512640 135726644 3221224592 3221223136 134736658 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11230 7690 300 300 0 10930 0
vsize: 44920
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20738 0 0 0 56935 74 0 0 25 0 1 0 749020843 46137344 7705 4294967295 134512640 135726644 3221224592 3221223088 134744211 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11264 7705 300 300 0 10964 0
vsize: 45056
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20755 0 0 0 57935 74 0 0 25 0 1 0 749020843 46137344 7722 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11264 7722 300 300 0 10964 0
vsize: 45056
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20816 0 0 0 58935 74 0 0 25 0 1 0 749020843 46137344 7783 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11264 7783 300 300 0 10964 0
vsize: 45056
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20898 0 0 0 59934 75 0 0 25 0 1 0 749020843 46137344 7865 4294967295 134512640 135726644 3221224592 3221223088 134744235 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11264 7865 300 300 0 10964 0
vsize: 45056
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 20985 0 0 0 60933 76 0 0 25 0 1 0 749020843 46284800 7952 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11300 7952 300 300 0 11000 0
vsize: 45200
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 21055 0 0 0 61932 77 0 0 25 0 1 0 749020843 46284800 8022 4294967295 134512640 135726644 3221224592 3221223088 134744286 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11300 8022 300 300 0 11000 0
vsize: 45200
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.82 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 21121 0 0 0 62932 78 0 0 25 0 1 0 749020843 46284800 8088 4294967295 134512640 135726644 3221224592 3221223088 134744147 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11300 8088 300 300 0 11000 0
vsize: 45200
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 21269 0 0 0 63932 78 0 0 25 0 1 0 749020843 46284800 8114 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11300 8114 300 300 0 11000 0
vsize: 45200
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 21412 0 0 0 64931 79 0 0 25 0 1 0 749020843 46440448 8135 4294967295 134512640 135726644 3221224592 3221223088 134744063 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11338 8135 300 300 0 11038 0
vsize: 45352
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/55 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 21669 0 0 0 65930 80 0 0 25 0 1 0 749020843 46440448 8148 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11338 8148 300 300 0 11038 0
vsize: 45352
[startup+661.675 s]
Raw data (loadavg): 0.99 0.97 0.83 1/54 18319
Raw data (stat): 18319 (pb2sat) R 18318 8378 8377 0 -1 0 21669 0 0 0 65930 80 0 0 25 0 1 0 749020843 46440448 8148 4294967295 134512640 135726644 3221224592 3221223088 134743955 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 11338 8148 300 300 0 11038 0
vsize: 0

Child status: 30
Real time (s): 661.675
CPU time (s): 661.758
CPU user time (s): 660.938
CPU system time (s): 0.819875
CPU usage (%): 100.013
Max. virtual memory (Kb): 45352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	15
#### END VERIFIER DATA ####