Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos13.opb |
MD5SUM | cf076aa1d04c57dc685f8035f0968734 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -1358524 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 103558656 |
Number of bits for the biggest coefficient in the objective function | 27 |
Sum of the numbers in the objective function | 2282563635 |
Number of bits of the sum of numbers in the objective function | 32 |
Biggest number in a constraint | 69966336000 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 636991772142 |
Number of bits of the biggest sum of numbers | 40 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 517.452 |
Number of variables | 1935 |
Total number of constraints | 22679 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 1816 |
Number of constraints which are nor clauses,nor cardinality constraints | 20863 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1815 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc18 THE 2005-05-25 00:27:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14550 boxname=wulflinc18 idbench=1120 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: cf076aa1d04c57dc685f8035f0968734 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-neos13.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-neos13.opb IDLAUNCH: 14550 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 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: 748848 kB Buffers: 18964 kB Cached: 245128 kB SwapCached: 836 kB Active: 81040 kB Inactive: 185580 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 748596 kB SwapTotal: 2097892 kB SwapFree: 2096620 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5660 kB Slab: 13512 kB Committed_AS: 63588 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 00:27:12 (client local time) WITH STATUS 0 IN 0.089986 SECONDS stats: 14550 7 0.089986 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c ERROR Parsing file!!! c ERROR parsing line: -41605800*x10_bit_10 -83211600*x10_bit_9 -166423200*x10_bit_8 -332846400*x10_bit_7 -665692800*x10_bit_6 -1331385600*x10_bit_5 -2662771200*x10_bit_4 -5325542400*x10_bit_3 -10651084800*x10_bit_2 -21302169600*x10_bit_1 +44444600*x11_bit_10 +88889200*x11_bit_9 +177778400*x11_bit_8 +355556800*x11_bit_7 +711113600*x11_bit_6 +1422227200*x11_bit_5 +2844454400*x11_bit_4 +5688908800*x11_bit_3 +11377817600*x11_bit_2 +22755635200*x11_bit_1 +101506000*x12_bit_10 +203012000*x12_bit_9 +406024000*x12_bit_8 +812048000*x12_bit_7 +1624096000*x12_bit_6 +3248192000*x12_bit_5 +6496384000*x12_bit_4 +12992768000*x12_bit_3 +25985536000*x12_bit_2 +51971072000*x12_bit_1 +27933200*x1_bit_10 +55866400*x1_bit_9 +111732800*x1_bit_8 +223465600*x1_bit_7 +446931200*x1_bit_6 +893862400*x1_bit_5 +1787724800*x1_bit_4 +3575449600*x1_bit_3 +7150899200*x1_bit_2 +14301798400*x1_bit_1 -52829700*x2_bit_10 -105659400*x2_bit_9 -211318800*x2_bit_8 -422637600*x2_bit_7 -845275200*x2_bit_6 -1690550400*x2_bit_5 -3381100800*x2_bit_4 -6762201600*x2_bit_3 -13524403200*x2_bit_2 -27048806400*x2_bit_1 +13607400*x3_bit_10 +27214800*x3_bit_9 +54429600*x3_bit_8 +108859200*x3_bit_7 +217718400*x3_bit_6 +435436800*x3_bit_5 +870873600*x3_bit_4 +1741747200*x3_bit_3 +3483494400*x3_bit_2 +6966988800*x3_bit_1 +83381200*x4_bit_10 +166762400*x4_bit_9 +333524800*x4_bit_8 +667049600*x4_bit_7 +1334099200*x4_bit_6 +2668198400*x4_bit_5 +5336396800*x4_bit_4 +10672793600*x4_bit_3 +21345587200*x4_bit_2 +42691174400*x4_bit_1 +173721*x5_bit_10 +347442*x5_bit_9 +694884*x5_bit_8 +1389768*x5_bit_7 +2779536*x5_bit_6 +5559072*x5_bit_5 +11118144*x5_bit_4 +22236288*x5_bit_3 +44472576*x5_bit_2 +88945152*x5_bit_1 -71966800*x6_bit_10 -143933600*x6_bit_9 -287867200*x6_bit_8 -575734400*x6_bit_7 -1151468800*x6_bit_6 -2302937600*x6_bit_5 -4605875200*x6_bit_4 -9211750400*x6_bit_3 -18423500800*x6_bit_2 -36847001600*x6_bit_1 +44444600*x7_bit_10 +88889200*x7_bit_9 +177778400*x7_bit_8 +355556800*x7_bit_7 +711113600*x7_bit_6 +1422227200*x7_bit_5 +2844454400*x7_bit_4 +5688908800*x7_bit_3 +11377817600*x7_bit_2 +22755635200*x7_bit_1 +85907300*x8_bit_10 +171814600*x8_bit_9 +343629200*x8_bit_8 +687258400*x8_bit_7 +1374516800*x8_bit_6 +2749033600*x8_bit_5 +5498067200*x8_bit_4 +10996134400*x8_bit_3 +21992268800*x8_bit_2 +43984537600*x8_bit_1 +29560000*x9_bit_10 +59120000*x9_bit_9 +118240000*x9_bit_8 +236480000*x9_bit_7 +472960000*x9_bit_6 +945920000*x9_bit_5 +1891840000*x9_bit_4 +3783680000*x9_bit_3 +7567360000*x9_bit_2 +15134720000*x9_bit_1 >= +0; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-neos13.opb s UNKNOWN c Exit Code: 0 c Total time: 0.08 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.94 0.96 0.91 2/54 27703 Raw data (stat): 27703 (runsolver) R 27702 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834538410 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.243133 s] Raw data (loadavg): 0.94 0.96 0.91 1/53 27703 Raw data (stat): 27703 (runsolver) R 27702 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834538410 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.242857 CPU time (s): 0.089986 CPU user time (s): 0.076988 CPU system time (s): 0.012998 CPU usage (%): 37.0531 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####