Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-bnl2.opb |
MD5SUM | 25ba81ffd6b61270ad99e5bd6f700914 |
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 | 33700 |
Biggest coefficient in the objective function | 314887372800 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 11048951166825 |
Number of bits of the sum of numbers in the objective function | 44 |
Biggest number in a constraint | 314887372800 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 11048951166825 |
Number of bits of the biggest sum of numbers | 44 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.632903 |
Number of variables | 69780 |
Total number of constraints | 2280 |
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 | 2280 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 1640 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-06-09 10:55:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29413 boxname=wulflinc5 idbench=1197 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: 25ba81ffd6b61270ad99e5bd6f700914 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-bnl2.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-bnl2.opb IDLAUNCH: 29413 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 611608 kB Buffers: 21632 kB Cached: 379516 kB SwapCached: 664 kB Active: 31892 kB Inactive: 371324 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 611356 kB SwapTotal: 2097136 kB SwapFree: 2095460 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5072 kB Slab: 14080 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 10:58:43 (client local time) WITH STATUS 0 IN 207.407 SECONDS stats: 29413 7 207.407 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c ERROR Parsing file!!! c ERROR parsing line: -3053*X1001001_bit_7 -6106*X1001001_bit_6 -12212*X1001001_bit_5 -24424*X1001001_bit_4 -48848*X1001001_bit_3 -97696*X1001001_bit_2 -195392*X1001001_bit_1 -390784*X1001001_bit0 -781568*X1001001_bit1 -1563136*X1001001_bit2 -3126272*X1001001_bit3 -6252544*X1001001_bit4 -12505088*X1001001_bit5 -25010176*X1001001_bit6 -50020352*X1001001_bit7 -100040704*X1001001_bit8 -200081408*X1001001_bit9 -400162816*X1001001_bit10 -800325632*X1001001_bit11 -1600651264*X1001001_bit12 -4884*X1001002_bit_7 -9768*X1001002_bit_6 -19536*X1001002_bit_5 -39072*X1001002_bit_4 -78144*X1001002_bit_3 -156288*X1001002_bit_2 -312576*X1001002_bit_1 -625152*X1001002_bit0 -1250304*X1001002_bit1 -2500608*X1001002_bit2 -5001216*X1001002_bit3 -10002432*X1001002_bit4 -20004864*X1001002_bit5 -40009728*X1001002_bit6 -80019456*X1001002_bit7 -160038912*X1001002_bit8 -320077824*X1001002_bit9 -640155648*X1001002_bit10 -1280311296*X1001002_bit11 -2560622592*X1001002_bit12 -24420*X1001003_bit_7 -48840*X1001003_bit_6 -97680*X1001003_bit_5 -195360*X1001003_bit_4 -390720*X1001003_bit_3 -781440*X1001003_bit_2 -1562880*X1001003_bit_1 -3125760*X1001003_bit0 -6251520*X1001003_bit1 -12503040*X1001003_bit2 -25006080*X1001003_bit3 -50012160*X1001003_bit4 -100024320*X1001003_bit5 -200048640*X1001003_bit6 -400097280*X1001003_bit7 -800194560*X1001003_bit8 -1600389120*X1001003_bit9 -3200778240*X1001003_bit10 -6401556480*X1001003_bit11 -12803112960*X1001003_bit12 -3256*X1001009_bit_7 -6512*X1001009_bit_6 -13024*X1001009_bit_5 -26048*X1001009_bit_4 -52096*X1001009_bit_3 -104192*X1001009_bit_2 -208384*X1001009_bit_1 -416768*X1001009_bit0 -833536*X1001009_bit1 -1667072*X1001009_bit2 -3334144*X1001009_bit3 -6668288*X1001009_bit4 -13336576*X1001009_bit5 -26673152*X1001009_bit6 -53346304*X1001009_bit7 -106692608*X1001009_bit8 -213385216*X1001009_bit9 -426770432*X1001009_bit10 -853540864*X1001009_bit11 -1707081728*X1001009_bit12 -5814*X1001013_bit_7 -11628*X1001013_bit_6 -23256*X1001013_bit_5 -46512*X1001013_bit_4 -93024*X1001013_bit_3 -186048*X1001013_bit_2 -372096*X1001013_bit_1 -744192*X1001013_bit0 -1488384*X1001013_bit1 -2976768*X1001013_bit2 -5953536*X1001013_bit3 -11907072*X1001013_bit4 -23814144*X1001013_bit5 -47628288*X1001013_bit6 -95256576*X1001013_bit7 -190513152*X1001013_bit8 -381026304*X1001013_bit9 -762052608*X1001013_bit10 -1524105216*X1001013_bit11 -3048210432*X1001013_bit12 -5814*X1001014_bit_7 -11628*X1001014_bit_6 -23256*X1001014_bit_5 -46512*X1001014_bit_4 -93024*X1001014_bit_3 -186048*X1001014_bit_2 -372096*X1001014_bit_1 -744192*X1001014_bit0 -1488384*X1001014_bit1 -2976768*X1001014_bit2 -5953536*X1001014_bit3 -11907072*X1001014_bit4 -23814144*X1001014_bit5 -47628288*X1001014_bit6 -95256576*X1001014_bit7 -190513152*X1001014_bit8 -381026304*X1001014_bit9 -762052608*X1001014_bit10 -1524105216*X1001014_bit11 -3048210432*X1001014_bit12 -3053*X1001015_bit_7 -6106*X1001015_bit_6 -12212*X1001015_bit_5 -24424*X1001015_bit_4 -48848*X1001015_bit_3 -97696*X1001015_bit_2 -195392*X1001015_bit_1 -390784*X1001015_bit0 -781568*X1001015_bit1 -1563136*X1001015_bit2 -3126272*X1001015_bit3 -6252544*X1001015_bit4 -12505088*X1001015_bit5 -25010176*X1001015_bit6 -50020352*X1001015_bit7 -100040704*X1001015_bit8 -200081408*X1001015_bit9 -400162816*X1001015_bit10 -800325632*X1001015_bit11 -1600651264*X1001015_bit12 -3053*X1001018_bit_7 -6106*X1001018_bit_6 -12212*X1001018_bit_5 -24424*X1001018_bit_4 -48848*X1001018_bit_3 -97696*X1001018_bit_2 -195392*X1001018_bit_1 -390784*X1001018_bit0 -781568*X1001018_bit1 -1563136*X1001018_bit2 -3126272*X1001018_bit3 -6252544*X1001018_bit4 -12505088*X1001018_bit5 -25010176*X1001018_bit6 -50020352*X1001018_bit7 -100040704*X1001018_bit8 -200081408*X1001018_bit9 -400162816*X1001018_bit10 -800325632*X1001018_bit11 -1600651264*X1001018_bit12 -4884*X1001021_bit_7 -9768*X1001021_bit_6 -19536*X1001021_bit_5 -39072*X1001021_bit_4 -78144*X1001021_bit_3 -156288*X1001021_bit_2 -312576*X1001021_bit_1 -625152*X1001021_bit0 -1250304*X1001021_bit1 -2500608*X1001021_bit2 -5001216*X1001021_bit3 -10002432*X1001021_bit4 -20004864*X1001021_bit5 -40009728*X1001021_bit6 -80019456*X1001021_bit7 -160038912*X1001021_bit8 -320077824*X1001021_bit9 -640155648*X1001021_bit10 -1280311296*X1001021_bit11 -2560622592*X1001021_bit12 >= -7040000; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-bnl2.opb s UNKNOWN c Exit Code: 0 c Total time: 207.353 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.85 0.94 0.90 2/54 838 Raw data (stat): 838 (runsolver) R 837 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 909717359 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0006 s] Raw data (loadavg): 0.88 0.94 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 1353 0 0 0 994 3 0 0 25 0 1 0 909717359 17895424 1273 4294967295 134512640 134716908 3221224560 3221223216 134528065 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4369 1273 1111 63 0 4306 0 vsize: 17476 [startup+20.0013 s] Raw data (loadavg): 0.89 0.94 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 2082 0 0 0 1992 5 0 0 25 0 1 0 909717359 21008384 2002 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5129 2002 1111 63 0 5066 0 vsize: 20516 [startup+30.001 s] Raw data (loadavg): 0.91 0.94 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 2841 0 0 0 2990 7 0 0 25 0 1 0 909717359 24113152 2761 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5887 2761 1111 63 0 5824 0 vsize: 23548 [startup+40.0018 s] Raw data (loadavg): 0.92 0.94 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 3627 0 0 0 3989 8 0 0 25 0 1 0 909717359 27242496 3547 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6651 3547 1111 63 0 6588 0 vsize: 26604 [startup+50.0025 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 4421 0 0 0 4988 10 0 0 25 0 1 0 909717359 30486528 4341 4294967295 134512640 134716908 3221224560 3221222788 1077414395 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7443 4341 1111 63 0 7380 0 vsize: 29772 [startup+60.0023 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 5224 0 0 0 5986 12 0 0 25 0 1 0 909717359 33873920 5144 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8270 5144 1111 63 0 8207 0 vsize: 33080 [startup+70.003 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 6038 0 0 0 6984 13 0 0 25 0 1 0 909717359 37126144 5958 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9064 5958 1111 63 0 9001 0 vsize: 36256 [startup+80.0038 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 6899 0 0 0 7982 16 0 0 25 0 1 0 909717359 40669184 6819 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9929 6819 1111 63 0 9866 0 vsize: 39716 [startup+90.0045 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 7777 0 0 0 8981 18 0 0 25 0 1 0 909717359 44339200 7697 4294967295 134512640 134716908 3221224560 3221222788 1077414424 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10825 7697 1111 63 0 10762 0 vsize: 43300 [startup+100.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 8677 0 0 0 9979 19 0 0 25 0 1 0 909717359 48009216 8597 4294967295 134512640 134716908 3221224560 3221222788 1077414422 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11721 8597 1111 63 0 11658 0 vsize: 46884 [startup+110.006 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 9609 0 0 0 10977 21 0 0 25 0 1 0 909717359 51818496 9529 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12651 9529 1111 63 0 12588 0 vsize: 50604 [startup+120.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 10583 0 0 0 11975 23 0 0 25 0 1 0 909717359 55771136 10503 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 13616 10503 1111 63 0 13553 0 vsize: 54464 [startup+130.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 11619 0 0 0 12974 24 0 0 25 0 1 0 909717359 60010496 11539 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 14651 11539 1111 63 0 14588 0 vsize: 58604 [startup+140.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 12744 0 0 0 13972 26 0 0 25 0 1 0 909717359 64753664 12664 4294967295 134512640 134716908 3221224560 3221222788 1077414360 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 15809 12664 1111 63 0 15746 0 vsize: 63236 [startup+150.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 14014 0 0 0 14969 30 0 0 25 0 1 0 909717359 69971968 13934 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17083 13934 1111 63 0 17020 0 vsize: 68332 [startup+160.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 15369 0 0 0 15967 32 0 0 25 0 1 0 909717359 75476992 15289 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18427 15289 1111 63 0 18364 0 vsize: 73708 [startup+170.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 16827 0 0 0 16964 35 0 0 25 0 1 0 909717359 81408000 16747 4294967295 134512640 134716908 3221224560 3221222788 1077414385 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19875 16747 1111 63 0 19812 0 vsize: 79500 [startup+180.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 18480 0 0 0 17961 38 0 0 25 0 1 0 909717359 88186880 18400 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21530 18400 1111 63 0 21467 0 vsize: 86120 [startup+190.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 20360 0 0 0 18959 40 0 0 25 0 1 0 909717359 95813632 20280 4294967295 134512640 134716908 3221224560 3221223216 134527935 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 23392 20280 1111 63 0 23329 0 vsize: 93568 [startup+200.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 22407 0 0 0 19955 44 0 0 25 0 1 0 909717359 104140800 22327 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25425 22327 1111 63 0 25362 0 vsize: 101700 [startup+207.417 s] Raw data (loadavg): 0.99 0.96 0.91 1/53 838 Raw data (stat): 838 (bsolo_lpr_cuts-) R 837 7266 7265 0 -1 0 22407 0 0 0 19955 44 0 0 25 0 1 0 909717359 104140800 22327 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25425 22327 1111 63 0 25362 0 vsize: 0 Child status: 0 Real time (s): 207.416 CPU time (s): 207.407 CPU user time (s): 206.847 CPU system time (s): 0.560914 CPU usage (%): 99.9958 Max. virtual memory (Kb): 101700 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####