Name | normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.3.accl.ucl.opb |
MD5SUM | 9fbb3a49a26e96e8ca349ca5e732b02f |
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 | 36 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 130 |
Number of bits of the biggest sum of numbers | 8 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 9.8365 |
Number of variables | 4622 |
Total number of constraints | 12569 |
Number of constraints which are clauses | 11753 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 816 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 11 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-06-07 16:03:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=27739 boxname=wulflinc4 idbench=297 idsolver=20 numberseed=0 MD5SUM SOLVER: f6aa7fb267fa9710116626be7e6d3048 /oldhome/oroussel/solvers/bsolo_lpr-v2 MD5SUM BENCH: 9fbb3a49a26e96e8ca349ca5e732b02f /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.burch_dill.3.accl.ucl.opb REAL COMMAND: bsolo_lpr-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.burch_dill.3.accl.ucl.opb IDLAUNCH: 27739 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 922832 kB Buffers: 33820 kB Cached: 55132 kB SwapCached: 944 kB Active: 19008 kB Inactive: 72080 kB HighTotal: 131008 kB HighFree: 104776 kB LowTotal: 903652 kB LowFree: 818056 kB SwapTotal: 2097136 kB SwapFree: 2095204 kB Dirty: 28 kB Writeback: 0 kB Mapped: 4800 kB Slab: 15088 kB Committed_AS: 71788 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-07 16:17:11 (client local time) WITH STATUS 20 IN 804.235 SECONDS stats: 27739 7 804.235 20 #### 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 4622 variables and 12569 constraints. c After prepocess the problem consists of 3453 variables and 9923 constraints. c preprocess terminated 102.426 s c Not use computed LB before first solution. s UNSATISFIABLE c Exit Code: 20 c Total time: 804.189 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 Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.91 0.95 0.91 1/54 18126 Raw data (stat): 18126 (runsolver) R 18125 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 894277056 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.0011 s] Raw data (loadavg): 0.92 0.95 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 954 42 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223200 134594947 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+20.0024 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 1954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223360 134617258 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+30.0033 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 2954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223040 134539376 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+40.0034 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 3954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223184 134594959 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+50.0039 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 4954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223200 134606484 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+60.0037 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 5955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223288 134543552 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+70.005 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 6955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223312 134630808 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+80.0054 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 7955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223200 134594947 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+90.0053 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 8955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221222924 134539296 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+100.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 9955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223176 134543796 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17005 16145 1111 63 0 16942 0 vsize: 68020 [startup+110.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 10954 45 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223124 134699247 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+120.007 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 18126 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 11952 46 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223144 134543600 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+130.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 12952 47 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223320 134588009 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+140.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 13951 48 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134543740 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+150.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 14950 49 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223120 134542300 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+160.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 15949 50 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134539460 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 16948 51 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223072 134535032 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 17948 52 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134549700 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 18947 53 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223304 134558492 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 19946 54 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223288 134535787 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+210.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 20946 54 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223264 134528481 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 21945 55 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223216 134536638 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 22944 56 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134543686 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+240.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 23944 57 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223116 134539243 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 24944 57 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223164 134536788 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 25943 58 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223328 134529276 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+270.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 26943 58 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223264 134528595 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+280.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 27942 59 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221222956 134613768 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+290.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 28941 60 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223116 134539324 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 29941 60 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223284 134655251 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+310.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 30940 61 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223212 134536763 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+320.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 31939 62 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+330.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 32939 63 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223284 134535756 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+340.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 33949 63 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223200 134698487 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+350.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 34948 64 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+360.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 35948 65 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223264 134535812 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+370.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 36947 65 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+380.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 37947 66 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223116 134535903 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17051 16174 1111 63 0 16988 0 vsize: 68204 [startup+390.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16295 0 0 0 38946 67 0 0 25 0 1 0 894277056 69976064 16213 4294967295 134512640 134716908 3221224560 3221223056 134699780 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17084 16213 1111 63 0 17021 0 vsize: 68336 [startup+400.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16522 0 0 0 39945 69 0 0 25 0 1 0 894277056 70922240 16440 4294967295 134512640 134716908 3221224560 3221223192 134543090 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17315 16440 1111 63 0 17252 0 vsize: 69260 [startup+410.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16682 0 0 0 40943 70 0 0 25 0 1 0 894277056 71462912 16600 4294967295 134512640 134716908 3221224560 3221223216 134536643 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17447 16600 1111 63 0 17384 0 vsize: 69788 [startup+420.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16868 0 0 0 41942 72 0 0 25 0 1 0 894277056 72273920 16786 4294967295 134512640 134716908 3221224560 3221223312 134594947 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17645 16786 1111 63 0 17582 0 vsize: 70580 [startup+430.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16978 0 0 0 42942 72 0 0 25 0 1 0 894277056 72679424 16896 4294967295 134512640 134716908 3221224560 3221223212 134543588 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17744 16896 1111 63 0 17681 0 vsize: 70976 [startup+440.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17109 0 0 0 43941 73 0 0 25 0 1 0 894277056 73220096 17027 4294967295 134512640 134716908 3221224560 3221223204 134536649 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17876 17027 1111 63 0 17813 0 vsize: 71504 [startup+450.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17224 0 0 0 44940 75 0 0 25 0 1 0 894277056 73752576 17142 4294967295 134512640 134716908 3221224560 3221223228 134551979 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18006 17142 1111 63 0 17943 0 vsize: 72024 [startup+460.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17409 0 0 0 45939 76 0 0 25 0 1 0 894277056 74563584 17327 4294967295 134512640 134716908 3221224560 3221223224 134543600 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18204 17327 1111 63 0 18141 0 vsize: 72816 [startup+470.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17575 0 0 0 46938 76 0 0 25 0 1 0 894277056 75239424 17493 4294967295 134512640 134716908 3221224560 3221223216 134613601 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18369 17493 1111 63 0 18306 0 vsize: 73476 [startup+480.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17706 0 0 0 47937 78 0 0 25 0 1 0 894277056 75780096 17624 4294967295 134512640 134716908 3221224560 3221223200 134539376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18501 17624 1111 63 0 18438 0 vsize: 74004 [startup+490.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17809 0 0 0 48936 79 0 0 25 0 1 0 894277056 76185600 17727 4294967295 134512640 134716908 3221224560 3221223248 134542836 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18600 17727 1111 63 0 18537 0 vsize: 74400 [startup+500.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17902 0 0 0 49936 80 0 0 25 0 1 0 894277056 76595200 17820 4294967295 134512640 134716908 3221224560 3221223196 134543664 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18700 17820 1111 63 0 18637 0 vsize: 74800 [startup+510.126 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18107 0 0 0 50934 81 0 0 25 0 1 0 894277056 77406208 18025 4294967295 134512640 134716908 3221224560 3221223296 134528677 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18898 18025 1111 63 0 18835 0 vsize: 75592 [startup+520.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18227 0 0 0 51934 82 0 0 25 0 1 0 894277056 77811712 18145 4294967295 134512640 134716908 3221224560 3221223164 134536817 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18997 18145 1111 63 0 18934 0 vsize: 75988 [startup+530.126 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18297 0 0 0 52933 83 0 0 25 0 1 0 894277056 78082048 18215 4294967295 134512640 134716908 3221224560 3221223200 134543070 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19063 18215 1111 63 0 19000 0 vsize: 76252 [startup+540.126 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18321 0 0 0 53933 83 0 0 25 0 1 0 894277056 78217216 18239 4294967295 134512640 134716908 3221224560 3221223192 134543665 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19096 18239 1111 63 0 19033 0 vsize: 76384 [startup+550.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18363 0 0 0 54933 83 0 0 25 0 1 0 894277056 78352384 18281 4294967295 134512640 134716908 3221224560 3221223196 134699250 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19129 18281 1111 63 0 19066 0 vsize: 76516 [startup+560.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18452 0 0 0 55932 84 0 0 25 0 1 0 894277056 78757888 18370 4294967295 134512640 134716908 3221224560 3221223200 134542352 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19228 18370 1111 63 0 19165 0 vsize: 76912 [startup+570.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18608 0 0 0 56931 85 0 0 25 0 1 0 894277056 79429632 18526 4294967295 134512640 134716908 3221224560 3221223232 134542936 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19392 18526 1111 63 0 19329 0 vsize: 77568 [startup+580.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18659 0 0 0 57931 86 0 0 25 0 1 0 894277056 79564800 18577 4294967295 134512640 134716908 3221224560 3221223284 134535756 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19425 18577 1111 63 0 19362 0 vsize: 77700 [startup+590.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18780 0 0 0 58930 87 0 0 25 0 1 0 894277056 80089088 18698 4294967295 134512640 134716908 3221224560 3221223320 134592149 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19553 18698 1111 63 0 19490 0 vsize: 78212 [startup+600.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18840 0 0 0 59929 88 0 0 25 0 1 0 894277056 80359424 18758 4294967295 134512640 134716908 3221224560 3221223344 134529091 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19619 18758 1111 63 0 19556 0 vsize: 78476 [startup+610.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19024 0 0 0 60929 89 0 0 25 0 1 0 894277056 81170432 18942 4294967295 134512640 134716908 3221224560 3221223304 134558485 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19817 18942 1111 63 0 19754 0 vsize: 79268 [startup+620.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19149 0 0 0 61928 89 0 0 25 0 1 0 894277056 81575936 19067 4294967295 134512640 134716908 3221224560 3221223296 134524376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19916 19067 1111 63 0 19853 0 vsize: 79664 [startup+630.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19218 0 0 0 62928 90 0 0 25 0 1 0 894277056 81973248 19136 4294967295 134512640 134716908 3221224560 3221223140 134549630 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20013 19136 1111 63 0 19950 0 vsize: 80052 [startup+640.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19351 0 0 0 63927 91 0 0 25 0 1 0 894277056 82513920 19269 4294967295 134512640 134716908 3221224560 3221223236 134551958 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20145 19269 1111 63 0 20082 0 vsize: 80580 [startup+650.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19495 0 0 0 64927 91 0 0 25 0 1 0 894277056 83054592 19413 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20277 19413 1111 63 0 20214 0 vsize: 81108 [startup+660.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19668 0 0 0 65926 92 0 0 25 0 1 0 894277056 83726336 19586 4294967295 134512640 134716908 3221224560 3221223140 134549630 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20441 19586 1111 63 0 20378 0 vsize: 81764 [startup+670.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19802 0 0 0 66926 93 0 0 25 0 1 0 894277056 84267008 19720 4294967295 134512640 134716908 3221224560 3221223264 134528617 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20573 19720 1111 63 0 20510 0 vsize: 82292 [startup+680.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19955 0 0 0 67925 94 0 0 25 0 1 0 894277056 84942848 19873 4294967295 134512640 134716908 3221224560 3221223164 134536848 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20738 19873 1111 63 0 20675 0 vsize: 82952 [startup+690.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20000 0 0 0 68925 94 0 0 25 0 1 0 894277056 85078016 19918 4294967295 134512640 134716908 3221224560 3221223204 134536649 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20771 19918 1111 63 0 20708 0 vsize: 83084 [startup+700.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20070 0 0 0 69924 94 0 0 25 0 1 0 894277056 85348352 19988 4294967295 134512640 134716908 3221224560 3221223200 134539374 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20837 19988 1111 63 0 20774 0 vsize: 83348 [startup+710.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20137 0 0 0 70924 95 0 0 25 0 1 0 894277056 85618688 20055 4294967295 134512640 134716908 3221224560 3221223120 134542347 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20903 20055 1111 63 0 20840 0 vsize: 83612 [startup+720.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20187 0 0 0 71924 95 0 0 25 0 1 0 894277056 85889024 20105 4294967295 134512640 134716908 3221224560 3221223116 134535956 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20969 20105 1111 63 0 20906 0 vsize: 83876 [startup+730.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20330 0 0 0 72923 96 0 0 25 0 1 0 894277056 86429696 20248 4294967295 134512640 134716908 3221224560 3221223188 134698632 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21101 20248 1111 63 0 21038 0 vsize: 84404 [startup+740.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20500 0 0 0 73923 97 0 0 25 0 1 0 894277056 87105536 20418 4294967295 134512640 134716908 3221224560 3221223192 134552673 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21266 20418 1111 63 0 21203 0 vsize: 85064 [startup+750.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20647 0 0 0 74922 98 0 0 25 0 1 0 894277056 87785472 20565 4294967295 134512640 134716908 3221224560 3221223216 134536638 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21432 20565 1111 63 0 21369 0 vsize: 85728 [startup+760.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20791 0 0 0 75921 98 0 0 25 0 1 0 894277056 88326144 20709 4294967295 134512640 134716908 3221224560 3221223344 134529368 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21564 20709 1111 63 0 21501 0 vsize: 86256 [startup+770.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20852 0 0 0 76921 99 0 0 25 0 1 0 894277056 88596480 20770 4294967295 134512640 134716908 3221224560 3221223216 134524067 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21630 20770 1111 63 0 21567 0 vsize: 86520 [startup+780.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20910 0 0 0 77921 99 0 0 25 0 1 0 894277056 88854528 20828 4294967295 134512640 134716908 3221224560 3221223152 134549773 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21693 20828 1111 63 0 21630 0 vsize: 86772 [startup+790.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20950 0 0 0 78920 100 0 0 25 0 1 0 894277056 88989696 20868 4294967295 134512640 134716908 3221224560 3221223140 134698632 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21726 20868 1111 63 0 21663 0 vsize: 86904 [startup+800.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 21004 0 0 0 79919 101 0 0 25 0 1 0 894277056 89268224 20922 4294967295 134512640 134716908 3221224560 3221223280 134529381 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21794 20922 1111 63 0 21731 0 vsize: 87176 [startup+804.152 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 18128 Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 21004 0 0 0 79919 101 0 0 25 0 1 0 894277056 89268224 20922 4294967295 134512640 134716908 3221224560 3221223280 134529381 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21794 20922 1111 63 0 21731 0 vsize: 0 Child status: 20 Real time (s): 804.152 CPU time (s): 804.235 CPU user time (s): 803.174 CPU system time (s): 1.06084 CPU usage (%): 100.01 Max. virtual memory (Kb): 87176 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####