Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gesa2_o.opb |
MD5SUM | 70d38efa2ca4db2a9200144005e211ed |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
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 | 10368 |
Biggest coefficient in the objective function | 418848431931392 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 180197911475330400 |
Number of bits of the sum of numbers in the objective function | 58 |
Biggest number in a constraint | 418848431931392 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 180197911475330400 |
Number of bits of the biggest sum of numbers | 58 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.141977 |
Number of variables | 16224 |
Total number of constraints | 1584 |
Number of constraints which are clauses | 192 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1392 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 309 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc1 THE 2005-06-09 07:40:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29248 boxname=wulflinc1 idbench=1032 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: 70d38efa2ca4db2a9200144005e211ed /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-gesa2_o.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-gesa2_o.opb IDLAUNCH: 29248 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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.053 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: 902676 kB Buffers: 11492 kB Cached: 96440 kB SwapCached: 1140 kB Active: 25104 kB Inactive: 84976 kB HighTotal: 131008 kB HighFree: 32200 kB LowTotal: 903652 kB LowFree: 870476 kB SwapTotal: 2097136 kB SwapFree: 2094820 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5260 kB Slab: 16144 kB Committed_AS: 92716 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 07:40:30 (client local time) WITH STATUS 0 IN 25.5671 SECONDS stats: 29248 7 25.5671 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c ERROR Parsing file!!! c ERROR parsing line: +200000*XCW_0x2e_1201_bit_10 +400000*XCW_0x2e_1201_bit_9 +800000*XCW_0x2e_1201_bit_8 +1600000*XCW_0x2e_1201_bit_7 +3200000*XCW_0x2e_1201_bit_6 +6400000*XCW_0x2e_1201_bit_5 +12800000*XCW_0x2e_1201_bit_4 +25600000*XCW_0x2e_1201_bit_3 +51200000*XCW_0x2e_1201_bit_2 +102400000*XCW_0x2e_1201_bit_1 +204800000*XCW_0x2e_1201_bit0 +409600000*XCW_0x2e_1201_bit1 +819200000*XCW_0x2e_1201_bit2 +1638400000*XCW_0x2e_1201_bit3 +3276800000*XCW_0x2e_1201_bit4 +6553600000*XCW_0x2e_1201_bit5 +13107200000*XCW_0x2e_1201_bit6 +26214400000*XCW_0x2e_1201_bit7 +52428800000*XCW_0x2e_1201_bit8 +104857600000*XCW_0x2e_1201_bit9 +209715200000*XCW_0x2e_1201_bit10 +419430400000*XCW_0x2e_1201_bit11 +838860800000*XCW_0x2e_1201_bit12 +1677721600000*XCW_0x2e_1201_bit13 +3355443200000*XCW_0x2e_1201_bit14 +6710886400000*XCW_0x2e_1201_bit15 +13421772800000*XCW_0x2e_1201_bit16 +26843545600000*XCW_0x2e_1201_bit17 +53687091200000*XCW_0x2e_1201_bit18 +107374182400000*XCW_0x2e_1201_bit19 +200000*XCW_0x2e_1301_bit_10 +400000*XCW_0x2e_1301_bit_9 +800000*XCW_0x2e_1301_bit_8 +1600000*XCW_0x2e_1301_bit_7 +3200000*XCW_0x2e_1301_bit_6 +6400000*XCW_0x2e_1301_bit_5 +12800000*XCW_0x2e_1301_bit_4 +25600000*XCW_0x2e_1301_bit_3 +51200000*XCW_0x2e_1301_bit_2 +102400000*XCW_0x2e_1301_bit_1 +204800000*XCW_0x2e_1301_bit0 +409600000*XCW_0x2e_1301_bit1 +819200000*XCW_0x2e_1301_bit2 +1638400000*XCW_0x2e_1301_bit3 +3276800000*XCW_0x2e_1301_bit4 +6553600000*XCW_0x2e_1301_bit5 +13107200000*XCW_0x2e_1301_bit6 +26214400000*XCW_0x2e_1301_bit7 +52428800000*XCW_0x2e_1301_bit8 +104857600000*XCW_0x2e_1301_bit9 +209715200000*XCW_0x2e_1301_bit10 +419430400000*XCW_0x2e_1301_bit11 +838860800000*XCW_0x2e_1301_bit12 +1677721600000*XCW_0x2e_1301_bit13 +3355443200000*XCW_0x2e_1301_bit14 +6710886400000*XCW_0x2e_1301_bit15 +13421772800000*XCW_0x2e_1301_bit16 +26843545600000*XCW_0x2e_1301_bit17 +53687091200000*XCW_0x2e_1301_bit18 +107374182400000*XCW_0x2e_1301_bit19 +200000*XCW_0x2e_1401_bit_10 +400000*XCW_0x2e_1401_bit_9 +800000*XCW_0x2e_1401_bit_8 +1600000*XCW_0x2e_1401_bit_7 +3200000*XCW_0x2e_1401_bit_6 +6400000*XCW_0x2e_1401_bit_5 +12800000*XCW_0x2e_1401_bit_4 +25600000*XCW_0x2e_1401_bit_3 +51200000*XCW_0x2e_1401_bit_2 +102400000*XCW_0x2e_1401_bit_1 +204800000*XCW_0x2e_1401_bit0 +409600000*XCW_0x2e_1401_bit1 +819200000*XCW_0x2e_1401_bit2 +1638400000*XCW_0x2e_1401_bit3 +3276800000*XCW_0x2e_1401_bit4 +6553600000*XCW_0x2e_1401_bit5 +13107200000*XCW_0x2e_1401_bit6 +26214400000*XCW_0x2e_1401_bit7 +52428800000*XCW_0x2e_1401_bit8 +104857600000*XCW_0x2e_1401_bit9 +209715200000*XCW_0x2e_1401_bit10 +419430400000*XCW_0x2e_1401_bit11 +838860800000*XCW_0x2e_1401_bit12 +1677721600000*XCW_0x2e_1401_bit13 +3355443200000*XCW_0x2e_1401_bit14 +6710886400000*XCW_0x2e_1401_bit15 +13421772800000*XCW_0x2e_1401_bit16 +26843545600000*XCW_0x2e_1401_bit17 +53687091200000*XCW_0x2e_1401_bit18 +107374182400000*XCW_0x2e_1401_bit19 +200000*XCW_0x2e_1501_bit_10 +400000*XCW_0x2e_1501_bit_9 +800000*XCW_0x2e_1501_bit_8 +1600000*XCW_0x2e_1501_bit_7 +3200000*XCW_0x2e_1501_bit_6 +6400000*XCW_0x2e_1501_bit_5 +12800000*XCW_0x2e_1501_bit_4 +25600000*XCW_0x2e_1501_bit_3 +51200000*XCW_0x2e_1501_bit_2 +102400000*XCW_0x2e_1501_bit_1 +204800000*XCW_0x2e_1501_bit0 +409600000*XCW_0x2e_1501_bit1 +819200000*XCW_0x2e_1501_bit2 +1638400000*XCW_0x2e_1501_bit3 +3276800000*XCW_0x2e_1501_bit4 +6553600000*XCW_0x2e_1501_bit5 +13107200000*XCW_0x2e_1501_bit6 +26214400000*XCW_0x2e_1501_bit7 +52428800000*XCW_0x2e_1501_bit8 +104857600000*XCW_0x2e_1501_bit9 +209715200000*XCW_0x2e_1501_bit10 +419430400000*XCW_0x2e_1501_bit11 +838860800000*XCW_0x2e_1501_bit12 +1677721600000*XCW_0x2e_1501_bit13 +3355443200000*XCW_0x2e_1501_bit14 +6710886400000*XCW_0x2e_1501_bit15 +13421772800000*XCW_0x2e_1501_bit16 +26843545600000*XCW_0x2e_1501_bit17 +53687091200000*XCW_0x2e_1501_bit18 +107374182400000*XCW_0x2e_1501_bit19 +200000*XCW_0x2e_1601_bit_10 +400000*XCW_0x2e_1601_bit_9 +800000*XCW_0x2e_1601_bit_8 +1600000*XCW_0x2e_1601_bit_7 +3200000*XCW_0x2e_1601_bit_6 +6400000*XCW_0x2e_1601_bit_5 +12800000*XCW_0x2e_1601_bit_4 +25600000*XCW_0x2e_1601_bit_3 +51200000*XCW_0x2e_1601_bit_2 +102400000*XCW_0x2e_1601_bit_1 +204800000*XCW_0x2e_1601_bit0 +409600000*XCW_0x2e_1601_bit1 +819200000*XCW_0x2e_1601_bit2 +1638400000*XCW_0x2e_1601_bit3 +3276800000*XCW_0x2e_1601_bit4 +6553600000*XCW_0x2e_1601_bit5 +13107200000*XCW_0x2e_1601_bit6 +26214400000*XCW_0x2e_1601_bit7 +52428800000*XCW_0x2e_1601_bit8 +104857600000*XCW_0x2e_1601_bit9 +209715200000*XCW_0x2e_1601_bit10 +419430400000*XCW_0x2e_1601_bit11 +838860800000*XCW_0x2e_1601_bit12 +1677721600000*XCW_0x2e_1601_bit13 +3355443200000*XCW_0x2e_1601_bit14 +6710886400000*XCW_0x2e_1601_bit15 +13421772800000*XCW_0x2e_1601_bit16 +26843545600000*XCW_0x2e_1601_bit17 +53687091200000*XCW_0x2e_1601_bit18 +107374182400000*XCW_0x2e_1601_bit19 -26624000*XEE_0x2e_1201_bit0 -45056000*XEE_0x2e_1301_bit0 -30720000*XEE_0x2e_1401_bit0 -61440000*XEE_0x2e_1401_bit1 -122880000*XEE_0x2e_1401_bit2 -71680000*XEE_0x2e_1501_bit0 -143360000*XEE_0x2e_1501_bit1 -71680000*XEE_0x2e_1601_bit0 -143360000*XEE_0x2e_1601_bit1 -200000*XCIFMA01_bit_10 -400000*XCIFMA01_bit_9 -800000*XCIFMA01_bit_8 -1600000*XCIFMA01_bit_7 -3200000*XCIFMA01_bit_6 -6400000*XCIFMA01_bit_5 -12800000*XCIFMA01_bit_4 -25600000*XCIFMA01_bit_3 -51200000*XCIFMA01_bit_2 -102400000*XCIFMA01_bit_1 -204800000*XCIFMA01_bit0 -409600000*XCIFMA01_bit1 -819200000*XCIFMA01_bit2 -1638400000*XCIFMA01_bit3 -3276800000*XCIFMA01_bit4 -6553600000*XCIFMA01_bit5 -13107200000*XCIFMA01_bit6 -26214400000*XCIFMA01_bit7 -52428800000*XCIFMA01_bit8 -104857600000*XCIFMA01_bit9 -209715200000*XCIFMA01_bit10 -419430400000*XCIFMA01_bit11 -838860800000*XCIFMA01_bit12 -1677721600000*XCIFMA01_bit13 -3355443200000*XCIFMA01_bit14 -6710886400000*XCIFMA01_bit15 -13421772800000*XCIFMA01_bit16 -26843545600000*XCIFMA01_bit17 -53687091200000*XCIFMA01_bit18 -107374182400000*XCIFMA01_bit19 +192785*XCMI1_0x2e_01_bit_10 +385570*XCMI1_0x2e_01_bit_9 +771140*XCMI1_0x2e_01_bit_8 +1542280*XCMI1_0x2e_01_bit_7 +3084560*XCMI1_0x2e_01_bit_6 +6169120*XCMI1_0x2e_01_bit_5 +12338240*XCMI1_0x2e_01_bit_4 +24676480*XCMI1_0x2e_01_bit_3 +49352960*XCMI1_0x2e_01_bit_2 +98705920*XCMI1_0x2e_01_bit_1 +197411840*XCMI1_0x2e_01_bit0 +394823680*XCMI1_0x2e_01_bit1 +789647360*XCMI1_0x2e_01_bit2 +1579294720*XCMI1_0x2e_01_bit3 +3158589440*XCMI1_0x2e_01_bit4 +6317178880*XCMI1_0x2e_01_bit5 +12634357760*XCMI1_0x2e_01_bit6 +25268715520*XCMI1_0x2e_01_bit7 +50537431040*XCMI1_0x2e_01_bit8 +101074862080*XCMI1_0x2e_01_bit9 +202149724160*XCMI1_0x2e_01_bit10 +404299448320*XCMI1_0x2e_01_bit11 +808598896640*XCMI1_0x2e_01_bit12 +1617197793280*XCMI1_0x2e_01_bit13 +3234395586560*XCMI1_0x2e_01_bit14 +6468791173120*XCMI1_0x2e_01_bit15 +12937582346240*XCMI1_0x2e_01_bit16 +25875164692480*XCMI1_0x2e_01_bit17 +51750329384960*XCMI1_0x2e_01_bit18 +103500658769920*XCMI1_0x2e_01_bit19 +179741*XCMI2_0x2e_01_bit_10 +359482*XCMI2_0x2e_01_bit_9 +718964*XCMI2_0x2e_01_bit_8 +1437928*XCMI2_0x2e_01_bit_7 +2875856*XCMI2_0x2e_01_bit_6 +5751712*XCMI2_0x2e_01_bit_5 +11503424*XCMI2_0x2e_01_bit_4 +23006848*XCMI2_0x2e_01_bit_3 +46013696*XCMI2_0x2e_01_bit_2 +92027392*XCMI2_0x2e_01_bit_1 +184054784*XCMI2_0x2e_01_bit0 +368109568*XCMI2_0x2e_01_bit1 +736219136*XCMI2_0x2e_01_bit2 +1472438272*XCMI2_0x2e_01_bit3 +2944876544*XCMI2_0x2e_01_bit4 +5889753088*XCMI2_0x2e_01_bit5 +11779506176*XCMI2_0x2e_01_bit6 +23559012352*XCMI2_0x2e_01_bit7 +47118024704*XCMI2_0x2e_01_bit8 +94236049408*XCMI2_0x2e_01_bit9 +188472098816*XCMI2_0x2e_01_bit10 +376944197632*XCMI2_0x2e_01_bit11 +753888395264*XCMI2_0x2e_01_bit12 +1507776790528*XCMI2_0x2e_01_bit13 +3015553581056*XCMI2_0x2e_01_bit14 +6031107162112*XCMI2_0x2e_01_bit15 +12062214324224*XCMI2_0x2e_01_bit16 +24124428648448*XCMI2_0x2e_01_bit17 +48248857296896*XCMI2_0x2e_01_bit18 +96497714593792*XCMI2_0x2e_01_bit19 = +6076416000; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-gesa2_o.opb s UNKNOWN c Exit Code: 0 c Total time: 25.542 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.93 0.96 0.91 2/55 1007 Raw data (stat): 1007 (runsolver) R 1006 8378 8377 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 851689152 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.0012 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 1007 Raw data (stat): 1007 (bsolo_lpr_cuts-) R 1006 8378 8377 0 -1 0 1811 0 0 0 993 4 0 0 25 0 1 0 851689152 20213760 1731 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4935 1731 1111 63 0 4872 0 vsize: 19740 [startup+20.002 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 1007 Raw data (stat): 1007 (bsolo_lpr_cuts-) R 1006 8378 8377 0 -1 0 3874 0 0 0 1987 10 0 0 25 0 1 0 851689152 28725248 3794 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7013 3794 1111 63 0 6950 0 vsize: 28052 [startup+25.5916 s] Raw data (loadavg): 0.95 0.96 0.91 1/54 1007 Raw data (stat): 1007 (bsolo_lpr_cuts-) R 1006 8378 8377 0 -1 0 3874 0 0 0 1987 10 0 0 25 0 1 0 851689152 28725248 3794 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7013 3794 1111 63 0 6950 0 vsize: 0 Child status: 0 Real time (s): 25.5913 CPU time (s): 25.5671 CPU user time (s): 25.3182 CPU system time (s): 0.248962 CPU usage (%): 99.9056 Max. virtual memory (Kb): 28052 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####