Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-atlanta-ip.opb |
MD5SUM | 5c887381904b4849f12f155c2e7ab40c |
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 | 31296 |
Biggest coefficient in the objective function | 1700000000000 |
Number of bits for the biggest coefficient in the objective function | 41 |
Sum of the numbers in the objective function | 81421012358779 |
Number of bits of the sum of numbers in the objective function | 47 |
Biggest number in a constraint | 1700000000000 |
Number of bits of the biggest number in a constraint | 41 |
Biggest sum of numbers in a constraint | 81421012358779 |
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.841871 |
Number of variables | 71516 |
Total number of constraints | 70354 |
Number of constraints which are clauses | 2311 |
Number of constraints which are cardinality constraints (but not clauses) | 47534 |
Number of constraints which are nor clauses,nor cardinality constraints | 20509 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2790 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-05-24 21:05:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17461 boxname=wulflinc11 idbench=1344 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: 5c887381904b4849f12f155c2e7ab40c /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-atlanta-ip.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-atlanta-ip.opb IDLAUNCH: 17461 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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.028 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: 512344 kB Buffers: 36968 kB Cached: 443572 kB SwapCached: 84 kB Active: 60476 kB Inactive: 436420 kB HighTotal: 131008 kB HighFree: 48412 kB LowTotal: 903652 kB LowFree: 463932 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 704 kB Writeback: 0 kB Mapped: 6880 kB Slab: 19680 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-24 21:09:53 (client local time) WITH STATUS 0 IN 251.623 SECONDS stats: 17461 7 251.623 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. #### 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.99 1.00 1.00 2/54 30496 Raw data (stat): 30496 (runsolver) R 30495 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 775117731 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 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+10.0005 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30496 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 7021 0 0 0 982 15 0 0 25 0 1 0 775117731 41349120 6945 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 10095 6945 1111 63 0 10032 0 vsize: 40380 [startup+20.0011 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30496 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 14354 0 0 0 1970 28 0 0 25 0 1 0 775117731 71331840 14278 4294967295 134512640 134714508 3221224576 3221222804 1077414382 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17415 14278 1111 63 0 17352 0 vsize: 69660 [startup+30.0016 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30496 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 21632 0 0 0 2959 39 0 0 25 0 1 0 775117731 101191680 21556 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 24705 21556 1111 63 0 24642 0 vsize: 98820 [startup+40.0016 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30496 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 29081 0 0 0 3947 51 0 0 25 0 1 0 775117731 131772416 29005 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 32171 29005 1111 63 0 32108 0 vsize: 128684 [startup+50.0024 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 36416 0 0 0 4936 62 0 0 25 0 1 0 775117731 161783808 36340 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 39498 36340 1111 63 0 39435 0 vsize: 157992 [startup+60.0019 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 44262 0 0 0 5923 75 0 0 25 0 1 0 775117731 193884160 44186 4294967295 134512640 134714508 3221224576 3221222804 1077414435 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 47335 44186 1111 63 0 47272 0 vsize: 189340 [startup+70.002 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 52163 0 0 0 6911 88 0 0 25 0 1 0 775117731 226279424 52087 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 55244 52088 1111 63 0 55181 0 vsize: 220976 [startup+80.0028 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 60228 0 0 0 7898 100 0 0 25 0 1 0 775117731 259276800 60152 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 63300 60152 1111 63 0 63237 0 vsize: 253200 [startup+90.0023 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 68700 0 0 0 8884 115 0 0 25 0 1 0 775117731 294064128 68624 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 71793 68624 1111 63 0 71730 0 vsize: 287172 [startup+100.002 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 77634 0 0 0 9867 132 0 0 25 0 1 0 775117731 330645504 77558 4294967295 134512640 134714508 3221224576 3221223232 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 80724 77558 1111 63 0 80661 0 vsize: 322896 [startup+110.003 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 86481 0 0 0 10854 145 0 0 25 0 1 0 775117731 366772224 86405 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 89544 86405 1111 63 0 89481 0 vsize: 358176 [startup+120.003 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 95821 0 0 0 11840 159 0 0 25 0 1 0 775117731 404996096 95745 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 98876 95745 1111 63 0 98813 0 vsize: 395504 [startup+130.003 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 105215 0 0 0 12823 177 0 0 25 0 1 0 775117731 443588608 105139 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 108298 105139 1111 63 0 108235 0 vsize: 433192 [startup+140.003 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 114403 0 0 0 13808 192 0 0 25 0 1 0 775117731 481206272 114327 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 117482 114327 1111 63 0 117419 0 vsize: 469928 [startup+150.003 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 123713 0 0 0 14792 208 0 0 25 0 1 0 775117731 519430144 123637 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 126814 123637 1111 63 0 126751 0 vsize: 507256 [startup+160.003 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 133189 0 0 0 15778 223 0 0 25 0 1 0 775117731 558256128 133113 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 136293 133113 1111 63 0 136230 0 vsize: 545172 [startup+170.004 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 142954 0 0 0 16760 240 0 0 25 0 1 0 775117731 598114304 142878 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 146024 142878 1111 63 0 145961 0 vsize: 584096 [startup+180.005 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 152726 0 0 0 17741 260 0 0 25 0 1 0 775117731 638128128 152650 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 155793 152650 1111 63 0 155730 0 vsize: 623172 [startup+190.005 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 162225 0 0 0 18723 278 0 0 25 0 1 0 775117731 677093376 162149 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 165306 162149 1111 63 0 165243 0 vsize: 661224 [startup+200.005 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 171670 0 0 0 19706 296 0 0 25 0 1 0 775117731 715767808 171594 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 174748 171594 1111 63 0 174685 0 vsize: 698992 [startup+210.006 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 181380 0 0 0 20690 312 0 0 25 0 1 0 775117731 755482624 181304 4294967295 134512640 134714508 3221224576 3221222696 1077378037 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 184444 181309 1111 63 0 184381 0 vsize: 737776 [startup+220.006 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 192869 0 0 0 21668 332 0 0 25 0 1 0 775117731 802758656 192793 4294967295 134512640 134714508 3221224576 3221222860 1077399562 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 195986 192793 1111 63 0 195923 0 vsize: 783944 [startup+230.007 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 219209 0 0 0 22583 387 0 0 25 0 1 0 775117731 910561280 216197 4294967295 134512640 134714508 3221224576 3221222852 1077414358 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 222305 216197 1111 63 0 222242 0 vsize: 889220 [startup+240.006 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 225085 0 114 0 23424 402 0 0 25 0 1 0 775117731 934240256 219893 4294967295 134512640 134714508 3221224576 3221222588 1077360160 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 228086 219893 1111 63 0 228023 0 vsize: 912344 [startup+250.007 s] Raw data (loadavg): 0.99 1.00 1.00 2/54 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 226919 0 122 0 24408 408 0 0 25 0 1 0 775117731 941703168 221581 4294967295 134512640 134714508 3221224576 3221222880 134566799 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 229908 221581 1111 63 0 229845 0 vsize: 919632 [startup+253.672 s] Raw data (loadavg): 0.99 1.00 1.00 1/53 30498 Raw data (stat): 30496 (bsolo_lpr_cuts) R 30495 25830 25829 0 -1 0 226919 0 122 0 24408 408 0 0 25 0 1 0 775117731 941703168 221581 4294967295 134512640 134714508 3221224576 3221222880 134566799 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 229908 221581 1111 63 0 229845 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 253.672 CPU time (s): 251.623 CPU user time (s): 247.091 CPU system time (s): 4.53131 CPU usage (%): 99.1923 Max. virtual memory (Kb): 919632 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####