Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-shell.opb |
MD5SUM | 0f9e797b4b986a37159e9b1332a4b629 |
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 | 39844 |
Biggest coefficient in the objective function | 2101312749568 |
Number of bits for the biggest coefficient in the objective function | 41 |
Sum of the numbers in the objective function | 249967315526150 |
Number of bits of the sum of numbers in the objective function | 48 |
Biggest number in a constraint | 2101312749568 |
Number of bits of the biggest number in a constraint | 41 |
Biggest sum of numbers in a constraint | 249967315526150 |
Number of bits of the biggest sum of numbers | 48 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.398939 |
Number of variables | 45231 |
Total number of constraints | 653 |
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 | 653 |
Minimum length of a constraint | 19 |
Maximum length of a constraint | 1560 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-05-25 04:06:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=11391 boxname=wulflinc6 idbench=877 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: 0f9e797b4b986a37159e9b1332a4b629 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-shell.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-shell.opb IDLAUNCH: 11391 /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: 909896 kB Buffers: 10812 kB Cached: 88328 kB SwapCached: 412 kB Active: 22348 kB Inactive: 79128 kB HighTotal: 131008 kB HighFree: 88256 kB LowTotal: 903652 kB LowFree: 821640 kB SwapTotal: 2097136 kB SwapFree: 2096036 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5692 kB Slab: 17544 kB Committed_AS: 63720 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 04:12:27 (client local time) WITH STATUS 20 IN 347.023 SECONDS stats: 11391 7 347.023 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Initial problem consists of 45231 variables and 973 constraints. s UNSATISFIABLE c Exit Code: 20 c Total time: 346.962 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.93 0.97 0.98 2/54 2589 Raw data (stat): 2589 (runsolver) R 2588 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 777647312 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 0.94 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 888 0 0 0 997 2 0 0 25 0 1 0 777647312 16551936 866 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4041 866 1111 63 0 3978 0 vsize: 16164 [startup+20.0024 s] Raw data (loadavg): 0.95 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 1279 0 0 0 1997 2 0 0 25 0 1 0 777647312 18182144 1257 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4439 1257 1111 63 0 4376 0 vsize: 17756 [startup+30.0032 s] Raw data (loadavg): 0.95 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 1679 0 0 0 2996 3 0 0 25 0 1 0 777647312 19795968 1657 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4833 1657 1111 63 0 4770 0 vsize: 19332 [startup+40.0034 s] Raw data (loadavg): 0.96 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 2063 0 0 0 3996 4 0 0 25 0 1 0 777647312 21295104 2041 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5199 2041 1111 63 0 5136 0 vsize: 20796 [startup+50.0035 s] Raw data (loadavg): 0.97 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 2476 0 0 0 4995 4 0 0 25 0 1 0 777647312 23089152 2454 4294967295 134512640 134714540 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5637 2454 1111 63 0 5574 0 vsize: 22548 [startup+60.0036 s] Raw data (loadavg): 0.97 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 2933 0 0 0 5994 6 0 0 25 0 1 0 777647312 24858624 2911 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6069 2911 1111 63 0 6006 0 vsize: 24276 [startup+70.0038 s] Raw data (loadavg): 0.97 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 3338 0 0 0 6994 7 0 0 25 0 1 0 777647312 26628096 3316 4294967295 134512640 134714540 3221224592 3221222820 1077414424 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6501 3316 1111 63 0 6438 0 vsize: 26004 [startup+80.004 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 3758 0 0 0 7993 8 0 0 25 0 1 0 777647312 28282880 3736 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6905 3736 1111 63 0 6842 0 vsize: 27620 [startup+90.0041 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 4191 0 0 0 8993 9 0 0 25 0 1 0 777647312 30052352 4169 4294967295 134512640 134714540 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7337 4169 1111 63 0 7274 0 vsize: 29348 [startup+100.005 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 4656 0 0 0 9992 9 0 0 25 0 1 0 777647312 32010240 4634 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7815 4634 1111 63 0 7752 0 vsize: 31260 [startup+110.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 5118 0 0 0 10992 10 0 0 25 0 1 0 777647312 33955840 5096 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8290 5096 1111 63 0 8227 0 vsize: 33160 [startup+120.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 5581 0 0 0 11991 11 0 0 25 0 1 0 777647312 35753984 5559 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8729 5559 1111 63 0 8666 0 vsize: 34916 [startup+130.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 6052 0 0 0 12991 12 0 0 25 0 1 0 777647312 37703680 6030 4294967295 134512640 134714540 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9205 6030 1111 63 0 9142 0 vsize: 36820 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 6539 0 0 0 13990 13 0 0 25 0 1 0 777647312 39661568 6517 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9683 6517 1111 63 0 9620 0 vsize: 38732 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 7042 0 0 0 14990 14 0 0 25 0 1 0 777647312 41766912 7020 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10197 7020 1111 63 0 10134 0 vsize: 40788 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 7556 0 0 0 15988 15 0 0 25 0 1 0 777647312 43835392 7534 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 10702 7534 1111 63 0 10639 0 vsize: 42808 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 8085 0 0 0 16988 16 0 0 25 0 1 0 777647312 45936640 8063 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11215 8063 1111 63 0 11152 0 vsize: 44860 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 8660 0 0 0 17987 17 0 0 25 0 1 0 777647312 48529408 8638 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11848 8638 1111 63 0 11785 0 vsize: 47392 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 9219 0 0 0 18987 18 0 0 25 0 1 0 777647312 50778112 9197 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12397 9197 1111 63 0 12334 0 vsize: 49588 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 9800 0 0 0 19986 19 0 0 25 0 1 0 777647312 53186560 9778 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12985 9778 1111 63 0 12922 0 vsize: 51940 [startup+210.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 10403 0 0 0 20985 21 0 0 25 0 1 0 777647312 55566336 10381 4294967295 134512640 134714540 3221224592 3221222820 1077414345 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 13566 10381 1111 63 0 13503 0 vsize: 54264 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 11058 0 0 0 21984 22 0 0 25 0 1 0 777647312 58253312 11036 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 14222 11036 1111 63 0 14159 0 vsize: 56888 [startup+230.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 11718 0 0 0 22984 23 0 0 25 0 1 0 777647312 60944384 11696 4294967295 134512640 134714540 3221224592 3221223248 134527930 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 14879 11696 1111 63 0 14816 0 vsize: 59516 [startup+240.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 12389 0 0 0 23983 24 0 0 25 0 1 0 777647312 63647744 12367 4294967295 134512640 134714540 3221224592 3221222820 1077414351 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 15539 12367 1111 63 0 15476 0 vsize: 62156 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 13086 0 0 0 24982 25 0 0 25 0 1 0 777647312 66465792 13064 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16227 13064 1111 63 0 16164 0 vsize: 64908 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 13792 0 0 0 25980 27 0 0 25 0 1 0 777647312 69439488 13770 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16953 13770 1111 63 0 16890 0 vsize: 67812 [startup+270.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 14528 0 0 0 26979 29 0 0 25 0 1 0 777647312 72441856 14506 4294967295 134512640 134714540 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17686 14506 1111 63 0 17623 0 vsize: 70744 [startup+280.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 15309 0 0 0 27977 31 0 0 25 0 1 0 777647312 75591680 15287 4294967295 134512640 134714540 3221224592 3221222820 1077414408 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 18455 15287 1111 63 0 18392 0 vsize: 73820 [startup+290.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 16141 0 0 0 28977 32 0 0 25 0 1 0 777647312 78995456 16119 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 19286 16119 1111 63 0 19223 0 vsize: 77144 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 17012 0 0 0 29976 33 0 0 25 0 1 0 777647312 82784256 16990 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 20211 16990 1111 63 0 20148 0 vsize: 80844 [startup+310.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 17874 0 0 0 30975 35 0 0 25 0 1 0 777647312 86388736 17852 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21091 17852 1111 63 0 21028 0 vsize: 84364 [startup+320.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 18764 0 0 0 31975 36 0 0 25 0 1 0 777647312 89989120 18742 4294967295 134512640 134714540 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21970 18742 1111 63 0 21907 0 vsize: 87880 [startup+330.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 19690 0 0 0 32973 38 0 0 25 0 1 0 777647312 93679616 19668 4294967295 134512640 134714540 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 22871 19668 1111 63 0 22808 0 vsize: 91484 [startup+340.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 23189 0 0 0 33966 45 0 0 25 0 1 0 777647312 107339776 23007 4294967295 134512640 134714540 3221224592 3221222880 134566542 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 26206 23007 1111 63 0 26143 0 vsize: 104824 [startup+346.959 s] Raw data (loadavg): 0.99 0.97 0.98 1/53 2589 Raw data (stat): 2589 (bsolo_mis) R 2588 25568 25567 0 -1 0 23189 0 0 0 33966 45 0 0 25 0 1 0 777647312 107339776 23007 4294967295 134512640 134714540 3221224592 3221222880 134566542 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 26206 23007 1111 63 0 26143 0 vsize: 0 Child status: 20 Real time (s): 346.958 CPU time (s): 347.023 CPU user time (s): 346.373 CPU system time (s): 0.649901 CPU usage (%): 100.019 Max. virtual memory (Kb): 104824 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####