| Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scorpion.opb |
| MD5SUM | 407688f2ee1c26681a4ae06671027d6f |
| 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 | 5640 |
| Biggest coefficient in the objective function | 10536091648 |
| Number of bits for the biggest coefficient in the objective function | 34 |
| Sum of the numbers in the objective function | 589543467975 |
| Number of bits of the sum of numbers in the objective function | 40 |
| Biggest number in a constraint | 32768000000 |
| Number of bits of the biggest number in a constraint | 35 |
| Biggest sum of numbers in a constraint | 589543467975 |
| Number of bits of the biggest sum of numbers | 40 |
| Best result obtained on this benchmark | |
| Best CPU time to get the best result obtained on this benchmark | |
| Number of variables | 7160 |
| Total number of constraints | 388 |
| 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 | 388 |
| Minimum length of a constraint | 20 |
| Maximum length of a constraint | 400 |
LAUNCH ON wulflinc32 THE 2005-09-23 17:48:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9049 boxname=wulflinc32 idbench=845 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 407688f2ee1c26681a4ae06671027d6f /oldhome/oroussel/tmp/wulflinc32/normalized-mps-v2-13-7-scorpion.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc32/normalized-mps-v2-13-7-scorpion.opb IDLAUNCH: 9049 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.145 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.145 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: 1034724 kB MemFree: 920996 kB Buffers: 15296 kB Cached: 78544 kB SwapCached: 0 kB Active: 42660 kB Inactive: 54096 kB HighTotal: 131072 kB HighFree: 48096 kB LowTotal: 903652 kB LowFree: 872900 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6988 kB Slab: 11344 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 17:49:29 (client local time) WITH STATUS 0 IN 86.8908 SECONDS stats: 9049 7 86.8908 0
c This solver internally uses Chaff 2004.11.15 Simplified *** glibc detected *** pb2sat: free(): invalid pointer: 0x109a1ab8 *** ======= Backtrace: ========= [0x8133e0b] [0x81342a2] [0x806658b] [0x8054311] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8054360] [0x8056e70] [0x8057c4e] [0x805fe7b] [0x804a6f2] [0x8110e79] [0x8048141] ======= Memory map: ======== 08048000-081b1000 r-xp 00000000 00:14 3276939 /oldhome/oroussel/solvers/pb2sat 081b1000-081b4000 rw-p 00168000 00:14 3276939 /oldhome/oroussel/solvers/pb2sat 081b4000-10a2f000 rw-p 081b4000 00:00 0 40000000-40001000 rw-p 40000000 00:00 0 40024000-40045000 rw-p 40024000 00:00 0 4e2e7000-4eae8000 rw-p 4e2e7000 00:00 0 526e8000-5b6e9000 rw-p 400ca000 00:00 0 5b700000-5b724000 rw-p 5b700000 00:00 0 5b724000-5b800000 ---p 5b724000 00:00 0 5c6ea000-70eec000 rw-p 5c6ea000 00:00 0 bfff3000-c0000000 rw-p bfff3000 00:00 0 ffffe000-fffff000 ---p 00000000 00:00 0
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/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22065634 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 373 2 364 364 0 9 0 [pid=8812] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc32/normalized-mps-v2-13-7-scorpion.opb [startup+10.0026 s] Raw data (loadavg): 0.92 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 27835 0 0 0 932 65 0 0 25 0 1 0 22065634 83030016 16688 4294967295 134512640 135987407 3221224560 3221212312 134636909 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 20271 16688 364 364 0 19907 0 [pid=8812] vsize: 81084 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 81084 [startup+20.0033 s] Raw data (loadavg): 0.94 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 55482 0 0 0 1863 132 0 0 25 0 1 0 22065634 160202752 33093 4294967295 134512640 135987407 3221224560 3221192448 134537552 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 39112 33093 364 364 0 38748 0 [pid=8812] vsize: 156448 Current children cumulated CPU time (s) 19.95 Current children cumulated vsize (Kb) 156448 [startup+30.0041 s] Raw data (loadavg): 0.95 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 95023 0 0 0 2779 214 0 0 25 0 1 0 22065634 310222848 50420 4294967295 134512640 135987407 3221224560 3221192320 134856405 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 75738 50420 364 364 0 75374 0 [pid=8812] vsize: 302952 Current children cumulated CPU time (s) 29.93 Current children cumulated vsize (Kb) 302952 [startup+40.0049 s] Raw data (loadavg): 0.95 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 111984 0 0 0 3738 255 0 0 25 0 1 0 22065634 315494400 67092 4294967295 134512640 135987407 3221224560 3221221184 134636933 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 77025 67092 364 364 0 76661 0 [pid=8812] vsize: 308100 Current children cumulated CPU time (s) 39.93 Current children cumulated vsize (Kb) 308100 [startup+50.0056 s] Raw data (loadavg): 0.96 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 165800 0 0 0 4619 368 0 0 25 0 1 0 22065634 645173248 101285 4294967295 134512640 135987407 3221224560 3221211664 134887487 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 157513 101285 364 364 0 157149 0 [pid=8812] vsize: 630052 Current children cumulated CPU time (s) 49.87 Current children cumulated vsize (Kb) 630052 [startup+60.0064 s] Raw data (loadavg): 0.97 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 191091 0 0 0 5557 430 0 0 25 0 1 0 22065634 586035200 101794 4294967295 134512640 135987407 3221224560 3221192016 134862265 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 143075 101794 364 364 0 142711 0 [pid=8812] vsize: 572300 Current children cumulated CPU time (s) 59.87 Current children cumulated vsize (Kb) 572300 [startup+70.0072 s] Raw data (loadavg): 0.97 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 206373 0 0 0 6526 461 0 0 25 0 1 0 22065634 590495744 116817 4294967295 134512640 135987407 3221224560 3221194172 134636908 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 144164 116817 364 364 0 143800 0 [pid=8812] vsize: 576656 Current children cumulated CPU time (s) 69.87 Current children cumulated vsize (Kb) 576656 [startup+80.008 s] Raw data (loadavg): 0.97 0.98 0.97 2/55 8812 Raw data (/proc/8812/stat): 8812 (pb2sat) R 8811 8812 4005 0 -1 0 221672 0 0 0 7492 495 0 0 25 0 1 0 22065634 595091456 131859 4294967295 134512640 135987407 3221224560 3221195792 134537477 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8812/statm): 145286 131859 364 364 0 144922 0 [pid=8812] vsize: 581144 Current children cumulated CPU time (s) 79.87 Current children cumulated vsize (Kb) 581144 open syscall for file /dev/tty open syscall for file /proc/self/maps One traced child (pid=8812) ended because it received signal 6 (SIGABRT) All traced children have exited ! Game is over. Child ended because it received signal 6 (SIGABRT) Real time (s): 87.0316 CPU time (s): 86.8908 CPU user time (s): 81.4836 CPU system time (s): 5.40718 CPU usage (%): 99.8382 Max. virtual memory (cumulated for all children) (Kb): 630052
ERROR: no interpretation found !