Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-bore3d.opb |
MD5SUM | 2e72d5e95ef7d95d0e7b98fd7ceb407d |
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 | 1774 |
Biggest coefficient in the objective function | 17582255505408 |
Number of bits for the biggest coefficient in the objective function | 44 |
Sum of the numbers in the objective function | 115871619043950 |
Number of bits of the sum of numbers in the objective function | 47 |
Biggest number in a constraint | 17582255505408 |
Number of bits of the biggest number in a constraint | 44 |
Biggest sum of numbers in a constraint | 115871619043950 |
Number of bits of the biggest sum of numbers | 47 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.31995 |
Number of variables | 6214 |
Total number of constraints | 244 |
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 | 244 |
Minimum length of a constraint | 14 |
Maximum length of a constraint | 1460 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-24 02:14:43 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15590 boxname=wulflinc31 idbench=1200 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: 2e72d5e95ef7d95d0e7b98fd7ceb407d /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-bore3d.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-bore3d.opb IDLAUNCH: 15590 /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: 621776 kB Buffers: 26500 kB Cached: 365256 kB SwapCached: 1352 kB Active: 276752 kB Inactive: 117472 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 621524 kB SwapTotal: 2097892 kB SwapFree: 2095532 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5104 kB Slab: 12964 kB Committed_AS: 63860 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-24 02:14:44 (client local time) WITH STATUS 0 IN 0.620905 SECONDS stats: 15590 7 0.620905 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c ERROR Parsing file!!! c ERROR parsing line: -100000*M6H_0x2e_FPXI_bit_7 -200000*M6H_0x2e_FPXI_bit_6 -400000*M6H_0x2e_FPXI_bit_5 -800000*M6H_0x2e_FPXI_bit_4 -1600000*M6H_0x2e_FPXI_bit_3 -3200000*M6H_0x2e_FPXI_bit_2 -6400000*M6H_0x2e_FPXI_bit_1 -12800000*M6H_0x2e_FPXI_bit0 -25600000*M6H_0x2e_FPXI_bit1 -51200000*M6H_0x2e_FPXI_bit2 -102400000*M6H_0x2e_FPXI_bit3 -204800000*M6H_0x2e_FPXI_bit4 -409600000*M6H_0x2e_FPXI_bit5 -819200000*M6H_0x2e_FPXI_bit6 -1638400000*M6H_0x2e_FPXI_bit7 -3276800000*M6H_0x2e_FPXI_bit8 -6553600000*M6H_0x2e_FPXI_bit9 -13107200000*M6H_0x2e_FPXI_bit10 -26214400000*M6H_0x2e_FPXI_bit11 -52428800000*M6H_0x2e_FPXI_bit12 +370*PYN_0x2e_COXI_bit_7 +740*PYN_0x2e_COXI_bit_6 +1480*PYN_0x2e_COXI_bit_5 +2960*PYN_0x2e_COXI_bit_4 +5920*PYN_0x2e_COXI_bit_3 +11840*PYN_0x2e_COXI_bit_2 +23680*PYN_0x2e_COXI_bit_1 +47360*PYN_0x2e_COXI_bit0 +94720*PYN_0x2e_COXI_bit1 +189440*PYN_0x2e_COXI_bit2 +378880*PYN_0x2e_COXI_bit3 +757760*PYN_0x2e_COXI_bit4 +1515520*PYN_0x2e_COXI_bit5 +3031040*PYN_0x2e_COXI_bit6 +6062080*PYN_0x2e_COXI_bit7 +12124160*PYN_0x2e_COXI_bit8 +24248320*PYN_0x2e_COXI_bit9 +48496640*PYN_0x2e_COXI_bit10 +96993280*PYN_0x2e_COXI_bit11 +193986560*PYN_0x2e_COXI_bit12 +450*PYN_0x2e_CRXI_bit_7 +900*PYN_0x2e_CRXI_bit_6 +1800*PYN_0x2e_CRXI_bit_5 +3600*PYN_0x2e_CRXI_bit_4 +7200*PYN_0x2e_CRXI_bit_3 +14400*PYN_0x2e_CRXI_bit_2 +28800*PYN_0x2e_CRXI_bit_1 +57600*PYN_0x2e_CRXI_bit0 +115200*PYN_0x2e_CRXI_bit1 +230400*PYN_0x2e_CRXI_bit2 +460800*PYN_0x2e_CRXI_bit3 +921600*PYN_0x2e_CRXI_bit4 +1843200*PYN_0x2e_CRXI_bit5 +3686400*PYN_0x2e_CRXI_bit6 +7372800*PYN_0x2e_CRXI_bit7 +14745600*PYN_0x2e_CRXI_bit8 +29491200*PYN_0x2e_CRXI_bit9 +58982400*PYN_0x2e_CRXI_bit10 +117964800*PYN_0x2e_CRXI_bit11 +235929600*PYN_0x2e_CRXI_bit12 -100000*P6H_0x2e_HYXI_bit_7 -200000*P6H_0x2e_HYXI_bit_6 -400000*P6H_0x2e_HYXI_bit_5 -800000*P6H_0x2e_HYXI_bit_4 -1600000*P6H_0x2e_HYXI_bit_3 -3200000*P6H_0x2e_HYXI_bit_2 -6400000*P6H_0x2e_HYXI_bit_1 -12800000*P6H_0x2e_HYXI_bit0 -25600000*P6H_0x2e_HYXI_bit1 -51200000*P6H_0x2e_HYXI_bit2 -102400000*P6H_0x2e_HYXI_bit3 -204800000*P6H_0x2e_HYXI_bit4 -409600000*P6H_0x2e_HYXI_bit5 -819200000*P6H_0x2e_HYXI_bit6 -1638400000*P6H_0x2e_HYXI_bit7 -3276800000*P6H_0x2e_HYXI_bit8 -6553600000*P6H_0x2e_HYXI_bit9 -13107200000*P6H_0x2e_HYXI_bit10 -26214400000*P6H_0x2e_HYXI_bit11 -52428800000*P6H_0x2e_HYXI_bit12 +729*PIC_0x2e_M3XI_bit_7 +1458*PIC_0x2e_M3XI_bit_6 +2916*PIC_0x2e_M3XI_bit_5 +5832*PIC_0x2e_M3XI_bit_4 +11664*PIC_0x2e_M3XI_bit_3 +23328*PIC_0x2e_M3XI_bit_2 +46656*PIC_0x2e_M3XI_bit_1 +93312*PIC_0x2e_M3XI_bit0 +186624*PIC_0x2e_M3XI_bit1 +373248*PIC_0x2e_M3XI_bit2 +746496*PIC_0x2e_M3XI_bit3 +1492992*PIC_0x2e_M3XI_bit4 +2985984*PIC_0x2e_M3XI_bit5 +5971968*PIC_0x2e_M3XI_bit6 +11943936*PIC_0x2e_M3XI_bit7 +23887872*PIC_0x2e_M3XI_bit8 +47775744*PIC_0x2e_M3XI_bit9 +95551488*PIC_0x2e_M3XI_bit10 +191102976*PIC_0x2e_M3XI_bit11 +382205952*PIC_0x2e_M3XI_bit12 +112*PD1_0x2e_SHXI_bit_7 +224*PD1_0x2e_SHXI_bit_6 +448*PD1_0x2e_SHXI_bit_5 +896*PD1_0x2e_SHXI_bit_4 +1792*PD1_0x2e_SHXI_bit_3 +3584*PD1_0x2e_SHXI_bit_2 +7168*PD1_0x2e_SHXI_bit_1 +14336*PD1_0x2e_SHXI_bit0 +28672*PD1_0x2e_SHXI_bit1 +57344*PD1_0x2e_SHXI_bit2 +114688*PD1_0x2e_SHXI_bit3 +229376*PD1_0x2e_SHXI_bit4 +458752*PD1_0x2e_SHXI_bit5 +917504*PD1_0x2e_SHXI_bit6 +1835008*PD1_0x2e_SHXI_bit7 +3670016*PD1_0x2e_SHXI_bit8 +7340032*PD1_0x2e_SHXI_bit9 +14680064*PD1_0x2e_SHXI_bit10 +29360128*PD1_0x2e_SHXI_bit11 +58720256*PD1_0x2e_SHXI_bit12 +112*PH1_0x2e_SHXI_bit_7 +224*PH1_0x2e_SHXI_bit_6 +448*PH1_0x2e_SHXI_bit_5 +896*PH1_0x2e_SHXI_bit_4 +1792*PH1_0x2e_SHXI_bit_3 +3584*PH1_0x2e_SHXI_bit_2 +7168*PH1_0x2e_SHXI_bit_1 +14336*PH1_0x2e_SHXI_bit0 +28672*PH1_0x2e_SHXI_bit1 +57344*PH1_0x2e_SHXI_bit2 +114688*PH1_0x2e_SHXI_bit3 +229376*PH1_0x2e_SHXI_bit4 +458752*PH1_0x2e_SHXI_bit5 +917504*PH1_0x2e_SHXI_bit6 +1835008*PH1_0x2e_SHXI_bit7 +3670016*PH1_0x2e_SHXI_bit8 +7340032*PH1_0x2e_SHXI_bit9 +14680064*PH1_0x2e_SHXI_bit10 +29360128*PH1_0x2e_SHXI_bit11 +58720256*PH1_0x2e_SHXI_bit12 +112*PSS_0x2e_SHXI_bit_7 +224*PSS_0x2e_SHXI_bit_6 +448*PSS_0x2e_SHXI_bit_5 +896*PSS_0x2e_SHXI_bit_4 +1792*PSS_0x2e_SHXI_bit_3 +3584*PSS_0x2e_SHXI_bit_2 +7168*PSS_0x2e_SHXI_bit_1 +14336*PSS_0x2e_SHXI_bit0 +28672*PSS_0x2e_SHXI_bit1 +57344*PSS_0x2e_SHXI_bit2 +114688*PSS_0x2e_SHXI_bit3 +229376*PSS_0x2e_SHXI_bit4 +458752*PSS_0x2e_SHXI_bit5 +917504*PSS_0x2e_SHXI_bit6 +1835008*PSS_0x2e_SHXI_bit7 +3670016*PSS_0x2e_SHXI_bit8 +7340032*PSS_0x2e_SHXI_bit9 +14680064*PSS_0x2e_SHXI_bit10 +29360128*PSS_0x2e_SHXI_bit11 +58720256*PSS_0x2e_SHXI_bit12 = +0; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-bore3d.opb s UNKNOWN c Exit Code: 0 c Total time: 0.598 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.77 0.92 0.90 1/55 21532 Raw data (stat): 21532 (runsolver) R 21531 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 826537049 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 0 1 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+0.65333 s] Raw data (loadavg): 0.77 0.92 0.90 1/54 21532 Raw data (stat): 21532 (runsolver) R 21531 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 826537049 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 0 1 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 0 Child status: 0 Real time (s): 0.652756 CPU time (s): 0.620905 CPU user time (s): 0.569913 CPU system time (s): 0.050992 CPU usage (%): 95.1205 Max. virtual memory (Kb): 1032 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####