Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ir98.opb |
MD5SUM | fb418db515bc70c21d294b6cce4dc63f |
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 | 31 |
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 | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 83886080000000 |
Number of bits of the biggest number in a constraint | 47 |
Biggest sum of numbers in a constraint | 400587756783443 |
Number of bits of the biggest sum of numbers | 49 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 7287 |
Total number of constraints | 6560 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 6451 |
Number of constraints which are nor clauses,nor cardinality constraints | 109 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 6062 |
LAUNCH ON wulflinc12 THE 2005-09-23 17:35:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8958 boxname=wulflinc12 idbench=754 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fb418db515bc70c21d294b6cce4dc63f /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-blp-ir98.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-blp-ir98.opb IDLAUNCH: 8958 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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 : 2 cpu MHz : 451.191 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: 938740 kB Buffers: 6268 kB Cached: 69960 kB SwapCached: 0 kB Active: 23244 kB Inactive: 55848 kB HighTotal: 131008 kB HighFree: 79016 kB LowTotal: 903652 kB LowFree: 859724 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 11228 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 17:37:42 (client local time) WITH STATUS 1 IN 104.396 SECONDS stats: 8958 7 104.396 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/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22034796 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 373 2 364 364 0 9 0 [pid=9986] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-blp-ir98.opb [startup+10.002 s] Raw data (loadavg): 0.93 0.94 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 23916 0 0 0 938 58 0 0 25 0 1 0 22034796 72306688 12833 4294967295 134512640 135987407 3221224560 3221221952 134616362 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 17653 12833 364 364 0 17289 0 [pid=9986] vsize: 70612 Current children cumulated CPU time (s) 9.96 Current children cumulated vsize (Kb) 70612 [startup+20.0029 s] Raw data (loadavg): 0.94 0.94 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 50153 0 0 0 1875 119 0 0 25 0 1 0 22034796 159526912 27865 4294967295 134512640 135987407 3221224560 3220762048 134637876 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 38947 27865 364 364 0 38583 0 [pid=9986] vsize: 155788 Current children cumulated CPU time (s) 19.94 Current children cumulated vsize (Kb) 155788 [startup+30.0027 s] Raw data (loadavg): 0.95 0.94 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 89652 0 0 0 2787 204 0 0 25 0 1 0 22034796 275992576 45158 4294967295 134512640 135987407 3221224560 3221054868 134931021 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 67381 45158 364 364 0 67017 0 [pid=9986] vsize: 269524 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 269524 [startup+40.0036 s] Raw data (loadavg): 0.95 0.94 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 103251 0 0 0 3750 241 0 0 25 0 1 0 22034796 313466880 58532 4294967295 134512640 135987407 3221224560 3220999072 134854984 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 76530 58532 364 364 0 76166 0 [pid=9986] vsize: 306120 Current children cumulated CPU time (s) 39.91 Current children cumulated vsize (Kb) 306120 [startup+50.0044 s] Raw data (loadavg): 0.96 0.94 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 116520 0 0 0 4717 273 0 0 25 0 1 0 22034796 318652416 71584 4294967295 134512640 135987407 3221224560 3219387760 134802906 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 77796 71584 364 364 0 77432 0 [pid=9986] vsize: 311184 Current children cumulated CPU time (s) 49.9 Current children cumulated vsize (Kb) 311184 [startup+60.0043 s] Raw data (loadavg): 0.97 0.94 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 182892 0 0 0 5571 413 0 0 25 0 1 0 22034796 559153152 93781 4294967295 134512640 135987407 3221224560 3219736192 134802822 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 136512 93781 364 364 0 136148 0 [pid=9986] vsize: 546048 Current children cumulated CPU time (s) 59.84 Current children cumulated vsize (Kb) 546048 [startup+70.0051 s] Raw data (loadavg): 0.97 0.95 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 200440 0 0 0 6528 453 0 0 25 0 1 0 22034796 621498368 111105 4294967295 134512640 135987407 3221224560 3219778400 134856382 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 151733 111105 364 364 0 151369 0 [pid=9986] vsize: 606932 Current children cumulated CPU time (s) 69.81 Current children cumulated vsize (Kb) 606932 [startup+80.006 s] Raw data (loadavg): 0.98 0.95 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 220355 0 0 0 7482 497 0 0 25 0 1 0 22034796 654614528 130768 4294967295 134512640 135987407 3221224560 3219596000 134877983 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 159818 130768 364 364 0 159454 0 [pid=9986] vsize: 639272 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 639272 [startup+90.0068 s] Raw data (loadavg): 0.98 0.95 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 239584 0 0 0 8439 537 0 0 25 0 1 0 22034796 685568000 149748 4294967295 134512640 135987407 3221224560 3219201292 135482121 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 167375 149748 364 364 0 167011 0 [pid=9986] vsize: 669500 Current children cumulated CPU time (s) 89.76 Current children cumulated vsize (Kb) 669500 [startup+100.007 s] Raw data (loadavg): 0.98 0.95 0.93 2/55 9986 Raw data (/proc/9986/stat): 9986 (pb2sat) R 9985 9986 4060 0 -1 0 256486 0 0 0 9396 578 0 0 25 0 1 0 22034796 715542528 166419 4294967295 134512640 135987407 3221224560 3221222852 135479922 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9986/statm): 174693 166419 364 364 0 174329 0 [pid=9986] vsize: 698772 Current children cumulated CPU time (s) 99.74 Current children cumulated vsize (Kb) 698772 One traced child (pid=9986) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 104.661 CPU time (s): 104.396 CPU user time (s): 98.2751 CPU system time (s): 6.12107 CPU usage (%): 99.7469 Max. virtual memory (cumulated for all children) (Kb): 698772
ERROR: no interpretation found !