Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-fast0507.opb |
MD5SUM | 2854384016ebafb26c8bfb47f81aee87 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63009 |
Biggest coefficient in the objective function | 2 |
Number of bits for the biggest coefficient in the objective function | 2 |
Sum of the numbers in the objective function | 122425 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 2 |
Number of bits of the biggest number in a constraint | 2 |
Biggest sum of numbers in a constraint | 122425 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.18 |
Number of variables | 63009 |
Total number of constraints | 63516 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63009 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 7753 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc26 THE 2005-05-24 19:41:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18319 boxname=wulflinc26 idbench=1410 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 18319 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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.061 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: 830140 kB Buffers: 34972 kB Cached: 145092 kB SwapCached: 680 kB Active: 56648 kB Inactive: 126132 kB HighTotal: 131008 kB HighFree: 34468 kB LowTotal: 903652 kB LowFree: 795672 kB SwapTotal: 2097892 kB SwapFree: 2096880 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6036 kB Slab: 15992 kB Committed_AS: 63732 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-24 19:47:28 (client local time) WITH STATUS 0 IN 383.078 SECONDS stats: 18319 7 383.078 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.95 0.91 2/54 23769 Raw data (stat): 23769 (runsolver) R 23768 20687 20686 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 832842090 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 4941 0 0 0 987 10 0 0 25 0 1 0 832842090 32555008 4865 4294967295 134512640 134714508 3221224576 3221222804 1077414401 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7948 4865 1111 63 0 7885 0 vsize: 31792 [startup+20.0011 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 9357 0 0 0 1981 17 0 0 25 0 1 0 832842090 50606080 9281 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12355 9284 1111 63 0 12292 0 vsize: 49420 [startup+30.0007 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 13830 0 0 0 2974 24 0 0 25 0 1 0 832842090 68939776 13754 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 16831 13754 1111 63 0 16768 0 vsize: 67324 [startup+40.0011 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 18339 0 0 0 3966 32 0 0 25 0 1 0 832842090 87310336 18263 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21316 18263 1111 63 0 21253 0 vsize: 85264 [startup+50.0012 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 22889 0 0 0 4959 40 0 0 25 0 1 0 832842090 105971712 22813 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25872 22813 1111 63 0 25809 0 vsize: 103488 [startup+60.0008 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 27483 0 0 0 5952 46 0 0 25 0 1 0 832842090 124907520 27407 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 30495 27407 1111 63 0 30432 0 vsize: 121980 [startup+70.0012 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 32126 0 0 0 6944 55 0 0 25 0 1 0 832842090 143867904 32050 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 35124 32050 1111 63 0 35061 0 vsize: 140496 [startup+80.0012 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 36818 0 0 0 7936 63 0 0 25 0 1 0 832842090 163131392 36742 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 39827 36742 1111 63 0 39764 0 vsize: 159308 [startup+90.0019 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 41564 0 0 0 8929 70 0 0 25 0 1 0 832842090 182538240 41488 4294967295 134512640 134714508 3221224576 3221222804 1077414358 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 44565 41488 1111 63 0 44502 0 vsize: 178260 [startup+100.001 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 46364 0 0 0 9921 79 0 0 25 0 1 0 832842090 202096640 46288 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 49340 46288 1111 63 0 49277 0 vsize: 197360 [startup+110.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 51246 0 0 0 10912 88 0 0 25 0 1 0 832842090 222244864 51170 4294967295 134512640 134714508 3221224576 3221222804 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 54259 51170 1111 63 0 54196 0 vsize: 217036 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 56199 0 0 0 11903 97 0 0 25 0 1 0 832842090 242552832 56123 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 59217 56123 1111 63 0 59154 0 vsize: 236868 [startup+130.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 61212 0 0 0 12894 106 0 0 25 0 1 0 832842090 263008256 61136 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 64211 61136 1111 63 0 64148 0 vsize: 256844 [startup+140.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 66324 0 0 0 13886 114 0 0 25 0 1 0 832842090 283910144 66248 4294967295 134512640 134714508 3221224576 3221222804 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 69314 66248 1111 63 0 69251 0 vsize: 277256 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 71484 0 0 0 14878 123 0 0 25 0 1 0 832842090 305115136 71408 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 74491 71408 1111 63 0 74428 0 vsize: 297964 [startup+160.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 76698 0 0 0 15869 132 0 0 25 0 1 0 832842090 326463488 76622 4294967295 134512640 134714508 3221224576 3221222804 1077414410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 79703 76622 1111 63 0 79640 0 vsize: 318812 [startup+170.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 81973 0 0 0 16861 140 0 0 25 0 1 0 832842090 347963392 81897 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 84952 81897 1111 63 0 84889 0 vsize: 339808 [startup+180.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 87326 0 0 0 17853 148 0 0 25 0 1 0 832842090 369909760 87250 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 90310 87250 1111 63 0 90247 0 vsize: 361240 [startup+190.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 92740 0 0 0 18845 156 0 0 25 0 1 0 832842090 392155136 92664 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 95741 92664 1111 63 0 95678 0 vsize: 382964 [startup+200.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 98251 0 0 0 19837 164 0 0 25 0 1 0 832842090 414773248 98175 4294967295 134512640 134714508 3221224576 3221222804 1077414358 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 101263 98175 1111 63 0 101200 0 vsize: 405052 [startup+210.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 103828 0 0 0 20828 173 0 0 25 0 1 0 832842090 437612544 103752 4294967295 134512640 134714508 3221224576 3221222804 1077414433 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 106839 103752 1111 63 0 106776 0 vsize: 427356 [startup+220.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 109505 0 0 0 21819 182 0 0 25 0 1 0 832842090 460906496 109429 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 112526 109429 1111 63 0 112463 0 vsize: 450104 [startup+230.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 115308 0 0 0 22809 193 0 0 25 0 1 0 832842090 484642816 115232 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 118321 115232 1111 63 0 118258 0 vsize: 473284 [startup+240.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 121343 0 0 0 23800 202 0 0 25 0 1 0 832842090 509427712 121267 4294967295 134512640 134714508 3221224576 3221222804 1077414407 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 124372 121267 1111 63 0 124309 0 vsize: 497488 [startup+250.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 127542 0 0 0 24789 213 0 0 25 0 1 0 832842090 534810624 127466 4294967295 134512640 134714508 3221224576 3221222804 1077414385 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 130569 127466 1111 63 0 130506 0 vsize: 522276 [startup+260.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 133759 0 0 0 25777 225 0 0 25 0 1 0 832842090 560193536 133683 4294967295 134512640 134714508 3221224576 3221222804 1077414357 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 136766 133683 1111 63 0 136703 0 vsize: 547064 [startup+270.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 140085 0 0 0 26766 237 0 0 25 0 1 0 832842090 586170368 140009 4294967295 134512640 134714508 3221224576 3221222804 1077414336 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 143108 140009 1111 63 0 143045 0 vsize: 572432 [startup+280.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 146703 0 0 0 27755 247 0 0 25 0 1 0 832842090 613191680 146627 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 149705 146627 1111 63 0 149642 0 vsize: 598820 [startup+290.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 153468 0 0 0 28742 261 0 0 25 0 1 0 832842090 640966656 153392 4294967295 134512640 134714508 3221224576 3221222804 1077414399 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 156486 153392 1111 63 0 156423 0 vsize: 625944 [startup+300.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 160360 0 0 0 29731 272 0 0 25 0 1 0 832842090 669188096 160284 4294967295 134512640 134714508 3221224576 3221222804 1077414410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 163376 160284 1111 63 0 163313 0 vsize: 653504 [startup+310.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 167462 0 0 0 30718 285 0 0 25 0 1 0 832842090 698146816 167386 4294967295 134512640 134714508 3221224576 3221222804 1077414349 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 170446 167386 1111 63 0 170383 0 vsize: 681784 [startup+320.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 174718 0 0 0 31707 296 0 0 25 0 1 0 832842090 727859200 174642 4294967295 134512640 134714508 3221224576 3221222804 1077414395 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 177700 174642 1111 63 0 177637 0 vsize: 710800 [startup+330.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 182248 0 0 0 32694 310 0 0 25 0 1 0 832842090 758767616 182172 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 185246 182172 1111 63 0 185183 0 vsize: 740984 [startup+340.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 190185 0 0 0 33679 325 0 0 25 0 1 0 832842090 791314432 190109 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 193192 190109 1111 63 0 193129 0 vsize: 772768 [startup+350.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 198359 0 0 0 34667 337 0 0 25 0 1 0 832842090 824971264 198283 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 201409 198283 1111 63 0 201346 0 vsize: 805636 [startup+360.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 206867 0 0 0 35650 354 0 0 25 0 1 0 832842090 859758592 206791 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 209902 206791 1111 63 0 209839 0 vsize: 839608 [startup+370.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 215698 0 0 0 36628 374 0 0 25 0 1 0 832842090 896040960 215110 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 218760 215110 1111 63 0 218697 0 vsize: 875040 [startup+380.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 224948 0 0 0 37607 394 0 0 25 0 1 0 832842090 933818368 222952 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 227983 222952 1111 63 0 227920 0 vsize: 911932 [startup+383.062 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 23769 Raw data (stat): 23769 (bsolo_lpr_cuts) R 23768 20687 20686 0 -1 0 224948 0 0 0 37607 394 0 0 25 0 1 0 832842090 933818368 222952 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 227983 222952 1111 63 0 227920 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 383.062 CPU time (s): 383.078 CPU user time (s): 378.643 CPU system time (s): 4.43433 CPU usage (%): 100.004 Max. virtual memory (Kb): 911932 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####