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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sctap3.opb
MD5SUM	b5066922b496d65f6fab47243caf450a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	55800
Biggest coefficient in the objective function	42949672960
Number of bits for the biggest coefficient in the objective function	36
Sum of the numbers in the objective function	31374736068060
Number of bits of the sum of numbers in the objective function	45
Biggest number in a constraint	42949672960
Number of bits of the biggest number in a constraint	36
Biggest sum of numbers in a constraint	31374736068060
Number of bits of the biggest sum of numbers	45
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.674897
Number of variables	74400
Total number of constraints	1480
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1480
Minimum length of a constraint	90
Maximum length of a constraint	930
Trace number 26803

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-24 17:02:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11338 boxname=wulflinc23 idbench=873 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  b5066922b496d65f6fab47243caf450a  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-sctap3.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-sctap3.opb
IDLAUNCH: 11338
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        880176 kB
Buffers:         35300 kB
Cached:          96772 kB
SwapCached:        664 kB
Active:          80472 kB
Inactive:        54148 kB
HighTotal:      131008 kB
HighFree:        33124 kB
LowTotal:       903652 kB
LowFree:        847052 kB
SwapTotal:     2097136 kB
SwapFree:      2096032 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            14264 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-24 17:14:25 (client local time) WITH STATUS 0 IN 705.971 SECONDS
stats: 11338 7 705.971 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c ERROR Parsing file!!!
c ERROR parsing line: -5*Z3Z10ZZ9_bit_10 -10*Z3Z10ZZ9_bit_9 -20*Z3Z10ZZ9_bit_8 -40*Z3Z10ZZ9_bit_7 -80*Z3Z10ZZ9_bit_6 -160*Z3Z10ZZ9_bit_5 -320*Z3Z10ZZ9_bit_4 -640*Z3Z10ZZ9_bit_3 -1280*Z3Z10ZZ9_bit_2 -2560*Z3Z10ZZ9_bit_1 -5120*Z3Z10ZZ9_bit0 -10240*Z3Z10ZZ9_bit1 -20480*Z3Z10ZZ9_bit2 -40960*Z3Z10ZZ9_bit3 -81920*Z3Z10ZZ9_bit4 -163840*Z3Z10ZZ9_bit5 -327680*Z3Z10ZZ9_bit6 -655360*Z3Z10ZZ9_bit7 -1310720*Z3Z10ZZ9_bit8 -2621440*Z3Z10ZZ9_bit9 -5242880*Z3Z10ZZ9_bit10 -10485760*Z3Z10ZZ9_bit11 -20971520*Z3Z10ZZ9_bit12 -41943040*Z3Z10ZZ9_bit13 -83886080*Z3Z10ZZ9_bit14 -167772160*Z3Z10ZZ9_bit15 -335544320*Z3Z10ZZ9_bit16 -671088640*Z3Z10ZZ9_bit17 -1342177280*Z3Z10ZZ9_bit18 -2684354560*Z3Z10ZZ9_bit19 -1*Z4Z10ZZ9_bit_10 -2*Z4Z10ZZ9_bit_9 -4*Z4Z10ZZ9_bit_8 -8*Z4Z10ZZ9_bit_7 -16*Z4Z10ZZ9_bit_6 -32*Z4Z10ZZ9_bit_5 -64*Z4Z10ZZ9_bit_4 -128*Z4Z10ZZ9_bit_3 -256*Z4Z10ZZ9_bit_2 -512*Z4Z10ZZ9_bit_1 -1024*Z4Z10ZZ9_bit0 -2048*Z4Z10ZZ9_bit1 -4096*Z4Z10ZZ9_bit2 -8192*Z4Z10ZZ9_bit3 -16384*Z4Z10ZZ9_bit4 -32768*Z4Z10ZZ9_bit5 -65536*Z4Z10ZZ9_bit6 -131072*Z4Z10ZZ9_bit7 -262144*Z4Z10ZZ9_bit8 -524288*Z4Z10ZZ9_bit9 -1048576*Z4Z10ZZ9_bit10 -2097152*Z4Z10ZZ9_bit11 -4194304*Z4Z10ZZ9_bit12 -8388608*Z4Z10ZZ9_bit13 -16777216*Z4Z10ZZ9_bit14 -33554432*Z4Z10ZZ9_bit15 -67108864*Z4Z10ZZ9_bit16 -134217728*Z4Z10ZZ9_bit17 -268435456*Z4Z10ZZ9_bit18 -536870912*Z4Z10ZZ9_bit19 +10*Z2Z10Z10_bit_10 +20*Z2Z10Z10_bit_9 +40*Z2Z10Z10_bit_8 +80*Z2Z10Z10_bit_7 +160*Z2Z10Z10_bit_6 +320*Z2Z10Z10_bit_5 +640*Z2Z10Z10_bit_4 +1280*Z2Z10Z10_bit_3 +2560*Z2Z10Z10_bit_2 +5120*Z2Z10Z10_bit_1 +10240*Z2Z10Z10_bit0 +20480*Z2Z10Z10_bit1 +40960*Z2Z10Z10_bit2 +81920*Z2Z10Z10_bit3 +163840*Z2Z10Z10_bit4 +327680*Z2Z10Z10_bit5 +655360*Z2Z10Z10_bit6 +1310720*Z2Z10Z10_bit7 +2621440*Z2Z10Z10_bit8 +5242880*Z2Z10Z10_bit9 +10485760*Z2Z10Z10_bit10 +20971520*Z2Z10Z10_bit11 +41943040*Z2Z10Z10_bit12 +83886080*Z2Z10Z10_bit13 +167772160*Z2Z10Z10_bit14 +335544320*Z2Z10Z10_bit15 +671088640*Z2Z10Z10_bit16 +1342177280*Z2Z10Z10_bit17 +2684354560*Z2Z10Z10_bit18 +5368709120*Z2Z10Z10_bit19 +20*Z3Z10Z10_bit_10 +40*Z3Z10Z10_bit_9 +80*Z3Z10Z10_bit_8 +160*Z3Z10Z10_bit_7 +320*Z3Z10Z10_bit_6 +640*Z3Z10Z10_bit_5 +1280*Z3Z10Z10_bit_4 +2560*Z3Z10Z10_bit_3 +5120*Z3Z10Z10_bit_2 +10240*Z3Z10Z10_bit_1 +20480*Z3Z10Z10_bit0 +40960*Z3Z10Z10_bit1 +81920*Z3Z10Z10_bit2 +163840*Z3Z10Z10_bit3 +327680*Z3Z10Z10_bit4 +655360*Z3Z10Z10_bit5 +1310720*Z3Z10Z10_bit6 +2621440*Z3Z10Z10_bit7 +5242880*Z3Z10Z10_bit8 +10485760*Z3Z10Z10_bit9 +20971520*Z3Z10Z10_bit10 +41943040*Z3Z10Z10_bit11 +83886080*Z3Z10Z10_bit12 +167772160*Z3Z10Z10_bit13 +335544320*Z3Z10Z10_bit14 +671088640*Z3Z10Z10_bit15 +1342177280*Z3Z10Z10_bit16 +2684354560*Z3Z10Z10_bit17 +5368709120*Z3Z10Z10_bit18 +10737418240*Z3Z10Z10_bit19 +1*Z4Z10Z10_bit_10 +2*Z4Z10Z10_bit_9 +4*Z4Z10Z10_bit_8 +8*Z4Z10Z10_bit_7 +16*Z4Z10Z10_bit_6 +32*Z4Z10Z10_bit_5 +64*Z4Z10Z10_bit_4 +128*Z4Z10Z10_bit_3 +256*Z4Z10Z10_bit_2 +512*Z4Z10Z10_bit_1 +1024*Z4Z10Z10_bit0 +2048*Z4Z10Z10_bit1 +4096*Z4Z10Z10_bit2 +8192*Z4Z10Z10_bit3 +16384*Z4Z10Z10_bit4 +32768*Z4Z10Z10_bit5 +65536*Z4Z10Z10_bit6 +131072*Z4Z10Z10_bit7 +262144*Z4Z10Z10_bit8 +524288*Z4Z10Z10_bit9 +1048576*Z4Z10Z10_bit10 +2097152*Z4Z10Z10_bit11 +4194304*Z4Z10Z10_bit12 +8388608*Z4Z10Z10_bit13 +16777216*Z4Z10Z10_bit14 +33554432*Z4Z10Z10_bit15 +67108864*Z4Z10Z10_bit16 +134217728*Z4Z10Z10_bit17 +268435456*Z4Z10Z10_bit18 +536870912*Z4Z10Z10_bit19 >= +0;
c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-sctap3.opb
s UNKNOWN
c Exit Code: 0
c Total time: 705.906 s
#### 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): 1.14 1.00 0.97 2/54 7574
Raw data (stat): 7574 (runsolver) R 7573 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 831886953 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 1.11 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 1019 0 0 0 994 3 0 0 25 0 1 0 831886953 16089088 943 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 3928 943 1111 63 0 3865 0
vsize: 15712
[startup+20.0007 s]
Raw data (loadavg): 1.10 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 1278 0 0 0 1994 4 0 0 25 0 1 0 831886953 17137664 1202 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4184 1202 1111 63 0 4121 0
vsize: 16736
[startup+30.0013 s]
Raw data (loadavg): 1.08 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 1535 0 0 0 2994 4 0 0 25 0 1 0 831886953 18292736 1459 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4466 1459 1111 63 0 4403 0
vsize: 17864
[startup+40.001 s]
Raw data (loadavg): 1.07 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 1797 0 0 0 3994 5 0 0 25 0 1 0 831886953 19341312 1721 4294967295 134512640 134714508 3221224576 3221222804 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4722 1721 1111 63 0 4659 0
vsize: 18888
[startup+50.0016 s]
Raw data (loadavg): 1.06 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 2055 0 0 0 4993 5 0 0 25 0 1 0 831886953 20393984 1979 4294967295 134512640 134714508 3221224576 3221222804 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 4979 1979 1111 63 0 4916 0
vsize: 19916
[startup+60.0013 s]
Raw data (loadavg): 1.05 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 2320 0 0 0 5993 6 0 0 25 0 1 0 831886953 21450752 2244 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5237 2244 1111 63 0 5174 0
vsize: 20948
[startup+70.0009 s]
Raw data (loadavg): 1.04 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 2577 0 0 0 6992 7 0 0 25 0 1 0 831886953 22503424 2501 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5494 2501 1111 63 0 5431 0
vsize: 21976
[startup+80.0018 s]
Raw data (loadavg): 1.03 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 2841 0 0 0 7991 8 0 0 25 0 1 0 831886953 23543808 2765 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 5748 2765 1111 63 0 5685 0
vsize: 22992
[startup+90.0014 s]
Raw data (loadavg): 1.03 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 3106 0 0 0 8991 8 0 0 25 0 1 0 831886953 24743936 3030 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6041 3030 1111 63 0 5978 0
vsize: 24164
[startup+100.002 s]
Raw data (loadavg): 1.02 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 3372 0 0 0 9990 10 0 0 25 0 1 0 831886953 25800704 3296 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6299 3296 1111 63 0 6236 0
vsize: 25196
[startup+110.003 s]
Raw data (loadavg): 1.02 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 3645 0 0 0 10989 11 0 0 25 0 1 0 831886953 26849280 3569 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6555 3569 1111 63 0 6492 0
vsize: 26220
[startup+120.002 s]
Raw data (loadavg): 1.02 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 3918 0 0 0 11988 12 0 0 25 0 1 0 831886953 28028928 3842 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6843 3842 1111 63 0 6780 0
vsize: 27372
[startup+130.003 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 4197 0 0 0 12988 12 0 0 25 0 1 0 831886953 29081600 4121 4294967295 134512640 134714508 3221224576 3221222804 1077414372 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7100 4121 1111 63 0 7037 0
vsize: 28400
[startup+140.003 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 4469 0 0 0 13987 13 0 0 25 0 1 0 831886953 30281728 4393 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7393 4393 1111 63 0 7330 0
vsize: 29572
[startup+150.003 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 4755 0 0 0 14987 14 0 0 25 0 1 0 831886953 31526912 4679 4294967295 134512640 134714508 3221224576 3221222804 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7697 4679 1111 63 0 7634 0
vsize: 30788
[startup+160.003 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 5033 0 0 0 15986 15 0 0 25 0 1 0 831886953 32583680 4957 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7955 4957 1111 63 0 7892 0
vsize: 31820
[startup+170.002 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 5314 0 0 0 16985 16 0 0 25 0 1 0 831886953 33783808 5238 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8248 5238 1111 63 0 8185 0
vsize: 32992
[startup+180.003 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 5592 0 0 0 17984 17 0 0 25 0 1 0 831886953 34836480 5516 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8505 5516 1111 63 0 8442 0
vsize: 34020
[startup+190.004 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7574
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 5876 0 0 0 18984 18 0 0 25 0 1 0 831886953 36044800 5800 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8800 5800 1111 63 0 8737 0
vsize: 35200
[startup+200.005 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 6169 0 0 0 19982 19 0 0 25 0 1 0 831886953 37244928 6093 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9093 6093 1111 63 0 9030 0
vsize: 36372
[startup+210.007 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 6456 0 0 0 20982 20 0 0 25 0 1 0 831886953 38445056 6380 4294967295 134512640 134714508 3221224576 3221222804 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9386 6380 1111 63 0 9323 0
vsize: 37544
[startup+220.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 6747 0 0 0 21982 20 0 0 25 0 1 0 831886953 39653376 6671 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9681 6671 1111 63 0 9618 0
vsize: 38724
[startup+230.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 7040 0 0 0 22982 21 0 0 25 0 1 0 831886953 40857600 6964 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9975 6964 1111 63 0 9912 0
vsize: 39900
[startup+240.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 7342 0 0 0 23981 22 0 0 25 0 1 0 831886953 42057728 7266 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10268 7266 1111 63 0 10205 0
vsize: 41072
[startup+250.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 7644 0 0 0 24980 24 0 0 25 0 1 0 831886953 43233280 7568 4294967295 134512640 134714508 3221224576 3221222804 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10555 7568 1111 63 0 10492 0
vsize: 42220
[startup+260.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 7940 0 0 0 25979 25 0 0 25 0 1 0 831886953 44441600 7864 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10850 7864 1111 63 0 10787 0
vsize: 43400
[startup+270.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 8241 0 0 0 26978 26 0 0 25 0 1 0 831886953 45641728 8165 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11143 8165 1111 63 0 11080 0
vsize: 44572
[startup+280.026 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 8543 0 0 0 27979 26 0 0 25 0 1 0 831886953 46997504 8467 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11474 8467 1111 63 0 11411 0
vsize: 45896
[startup+290.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 8871 0 0 0 28978 28 0 0 25 0 1 0 831886953 48451584 8795 4294967295 134512640 134714508 3221224576 3221222536 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11829 8795 1111 63 0 11766 0
vsize: 47316
[startup+300.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 9187 0 0 0 29977 29 0 0 25 0 1 0 831886953 49627136 9111 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12116 9111 1111 63 0 12053 0
vsize: 48464
[startup+310.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 9504 0 0 0 30976 30 0 0 25 0 1 0 831886953 50954240 9428 4294967295 134512640 134714508 3221224576 3221222444 1077244511 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12440 9428 1111 63 0 12377 0
vsize: 49760
[startup+320.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 9821 0 0 0 31976 30 0 0 25 0 1 0 831886953 52305920 9745 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12770 9745 1111 63 0 12707 0
vsize: 51080
[startup+330.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 10140 0 0 0 32975 31 0 0 25 0 1 0 831886953 53510144 10064 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13064 10064 1111 63 0 13001 0
vsize: 52256
[startup+340.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 10464 0 0 0 33975 32 0 0 25 0 1 0 831886953 54865920 10388 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13395 10388 1111 63 0 13332 0
vsize: 53580
[startup+350.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 10790 0 0 0 34974 33 0 0 25 0 1 0 831886953 56221696 10714 4294967295 134512640 134714508 3221224576 3221222804 1077414385 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13726 10714 1111 63 0 13663 0
vsize: 54904
[startup+360.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 11120 0 0 0 35973 33 0 0 25 0 1 0 831886953 57573376 11044 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14056 11044 1111 63 0 13993 0
vsize: 56224
[startup+370.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 11453 0 0 0 36972 34 0 0 25 0 1 0 831886953 58929152 11377 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14387 11377 1111 63 0 14324 0
vsize: 57548
[startup+380.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 11792 0 0 0 37971 36 0 0 25 0 1 0 831886953 60284928 11716 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14718 11716 1111 63 0 14655 0
vsize: 58872
[startup+390.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 12134 0 0 0 38970 37 0 0 25 0 1 0 831886953 61640704 12058 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15049 12058 1111 63 0 14986 0
vsize: 60196
[startup+400.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 12484 0 0 0 39969 38 0 0 25 0 1 0 831886953 63139840 12408 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15415 12408 1111 63 0 15352 0
vsize: 61660
[startup+410.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 12833 0 0 0 40968 39 0 0 25 0 1 0 831886953 64499712 12757 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15747 12757 1111 63 0 15684 0
vsize: 62988
[startup+420.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 13193 0 0 0 41968 40 0 0 25 0 1 0 831886953 65998848 13117 4294967295 134512640 134714508 3221224576 3221222804 1077414370 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16113 13117 1111 63 0 16050 0
vsize: 64452
[startup+430.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 13547 0 0 0 42969 40 0 0 25 0 1 0 831886953 67506176 13471 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16481 13471 1111 63 0 16418 0
vsize: 65924
[startup+440.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 13910 0 0 0 43969 41 0 0 25 0 1 0 831886953 69013504 13834 4294967295 134512640 134714508 3221224576 3221223232 134527972 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16849 13834 1111 63 0 16786 0
vsize: 67396
[startup+450.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 14286 0 0 0 44968 42 0 0 25 0 1 0 831886953 70516736 14210 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17216 14210 1111 63 0 17153 0
vsize: 68864
[startup+460.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 14671 0 0 0 45967 43 0 0 25 0 1 0 831886953 72024064 14595 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17584 14595 1111 63 0 17521 0
vsize: 70336
[startup+470.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 15075 0 0 0 46966 44 0 0 25 0 1 0 831886953 73650176 14999 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17981 14999 1111 63 0 17918 0
vsize: 71924
[startup+480.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 15488 0 0 0 47965 45 0 0 25 0 1 0 831886953 75456512 15412 4294967295 134512640 134714508 3221224576 3221222804 1077414410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18422 15412 1111 63 0 18359 0
vsize: 73688
[startup+490.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 15923 0 0 0 48965 46 0 0 25 0 1 0 831886953 77111296 15847 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18826 15847 1111 63 0 18763 0
vsize: 75304
[startup+500.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 16365 0 0 0 49964 46 0 0 25 0 1 0 831886953 78917632 16289 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19267 16289 1111 63 0 19204 0
vsize: 77068
[startup+510.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 16876 0 0 0 50963 48 0 0 25 0 1 0 831886953 81350656 16800 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19861 16800 1111 63 0 19798 0
vsize: 79444
[startup+520.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 17370 0 0 0 51962 49 0 0 25 0 1 0 831886953 83308544 17294 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20339 17294 1111 63 0 20276 0
vsize: 81356
[startup+530.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 17871 0 0 0 52961 50 0 0 25 0 1 0 831886953 85413888 17795 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20853 17795 1111 63 0 20790 0
vsize: 83412
[startup+540.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 18375 0 0 0 53960 52 0 0 25 0 1 0 831886953 87371776 18299 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21331 18299 1111 63 0 21268 0
vsize: 85324
[startup+550.052 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 18891 0 0 0 54959 53 0 0 25 0 1 0 831886953 89477120 18815 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21845 18815 1111 63 0 21782 0
vsize: 87380
[startup+560.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 19421 0 0 0 55959 53 0 0 25 0 1 0 831886953 91701248 19345 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 22388 19345 1111 63 0 22325 0
vsize: 89552
[startup+570.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 19967 0 0 0 56959 54 0 0 25 0 1 0 831886953 93966336 19891 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 22941 19891 1111 63 0 22878 0
vsize: 91764
[startup+580.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 20514 0 0 0 57958 55 0 0 25 0 1 0 831886953 96215040 20438 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 23490 20438 1111 63 0 23427 0
vsize: 93960
[startup+590.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 21069 0 0 0 58957 56 0 0 25 0 1 0 831886953 98480128 20993 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 24043 20993 1111 63 0 23980 0
vsize: 96172
[startup+600.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 21627 0 0 0 59956 58 0 0 25 0 1 0 831886953 100732928 21551 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 24593 21551 1111 63 0 24530 0
vsize: 98372
[startup+610.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 22209 0 0 0 60955 58 0 0 25 0 1 0 831886953 103141376 22133 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 25181 22133 1111 63 0 25118 0
vsize: 100724
[startup+620.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 22794 0 0 0 61954 60 0 0 25 0 1 0 831886953 105398272 22718 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 25732 22718 1111 63 0 25669 0
vsize: 102928
[startup+630.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 23390 0 0 0 62952 62 0 0 25 0 1 0 831886953 107958272 23314 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 26357 23314 1111 63 0 26294 0
vsize: 105428
[startup+640.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 23995 0 0 0 63951 63 0 0 25 0 1 0 831886953 110366720 23919 4294967295 134512640 134714508 3221224576 3221223232 134527972 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 26945 23919 1111 63 0 26882 0
vsize: 107780
[startup+650.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 24609 0 0 0 64950 64 0 0 25 0 1 0 831886953 112926720 24533 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 27570 24533 1111 63 0 27507 0
vsize: 110280
[startup+660.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 25236 0 0 0 65949 66 0 0 25 0 1 0 831886953 115486720 25160 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28195 25160 1111 63 0 28132 0
vsize: 112780
[startup+670.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 25883 0 0 0 66949 66 0 0 25 0 1 0 831886953 118042624 25807 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28819 25807 1111 63 0 28756 0
vsize: 115276
[startup+680.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 26534 0 0 0 67947 68 0 0 25 0 1 0 831886953 120750080 26458 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 29480 26458 1111 63 0 29417 0
vsize: 117920
[startup+690.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 27197 0 0 0 68946 69 0 0 25 0 1 0 831886953 123428864 27121 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 30134 27121 1111 63 0 30071 0
vsize: 120536
[startup+700.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 27876 0 0 0 69945 70 0 0 25 0 1 0 831886953 126136320 27800 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 30795 27800 1111 63 0 30732 0
vsize: 123180
[startup+705.885 s]
Raw data (loadavg): 1.00 1.00 0.97 1/53 7576
Raw data (stat): 7574 (bsolo_lpr_cuts) R 7573 5562 5561 0 -1 0 27876 0 0 0 69945 70 0 0 25 0 1 0 831886953 126136320 27800 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 30795 27800 1111 63 0 30732 0
vsize: 0

Child status: 0
Real time (s): 705.884
CPU time (s): 705.971
CPU user time (s): 705.194
CPU system time (s): 0.776881
CPU usage (%): 100.012
Max. virtual memory (Kb): 123180
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####