Name | mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos19.opb |
MD5SUM | 6eb30c4e664b9c0e8d94f2aea74a91a3 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 1611 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1611 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 24576 |
Number of bits of the biggest number in a constraint | 15 |
Biggest sum of numbers in a constraint | 98256 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 1041679 |
Total number of constraints | 137871 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 10091 |
Number of constraints which are nor clauses,nor cardinality constraints | 127780 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 275 |
LAUNCH ON wulflinc23 THE 2005-09-23 17:23:19 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8929 boxname=wulflinc23 idbench=725 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6eb30c4e664b9c0e8d94f2aea74a91a3 /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos19.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos19.opb IDLAUNCH: 8929 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.185 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 : 3 cpu MHz : 451.185 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 838416 kB Buffers: 14848 kB Cached: 162564 kB SwapCached: 0 kB Active: 120944 kB Inactive: 59380 kB HighTotal: 131008 kB HighFree: 3780 kB LowTotal: 903652 kB LowFree: 834636 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 10312 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 17:25:48 (client local time) WITH STATUS 1 IN 147.151 SECONDS stats: 8929 7 147.151 1
c This solver internally uses Chaff 2004.11.15 Simplified Unexpected exception : St9bad_alloc
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/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 21954453 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9581/statm): 373 2 364 364 0 9 0 [pid=9581] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos19.opb [startup+10.0011 s] Raw data (loadavg): 1.08 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 165 0 0 0 993 4 0 0 25 0 1 0 21954453 1806336 146 4294967295 134512640 135987407 3221224560 3221221952 134616293 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9581/statm): 441 146 364 364 0 77 0 [pid=9581] vsize: 1764 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 1764 [startup+20.0018 s] Raw data (loadavg): 1.06 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 16079 0 0 0 1949 44 0 0 25 0 1 0 21954453 52101120 9620 4294967295 134512640 135987407 3221224560 3221221904 134612687 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9581/statm): 12720 9620 364 364 0 12356 0 [pid=9581] vsize: 50880 Current children cumulated CPU time (s) 19.93 Current children cumulated vsize (Kb) 50880 [startup+30.0014 s] Raw data (loadavg): 1.05 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 34591 0 0 0 2900 88 0 0 25 0 1 0 21954453 105791488 21541 4294967295 134512640 135987407 3221224560 3221221760 135141362 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 25828 21541 364 364 0 25464 0 [pid=9581] vsize: 103312 Current children cumulated CPU time (s) 29.88 Current children cumulated vsize (Kb) 103312 [startup+40.0021 s] Raw data (loadavg): 1.05 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 54616 0 0 0 3847 139 0 0 25 0 1 0 21954453 222670848 38039 4294967295 134512640 135987407 3221224560 3221221296 134856505 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 54363 38042 364 364 0 53999 0 [pid=9581] vsize: 217452 Current children cumulated CPU time (s) 39.86 Current children cumulated vsize (Kb) 217452 [startup+50.0027 s] Raw data (loadavg): 1.04 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 75875 0 0 0 4794 188 0 0 25 0 1 0 21954453 262696960 49657 4294967295 134512640 135987407 3221224560 3221220400 134887487 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 64135 49661 364 364 0 63771 0 [pid=9581] vsize: 256540 Current children cumulated CPU time (s) 49.82 Current children cumulated vsize (Kb) 256540 [startup+60.0023 s] Raw data (loadavg): 1.03 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 87260 0 0 0 5761 219 0 0 25 0 1 0 21954453 269578240 54706 4294967295 134512640 135987407 3221224560 3221220204 135481666 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 65815 54706 364 364 0 65451 0 [pid=9581] vsize: 263260 Current children cumulated CPU time (s) 59.8 Current children cumulated vsize (Kb) 263260 [startup+70.002 s] Raw data (loadavg): 1.03 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 122180 0 0 0 6685 295 0 0 25 0 1 0 21954453 389406720 71052 4294967295 134512640 135987407 3221224560 3221221304 135544177 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 95070 71052 364 364 0 94706 0 [pid=9581] vsize: 380280 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 380280 [startup+80.0316 s] Raw data (loadavg): 1.02 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 133768 0 0 0 7650 327 0 0 25 0 1 0 21954453 409821184 81414 4294967295 134512640 135987407 3221224560 3221221952 134615218 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 100054 81414 364 364 0 99690 0 [pid=9581] vsize: 400216 Current children cumulated CPU time (s) 79.77 Current children cumulated vsize (Kb) 400216 [startup+90.0322 s] Raw data (loadavg): 1.02 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 155852 0 0 0 8595 381 0 0 25 0 1 0 21954453 475021312 91022 4294967295 134512640 135987407 3221224560 3221218848 134866053 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 115972 91022 364 364 0 115608 0 [pid=9581] vsize: 463888 Current children cumulated CPU time (s) 89.76 Current children cumulated vsize (Kb) 463888 [startup+100.032 s] Raw data (loadavg): 1.02 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 166328 0 0 0 9564 410 0 0 25 0 1 0 21954453 490971136 101298 4294967295 134512640 135987407 3221224560 3221222028 134609745 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 119866 101298 364 364 0 119502 0 [pid=9581] vsize: 479464 Current children cumulated CPU time (s) 99.74 Current children cumulated vsize (Kb) 479464 [startup+110.032 s] Raw data (loadavg): 1.01 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 175593 0 0 0 10535 438 0 0 25 0 1 0 21954453 521940992 110387 4294967295 134512640 135987407 3221224560 3221220736 134887887 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 127427 110388 364 364 0 127063 0 [pid=9581] vsize: 509708 Current children cumulated CPU time (s) 109.73 Current children cumulated vsize (Kb) 509708 [startup+120.032 s] Raw data (loadavg): 1.01 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 186100 0 0 0 11497 474 0 0 25 0 1 0 21954453 538025984 120693 4294967295 134512640 135987407 3221224560 3221221296 134856587 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 131354 120693 364 364 0 130990 0 [pid=9581] vsize: 525416 Current children cumulated CPU time (s) 119.71 Current children cumulated vsize (Kb) 525416 [startup+130.032 s] Raw data (loadavg): 1.01 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 247618 0 0 0 12364 600 0 0 25 0 1 0 21954453 767868928 143222 4294967295 134512640 135987407 3221224560 3221219968 135486786 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 187468 143222 364 364 0 187104 0 [pid=9581] vsize: 749872 Current children cumulated CPU time (s) 129.64 Current children cumulated vsize (Kb) 749872 [startup+140.032 s] Raw data (loadavg): 1.01 0.99 0.92 2/55 9581 Raw data (/proc/9581/stat): 9581 (pb2sat) R 9580 9581 4060 0 -1 0 257939 0 0 0 13335 627 0 0 25 0 1 0 21954453 796323840 153363 4294967295 134512640 135987407 3221224560 3221180300 134677714 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9581/statm): 194415 153363 364 364 0 194051 0 [pid=9581] vsize: 777660 Current children cumulated CPU time (s) 139.62 Current children cumulated vsize (Kb) 777660 One traced child (pid=9581) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 147.555 CPU time (s): 147.151 CPU user time (s): 140.453 CPU system time (s): 6.69798 CPU usage (%): 99.726 Max. virtual memory (cumulated for all children) (Kb): 777660
ERROR: no interpretation found !