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/web/uclid_pb_benchmarks/normalized-22s.smv.opb
MD5SUM	a99dcbcd7e95de487b31a7960db472c5
Bench Category	no optimization function (SAT)
Has Objective Function	NO
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	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	165
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	546
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.69674
Number of variables	5985
Total number of constraints	15365
Number of constraints which are clauses	14013
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1352
Minimum length of a constraint	1
Maximum length of a constraint	15

Trace number 24464

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-10 17:46:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2379 boxname=wulflinc31 idbench=265 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  a99dcbcd7e95de487b31a7960db472c5  /oldhome/oroussel/tmp/wulflinc31/normalized-22s.smv.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-22s.smv.opb
IDLAUNCH: 2379
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        287944 kB
Buffers:         47116 kB
Cached:         665492 kB
SwapCached:        644 kB
Active:         313964 kB
Inactive:       400996 kB
HighTotal:      131008 kB
HighFree:        24976 kB
LowTotal:       903652 kB
LowFree:        262968 kB
SwapTotal:     2097892 kB
SwapFree:      2096612 kB
Dirty:              60 kB
Writeback:           0 kB
Mapped:           5608 kB
Slab:            26000 kB
Committed_AS:    63632 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-10 17:57:41 (client local time) WITH STATUS 20 IN 679.598 SECONDS
stats: 2379 7 679.598 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 5985 variables and 15365 constraints.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 679.542 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): 0.92 0.97 0.93 2/54 12403
Raw data (stat): 12403 (runsolver) R 12402 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 711153629 1056768 100 4294967295 134512640 135381576 3221221696 3221216916 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 10877 0 0 0 966 30 0 0 25 0 1 0 711153629 48365568 10852 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11808 10852 1111 63 0 11745 0
vsize: 47232
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 10877 0 0 0 1966 30 0 0 25 0 1 0 711153629 48365568 10852 4294967295 134512640 134714540 3221221792 3221220300 1077374048 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11808 10852 1111 63 0 11745 0
vsize: 47232
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 2960 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 3960 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606494 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 4961 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220520 134672929 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 5961 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220592 134617431 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 6961 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 7961 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 8961 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 9962 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 13198 0 0 0 10962 36 0 0 25 0 1 0 711153629 57827328 13173 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14118 13173 1111 63 0 14055 0
vsize: 56472
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 11958 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 12958 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220544 134630792 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 13958 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220432 134606494 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 14958 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220208 134543740 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 15959 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220432 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 16959 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 17959 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220432 134606498 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 15175 0 0 0 18959 40 0 0 25 0 1 0 711153629 65945600 15150 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16100 15150 1111 63 0 16037 0
vsize: 64400
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 19956 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 20956 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 21956 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134594970 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 22956 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 23956 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606456 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 24957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220236 134536766 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 25957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606456 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 26957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 27957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220592 134617238 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 28957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 29957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 16188 0 0 0 30957 43 0 0 25 0 1 0 711153629 69689344 16063 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17014 16063 1111 63 0 16951 0
vsize: 68056
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 31953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220544 134630798 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 32953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 33953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220156 134539298 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 34952 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220440 134558492 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 35953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 36953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 37953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 38953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 39953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 40953 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 41954 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 42954 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220216 1077377891 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 43954 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 44954 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220260 134536649 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 45954 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606498 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 46954 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 47955 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220156 134539237 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 48955 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220216 1077377833 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 49955 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606494 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 50955 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220216 1077377565 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 51955 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220544 134630795 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 52956 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 53956 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 54956 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 55956 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 56956 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 57956 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606474 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 58957 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220176 134542303 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 59957 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220204 134543616 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 60957 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 61957 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220216 1077377891 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 62957 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 63957 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606498 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 64958 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220520 134672911 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 65958 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606485 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 66958 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606456 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 76920
[startup+679.549 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 12403
Raw data (stat): 12403 (bsolo_mis) R 12402 7876 7672 0 -1 0 18410 0 0 0 66958 48 0 0 25 0 1 0 711153629 78766080 18285 4294967295 134512640 134714540 3221221792 3221220432 134606456 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19230 18285 1111 63 0 19167 0
vsize: 0

Child status: 20
Real time (s): 679.548
CPU time (s): 679.598
CPU user time (s): 679.076
CPU system time (s): 0.52192
CPU usage (%): 100.007
Max. virtual memory (Kb): 76920
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####