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/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
MD5SUMdcb6d1c3f66e900ae345e6fa455bef2a
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
Satisfiable
(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 130
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 512
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables168111
Total number of constraints487525
Number of constraints which are clauses468727
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints18798
Minimum length of a constraint1
Maximum length of a constraint15

Trace number 39686

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-06-07 16:08:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=27744 boxname=wulflinc1 idbench=302 idsolver=20 numberseed=0
MD5SUM SOLVER: f6aa7fb267fa9710116626be7e6d3048  /oldhome/oroussel/solvers/bsolo_lpr-v2
MD5SUM BENCH:  dcb6d1c3f66e900ae345e6fa455bef2a  /oldhome/oroussel/tmp/wulflinc1/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
REAL COMMAND:  bsolo_lpr-v2 /oldhome/oroussel/tmp/wulflinc1/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
IDLAUNCH: 27744
/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:        891672 kB
Buffers:         33388 kB
Cached:          81528 kB
SwapCached:       3336 kB
Active:          36048 kB
Inactive:        83324 kB
HighTotal:      131008 kB
HighFree:        61964 kB
LowTotal:       903652 kB
LowFree:        829708 kB
SwapTotal:     2097136 kB
SwapFree:      2092692 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5684 kB
Slab:            17776 kB
Committed_AS:    92716 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-07 16:20:17 (client local time) WITH STATUS 0 IN 722.571 SECONDS
stats: 27744 7 722.571 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 168111 variables and 487525 constraints.
#### 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.89 0.96 0.92 2/55 7496
Raw data (stat): 7496 (runsolver) R 7495 8378 8377 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 837456309 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0015 s]
Raw data (loadavg): 0.91 0.96 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 32187 0 0 0 927 71 0 0 25 0 1 0 837456309 40521728 6569 4294967295 134512640 134716908 3221224560 3221222864 134568040 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9843 6551 1111 63 0 9780 0
vsize: 39572
[startup+20.0018 s]
Raw data (loadavg): 0.92 0.96 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 150960 0 0 0 1709 289 0 0 25 0 1 0 837456309 56877056 10585 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13852 10556 1111 63 0 13789 0
vsize: 55544
[startup+30.0016 s]
Raw data (loadavg): 0.93 0.96 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 379632 0 0 0 2293 705 0 0 25 0 1 0 837456309 67420160 13098 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16460 13099 1111 63 0 16397 0
vsize: 65840
[startup+40.0024 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 605934 0 0 0 2885 1113 0 0 25 0 1 0 837456309 76410880 15270 4294967295 134512640 134716908 3221224560 3221222584 1077799011 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18655 15277 1111 63 0 18592 0
vsize: 74620
[startup+50.0022 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 823240 0 0 0 3490 1508 0 0 25 0 1 0 837456309 84164608 17180 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20548 17187 1111 63 0 20485 0
vsize: 82192
[startup+60.003 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 1037832 0 0 0 4104 1894 0 0 25 0 1 0 837456309 91234304 18924 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 22274 18931 1111 63 0 22211 0
vsize: 89096
[startup+70.0032 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 1252093 0 0 0 4707 2291 0 0 25 0 1 0 837456309 97755136 20519 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 23866 20525 1111 63 0 23803 0
vsize: 95464
[startup+80.0036 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 1463326 0 0 0 5325 2674 0 0 25 0 1 0 837456309 104583168 22197 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 25533 22203 1111 63 0 25470 0
vsize: 102132
[startup+90.0034 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 1673843 0 0 0 5933 3066 0 0 25 0 1 0 837456309 110149632 23562 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 26892 23568 1111 63 0 26829 0
vsize: 107568
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 1881860 0 0 0 6532 3468 0 0 25 0 1 0 837456309 115585024 24873 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 28219 24878 1111 63 0 28156 0
vsize: 112876
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 2087281 0 0 0 7136 3864 0 0 25 0 1 0 837456309 121511936 26150 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29666 26156 1111 63 0 29603 0
vsize: 118664
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 2291492 0 0 0 7745 4255 0 0 25 0 1 0 837456309 126267392 27328 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30827 27333 1111 63 0 30764 0
vsize: 123308
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 2493730 0 0 0 8355 4645 0 0 25 0 1 0 837456309 130891776 28459 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 31956 28464 1111 63 0 31893 0
vsize: 127824
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 2694005 0 0 0 8967 5033 0 0 25 0 1 0 837456309 135049216 29514 4294967295 134512640 134716908 3221224560 3221222964 1077374508 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 32971 29514 1111 63 0 32908 0
vsize: 131884
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 2894855 0 0 0 9584 5416 0 0 25 0 1 0 837456309 139255808 30564 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34079 30564 1111 63 0 34016 0
vsize: 135992
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 3093962 0 0 0 10187 5813 0 0 25 0 1 0 837456309 143319040 31563 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34990 31564 1111 63 0 34927 0
vsize: 139960
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 3290859 0 0 0 10796 6204 0 0 25 0 1 0 837456309 147595264 32588 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 36034 32593 1111 63 0 35971 0
vsize: 144136
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 3488626 0 0 0 11402 6599 0 0 25 0 1 0 837456309 151539712 33509 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 36997 33515 1111 63 0 36934 0
vsize: 147988
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 3686044 0 0 0 12014 6987 0 0 25 0 1 0 837456309 155340800 34425 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 37925 34431 1111 63 0 37862 0
vsize: 151700
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 3881651 0 0 0 12624 7377 0 0 25 0 1 0 837456309 159006720 35374 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 38820 35379 1111 63 0 38757 0
vsize: 155280
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 4077567 0 0 0 13235 7766 0 0 25 0 1 0 837456309 162537472 36282 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39682 36287 1111 63 0 39619 0
vsize: 158728
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 4271577 0 0 0 13849 8152 0 0 25 0 1 0 837456309 166068224 37120 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 40544 37125 1111 63 0 40481 0
vsize: 162176
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 4464683 0 0 0 14465 8537 0 0 25 0 1 0 837456309 169467904 37902 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 41374 37907 1111 63 0 41311 0
vsize: 165496
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 4656756 0 0 0 15075 8926 0 0 25 0 1 0 837456309 172728320 38789 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 42170 38794 1111 63 0 42107 0
vsize: 168680
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 4850354 0 0 0 15693 9309 0 0 25 0 1 0 837456309 175988736 39576 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 42966 39581 1111 63 0 42903 0
vsize: 171864
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 5042208 0 0 0 16312 9690 0 0 25 0 1 0 837456309 179240960 40313 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 43760 40319 1111 63 0 43697 0
vsize: 175040
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 5235790 0 0 0 16927 10075 0 0 25 0 1 0 837456309 182505472 41153 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44557 41158 1111 63 0 44494 0
vsize: 178228
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 5426860 0 0 0 17545 10458 0 0 25 0 1 0 837456309 185630720 41856 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 45320 41862 1111 63 0 45257 0
vsize: 181280
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 5616551 0 0 0 18161 10841 0 0 25 0 1 0 837456309 190308352 43021 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 46462 43026 1111 63 0 46399 0
vsize: 185848
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 5807228 0 0 0 18774 11229 0 0 25 0 1 0 837456309 193155072 43740 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47157 43745 1111 63 0 47094 0
vsize: 188628
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 5998333 0 0 0 19387 11616 0 0 25 0 1 0 837456309 196145152 44487 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47887 44491 1111 63 0 47824 0
vsize: 191548
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 6188710 0 0 0 20009 11994 0 0 25 0 1 0 837456309 199000064 45174 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 48584 45179 1111 63 0 48521 0
vsize: 194336
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 6378645 0 0 0 20624 12379 0 0 25 0 1 0 837456309 201846784 45897 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49279 45902 1111 63 0 49216 0
vsize: 197116
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 6567298 0 0 0 21237 12766 0 0 25 0 1 0 837456309 204570624 46542 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49944 46547 1111 63 0 49881 0
vsize: 199776
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 6757670 0 0 0 21853 13151 0 0 25 0 1 0 837456309 207282176 47262 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 50606 47267 1111 63 0 50543 0
vsize: 202424
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 6946627 0 0 0 22480 13524 0 0 25 0 1 0 837456309 209514496 47829 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 51151 47829 1111 63 0 51088 0
vsize: 204604
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 7136770 0 0 0 23091 13913 0 0 25 0 1 0 837456309 212717568 48563 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 51933 48568 1111 63 0 51870 0
vsize: 207732
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 7326284 0 0 0 23702 14302 0 0 25 0 1 0 837456309 215302144 49219 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 52564 49224 1111 63 0 52501 0
vsize: 210256
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 7513549 0 0 0 24318 14686 0 0 25 0 1 0 837456309 217370624 49763 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 53069 49763 1111 63 0 53006 0
vsize: 212276
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 7701336 0 0 0 24935 15070 0 0 25 0 1 0 837456309 220463104 50393 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 53824 50398 1111 63 0 53761 0
vsize: 215296
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 7889176 0 0 0 25558 15447 0 0 25 0 1 0 837456309 222904320 51111 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 54420 51116 1111 63 0 54357 0
vsize: 217680
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 8077383 0 0 0 26177 15828 0 0 25 0 1 0 837456309 227024896 51752 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 55426 51756 1111 63 0 55363 0
vsize: 221704
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 8265561 0 0 0 26790 16215 0 0 25 0 1 0 837456309 229466112 52271 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 56022 52276 1111 63 0 55959 0
vsize: 224088
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 8454916 0 0 0 27412 16593 0 0 25 0 1 0 837456309 231919616 52878 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 56621 52878 1111 63 0 56558 0
vsize: 226484
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 8645025 0 0 0 28028 16978 0 0 25 0 1 0 837456309 233816064 53423 4294967295 134512640 134716908 3221224560 3221223192 134526221 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 57084 53423 1111 63 0 57021 0
vsize: 228336
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 8832307 0 0 0 28647 17358 0 0 25 0 1 0 837456309 236670976 54125 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 57781 54130 1111 63 0 57718 0
vsize: 231124
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 9018766 0 0 0 29264 17741 0 0 25 0 1 0 837456309 238985216 54696 4294967295 134512640 134716908 3221224560 3221222864 134568032 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 58346 54696 1111 63 0 58283 0
vsize: 233384
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 9207904 0 0 0 29887 18118 0 0 25 0 1 0 837456309 240869376 55147 4294967295 134512640 134716908 3221224560 3221222844 1077399556 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 58806 55147 1111 63 0 58743 0
vsize: 235224
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 9396511 0 0 0 30510 18495 0 0 25 0 1 0 837456309 243736576 55809 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 59506 55814 1111 63 0 59443 0
vsize: 238024
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 9585301 0 0 0 31132 18873 0 0 25 0 1 0 837456309 245915648 56371 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 60038 56375 1111 63 0 59975 0
vsize: 240152
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 9774384 0 0 0 31750 19256 0 0 25 0 1 0 837456309 248221696 56870 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 60601 56875 1111 63 0 60538 0
vsize: 242404
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 9962249 0 0 0 32372 19633 0 0 25 0 1 0 837456309 250527744 57471 4294967295 134512640 134716908 3221224560 3221222864 134568032 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 61164 57471 1111 63 0 61101 0
vsize: 244656
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 10150565 0 0 0 32980 20026 0 0 25 0 1 0 837456309 252710912 58063 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 61697 58068 1111 63 0 61634 0
vsize: 246788
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 10339748 0 0 0 33598 20407 0 0 25 0 1 0 837456309 254881792 58483 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 62227 58489 1111 63 0 62164 0
vsize: 248908
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 10530228 0 0 0 34215 20790 0 0 25 0 1 0 837456309 257191936 59046 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 62791 59051 1111 63 0 62728 0
vsize: 251164
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 10719008 0 0 0 34831 21175 0 0 25 0 1 0 837456309 258760704 59557 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 63174 59557 1111 63 0 63111 0
vsize: 252696
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 10907881 0 0 0 35448 21558 0 0 25 0 1 0 837456309 261541888 60221 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 63853 60226 1111 63 0 63790 0
vsize: 255412
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 11096259 0 0 0 36062 21944 0 0 25 0 1 0 837456309 263577600 60749 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 64350 60754 1111 63 0 64287 0
vsize: 257400
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 11285106 0 0 0 36677 22329 0 0 25 0 1 0 837456309 265748480 61160 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 64880 61165 1111 63 0 64817 0
vsize: 259520
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 11473840 0 0 0 37287 22719 0 0 25 0 1 0 837456309 267788288 61647 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 65378 61652 1111 63 0 65315 0
vsize: 261512
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 11661722 0 0 0 37898 23108 0 0 25 0 1 0 837456309 269967360 62239 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 65910 62244 1111 63 0 65847 0
vsize: 263640
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 11850239 0 0 0 38524 23483 0 0 25 0 1 0 837456309 272003072 62802 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 66407 62807 1111 63 0 66344 0
vsize: 265628
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 12038753 0 0 0 39144 23863 0 0 25 0 1 0 837456309 274038784 63196 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 66904 63201 1111 63 0 66841 0
vsize: 267616
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 12226268 0 0 0 39764 24242 0 0 25 0 1 0 837456309 276074496 63705 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 67401 63710 1111 63 0 67338 0
vsize: 269604
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 12415891 0 0 0 40378 24628 0 0 25 0 1 0 837456309 278110208 64324 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 67898 64328 1111 63 0 67835 0
vsize: 271592
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 12603647 0 0 0 41008 24998 0 0 25 0 1 0 837456309 280154112 64723 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 68397 64728 1111 63 0 68334 0
vsize: 273588
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 12792314 0 0 0 41629 25377 0 0 25 0 1 0 837456309 282198016 65292 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 68896 65297 1111 63 0 68833 0
vsize: 275584
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 12980753 0 0 0 42245 25762 0 0 25 0 1 0 837456309 284098560 65656 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 69360 65661 1111 63 0 69297 0
vsize: 277440
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 13169683 0 0 0 42860 26147 0 0 25 0 1 0 837456309 286134272 66176 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 69857 66180 1111 63 0 69794 0
vsize: 279428
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 13357114 0 0 0 43472 26535 0 0 25 0 1 0 837456309 288034816 66687 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 70321 66692 1111 63 0 70258 0
vsize: 281284
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 13483277 0 0 0 44217 26789 0 0 25 0 1 0 837456309 297910272 69181 4294967295 134512640 134716908 3221224560 3221223184 134556539 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 72732 69181 1111 63 0 72669 0
vsize: 290928
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 13592957 0 0 0 44966 27041 0 0 25 0 1 0 837456309 741556224 178859 4294967295 134512640 134716908 3221224560 3221223200 134606484 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 181044 178859 1111 63 0 180981 0
vsize: 724176
[startup+722.52 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 7496
Raw data (stat): 7496 (bsolo_lpr-v2) R 7495 8378 8377 0 -1 0 13592957 0 0 0 44966 27041 0 0 25 0 1 0 837456309 741556224 178859 4294967295 134512640 134716908 3221224560 3221223200 134606484 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 181044 178859 1111 63 0 180981 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 722.519
CPU time (s): 722.571
CPU user time (s): 450.5
CPU system time (s): 272.071
CPU usage (%): 100.007
Max. virtual memory (Kb): 724176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####