Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scsd1.opb |
MD5SUM | 0d161f98f04bb13a3a82ce824c7be961 |
Bench Category | optimization, big integers (OPTBIGINT) |
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 | 15200 |
Biggest coefficient in the objective function | 262144000000000 |
Number of bits for the biggest coefficient in the objective function | 48 |
Sum of the numbers in the objective function | 183748611699849900 |
Number of bits of the sum of numbers in the objective function | 58 |
Biggest number in a constraint | 262144000000000 |
Number of bits of the biggest number in a constraint | 48 |
Biggest sum of numbers in a constraint | 183748611699849900 |
Number of bits of the biggest sum of numbers | 58 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 15200 |
Total number of constraints | 77 |
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 | 77 |
Minimum length of a constraint | 400 |
Maximum length of a constraint | 1000 |
LAUNCH ON wulflinc21 THE 2005-09-23 17:48:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9051 boxname=wulflinc21 idbench=847 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 0d161f98f04bb13a3a82ce824c7be961 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-scsd1.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-scsd1.opb IDLAUNCH: 9051 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.188 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.188 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: 925960 kB Buffers: 14132 kB Cached: 76240 kB SwapCached: 0 kB Active: 47540 kB Inactive: 45776 kB HighTotal: 131008 kB HighFree: 50372 kB LowTotal: 903652 kB LowFree: 875588 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6984 kB Slab: 9692 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 17:50:14 (client local time) WITH STATUS 1 IN 103.436 SECONDS stats: 9051 7 103.436 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/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22107955 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 373 10 364 364 0 9 0 [pid=10277] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-scsd1.opb [startup+10.0024 s] Raw data (loadavg): 0.90 0.94 0.90 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 23216 0 0 0 948 48 0 0 25 0 1 0 22107955 72552448 15166 4294967295 134512640 135987407 3221224560 3221065264 134865969 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 17713 15166 364 364 0 17349 0 [pid=10277] vsize: 70852 Current children cumulated CPU time (s) 9.96 Current children cumulated vsize (Kb) 70852 [startup+20.0031 s] Raw data (loadavg): 0.92 0.94 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 56854 0 0 0 1876 118 0 0 25 0 1 0 22107955 189976576 34505 4294967295 134512640 135987407 3221224560 3221063372 134636950 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 46381 34505 364 364 0 46017 0 [pid=10277] vsize: 185524 Current children cumulated CPU time (s) 19.94 Current children cumulated vsize (Kb) 185524 [startup+30.0028 s] Raw data (loadavg): 0.93 0.94 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 89329 0 0 0 2811 179 0 0 25 0 1 0 22107955 275824640 56905 4294967295 134512640 135987407 3221224560 3221062028 134636975 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 67340 56905 364 364 0 66976 0 [pid=10277] vsize: 269360 Current children cumulated CPU time (s) 29.9 Current children cumulated vsize (Kb) 269360 [startup+40.0035 s] Raw data (loadavg): 0.94 0.94 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 118609 0 0 0 3748 241 0 0 25 0 1 0 22107955 383365120 73676 4294967295 134512640 135987407 3221224560 3221063740 135479985 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 93595 73676 364 364 0 93231 0 [pid=10277] vsize: 374380 Current children cumulated CPU time (s) 39.89 Current children cumulated vsize (Kb) 374380 [startup+50.0042 s] Raw data (loadavg): 0.95 0.94 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 153068 0 0 0 4678 306 0 0 25 0 1 0 22107955 579698688 107090 4294967295 134512640 135987407 3221224560 3221065280 134856581 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 141528 107090 364 364 0 141164 0 [pid=10277] vsize: 566112 Current children cumulated CPU time (s) 49.84 Current children cumulated vsize (Kb) 566112 [startup+60.0049 s] Raw data (loadavg): 0.95 0.95 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 184142 0 0 0 5607 374 0 0 25 0 1 0 22107955 754941952 118491 4294967295 134512640 135987407 3221224560 3221061104 134887489 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 184312 118491 364 364 0 183948 0 [pid=10277] vsize: 737248 Current children cumulated CPU time (s) 59.81 Current children cumulated vsize (Kb) 737248 [startup+70.0056 s] Raw data (loadavg): 0.96 0.95 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 223696 0 0 0 6522 458 0 0 25 0 1 0 22107955 710402048 133258 4294967295 134512640 135987407 3221224560 3221062880 134877631 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 173438 133258 364 364 0 173074 0 [pid=10277] vsize: 693752 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 693752 [startup+80.0062 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 240667 0 0 0 7486 492 0 0 25 0 1 0 22107955 734056448 150009 4294967295 134512640 135987407 3221224560 3221061568 134866159 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 179213 150009 364 364 0 178849 0 [pid=10277] vsize: 716852 Current children cumulated CPU time (s) 79.78 Current children cumulated vsize (Kb) 716852 [startup+90.007 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 259827 0 0 0 8449 527 0 0 25 0 1 0 22107955 760557568 168923 4294967295 134512640 135987407 3221224560 3221061888 134876450 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 185683 168923 364 364 0 185319 0 [pid=10277] vsize: 742732 Current children cumulated CPU time (s) 89.76 Current children cumulated vsize (Kb) 742732 [startup+100.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10277 Raw data (/proc/10277/stat): 10277 (pb2sat) R 10276 10277 4059 0 -1 0 272244 0 0 0 9412 563 0 0 25 0 1 0 22107955 469225472 113918 4294967295 134512640 135987407 3221224560 3221223224 135477294 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10277/statm): 114557 113918 364 364 0 114193 0 [pid=10277] vsize: 458228 Current children cumulated CPU time (s) 99.75 Current children cumulated vsize (Kb) 458228 One traced child (pid=10277) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 103.694 CPU time (s): 103.436 CPU user time (s): 97.5652 CPU system time (s): 5.87111 CPU usage (%): 99.7513 Max. virtual memory (cumulated for all children) (Kb): 742732
ERROR: no interpretation found !