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 wulflinc31 THE 2005-05-24 15:39:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13406 boxname=wulflinc31 idbench=1032 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: 70d38efa2ca4db2a9200144005e211ed /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-gesa2_o.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-gesa2_o.opb IDLAUNCH: 13406 /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: 479936 kB Buffers: 33876 kB Cached: 499424 kB SwapCached: 1248 kB Active: 190268 kB Inactive: 345560 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 479684 kB SwapTotal: 2097892 kB SwapFree: 2096040 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5432 kB Slab: 13244 kB Committed_AS: 63808 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-24 15:40:17 (client local time) WITH STATUS 0 IN 23.0755 SECONDS stats: 13406 7 23.0755 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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/wulflinc31/normalized-mps-v2-20-10-gesa2_o.opb s UNKNOWN c Exit Code: 0 c Total time: 23.049 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 Raw data (loadavg): 0.68 0.88 0.88 2/55 30882 Raw data (stat): 30882 (runsolver) R 30881 29618 29617 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 831368663 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 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.0003 s] Raw data (loadavg): 0.73 0.89 0.88 2/55 30882 Raw data (stat): 30882 (bsolo_mis) R 30881 29618 29617 0 -1 0 2043 0 0 0 994 4 0 0 25 0 1 0 831368663 21807104 2021 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5324 2021 1111 63 0 5261 0 vsize: 21296 [startup+20.001 s] Raw data (loadavg): 0.77 0.89 0.88 2/55 30882 Raw data (stat): 30882 (bsolo_mis) R 30881 29618 29617 0 -1 0 4535 0 0 0 1989 9 0 0 25 0 1 0 831368663 32034816 4513 4294967295 134512640 134714540 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7821 4513 1111 63 0 7758 0 vsize: 31284 [startup+23.0846 s] Raw data (loadavg): 0.77 0.89 0.88 1/54 30882 Raw data (stat): 30882 (bsolo_mis) R 30881 29618 29617 0 -1 0 4535 0 0 0 1989 9 0 0 25 0 1 0 831368663 32034816 4513 4294967295 134512640 134714540 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7821 4513 1111 63 0 7758 0 vsize: 0 Child status: 0 Real time (s): 23.0839 CPU time (s): 23.0755 CPU user time (s): 22.8505 CPU system time (s): 0.224965 CPU usage (%): 99.9634 Max. virtual memory (Kb): 31284 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####