Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-arki001.opb |
MD5SUM | de7a38ae8a44ed9d515fc386211a643d |
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 | 31 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 2386602666496000 |
Number of bits of the biggest number in a constraint | 52 |
Biggest sum of numbers in a constraint | 5223634990318712 |
Number of bits of the biggest sum of numbers | 53 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.58391 |
Number of variables | 8268 |
Total number of constraints | 2018 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 436 |
Number of constraints which are nor clauses,nor cardinality constraints | 1582 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 8249 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc9 THE 2005-05-24 16:19:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12457 boxname=wulflinc9 idbench=959 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: de7a38ae8a44ed9d515fc386211a643d /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-arki001.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-arki001.opb IDLAUNCH: 12457 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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.242 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: 637864 kB Buffers: 2564 kB Cached: 372844 kB SwapCached: 88 kB Active: 42588 kB Inactive: 335748 kB HighTotal: 131008 kB HighFree: 20524 kB LowTotal: 903652 kB LowFree: 617340 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 48 kB Writeback: 0 kB Mapped: 6888 kB Slab: 12684 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-24 16:19:21 (client local time) WITH STATUS 0 IN 0.6499 SECONDS stats: 12457 7 0.6499 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c ERROR Parsing file!!! c ERROR parsing line: +1694439*x11_bit_10 +3388878*x11_bit_9 +6777756*x11_bit_8 +13555512*x11_bit_7 +27111024*x11_bit_6 +54222048*x11_bit_5 +108444096*x11_bit_4 +216888192*x11_bit_3 +433776384*x11_bit_2 +867552768*x11_bit_1 +1735105536*x11_bit0 +3470211072*x11_bit1 +1048454139*x25_bit_10 +2096908278*x25_bit_9 +4193816556*x25_bit_8 +8387633112*x25_bit_7 +16775266224*x25_bit_6 +33550532448*x25_bit_5 +67101064896*x25_bit_4 +134202129792*x25_bit_3 +268404259584*x25_bit_2 +536808519168*x25_bit_1 +1073617038336*x25_bit0 +2147234076672*x25_bit1 +4294468153344*x25_bit2 +1016855589*x37_bit_10 +2033711178*x37_bit_9 +4067422356*x37_bit_8 +8134844712*x37_bit_7 +16269689424*x37_bit_6 +32539378848*x37_bit_5 +65078757696*x37_bit_4 +130157515392*x37_bit_3 +260315030784*x37_bit_2 +520630061568*x37_bit_1 +1041260123136*x37_bit0 +2082520246272*x37_bit1 +4165040492544*x37_bit2 +8330080985088*x37_bit3 +16660161970176*x37_bit4 +1078627190*x68_bit_10 +2157254380*x68_bit_9 +4314508760*x68_bit_8 +8629017520*x68_bit_7 +17258035040*x68_bit_6 +34516070080*x68_bit_5 +69032140160*x68_bit_4 +138064280320*x68_bit_3 +276128560640*x68_bit_2 +552257121280*x68_bit_1 +1104514242560*x68_bit0 +2209028485120*x68_bit1 +4418056970240*x68_bit2 +8836113940480*x68_bit3 +17672227880960*x68_bit4 +947362538*x87_bit_10 +1894725076*x87_bit_9 +3789450152*x87_bit_8 +7578900304*x87_bit_7 +15157800608*x87_bit_6 +30315601216*x87_bit_5 +60631202432*x87_bit_4 +121262404864*x87_bit_3 +242524809728*x87_bit_2 +485049619456*x87_bit_1 +970099238912*x87_bit0 +1940198477824*x87_bit1 +3880396955648*x87_bit2 +7760793911296*x87_bit3 +15521587822592*x87_bit4 +3648942598*x149_bit_10 +7297885196*x149_bit_9 +14595770392*x149_bit_8 +29191540784*x149_bit_7 +58383081568*x149_bit_6 +116766163136*x149_bit_5 +233532326272*x149_bit_4 +467064652544*x149_bit_3 +934129305088*x149_bit_2 +1868258610176*x149_bit_1 +3736517220352*x149_bit0 +7473034440704*x149_bit1 +14946068881408*x149_bit2 +29892137762816*x149_bit3 +765611480*x168_bit_10 +1531222960*x168_bit_9 +3062445920*x168_bit_8 +6124891840*x168_bit_7 +12249783680*x168_bit_6 +24499567360*x168_bit_5 +48999134720*x168_bit_4 +97998269440*x168_bit_3 +195996538880*x168_bit_2 +391993077760*x168_bit_1 +783986155520*x168_bit0 +1567972311040*x168_bit1 +3135944622080*x168_bit2 +6271889244160*x168_bit3 +12543778488320*x168_bit4 +1191300967*x190_bit_10 +2382601934*x190_bit_9 +4765203868*x190_bit_8 +9530407736*x190_bit_7 +19060815472*x190_bit_6 +38121630944*x190_bit_5 +76243261888*x190_bit_4 +152486523776*x190_bit_3 +304973047552*x190_bit_2 +609946095104*x190_bit_1 +1219892190208*x190_bit0 +2439784380416*x190_bit1 +4879568760832*x190_bit2 +839262236*x224_bit_10 +1678524472*x224_bit_9 +3357048944*x224_bit_8 +6714097888*x224_bit_7 +13428195776*x224_bit_6 +26856391552*x224_bit_5 +53712783104*x224_bit_4 +107425566208*x224_bit_3 +214851132416*x224_bit_2 +429702264832*x224_bit_1 +859404529664*x224_bit0 +1718809059328*x224_bit1 +3437618118656*x224_bit2 +6875236237312*x224_bit3 +13750472474624*x224_bit4 +875493656*x233_bit_10 +1750987312*x233_bit_9 +3501974624*x233_bit_8 +7003949248*x233_bit_7 +14007898496*x233_bit_6 +28015796992*x233_bit_5 +56031593984*x233_bit_4 +112063187968*x233_bit_3 +224126375936*x233_bit_2 +448252751872*x233_bit_1 +896505503744*x233_bit0 +1793011007488*x233_bit1 +3586022014976*x233_bit2 +728700906*x250_bit_10 +1457401812*x250_bit_9 +2914803624*x250_bit_8 +5829607248*x250_bit_7 +11659214496*x250_bit_6 +23318428992*x250_bit_5 +46636857984*x250_bit_4 +93273715968*x250_bit_3 +186547431936*x250_bit_2 +373094863872*x250_bit_1 +746189727744*x250_bit0 +1492379455488*x250_bit1 +3638294864*x271_bit_10 +7276589728*x271_bit_9 +14553179456*x271_bit_8 +29106358912*x271_bit_7 +58212717824*x271_bit_6 +116425435648*x271_bit_5 +232850871296*x271_bit_4 +465701742592*x271_bit_3 +931403485184*x271_bit_2 +1862806970368*x271_bit_1 +3725613940736*x271_bit0 +7451227881472*x271_bit1 +14902455762944*x271_bit2 +29804911525888*x271_bit3 +4188986103*x309_bit_10 +8377972206*x309_bit_9 +16755944412*x309_bit_8 +33511888824*x309_bit_7 +67023777648*x309_bit_6 +134047555296*x309_bit_5 +268095110592*x309_bit_4 +536190221184*x309_bit_3 +1072380442368*x309_bit_2 +2144760884736*x309_bit_1 +4289521769472*x309_bit0 +8579043538944*x309_bit1 +17158087077888*x309_bit2 +34316174155776*x309_bit3 +68632348311552*x309_bit4 +3965981873*x328_bit_10 +7931963746*x328_bit_9 +15863927492*x328_bit_8 +31727854984*x328_bit_7 +63455709968*x328_bit_6 +126911419936*x328_bit_5 +253822839872*x328_bit_4 +507645679744*x328_bit_3 +1015291359488*x328_bit_2 +2030582718976*x328_bit_1 +4061165437952*x328_bit0 +8122330875904*x328_bit1 +4084064048*x347_bit_10 +8168128096*x347_bit_9 +16336256192*x347_bit_8 +32672512384*x347_bit_7 +65345024768*x347_bit_6 +130690049536*x347_bit_5 +261380099072*x347_bit_4 +522760198144*x347_bit_3 +1045520396288*x347_bit_2 +2091040792576*x347_bit_1 +4182081585152*x347_bit0 +8364163170304*x347_bit1 +16728326340608*x347_bit2 +33456652681216*x347_bit3 +66913305362432*x347_bit4 +720398792*x399_bit_10 +1440797584*x399_bit_9 +2881595168*x399_bit_8 +5763190336*x399_bit_7 +11526380672*x399_bit_6 +23052761344*x399_bit_5 +46105522688*x399_bit_4 +92211045376*x399_bit_3 +184422090752*x399_bit_2 +368844181504*x399_bit_1 +737688363008*x399_bit0 +1475376726016*x399_bit1 +2950753452032*x399_bit2 +5901506904064*x399_bit3 +536808518656*x875_bit0 +520630062080*x887_bit0 +552257121280*x918_bit0 +485049619456*x937_bit0 +1868258610176*x999_bit0 +391993077760*x1018_bit0 +609946094592*x1040_bit0 +429702264832*x1074_bit0 +448252751872*x1083_bit0 +373094863872*x1100_bit0 +1862806970368*x1121_bit0 +2144760884224*x1159_bit0 +2030582719488*x1178_bit0 +2091040792576*x1197_bit0 +729854976*x1216_bit0 +3885855744*x1235_bit0 +368844181504*x1249_bit0 +1201280881664*x1341_bit0 +2402561763328*x1341_bit1 +274778328064*x1368_bit0 +293003421696*x1381_bit0 >= +84470066679808; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-arki001.opb s UNKNOWN c Exit Code: 0 c Total time: 0.626 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.78 0.92 0.97 2/54 6297 Raw data (stat): 6297 (runsolver) R 6296 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 773402495 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+0.656764 s] Raw data (loadavg): 0.78 0.92 0.97 1/53 6297 Raw data (stat): 6297 (runsolver) R 6296 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 773402495 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 0 Child status: 0 Real time (s): 0.656456 CPU time (s): 0.6499 CPU user time (s): 0.463929 CPU system time (s): 0.185971 CPU usage (%): 99.0013 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####