Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-czprob.opb |
MD5SUM | 8225997c3fd9c39c0ae1e7fa3d3e4160 |
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 | 98250 |
Biggest coefficient in the objective function | 16496969383936000 |
Number of bits for the biggest coefficient in the objective function | 54 |
Sum of the numbers in the objective function | 33458351340667289600 |
Number of bits of the sum of numbers in the objective function | 65 |
Biggest number in a constraint | 16496969383936000 |
Number of bits of the biggest number in a constraint | 54 |
Biggest sum of numbers in a constraint | 33458351340667289600 |
Number of bits of the biggest sum of numbers | 65 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.886864 |
Number of variables | 98820 |
Total number of constraints | 927 |
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 | 927 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 11190 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc2 THE 2005-05-28 12:03:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=24348 boxname=wulflinc2 idbench=820 idsolver=17 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8225997c3fd9c39c0ae1e7fa3d3e4160 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-czprob.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-czprob.opb IDLAUNCH: 24348 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 720744 kB Buffers: 37036 kB Cached: 253456 kB SwapCached: 820 kB Active: 32072 kB Inactive: 260616 kB HighTotal: 131008 kB HighFree: 29288 kB LowTotal: 903652 kB LowFree: 691456 kB SwapTotal: 2097136 kB SwapFree: 2095480 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5340 kB Slab: 15404 kB Committed_AS: 71780 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-28 12:09:28 (client local time) WITH STATUS 1 IN 371.095 SECONDS stats: 24348 7 371.095 1 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c This solver internally uses Chaff 2004.11.15 Simplified Unexpected exception : St9bad_alloc #### 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.92 0.96 0.91 1/54 9582 Raw data (stat): 9582 (runsolver) D 9581 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 18 0 1 0 806434964 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 3225161850 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0003 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 2257 0 0 0 993 5 0 0 25 0 1 0 806434964 8228864 1581 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2009 1581 300 300 0 1709 0 vsize: 8036 [startup+20.0004 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 2794 0 0 0 1992 6 0 0 25 0 1 0 806434964 9715712 2109 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2372 2109 300 300 0 2072 0 vsize: 9488 [startup+30.0007 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 3943 0 0 0 2989 9 0 0 25 0 1 0 806434964 13819904 2547 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3374 2547 300 300 0 3074 0 vsize: 13496 [startup+40.0014 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 4196 0 0 0 3988 10 0 0 25 0 1 0 806434964 14360576 2795 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3506 2795 300 300 0 3206 0 vsize: 14024 [startup+50.0016 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 4461 0 0 0 4988 11 0 0 25 0 1 0 806434964 15036416 3056 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3671 3056 300 300 0 3371 0 vsize: 14684 [startup+60.0018 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 4703 0 0 0 5987 12 0 0 25 0 1 0 806434964 15712256 3294 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3836 3294 300 300 0 3536 0 vsize: 15344 [startup+70.0015 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 4925 0 0 0 6987 13 0 0 25 0 1 0 806434964 16388096 3512 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4001 3512 300 300 0 3701 0 vsize: 16004 [startup+80.0082 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 5129 0 0 0 7986 14 0 0 25 0 1 0 806434964 16928768 3713 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4133 3713 300 300 0 3833 0 vsize: 16532 [startup+90.0079 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 5323 0 0 0 8986 14 0 0 25 0 1 0 806434964 17334272 3904 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4232 3904 300 300 0 3932 0 vsize: 16928 [startup+100.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 5504 0 0 0 9985 15 0 0 25 0 1 0 806434964 17874944 4082 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4364 4082 300 300 0 4064 0 vsize: 17456 [startup+110.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 7582 0 0 0 10980 20 0 0 25 0 1 0 806434964 25948160 4748 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6335 4748 300 300 0 6035 0 vsize: 25340 [startup+120.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 7638 0 0 0 11980 21 0 0 25 0 1 0 806434964 25948160 4801 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6335 4801 300 300 0 6035 0 vsize: 25340 [startup+130.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 7691 0 0 0 12979 21 0 0 25 0 1 0 806434964 25948160 4852 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6335 4852 300 300 0 6035 0 vsize: 25340 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 7747 0 0 0 13979 22 0 0 25 0 1 0 806434964 25948160 4906 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6335 4906 300 300 0 6035 0 vsize: 25340 [startup+150.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 7836 0 0 0 14978 23 0 0 25 0 1 0 806434964 26083328 4992 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6368 4992 300 300 0 6068 0 vsize: 25472 [startup+160.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9582 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 7905 0 0 0 15978 23 0 0 25 0 1 0 806434964 26218496 5059 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6401 5059 300 300 0 6101 0 vsize: 25604 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8035 0 0 0 16977 24 0 0 25 0 1 0 806434964 26488832 5187 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6467 5187 300 300 0 6167 0 vsize: 25868 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8169 0 0 0 17977 25 0 0 25 0 1 0 806434964 26894336 5319 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6566 5319 300 300 0 6266 0 vsize: 26264 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8300 0 0 0 18977 25 0 0 25 0 1 0 806434964 27164672 5448 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6632 5448 300 300 0 6332 0 vsize: 26528 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8427 0 0 0 19976 26 0 0 25 0 1 0 806434964 27570176 5573 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6731 5573 300 300 0 6431 0 vsize: 26924 [startup+210.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8551 0 0 0 20975 27 0 0 25 0 1 0 806434964 27840512 5695 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6797 5695 300 300 0 6497 0 vsize: 27188 [startup+220.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8674 0 0 0 21975 27 0 0 25 0 1 0 806434964 28246016 5816 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6896 5816 300 300 0 6596 0 vsize: 27584 [startup+230.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8793 0 0 0 22974 28 0 0 25 0 1 0 806434964 28516352 5933 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6962 5933 300 300 0 6662 0 vsize: 27848 [startup+240.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 8910 0 0 0 23974 29 0 0 25 0 1 0 806434964 28786688 6048 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7028 6048 300 300 0 6728 0 vsize: 28112 [startup+250.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 9026 0 0 0 24974 29 0 0 25 0 1 0 806434964 29192192 6162 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7127 6162 300 300 0 6827 0 vsize: 28508 [startup+260.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 9138 0 0 0 25973 30 0 0 25 0 1 0 806434964 29462528 6273 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7193 6273 300 300 0 6893 0 vsize: 28772 [startup+270.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 35089 0 0 0 26912 91 0 0 25 0 1 0 806434964 118243328 26737 4294967295 134512640 135726644 3221224576 3182342716 134604415 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 28868 26737 300 300 0 28568 0 vsize: 115472 [startup+280.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 61276 0 0 0 27853 150 0 0 25 0 1 0 806434964 190910464 45008 4294967295 134512640 135726644 3221224576 3182076232 135282351 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 46609 45008 300 300 0 46309 0 vsize: 186436 [startup+290.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 92687 0 0 0 28791 212 0 0 25 0 1 0 806434964 293175296 60346 4294967295 134512640 135726644 3221224576 3181904000 135284836 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 71576 60347 300 300 0 71276 0 vsize: 286304 [startup+300.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 124086 0 0 0 29725 278 0 0 25 0 1 0 806434964 406806528 79231 4294967295 134512640 135726644 3221224576 3181939352 135282351 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 99318 79231 300 300 0 99018 0 vsize: 397272 [startup+310.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 164541 0 0 0 30653 351 0 0 25 0 1 0 806434964 537182208 100087 4294967295 134512640 135726644 3221224576 3181904464 134767136 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 131148 100088 300 300 0 130848 0 vsize: 524592 [startup+320.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 177897 0 0 0 31627 377 0 0 25 0 1 0 806434964 537182208 113203 4294967295 134512640 135726644 3221224576 3181979752 134784091 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 131148 113203 300 300 0 130848 0 vsize: 524592 [startup+330.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 219020 0 0 0 32536 468 0 0 25 0 1 0 806434964 657309696 129517 4294967295 134512640 135726644 3221224576 3182116844 134771400 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 160476 129517 300 300 0 160176 0 vsize: 641904 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 237353 0 0 0 33496 509 0 0 25 0 1 0 806434964 719114240 147627 4294967295 134512640 135726644 3221224576 3182018208 135280446 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 175565 147628 300 300 0 175265 0 vsize: 702260 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 258422 0 0 0 34450 554 0 0 25 0 1 0 806434964 751149056 168443 4294967295 134512640 135726644 3221224576 3182652252 134560228 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 183386 168443 300 300 0 183086 0 vsize: 733544 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 262616 0 0 0 35443 562 0 0 25 0 1 0 806434964 758820864 172582 4294967295 134512640 135726644 3221224576 3214939572 135131380 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 185259 172582 300 300 0 184959 0 vsize: 741036 [startup+370.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 262618 0 0 0 36430 574 0 0 25 0 1 0 806434964 446328832 108544 4294967295 134512640 135726644 3221224576 3221222928 135280446 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 108967 108544 300 300 0 108667 0 vsize: 435868 [startup+371.069 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 9584 Raw data (stat): 9582 (pb2sat) R 9581 31399 31398 0 -1 0 262618 0 0 0 36430 574 0 0 25 0 1 0 806434964 446328832 108544 4294967295 134512640 135726644 3221224576 3221222928 135280446 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 108967 108544 300 300 0 108667 0 vsize: 0 Child status: 1 Real time (s): 371.069 CPU time (s): 371.095 CPU user time (s): 365.123 CPU system time (s): 5.97209 CPU usage (%): 100.007 Max. virtual memory (Kb): 741036 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####