Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-egout.opb |
MD5SUM | fd101f0ba1a3813e843a38997ab7ed84 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 58880896 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1095 |
Biggest coefficient in the objective function | 533200896 |
Number of bits for the biggest coefficient in the objective function | 29 |
Sum of the numbers in the objective function | 14929722305 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 533200896 |
Number of bits of the biggest number in a constraint | 29 |
Biggest sum of numbers in a constraint | 14929722305 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04984 |
Number of variables | 1155 |
Total number of constraints | 153 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 55 |
Number of constraints which are nor clauses,nor cardinality constraints | 98 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 280 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-21 18:10:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18293 boxname=wulflinc31 idbench=1408 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: fd101f0ba1a3813e843a38997ab7ed84 /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-egout.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 18293 /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: 445556 kB Buffers: 2416 kB Cached: 554436 kB SwapCached: 816 kB Active: 8972 kB Inactive: 549860 kB HighTotal: 131008 kB HighFree: 2716 kB LowTotal: 903652 kB LowFree: 442840 kB SwapTotal: 2097892 kB SwapFree: 2095944 kB Dirty: 298292 kB Writeback: 0 kB Mapped: 4956 kB Slab: 24532 kB Committed_AS: 63860 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-21 18:11:56 (client local time) WITH STATUS 0 IN 62.1136 SECONDS stats: 18293 7 62.1136 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 1155 variables and 134 constraints. c After prepocess the problem consists of 481 variables and 145 constraints. c preprocess terminated 1.719 s c Initial Lower Bound: 48825430 c Lower Bound Elapsed time: 0.0585 c Use computed LB before first solution. c NEW SOLUTION FOUND: 90759296 @ 12.39 c NEW SOLUTION FOUND: 90751360 @ 12.494 c NEW SOLUTION FOUND: 87197312 @ 12.498 c NEW SOLUTION FOUND: 87191936 @ 12.711 c NEW SOLUTION FOUND: 87186560 @ 13.084 c NEW SOLUTION FOUND: 86908800 @ 13.328 c NEW SOLUTION FOUND: 83354752 @ 13.367 c NEW SOLUTION FOUND: 83347328 @ 17.531 #### 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): 1.70 2.46 1.70 1/55 14346 Raw data (stat): 14346 (runsolver) D 14345 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 18 0 1 0 806351736 1056768 100 4294967295 134512640 135381576 3221221680 3221216896 135158418 0 2147483391 1 90112 3225161850 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+10.0007 s] Raw data (loadavg): 1.59 2.41 1.69 2/55 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 6891 0 20 0 913 20 0 0 25 0 1 0 806351736 11399168 2094 4294967295 134512640 134714508 3221221776 3221219504 1075635647 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 2783 2094 1111 63 0 2720 0 vsize: 11132 [startup+20.0009 s] Raw data (loadavg): 1.50 2.37 1.68 2/55 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 16198 0 20 0 1881 52 0 0 25 0 1 0 806351736 14520320 2864 4294967295 134512640 134714508 3221221776 3221219888 1074867308 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 3545 2864 1111 63 0 3482 0 vsize: 14180 [startup+30.0005 s] Raw data (loadavg): 1.42 2.32 1.68 2/55 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 22325 0 20 0 2862 70 0 0 25 0 1 0 806351736 16510976 3350 4294967295 134512640 134714508 3221221776 3221220176 1074153792 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 4031 3350 1111 63 0 3968 0 vsize: 16124 [startup+40.0005 s] Raw data (loadavg): 1.58 2.33 1.68 2/55 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 30394 0 20 0 3841 92 0 0 25 0 1 0 806351736 20348928 4287 4294967295 134512640 134714508 3221221776 3221219504 1075828968 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 4968 4287 1111 63 0 4905 0 vsize: 19872 [startup+50.0006 s] Raw data (loadavg): 1.49 2.28 1.68 2/55 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 34679 0 20 0 4827 106 0 0 25 0 1 0 806351736 21073920 4464 4294967295 134512640 134714508 3221221776 3221219708 1077411564 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 5145 4464 1111 63 0 5082 0 vsize: 20580 [startup+60.0013 s] Raw data (loadavg): 1.42 2.24 1.67 2/55 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 38141 0 20 0 5811 122 0 0 25 0 1 0 806351736 21606400 4594 4294967295 134512640 134714508 3221221776 3221219504 1075635641 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 5275 4594 1111 63 0 5212 0 vsize: 21100 [startup+62.7755 s] Raw data (loadavg): 1.38 2.22 1.66 1/54 14346 Raw data (stat): 14346 (bsolo_lpr_cuts) R 14345 7876 7672 0 -1 0 38141 0 20 0 5811 122 0 0 25 0 1 0 806351736 21606400 4594 4294967295 134512640 134714508 3221221776 3221219504 1075635641 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 5275 4594 1111 63 0 5212 0 vsize: 0 Child status: 0 Real time (s): 62.7749 CPU time (s): 62.1136 CPU user time (s): 60.7968 CPU system time (s): 1.3168 CPU usage (%): 98.9464 Max. virtual memory (Kb): 21100 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####