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 wulflinc6 THE 2005-06-08 23:08:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=28916 boxname=wulflinc6 idbench=302 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: dcb6d1c3f66e900ae345e6fa455bef2a /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb IDLAUNCH: 28916 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 893924 kB Buffers: 24280 kB Cached: 93172 kB SwapCached: 2432 kB Active: 41216 kB Inactive: 79796 kB HighTotal: 131008 kB HighFree: 39116 kB LowTotal: 903652 kB LowFree: 854808 kB SwapTotal: 2097136 kB SwapFree: 2093696 kB Dirty: 4 kB Writeback: 0 kB Mapped: 4992 kB Slab: 13912 kB Committed_AS: 63736 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-08 23:20:50 (client local time) WITH STATUS 0 IN 717.097 SECONDS stats: 28916 7 717.097 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.88 0.95 0.91 2/54 3817 Raw data (stat): 3817 (runsolver) R 3816 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 905477648 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0001 s] Raw data (loadavg): 0.90 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 34024 0 0 0 928 70 0 0 25 0 1 0 905477648 41046016 6697 4294967295 134512640 134716908 3221224560 3221221324 1077191044 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9971 6679 1111 63 0 9908 0 vsize: 40084 [startup+20.0002 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 161416 0 0 0 1707 291 0 0 25 0 1 0 905477648 57155584 10637 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 13919 10607 1111 63 0 13856 0 vsize: 55816 [startup+30.0004 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 386785 0 0 0 2309 689 0 0 25 0 1 0 905477648 67690496 13171 4294967295 134512640 134716908 3221224560 3221222900 1077374114 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16526 13171 1111 63 0 16463 0 vsize: 66104 [startup+40.0005 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 611721 0 0 0 2910 1088 0 0 25 0 1 0 905477648 76689408 15355 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 18723 15362 1111 63 0 18660 0 vsize: 74892 [startup+50.0006 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 833415 0 0 0 3504 1494 0 0 25 0 1 0 905477648 84570112 17305 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 20647 17311 1111 63 0 20584 0 vsize: 82588 [startup+59.9997 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1052140 0 0 0 4106 1893 0 0 25 0 1 0 905477648 91639808 19030 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 22373 19037 1111 63 0 22310 0 vsize: 89492 [startup+69.9989 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1267530 0 0 0 4709 2289 0 0 25 0 1 0 905477648 98160640 20586 4294967295 134512640 134716908 3221224560 3221222604 1077387418 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 23965 20593 1111 63 0 23902 0 vsize: 95860 [startup+79.999 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1482868 0 0 0 5317 2682 0 0 25 0 1 0 905477648 104873984 22280 4294967295 134512640 134716908 3221224560 3221223368 134674635 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 25665 22283 1111 63 0 25602 0 vsize: 102416 [startup+89.9982 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1698253 0 0 0 5915 3084 0 0 25 0 1 0 905477648 110833664 23755 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 27059 23762 1111 63 0 26996 0 vsize: 108236 [startup+99.9974 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1908754 0 0 0 6520 3479 0 0 25 0 1 0 905477648 116269056 25061 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 28386 25067 1111 63 0 28323 0 vsize: 113544 [startup+109.998 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2118176 0 0 0 7119 3880 0 0 25 0 1 0 905477648 122195968 26348 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 29833 26354 1111 63 0 29770 0 vsize: 119332 [startup+119.998 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2324418 0 0 0 7733 4267 0 0 25 0 1 0 905477648 127078400 27477 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 31025 27483 1111 63 0 30962 0 vsize: 124100 [startup+129.997 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2532175 0 0 0 8349 4651 0 0 25 0 1 0 905477648 131702784 28677 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 32154 28682 1111 63 0 32091 0 vsize: 128616 [startup+139.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2736740 0 0 0 8960 5040 0 0 25 0 1 0 905477648 136323072 29739 4294967295 134512640 134716908 3221224560 3221222604 1077387418 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 33282 29745 1111 63 0 33219 0 vsize: 133128 [startup+149.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2939958 0 0 0 9573 5428 0 0 25 0 1 0 905477648 140201984 30793 4294967295 134512640 134716908 3221224560 3221222968 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 34310 30798 1111 63 0 34247 0 vsize: 136916 [startup+159.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3140328 0 0 0 10185 5815 0 0 25 0 1 0 905477648 144613376 31801 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 35306 31807 1111 63 0 35243 0 vsize: 141224 [startup+169.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3341105 0 0 0 10800 6200 0 0 25 0 1 0 905477648 148684800 32822 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 36300 32826 1111 63 0 36237 0 vsize: 145200 [startup+179.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3540938 0 0 0 11413 6587 0 0 25 0 1 0 905477648 152485888 33813 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 37140 33728 1111 63 0 37077 0 vsize: 148912 [startup+189.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3739475 0 0 0 12026 6976 0 0 25 0 1 0 905477648 155918336 34666 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 38066 34666 1111 63 0 38003 0 vsize: 152264 [startup+199.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3937881 0 0 0 12640 7361 0 0 25 0 1 0 905477648 160088064 35576 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 39084 35581 1111 63 0 39021 0 vsize: 156336 [startup+209.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4136520 0 0 0 13256 7746 0 0 25 0 1 0 905477648 163618816 36485 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 39946 36490 1111 63 0 39883 0 vsize: 159784 [startup+219.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4330968 0 0 0 13877 8124 0 0 25 0 1 0 905477648 167153664 37375 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 40809 37375 1111 63 0 40746 0 vsize: 163236 [startup+229.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4527875 0 0 0 14486 8515 0 0 25 0 1 0 905477648 170549248 38178 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 41638 38183 1111 63 0 41575 0 vsize: 166552 [startup+239.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4724130 0 0 0 15087 8915 0 0 25 0 1 0 905477648 173944832 39063 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 42467 39068 1111 63 0 42404 0 vsize: 169868 [startup+249.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4918385 0 0 0 15704 9298 0 0 25 0 1 0 905477648 176787456 39777 4294967295 134512640 134716908 3221224560 3221222568 1077364239 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 43263 39782 1111 63 0 43200 0 vsize: 172644 [startup+259.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5111767 0 0 0 16316 9686 0 0 25 0 1 0 905477648 180469760 40641 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 44060 40645 1111 63 0 43997 0 vsize: 176240 [startup+269.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5306223 0 0 0 16937 10066 0 0 25 0 1 0 905477648 183595008 41433 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 44823 41438 1111 63 0 44760 0 vsize: 179292 [startup+279.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5498434 0 0 0 17555 10448 0 0 25 0 1 0 905477648 188407808 42540 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 45998 42545 1111 63 0 45935 0 vsize: 183992 [startup+289.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5691796 0 0 0 18167 10836 0 0 25 0 1 0 905477648 191389696 43274 4294967295 134512640 134716908 3221224560 3221222604 1077387418 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 46726 43280 1111 63 0 46663 0 vsize: 186904 [startup+299.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5883556 0 0 0 18777 11226 0 0 25 0 1 0 905477648 194379776 44103 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 47456 44108 1111 63 0 47393 0 vsize: 189824 [startup+309.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6075782 0 0 0 19395 11609 0 0 25 0 1 0 905477648 197369856 44822 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 48186 44828 1111 63 0 48123 0 vsize: 192744 [startup+319.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6267958 0 0 0 20008 11997 0 0 25 0 1 0 905477648 199749632 45420 4294967295 134512640 134716908 3221224560 3221222220 1077244344 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 48881 45425 1111 63 0 48818 0 vsize: 195068 [startup+329.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6460007 0 0 0 20619 12386 0 0 25 0 1 0 905477648 203071488 46197 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 49578 46201 1111 63 0 49515 0 vsize: 198312 [startup+339.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6649873 0 0 0 21240 12764 0 0 25 0 1 0 905477648 205795328 46845 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 50243 46851 1111 63 0 50180 0 vsize: 200972 [startup+349.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6841915 0 0 0 21851 13154 0 0 25 0 1 0 905477648 208019456 47467 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 50786 47467 1111 63 0 50723 0 vsize: 203144 [startup+359.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7033100 0 0 0 22462 13543 0 0 25 0 1 0 905477648 211230720 48227 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 51570 48232 1111 63 0 51507 0 vsize: 206280 [startup+369.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7224446 0 0 0 23081 13925 0 0 25 0 1 0 905477648 213942272 48902 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 52232 48907 1111 63 0 52169 0 vsize: 208928 [startup+379.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7414570 0 0 0 23702 14305 0 0 25 0 1 0 905477648 216526848 49488 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 52863 49493 1111 63 0 52800 0 vsize: 211452 [startup+389.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7605613 0 0 0 24322 14685 0 0 25 0 1 0 905477648 219103232 50110 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 53492 50115 1111 63 0 53429 0 vsize: 213968 [startup+399.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7794357 0 0 0 24938 15069 0 0 25 0 1 0 905477648 221687808 50780 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 54123 50780 1111 63 0 54060 0 vsize: 216492 [startup+409.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7982161 0 0 0 25552 15454 0 0 25 0 1 0 905477648 224264192 51426 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 54752 51431 1111 63 0 54689 0 vsize: 219008 [startup+419.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8171518 0 0 0 26174 15833 0 0 25 0 1 0 905477648 228249600 51958 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 55725 51963 1111 63 0 55662 0 vsize: 222900 [startup+429.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8361285 0 0 0 26792 16215 0 0 25 0 1 0 905477648 230694912 52651 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 56322 52656 1111 63 0 56259 0 vsize: 225288 [startup+439.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8551202 0 0 0 27409 16598 0 0 25 0 1 0 905477648 233136128 53200 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 56918 53204 1111 63 0 56855 0 vsize: 227672 [startup+449.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8740814 0 0 0 28025 16982 0 0 25 0 1 0 905477648 235589632 53752 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 57517 53757 1111 63 0 57454 0 vsize: 230068 [startup+459.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8929411 0 0 0 28643 17365 0 0 25 0 1 0 905477648 237895680 54411 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 58080 54416 1111 63 0 58017 0 vsize: 232320 [startup+469.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9118029 0 0 0 29266 17742 0 0 25 0 1 0 905477648 240201728 54951 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 58643 54956 1111 63 0 58580 0 vsize: 234572 [startup+479.999 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9306816 0 0 0 29885 18123 0 0 25 0 1 0 905477648 242655232 55538 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 59242 55543 1111 63 0 59179 0 vsize: 236968 [startup+489.999 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9496977 0 0 0 30502 18507 0 0 25 0 1 0 905477648 244961280 56140 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 59805 56145 1111 63 0 59742 0 vsize: 239220 [startup+499.999 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9686333 0 0 0 31114 18895 0 0 25 0 1 0 905477648 247132160 56603 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 60335 56607 1111 63 0 60272 0 vsize: 241340 [startup+510 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9875855 0 0 0 31736 19273 0 0 25 0 1 0 905477648 249446400 57271 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 60900 57276 1111 63 0 60837 0 vsize: 243600 [startup+520 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10063062 0 0 0 32352 19656 0 0 25 0 1 0 905477648 251617280 57774 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 61430 57779 1111 63 0 61367 0 vsize: 245720 [startup+530 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10252102 0 0 0 32964 20044 0 0 25 0 1 0 905477648 253337600 58224 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 61850 58224 1111 63 0 61787 0 vsize: 247400 [startup+540 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10441846 0 0 0 33581 20428 0 0 25 0 1 0 905477648 256110592 58848 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 62527 58853 1111 63 0 62464 0 vsize: 250108 [startup+550 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10630409 0 0 0 34198 20812 0 0 25 0 1 0 905477648 258281472 59452 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 62910 59306 1111 63 0 62847 0 vsize: 252228 [startup+560.001 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10819099 0 0 0 34822 21187 0 0 25 0 1 0 905477648 260452352 59969 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 63587 59974 1111 63 0 63524 0 vsize: 254348 [startup+570 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11008127 0 0 0 35447 21563 0 0 25 0 1 0 905477648 262623232 60488 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 64117 60493 1111 63 0 64054 0 vsize: 256468 [startup+580.001 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11196461 0 0 0 36063 21948 0 0 25 0 1 0 905477648 264802304 61001 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 64649 61006 1111 63 0 64586 0 vsize: 258596 [startup+590.001 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11385064 0 0 0 36678 22333 0 0 25 0 1 0 905477648 266838016 61487 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 65146 61492 1111 63 0 65083 0 vsize: 260584 [startup+600.001 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11573596 0 0 0 37296 22714 0 0 25 0 1 0 905477648 268877824 61968 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 65644 61973 1111 63 0 65581 0 vsize: 262576 [startup+610.001 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11763387 0 0 0 37916 23095 0 0 25 0 1 0 905477648 271048704 62572 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 66174 62577 1111 63 0 66111 0 vsize: 264696 [startup+620.002 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11953716 0 0 0 38520 23491 0 0 25 0 1 0 905477648 273084416 63050 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 66671 63054 1111 63 0 66608 0 vsize: 266684 [startup+630.001 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12142811 0 0 0 39139 23873 0 0 25 0 1 0 905477648 275128320 63458 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 67170 63463 1111 63 0 67107 0 vsize: 268680 [startup+640.001 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12330952 0 0 0 39754 24257 0 0 25 0 1 0 905477648 277164032 64073 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 67667 64079 1111 63 0 67604 0 vsize: 270668 [startup+650.002 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12519576 0 0 0 40367 24645 0 0 25 0 1 0 905477648 278552576 64445 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 68165 64446 1111 63 0 68102 0 vsize: 272024 [startup+660.002 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12708685 0 0 0 40983 25029 0 0 25 0 1 0 905477648 281243648 65068 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 68663 65073 1111 63 0 68600 0 vsize: 274652 [startup+670.002 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12897525 0 0 0 41595 25418 0 0 25 0 1 0 905477648 283279360 65531 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 69160 65536 1111 63 0 69097 0 vsize: 276640 [startup+680.002 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13085739 0 0 0 42211 25802 0 0 25 0 1 0 905477648 285179904 65990 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 69624 65996 1111 63 0 69561 0 vsize: 278496 [startup+690.002 s] Raw data (loadavg): 1.15 1.02 0.93 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13274739 0 0 0 42828 26185 0 0 25 0 1 0 905477648 287215616 66423 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 70121 66428 1111 63 0 70058 0 vsize: 280484 [startup+700.002 s] Raw data (loadavg): 1.13 1.02 0.93 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13462429 0 0 0 43448 26565 0 0 25 0 1 0 905477648 289124352 66978 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 70587 66983 1111 63 0 70524 0 vsize: 282348 [startup+710.003 s] Raw data (loadavg): 1.11 1.02 0.93 2/54 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13492530 0 0 0 44382 26631 0 0 25 0 1 0 905477648 330108928 78432 4294967295 134512640 134716908 3221224560 3221223488 134606504 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 80593 78438 1111 63 0 80530 0 vsize: 322372 [startup+716.97 s] Raw data (loadavg): 1.17 1.03 0.93 1/53 3817 Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13492530 0 0 0 44382 26631 0 0 25 0 1 0 905477648 330108928 78432 4294967295 134512640 134716908 3221224560 3221223488 134606504 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 80593 78438 1111 63 0 80530 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 716.97 CPU time (s): 717.097 CPU user time (s): 446.822 CPU system time (s): 270.275 CPU usage (%): 100.018 Max. virtual memory (Kb): 322372 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####