Name | normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb |
MD5SUM | dcb6d1c3f66e900ae345e6fa455bef2a |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
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 numbers | 10 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 168111 |
Total number of constraints | 487525 |
Number of constraints which are clauses | 468727 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 18798 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 15 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-11 13:41:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2710 boxname=wulflinc31 idbench=302 idsolver=1 numberseed=0 MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef /oldhome/oroussel/solvers/bsolo_lpr MD5SUM BENCH: dcb6d1c3f66e900ae345e6fa455bef2a /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb REAL COMMAND: bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb IDLAUNCH: 2710 /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: 885808 kB Buffers: 15068 kB Cached: 107792 kB SwapCached: 4232 kB Active: 65680 kB Inactive: 62620 kB HighTotal: 131008 kB HighFree: 23072 kB LowTotal: 903652 kB LowFree: 862736 kB SwapTotal: 2097892 kB SwapFree: 2093028 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5312 kB Slab: 14736 kB Committed_AS: 63652 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-11 13:53:33 (client local time) WITH STATUS 0 IN 740.793 SECONDS stats: 2710 7 740.793 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 Raw data (loadavg): 0.93 0.98 0.99 2/54 30098 Raw data (stat): 30098 (runsolver) R 30097 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 718323505 1056768 100 4294967295 134512640 135381576 3221221664 3221216884 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+10.0006 s] Raw data (loadavg): 0.94 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 32388 0 0 0 922 72 0 0 25 0 1 0 718323505 40427520 6580 4294967295 134512640 134714508 3221221776 3221220092 1077360305 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 9870 6580 1111 63 0 9807 0 vsize: 39480 [startup+20.0015 s] Raw data (loadavg): 0.95 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 131821 0 0 0 1736 259 0 0 25 0 1 0 718323505 55214080 10154 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 13480 10154 1111 63 0 13417 0 vsize: 53920 [startup+30.0025 s] Raw data (loadavg): 0.96 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 352798 0 0 0 2343 652 0 0 25 0 1 0 718323505 66367488 12832 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 16203 12832 1111 63 0 16140 0 vsize: 64812 [startup+40.0034 s] Raw data (loadavg): 0.96 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 569730 0 0 0 2951 1043 0 0 25 0 1 0 718323505 75063296 14984 4294967295 134512640 134714508 3221221776 3221220080 134568040 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 18326 14984 1111 63 0 18263 0 vsize: 73304 [startup+50.0043 s] Raw data (loadavg): 0.97 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 786525 0 0 0 3563 1432 0 0 25 0 1 0 718323505 82944000 16872 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 20250 16872 1111 63 0 20187 0 vsize: 81000 [startup+60.0052 s] Raw data (loadavg): 0.97 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 1001415 0 0 0 4170 1825 0 0 25 0 1 0 718323505 90013696 18641 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 21976 18641 1111 63 0 21913 0 vsize: 87904 [startup+70.0052 s] Raw data (loadavg): 0.98 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 1214001 0 0 0 4781 2214 0 0 25 0 1 0 718323505 96534528 20243 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 23568 20243 1111 63 0 23505 0 vsize: 94272 [startup+80.0061 s] Raw data (loadavg): 0.98 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 1423153 0 0 0 5400 2595 0 0 25 0 1 0 718323505 103493632 21923 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 25267 21923 1111 63 0 25204 0 vsize: 101068 [startup+90.006 s] Raw data (loadavg): 0.98 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 1630529 0 0 0 6016 2979 0 0 25 0 1 0 718323505 108810240 23264 4294967295 134512640 134714508 3221221776 3221219692 1077247265 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 26565 23264 1111 63 0 26502 0 vsize: 106260 [startup+100.007 s] Raw data (loadavg): 0.98 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 1835639 0 0 0 6626 3369 0 0 25 0 1 0 718323505 114507776 24623 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 27956 24623 1111 63 0 27893 0 vsize: 111824 [startup+110.008 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 2039163 0 0 0 7227 3768 0 0 25 0 1 0 718323505 120299520 25850 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 29370 25850 1111 63 0 29307 0 vsize: 117480 [startup+120.009 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 2240090 0 0 0 7835 4160 0 0 25 0 1 0 718323505 125046784 27005 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 30529 27005 1111 63 0 30466 0 vsize: 122116 [startup+130.01 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 2439077 0 0 0 8455 4541 0 0 25 0 1 0 718323505 129671168 28134 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 31658 28134 1111 63 0 31595 0 vsize: 126632 [startup+140.01 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 2638166 0 0 0 9068 4928 0 0 25 0 1 0 718323505 134156288 29219 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 32753 29219 1111 63 0 32690 0 vsize: 131012 [startup+150.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 2834338 0 0 0 9682 5314 0 0 25 0 1 0 718323505 138366976 30295 4294967295 134512640 134714508 3221221776 3221220080 134568032 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 33781 30295 1111 63 0 33718 0 vsize: 135124 [startup+160.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 3029471 0 0 0 10302 5694 0 0 25 0 1 0 718323505 142102528 31244 4294967295 134512640 134714508 3221221776 3221220180 1077374508 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 34693 31244 1111 63 0 34630 0 vsize: 138772 [startup+170.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 3224975 0 0 0 10921 6075 0 0 25 0 1 0 718323505 146382848 32247 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 35738 32247 1111 63 0 35675 0 vsize: 142952 [startup+180.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 3418291 0 0 0 11525 6471 0 0 25 0 1 0 718323505 150183936 33151 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 36666 33151 1111 63 0 36603 0 vsize: 146664 [startup+190.013 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 3611002 0 0 0 12140 6856 0 0 25 0 1 0 718323505 153849856 34075 4294967295 134512640 134714508 3221221776 3221220080 134568044 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 37561 34075 1111 63 0 37498 0 vsize: 150244 [startup+200.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 3802491 0 0 0 12762 7234 0 0 25 0 1 0 718323505 157143040 34957 4294967295 134512640 134714508 3221221776 3221218652 1077253638 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 38365 34957 1111 63 0 38302 0 vsize: 153460 [startup+210.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 3994330 0 0 0 13380 7617 0 0 25 0 1 0 718323505 161046528 35890 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 39318 35890 1111 63 0 39255 0 vsize: 157272 [startup+220.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 4185316 0 0 0 14002 7994 0 0 25 0 1 0 718323505 164577280 36702 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 40180 36702 1111 63 0 40117 0 vsize: 160720 [startup+230.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 4374541 0 0 0 14622 8374 0 0 25 0 1 0 718323505 167841792 37573 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 40977 37573 1111 63 0 40914 0 vsize: 163908 [startup+240.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 4563686 0 0 0 15253 8743 0 0 25 0 1 0 718323505 171237376 38362 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 41806 38362 1111 63 0 41743 0 vsize: 167224 [startup+250.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 4753078 0 0 0 15880 9117 0 0 25 0 1 0 718323505 174362624 39112 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 42569 39112 1111 63 0 42506 0 vsize: 170276 [startup+260.02 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 4940831 0 0 0 16497 9500 0 0 25 0 1 0 718323505 177614848 39893 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 43363 39893 1111 63 0 43300 0 vsize: 173452 [startup+270.02 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 5127794 0 0 0 17120 9877 0 0 25 0 1 0 718323505 180609024 40660 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 44094 40660 1111 63 0 44031 0 vsize: 176376 [startup+280.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 5314900 0 0 0 17744 10253 0 0 25 0 1 0 718323505 183734272 41426 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 44857 41426 1111 63 0 44794 0 vsize: 179428 [startup+290.022 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 5499886 0 0 0 18370 10627 0 0 25 0 1 0 718323505 188411904 42596 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 45999 42596 1111 63 0 45936 0 vsize: 183996 [startup+300.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 5686477 0 0 0 18995 11002 0 0 25 0 1 0 718323505 191393792 43304 4294967295 134512640 134714508 3221221776 3221220080 134568032 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 46727 43304 1111 63 0 46664 0 vsize: 186908 [startup+310.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 5873546 0 0 0 19626 11372 0 0 25 0 1 0 718323505 194248704 43980 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 47424 43980 1111 63 0 47361 0 vsize: 189696 [startup+320.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 6059196 0 0 0 20250 11747 0 0 25 0 1 0 718323505 197103616 44742 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 48121 44746 1111 63 0 48058 0 vsize: 192484 [startup+330.024 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 6245946 0 0 0 20868 12130 0 0 25 0 1 0 718323505 199815168 45418 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 48783 45423 1111 63 0 48720 0 vsize: 195132 [startup+340.024 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 6430406 0 0 0 21494 12504 0 0 25 0 1 0 718323505 202534912 46068 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 49447 46068 1111 63 0 49384 0 vsize: 197788 [startup+350.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 6615808 0 0 0 22126 12872 0 0 25 0 1 0 718323505 205250560 46739 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 50110 46739 1111 63 0 50047 0 vsize: 200440 [startup+360.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 6800139 0 0 0 22748 13250 0 0 25 0 1 0 718323505 207970304 47349 4294967295 134512640 134714508 3221221776 3221220080 134568040 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 50774 47349 1111 63 0 50711 0 vsize: 203096 [startup+370.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 6982982 0 0 0 23371 13627 0 0 25 0 1 0 718323505 210550784 48072 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 51404 48072 1111 63 0 51341 0 vsize: 205616 [startup+380.027 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 7166631 0 0 0 24001 13997 0 0 25 0 1 0 718323505 213135360 48679 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 52035 48679 1111 63 0 51972 0 vsize: 208140 [startup+390.027 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 7350016 0 0 0 24627 14371 0 0 25 0 1 0 718323505 215207936 49220 4294967295 134512640 134714508 3221221776 3221218252 1077191424 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 52541 49220 1111 63 0 52478 0 vsize: 210164 [startup+400.028 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 7533302 0 0 0 25262 14736 0 0 25 0 1 0 718323505 218161152 49933 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 53262 49933 1111 63 0 53199 0 vsize: 213048 [startup+410.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 7715987 0 0 0 25890 15108 0 0 25 0 1 0 718323505 220086272 50436 4294967295 134512640 134714508 3221221776 3221218540 1077198905 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 53732 50436 1111 63 0 53669 0 vsize: 214928 [startup+420.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 7898909 0 0 0 26522 15476 0 0 25 0 1 0 718323505 223178752 51073 4294967295 134512640 134714508 3221221776 3221220080 134568044 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 54487 51073 1111 63 0 54424 0 vsize: 217948 [startup+430.03 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 8082163 0 0 0 27151 15848 0 0 25 0 1 0 718323505 227164160 51767 4294967295 134512640 134714508 3221221776 3221220080 134568044 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 55460 51767 1111 63 0 55397 0 vsize: 221840 [startup+440.03 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 8264874 0 0 0 27772 16226 0 0 25 0 1 0 718323505 229470208 52242 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 56023 52242 1111 63 0 55960 0 vsize: 224092 [startup+450.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 8447632 0 0 0 28391 16608 0 0 25 0 1 0 718323505 231788544 52862 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 56589 52862 1111 63 0 56526 0 vsize: 226356 [startup+460.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 8631086 0 0 0 29017 16982 0 0 25 0 1 0 718323505 234229760 53457 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 57185 53457 1111 63 0 57122 0 vsize: 228740 [startup+470.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 8813393 0 0 0 29648 17351 0 0 25 0 1 0 718323505 236404736 53979 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 57716 53979 1111 63 0 57653 0 vsize: 230864 [startup+480.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 8995883 0 0 0 30265 17734 0 0 25 0 1 0 718323505 238718976 54533 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 58281 54533 1111 63 0 58218 0 vsize: 233124 [startup+490.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 9177349 0 0 0 30889 18110 0 0 25 0 1 0 718323505 241025024 55151 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 58844 55151 1111 63 0 58781 0 vsize: 235376 [startup+500.033 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 9359917 0 0 0 31516 18483 0 0 25 0 1 0 718323505 243200000 55655 4294967295 134512640 134714508 3221221776 3221220080 134568040 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 59375 55655 1111 63 0 59312 0 vsize: 237500 [startup+510.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 9542607 0 0 0 32135 18864 0 0 25 0 1 0 718323505 245506048 56186 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 59938 56186 1111 63 0 59875 0 vsize: 239752 [startup+520.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 9724623 0 0 0 32762 19237 0 0 25 0 1 0 718323505 247685120 56749 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 60470 56749 1111 63 0 60407 0 vsize: 241880 [startup+530.035 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 9907540 0 0 0 33392 19608 0 0 25 0 1 0 718323505 249856000 57298 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 61000 57298 1111 63 0 60937 0 vsize: 244000 [startup+540.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 10090080 0 0 0 34007 19993 0 0 25 0 1 0 718323505 252030976 57773 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 61531 57773 1111 63 0 61468 0 vsize: 246124 [startup+550.037 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 10272492 0 0 0 34624 20376 0 0 25 0 1 0 718323505 254201856 58318 4294967295 134512640 134714508 3221221776 3221220080 134568040 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 62061 58318 1111 63 0 61998 0 vsize: 248244 [startup+560.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 10456286 0 0 0 35254 20746 0 0 25 0 1 0 718323505 256249856 58842 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 62561 58842 1111 63 0 62498 0 vsize: 250244 [startup+570.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 10638641 0 0 0 35884 21116 0 0 25 0 1 0 718323505 258420736 59460 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 63091 59460 1111 63 0 63028 0 vsize: 252364 [startup+580.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 10820454 0 0 0 36508 21492 0 0 25 0 1 0 718323505 260456448 59852 4294967295 134512640 134714508 3221221776 3221220080 134568040 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 63588 59852 1111 63 0 63525 0 vsize: 254352 [startup+590.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 11002901 0 0 0 37137 21863 0 0 25 0 1 0 718323505 262492160 60485 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 64085 60485 1111 63 0 64022 0 vsize: 256340 [startup+600.04 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 11187562 0 0 0 37767 22233 0 0 25 0 1 0 718323505 264048640 60860 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 64615 60861 1111 63 0 64552 0 vsize: 257860 [startup+610.04 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 11371719 0 0 0 38389 22611 0 0 25 0 1 0 718323505 266706944 61374 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 65114 61379 1111 63 0 65051 0 vsize: 260456 [startup+620.04 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 11556124 0 0 0 39009 22992 0 0 25 0 1 0 718323505 268746752 61946 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 65612 61950 1111 63 0 65549 0 vsize: 262448 [startup+630.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 11740025 0 0 0 39633 23368 0 0 25 0 1 0 718323505 270782464 62472 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 66109 62477 1111 63 0 66046 0 vsize: 264436 [startup+640.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 11922930 0 0 0 40248 23752 0 0 25 0 1 0 718323505 272818176 62961 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 66606 62961 1111 63 0 66543 0 vsize: 266424 [startup+650.042 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 12107661 0 0 0 40874 24126 0 0 25 0 1 0 718323505 274718720 63472 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 67070 63476 1111 63 0 67007 0 vsize: 268280 [startup+660.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 12291903 0 0 0 41500 24500 0 0 25 0 1 0 718323505 276754432 63879 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 67567 63883 1111 63 0 67504 0 vsize: 270268 [startup+670.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 12476329 0 0 0 42112 24889 0 0 25 0 1 0 718323505 278798336 64454 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 68066 64459 1111 63 0 68003 0 vsize: 272264 [startup+680.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 12660349 0 0 0 42738 25263 0 0 25 0 1 0 718323505 280707072 64900 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 68532 64905 1111 63 0 68469 0 vsize: 274128 [startup+690.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 12844915 0 0 0 43355 25646 0 0 25 0 1 0 718323505 282742784 65415 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 69029 65420 1111 63 0 68966 0 vsize: 276116 [startup+700.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 13026890 0 0 0 43983 26018 0 0 25 0 1 0 718323505 284643328 65793 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 69493 65793 1111 63 0 69430 0 vsize: 277972 [startup+710.046 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 13211460 0 0 0 44610 26391 0 0 25 0 1 0 718323505 286543872 66396 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 69794 66234 1111 63 0 69731 0 vsize: 279828 [startup+720.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 13396130 0 0 0 45227 26774 0 0 25 0 1 0 718323505 288444416 66843 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 70421 66847 1111 63 0 70358 0 vsize: 281684 [startup+730.046 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 13484490 0 0 0 46049 26952 0 0 25 0 1 0 718323505 302915584 70402 4294967295 134512640 134714508 3221221776 3221220024 1077378037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 73954 70403 1111 63 0 73891 0 vsize: 295816 [startup+740.074 s] Raw data (loadavg): 0.99 0.98 0.99 2/54 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 13638960 0 0 0 46685 27319 0 0 25 0 1 0 718323505 930119680 223478 4294967295 134512640 134714508 3221221776 3221220304 134554857 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 227080 223485 1111 63 0 227017 0 vsize: 908320 [startup+741.02 s] Raw data (loadavg): 0.99 0.98 0.99 1/53 30098 Raw data (stat): 30098 (bsolo_lpr) R 30097 7876 7672 0 -1 0 13638960 0 0 0 46685 27319 0 0 25 0 1 0 718323505 930119680 223478 4294967295 134512640 134714508 3221221776 3221220304 134554857 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 227080 223485 1111 63 0 227017 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 741.019 CPU time (s): 740.793 CPU user time (s): 467.017 CPU system time (s): 273.776 CPU usage (%): 99.9695 Max. virtual memory (Kb): 908320 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####