Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-rd-rplusc-21.opb |
MD5SUM | d2b612d978c6eb050af622d4cf2ae598 |
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 | 48 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2160590747 |
Number of bits of the sum of numbers in the objective function | 32 |
Biggest number in a constraint | 2962281908055777280 |
Number of bits of the biggest number in a constraint | 62 |
Biggest sum of numbers in a constraint | 6289973478481187311 |
Number of bits of the biggest sum of numbers | 63 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 708.041 |
Number of variables | 3616 |
Total number of constraints | 126450 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 699 |
Number of constraints which are nor clauses,nor cardinality constraints | 125751 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 189 |
LAUNCH ON wulflinc10 THE 2005-09-19 04:52:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4111 boxname=wulflinc10 idbench=595 idsolver=4 numberseed=0 MD5SUM SOLVER: 21c3ffd7205c96d5f0784fd273b92938 /oldhome/oroussel/solvers/PBS4 MD5SUM BENCH: d2b612d978c6eb050af622d4cf2ae598 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-rd-rplusc-21.opb REAL COMMAND: PBS4 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-rd-rplusc-21.opb IDLAUNCH: 4111 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 628172 kB Buffers: 37056 kB Cached: 341680 kB SwapCached: 228 kB Active: 293364 kB Inactive: 88344 kB HighTotal: 131008 kB HighFree: 3808 kB LowTotal: 903652 kB LowFree: 624364 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6272 kB Slab: 18980 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 04:55:54 (client local time) WITH STATUS 20 IN 198.755 SECONDS stats: 4111 7 198.755 20
c PBS v4 by Bashar Al-Rawi & Fadi Aloul c Solving /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-rd-rplusc-21.opb ...... s UNSATISFIABLE c Done, CPU Time=0.005999
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1788970594 978944 2 4294967295 134512640 135450776 3221224560 3221224560 134512960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 239 2 232 232 0 7 0 [pid=3542] vsize: 956 open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-rd-rplusc-21.opb open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-rd-rplusc-21.opb [startup+10.0032 s] Raw data (loadavg): 1.04 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 3219 0 0 0 977 16 0 0 25 0 1 0 1788970594 13783040 3104 4294967295 134512640 135450776 3221224560 3221223072 134599247 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 3365 3104 232 232 0 3133 0 [pid=3542] vsize: 13460 Current children cumulated CPU time (s) 9.93 Current children cumulated vsize (Kb) 13460 [startup+20.0038 s] Raw data (loadavg): 1.04 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 6240 0 0 0 1956 32 0 0 25 0 1 0 1788970594 25661440 5996 4294967295 134512640 135450776 3221224560 3221222928 134844223 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 6265 5996 232 232 0 6033 0 [pid=3542] vsize: 25060 Current children cumulated CPU time (s) 19.88 Current children cumulated vsize (Kb) 25060 [startup+30.0043 s] Raw data (loadavg): 1.03 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 12191 0 0 0 2925 55 0 0 25 0 1 0 1788970594 49688576 11690 4294967295 134512640 135450776 3221224560 3221222992 134527082 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 12131 11690 232 232 0 11899 0 [pid=3542] vsize: 48524 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 48524 [startup+40.0049 s] Raw data (loadavg): 1.02 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 12352 0 0 0 3912 65 0 0 25 0 1 0 1788970594 49688576 11851 4294967295 134512640 135450776 3221224560 3221223056 134524210 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 12131 11851 232 232 0 11899 0 [pid=3542] vsize: 48524 Current children cumulated CPU time (s) 39.77 Current children cumulated vsize (Kb) 48524 [startup+50.0065 s] Raw data (loadavg): 1.02 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 22283 0 0 0 4874 95 0 0 25 0 1 0 1788970594 90038272 21269 4294967295 134512640 135450776 3221224560 3221222932 134524558 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 21982 21269 232 232 0 21750 0 [pid=3542] vsize: 87928 Current children cumulated CPU time (s) 49.69 Current children cumulated vsize (Kb) 87928 [startup+60.006 s] Raw data (loadavg): 1.02 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 22379 0 0 0 5858 106 0 0 25 0 1 0 1788970594 90038272 21365 4294967295 134512640 135450776 3221224560 3221223088 134672169 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 21982 21365 232 232 0 21750 0 [pid=3542] vsize: 87928 Current children cumulated CPU time (s) 59.64 Current children cumulated vsize (Kb) 87928 [startup+70.0056 s] Raw data (loadavg): 1.01 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 22476 0 0 0 6843 115 0 0 25 0 1 0 1788970594 90038272 21462 4294967295 134512640 135450776 3221224560 3221223136 134675455 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 21982 21462 232 232 0 21750 0 [pid=3542] vsize: 87928 Current children cumulated CPU time (s) 69.58 Current children cumulated vsize (Kb) 87928 [startup+80.0061 s] Raw data (loadavg): 1.01 0.98 0.97 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) T 3541 3542 22582 0 -1 0 22573 0 0 0 7826 125 0 0 25 0 1 0 1788970594 90038272 21559 4294967295 134512640 135450776 3221224560 3221222800 135124493 0 0 5 0 3222434794 0 0 17 1 0 0 Raw data (/proc/3542/statm): 21982 21559 232 232 0 21750 0 [pid=3542] vsize: 87928 Current children cumulated CPU time (s) 79.51 Current children cumulated vsize (Kb) 87928 [startup+90.0057 s] Raw data (loadavg): 1.09 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 24483 0 0 0 8806 139 0 0 25 0 1 0 1788970594 97337344 23469 4294967295 134512640 135450776 3221224560 3221223056 134524258 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 23764 23469 232 232 0 23532 0 [pid=3542] vsize: 95056 Current children cumulated CPU time (s) 89.45 Current children cumulated vsize (Kb) 95056 [startup+100.006 s] Raw data (loadavg): 1.07 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 26443 0 0 0 9787 152 0 0 25 0 1 0 1788970594 105041920 25429 4294967295 134512640 135450776 3221224560 3221223056 134524204 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 25645 25429 232 232 0 25413 0 [pid=3542] vsize: 102580 Current children cumulated CPU time (s) 99.39 Current children cumulated vsize (Kb) 102580 [startup+110.007 s] Raw data (loadavg): 1.06 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46235 0 0 0 10731 200 0 0 25 0 1 0 1788970594 185741312 44196 4294967295 134512640 135450776 3221224560 3221223172 134864596 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44196 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 109.31 Current children cumulated vsize (Kb) 181388 [startup+120.007 s] Raw data (loadavg): 1.05 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46329 0 0 0 11715 211 0 0 25 0 1 0 1788970594 185741312 44290 4294967295 134512640 135450776 3221224560 3221223104 134855580 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44290 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 119.26 Current children cumulated vsize (Kb) 181388 [startup+130.008 s] Raw data (loadavg): 1.04 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46425 0 0 0 12700 220 0 0 25 0 1 0 1788970594 185741312 44386 4294967295 134512640 135450776 3221224560 3221223136 134675491 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44386 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 129.2 Current children cumulated vsize (Kb) 181388 [startup+140.009 s] Raw data (loadavg): 1.04 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46521 0 0 0 13686 229 0 0 25 0 1 0 1788970594 185741312 44482 4294967295 134512640 135450776 3221224560 3221223104 134846937 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44482 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 139.15 Current children cumulated vsize (Kb) 181388 [startup+150.009 s] Raw data (loadavg): 1.03 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46617 0 0 0 14669 240 0 0 25 0 1 0 1788970594 185741312 44578 4294967295 134512640 135450776 3221224560 3221222932 134524539 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44578 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 149.09 Current children cumulated vsize (Kb) 181388 [startup+160.009 s] Raw data (loadavg): 1.03 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46712 0 0 0 15655 249 0 0 25 0 1 0 1788970594 185741312 44673 4294967295 134512640 135450776 3221224560 3221223104 134855580 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44673 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 159.04 Current children cumulated vsize (Kb) 181388 [startup+170.008 s] Raw data (loadavg): 1.02 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 46808 0 0 0 16639 260 0 0 25 0 1 0 1788970594 185741312 44769 4294967295 134512640 135450776 3221224560 3221223056 134524341 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 45347 44769 232 232 0 45115 0 [pid=3542] vsize: 181388 Current children cumulated CPU time (s) 168.99 Current children cumulated vsize (Kb) 181388 [startup+180.009 s] Raw data (loadavg): 1.02 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 47789 0 0 0 17622 271 0 0 25 0 1 0 1788970594 189390848 45750 4294967295 134512640 135450776 3221224560 3221223056 134524204 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 46238 45750 232 232 0 46006 0 [pid=3542] vsize: 184952 Current children cumulated CPU time (s) 178.93 Current children cumulated vsize (Kb) 184952 [startup+190.009 s] Raw data (loadavg): 1.01 1.00 0.98 2/56 3542 Raw data (/proc/3542/stat): 3542 (PBS4) R 3541 3542 22582 0 -1 0 49745 0 0 0 18601 286 0 0 25 0 1 0 1788970594 196960256 47706 4294967295 134512640 135450776 3221224560 3221222932 134524541 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3542/statm): 48086 47706 232 232 0 47854 0 [pid=3542] vsize: 192344 Current children cumulated CPU time (s) 188.87 Current children cumulated vsize (Kb) 192344 One traced child (pid=3542) exited with status: 20 All traced children have exited ! Game is over. Child status: 20 Real time (s): 199.945 CPU time (s): 198.755 CPU user time (s): 195.662 CPU system time (s): 3.09253 CPU usage (%): 99.4046 Max. virtual memory (cumulated for all children) (Kb): 192344
ERROR: no interpretation found !