Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-rd-rplusc-21.opb |
MD5SUM | 62166f7982a2b3c488537a2a2dbe4149 |
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 | 35 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 3735451 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 383602153706972160 |
Number of bits of the biggest number in a constraint | 59 |
Biggest sum of numbers in a constraint | 772928706545624815 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 290.495 |
Number of variables | 2644 |
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 | 130 |
LAUNCH ON wulflinc21 THE 2005-09-20 08:12:13 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4495 boxname=wulflinc21 idbench=979 idsolver=4 numberseed=0 MD5SUM SOLVER: 21c3ffd7205c96d5f0784fd273b92938 /oldhome/oroussel/solvers/PBS4 MD5SUM BENCH: 62166f7982a2b3c488537a2a2dbe4149 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb REAL COMMAND: PBS4 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb IDLAUNCH: 4495 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 3 cpu MHz : 451.161 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: 629108 kB Buffers: 35328 kB Cached: 339880 kB SwapCached: 832 kB Active: 258536 kB Inactive: 119228 kB HighTotal: 131008 kB HighFree: 3780 kB LowTotal: 903652 kB LowFree: 625328 kB SwapTotal: 2097892 kB SwapFree: 2096456 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5776 kB Slab: 21988 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 08:14:38 (client local time) WITH STATUS 20 IN 140.903 SECONDS stats: 4495 7 140.903 20
c PBS v4 by Bashar Al-Rawi & Fadi Aloul c Solving /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb ...... s UNSATISFIABLE c Done, CPU Time=0.088987
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/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 18 0 0 0 0 0 0 0 21 0 1 0 1734271162 978944 2 4294967295 134512640 135450776 3221224560 3221224560 134512960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 239 2 232 232 0 7 0 [pid=15240] vsize: 956 open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb [startup+10.0028 s] Raw data (loadavg): 0.94 0.93 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 4791 0 0 0 971 20 0 0 25 0 1 0 1734271162 20033536 4547 4294967295 134512640 135450776 3221224560 3221223072 134855247 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 4891 4547 232 232 0 4659 0 [pid=15240] vsize: 19564 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 19564 [startup+20.0035 s] Raw data (loadavg): 0.95 0.93 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 9399 0 0 0 1944 41 0 0 25 0 1 0 1734271162 38383616 8898 4294967295 134512640 135450776 3221224560 3221223072 134600038 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 9371 8898 232 232 0 9139 0 [pid=15240] vsize: 37484 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 37484 [startup+30.0032 s] Raw data (loadavg): 0.96 0.93 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 9603 0 0 0 2930 51 0 0 25 0 1 0 1734271162 38383616 9102 4294967295 134512640 135450776 3221224560 3221223056 134524210 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 9371 9102 232 232 0 9139 0 [pid=15240] vsize: 37484 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 37484 [startup+40.0029 s] Raw data (loadavg): 0.96 0.93 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 17201 0 0 0 3898 76 0 0 25 0 1 0 1734271162 68866048 16187 4294967295 134512640 135450776 3221224560 3221222932 134524520 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 16813 16187 232 232 0 16581 0 [pid=15240] vsize: 67252 Current children cumulated CPU time (s) 39.74 Current children cumulated vsize (Kb) 67252 [startup+50.0035 s] Raw data (loadavg): 0.97 0.93 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 17337 0 0 0 4884 86 0 0 25 0 1 0 1734271162 68866048 16323 4294967295 134512640 135450776 3221224560 3221222992 134527082 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 16813 16323 232 232 0 16581 0 [pid=15240] vsize: 67252 Current children cumulated CPU time (s) 49.7 Current children cumulated vsize (Kb) 67252 [startup+60.0032 s] Raw data (loadavg): 0.97 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 18084 0 0 0 5866 98 0 0 25 0 1 0 1734271162 71438336 17070 4294967295 134512640 135450776 3221224560 3221222932 134524558 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 17441 17070 232 232 0 17209 0 [pid=15240] vsize: 69764 Current children cumulated CPU time (s) 59.64 Current children cumulated vsize (Kb) 69764 [startup+70.0039 s] Raw data (loadavg): 0.98 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 20213 0 0 0 6845 113 0 0 25 0 1 0 1734271162 79548416 19199 4294967295 134512640 135450776 3221224560 3221223072 134600478 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 19421 19199 232 232 0 19189 0 [pid=15240] vsize: 77684 Current children cumulated CPU time (s) 69.58 Current children cumulated vsize (Kb) 77684 [startup+80.0046 s] Raw data (loadavg): 0.98 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 35626 0 0 0 7800 151 0 0 25 0 1 0 1734271162 142135296 33587 4294967295 134512640 135450776 3221224560 3221223148 134675440 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 34701 33587 232 232 0 34469 0 [pid=15240] vsize: 138804 Current children cumulated CPU time (s) 79.51 Current children cumulated vsize (Kb) 138804 [startup+90.0043 s] Raw data (loadavg): 0.98 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 35762 0 0 0 8784 161 0 0 25 0 1 0 1734271162 142135296 33723 4294967295 134512640 135450776 3221224560 3221223056 134524234 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 34701 33723 232 232 0 34469 0 [pid=15240] vsize: 138804 Current children cumulated CPU time (s) 89.45 Current children cumulated vsize (Kb) 138804 [startup+100.005 s] Raw data (loadavg): 0.98 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 35897 0 0 0 9766 174 0 0 25 0 1 0 1734271162 142135296 33858 4294967295 134512640 135450776 3221224560 3221222932 134524541 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 34701 33858 232 232 0 34469 0 [pid=15240] vsize: 138804 Current children cumulated CPU time (s) 99.4 Current children cumulated vsize (Kb) 138804 [startup+110.006 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 36033 0 0 0 10748 187 0 0 25 0 1 0 1734271162 142135296 33994 4294967295 134512640 135450776 3221224560 3221223056 134524174 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 34701 33994 232 232 0 34469 0 [pid=15240] vsize: 138804 Current children cumulated CPU time (s) 109.35 Current children cumulated vsize (Kb) 138804 [startup+120.006 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 36168 0 0 0 11732 198 0 0 25 0 1 0 1734271162 142135296 34129 4294967295 134512640 135450776 3221224560 3221222932 134524475 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 34701 34129 232 232 0 34469 0 [pid=15240] vsize: 138804 Current children cumulated CPU time (s) 119.3 Current children cumulated vsize (Kb) 138804 [startup+130.006 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 37516 0 0 0 12715 209 0 0 25 0 1 0 1734271162 147136512 35477 4294967295 134512640 135450776 3221224560 3221222932 134524475 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 35922 35477 232 232 0 35690 0 [pid=15240] vsize: 143688 Current children cumulated CPU time (s) 129.24 Current children cumulated vsize (Kb) 143688 [startup+140.006 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 15240 Raw data (/proc/15240/stat): 15240 (PBS4) R 15239 15240 20602 0 -1 0 39641 0 0 0 13693 225 0 0 25 0 1 0 1734271162 155250688 37602 4294967295 134512640 135450776 3221224560 3221223036 135084757 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15240/statm): 37903 37602 232 232 0 37671 0 [pid=15240] vsize: 151612 Current children cumulated CPU time (s) 139.18 Current children cumulated vsize (Kb) 151612 One traced child (pid=15240) exited with status: 20 All traced children have exited ! Game is over. Child status: 20 Real time (s): 141.727 CPU time (s): 140.903 CPU user time (s): 138.558 CPU system time (s): 2.34464 CPU usage (%): 99.4181 Max. virtual memory (cumulated for all children) (Kb): 151612
ERROR: no interpretation found !