Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scfxm1.opb |
MD5SUM | 9724b70be00612c57ff3bed741e4e1b9 |
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 | 460 |
Biggest coefficient in the objective function | 5242880 |
Number of bits for the biggest coefficient in the objective function | 23 |
Sum of the numbers in the objective function | 137363325 |
Number of bits of the sum of numbers in the objective function | 28 |
Biggest number in a constraint | 52428800000 |
Number of bits of the biggest number in a constraint | 36 |
Biggest sum of numbers in a constraint | 319170501375 |
Number of bits of the biggest sum of numbers | 39 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.357944 |
Number of variables | 9140 |
Total number of constraints | 330 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 330 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 1140 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-06-09 11:39:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29463 boxname=wulflinc6 idbench=1247 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: 9724b70be00612c57ff3bed741e4e1b9 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-scfxm1.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-scfxm1.opb IDLAUNCH: 29463 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 440692 kB Buffers: 27140 kB Cached: 545236 kB SwapCached: 932 kB Active: 33216 kB Inactive: 541244 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 440440 kB SwapTotal: 2097136 kB SwapFree: 2095216 kB Dirty: 4 kB Writeback: 0 kB Mapped: 4996 kB Slab: 13808 kB Committed_AS: 63736 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 11:39:47 (client local time) WITH STATUS 0 IN 0.081986 SECONDS stats: 29463 7 0.081986 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c ERROR Parsing file!!! c ERROR parsing line: +50000*V1DC2P_bit_7 +100000*V1DC2P_bit_6 +200000*V1DC2P_bit_5 +400000*V1DC2P_bit_4 +800000*V1DC2P_bit_3 +1600000*V1DC2P_bit_2 +3200000*V1DC2P_bit_1 +6400000*V1DC2P_bit0 +12800000*V1DC2P_bit1 +25600000*V1DC2P_bit2 +51200000*V1DC2P_bit3 +102400000*V1DC2P_bit4 +204800000*V1DC2P_bit5 +409600000*V1DC2P_bit6 +819200000*V1DC2P_bit7 +1638400000*V1DC2P_bit8 +3276800000*V1DC2P_bit9 +6553600000*V1DC2P_bit10 +13107200000*V1DC2P_bit11 +26214400000*V1DC2P_bit12 -1050*V1DC65_bit_7 -2100*V1DC65_bit_6 -4200*V1DC65_bit_5 -8400*V1DC65_bit_4 -16800*V1DC65_bit_3 -33600*V1DC65_bit_2 -67200*V1DC65_bit_1 -134400*V1DC65_bit0 -268800*V1DC65_bit1 -537600*V1DC65_bit2 -1075200*V1DC65_bit3 -2150400*V1DC65_bit4 -4300800*V1DC65_bit5 -8601600*V1DC65_bit6 -17203200*V1DC65_bit7 -34406400*V1DC65_bit8 -68812800*V1DC65_bit9 -137625600*V1DC65_bit10 -275251200*V1DC65_bit11 -550502400*V1DC65_bit12 -1500*V1DC75_bit_7 -3000*V1DC75_bit_6 -6000*V1DC75_bit_5 -12000*V1DC75_bit_4 -24000*V1DC75_bit_3 -48000*V1DC75_bit_2 -96000*V1DC75_bit_1 -192000*V1DC75_bit0 -384000*V1DC75_bit1 -768000*V1DC75_bit2 -1536000*V1DC75_bit3 -3072000*V1DC75_bit4 -6144000*V1DC75_bit5 -12288000*V1DC75_bit6 -24576000*V1DC75_bit7 -49152000*V1DC75_bit8 -98304000*V1DC75_bit9 -196608000*V1DC75_bit10 -393216000*V1DC75_bit11 -786432000*V1DC75_bit12 -750*V1DFVB_bit_7 -1500*V1DFVB_bit_6 -3000*V1DFVB_bit_5 -6000*V1DFVB_bit_4 -12000*V1DFVB_bit_3 -24000*V1DFVB_bit_2 -48000*V1DFVB_bit_1 -96000*V1DFVB_bit0 -192000*V1DFVB_bit1 -384000*V1DFVB_bit2 -768000*V1DFVB_bit3 -1536000*V1DFVB_bit4 -3072000*V1DFVB_bit5 -6144000*V1DFVB_bit6 -12288000*V1DFVB_bit7 -24576000*V1DFVB_bit8 -49152000*V1DFVB_bit9 -98304000*V1DFVB_bit10 -196608000*V1DFVB_bit11 -393216000*V1DFVB_bit12 -1690*V1DI4R_bit_7 -3380*V1DI4R_bit_6 -6760*V1DI4R_bit_5 -13520*V1DI4R_bit_4 -27040*V1DI4R_bit_3 -54080*V1DI4R_bit_2 -108160*V1DI4R_bit_1 -216320*V1DI4R_bit0 -432640*V1DI4R_bit1 -865280*V1DI4R_bit2 -1730560*V1DI4R_bit3 -3461120*V1DI4R_bit4 -6922240*V1DI4R_bit5 -13844480*V1DI4R_bit6 -27688960*V1DI4R_bit7 -55377920*V1DI4R_bit8 -110755840*V1DI4R_bit9 -221511680*V1DI4R_bit10 -443023360*V1DI4R_bit11 -886046720*V1DI4R_bit12 -1570*V1DN4R_bit_7 -3140*V1DN4R_bit_6 -6280*V1DN4R_bit_5 -12560*V1DN4R_bit_4 -25120*V1DN4R_bit_3 -50240*V1DN4R_bit_2 -100480*V1DN4R_bit_1 -200960*V1DN4R_bit0 -401920*V1DN4R_bit1 -803840*V1DN4R_bit2 -1607680*V1DN4R_bit3 -3215360*V1DN4R_bit4 -6430720*V1DN4R_bit5 -12861440*V1DN4R_bit6 -25722880*V1DN4R_bit7 -51445760*V1DN4R_bit8 -102891520*V1DN4R_bit9 -205783040*V1DN4R_bit10 -411566080*V1DN4R_bit11 -823132160*V1DN4R_bit12 -5900*V1DO3R_bit_7 -11800*V1DO3R_bit_6 -23600*V1DO3R_bit_5 -47200*V1DO3R_bit_4 -94400*V1DO3R_bit_3 -188800*V1DO3R_bit_2 -377600*V1DO3R_bit_1 -755200*V1DO3R_bit0 -1510400*V1DO3R_bit1 -3020800*V1DO3R_bit2 -6041600*V1DO3R_bit3 -12083200*V1DO3R_bit4 -24166400*V1DO3R_bit5 -48332800*V1DO3R_bit6 -96665600*V1DO3R_bit7 -193331200*V1DO3R_bit8 -386662400*V1DO3R_bit9 -773324800*V1DO3R_bit10 -1546649600*V1DO3R_bit11 -3093299200*V1DO3R_bit12 -2075*V1DP94_bit_7 -4150*V1DP94_bit_6 -8300*V1DP94_bit_5 -16600*V1DP94_bit_4 -33200*V1DP94_bit_3 -66400*V1DP94_bit_2 -132800*V1DP94_bit_1 -265600*V1DP94_bit0 -531200*V1DP94_bit1 -1062400*V1DP94_bit2 -2124800*V1DP94_bit3 -4249600*V1DP94_bit4 -8499200*V1DP94_bit5 -16998400*V1DP94_bit6 -33996800*V1DP94_bit7 -67993600*V1DP94_bit8 -135987200*V1DP94_bit9 -271974400*V1DP94_bit10 -543948800*V1DP94_bit11 -1087897600*V1DP94_bit12 -1660*V1DR94_bit_7 -3320*V1DR94_bit_6 -6640*V1DR94_bit_5 -13280*V1DR94_bit_4 -26560*V1DR94_bit_3 -53120*V1DR94_bit_2 -106240*V1DR94_bit_1 -212480*V1DR94_bit0 -424960*V1DR94_bit1 -849920*V1DR94_bit2 -1699840*V1DR94_bit3 -3399680*V1DR94_bit4 -6799360*V1DR94_bit5 -13598720*V1DR94_bit6 -27197440*V1DR94_bit7 -54394880*V1DR94_bit8 -108789760*V1DR94_bit9 -217579520*V1DR94_bit10 -435159040*V1DR94_bit11 -870318080*V1DR94_bit12 -544*V1DRBT_bit_7 -1088*V1DRBT_bit_6 -2176*V1DRBT_bit_5 -4352*V1DRBT_bit_4 -8704*V1DRBT_bit_3 -17408*V1DRBT_bit_2 -34816*V1DRBT_bit_1 -69632*V1DRBT_bit0 -139264*V1DRBT_bit1 -278528*V1DRBT_bit2 -557056*V1DRBT_bit3 -1114112*V1DRBT_bit4 -2228224*V1DRBT_bit5 -4456448*V1DRBT_bit6 -8912896*V1DRBT_bit7 -17825792*V1DRBT_bit8 -35651584*V1DRBT_bit9 -71303168*V1DRBT_bit10 -142606336*V1DRBT_bit11 -285212672*V1DRBT_bit12 -1856*V1DSCO_bit_7 -3712*V1DSCO_bit_6 -7424*V1DSCO_bit_5 -14848*V1DSCO_bit_4 -29696*V1DSCO_bit_3 -59392*V1DSCO_bit_2 -118784*V1DSCO_bit_1 -237568*V1DSCO_bit0 -475136*V1DSCO_bit1 -950272*V1DSCO_bit2 -1900544*V1DSCO_bit3 -3801088*V1DSCO_bit4 -7602176*V1DSCO_bit5 -15204352*V1DSCO_bit6 -30408704*V1DSCO_bit7 -60817408*V1DSCO_bit8 -121634816*V1DSCO_bit9 -243269632*V1DSCO_bit10 -486539264*V1DSCO_bit11 -973078528*V1DSCO_bit12 -928*V1DSVB_bit_7 -1856*V1DSVB_bit_6 -3712*V1DSVB_bit_5 -7424*V1DSVB_bit_4 -14848*V1DSVB_bit_3 -29696*V1DSVB_bit_2 -59392*V1DSVB_bit_1 -118784*V1DSVB_bit0 -237568*V1DSVB_bit1 -475136*V1DSVB_bit2 -950272*V1DSVB_bit3 -1900544*V1DSVB_bit4 -3801088*V1DSVB_bit5 -7602176*V1DSVB_bit6 -15204352*V1DSVB_bit7 -30408704*V1DSVB_bit8 -60817408*V1DSVB_bit9 -121634816*V1DSVB_bit10 -243269632*V1DSVB_bit11 -486539264*V1DSVB_bit12 -544*V1DV6I_bit_7 -1088*V1DV6I_bit_6 -2176*V1DV6I_bit_5 -4352*V1DV6I_bit_4 -8704*V1DV6I_bit_3 -17408*V1DV6I_bit_2 -34816*V1DV6I_bit_1 -69632*V1DV6I_bit0 -139264*V1DV6I_bit1 -278528*V1DV6I_bit2 -557056*V1DV6I_bit3 -1114112*V1DV6I_bit4 -2228224*V1DV6I_bit5 -4456448*V1DV6I_bit6 -8912896*V1DV6I_bit7 -17825792*V1DV6I_bit8 -35651584*V1DV6I_bit9 -71303168*V1DV6I_bit10 -142606336*V1DV6I_bit11 -285212672*V1DV6I_bit12 -672*V1DV6Y_bit_7 -1344*V1DV6Y_bit_6 -2688*V1DV6Y_bit_5 -5376*V1DV6Y_bit_4 -10752*V1DV6Y_bit_3 -21504*V1DV6Y_bit_2 -43008*V1DV6Y_bit_1 -86016*V1DV6Y_bit0 -172032*V1DV6Y_bit1 -344064*V1DV6Y_bit2 -688128*V1DV6Y_bit3 -1376256*V1DV6Y_bit4 -2752512*V1DV6Y_bit5 -5505024*V1DV6Y_bit6 -11010048*V1DV6Y_bit7 -22020096*V1DV6Y_bit8 -44040192*V1DV6Y_bit9 -88080384*V1DV6Y_bit10 -176160768*V1DV6Y_bit11 -352321536*V1DV6Y_bit12 -6750*V1DYCO_bit_7 -13500*V1DYCO_bit_6 -27000*V1DYCO_bit_5 -54000*V1DYCO_bit_4 -108000*V1DYCO_bit_3 -216000*V1DYCO_bit_2 -432000*V1DYCO_bit_1 -864000*V1DYCO_bit0 -1728000*V1DYCO_bit1 -3456000*V1DYCO_bit2 -6912000*V1DYCO_bit3 -13824000*V1DYCO_bit4 -27648000*V1DYCO_bit5 -55296000*V1DYCO_bit6 -110592000*V1DYCO_bit7 -221184000*V1DYCO_bit8 -442368000*V1DYCO_bit9 -884736000*V1DYCO_bit10 -1769472000*V1DYCO_bit11 -3538944000*V1DYCO_bit12 = +0; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-scfxm1.opb s UNKNOWN c Exit Code: 0 c Total time: 0.07 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.82 0.93 0.90 2/54 11273 Raw data (stat): 11273 (runsolver) R 11272 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 909983674 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+0.10038 s] Raw data (loadavg): 0.82 0.93 0.90 1/53 11273 Raw data (stat): 11273 (runsolver) R 11272 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 909983674 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: 0 Child status: 0 Real time (s): 0.100075 CPU time (s): 0.081986 CPU user time (s): 0.05999 CPU system time (s): 0.021996 CPU usage (%): 81.9246 Max. virtual memory (Kb): 864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####