Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-momentum2.opb |
MD5SUM | 46da43c96f006f296bc8287cf17c977a |
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 | 24130 |
Biggest coefficient in the objective function | 655360000 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 3638660312 |
Number of bits of the sum of numbers in the objective function | 32 |
Biggest number in a constraint | 1024000000000000013606456393728 |
Number of bits of the biggest number in a constraint | 100 |
Biggest sum of numbers in a constraint | 3743132712137090149495810818048 |
Number of bits of the biggest sum of numbers | 102 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 137.696 |
Number of variables | 25930 |
Total number of constraints | 27909 |
Number of constraints which are clauses | 10362 |
Number of constraints which are cardinality constraints (but not clauses) | 1921 |
Number of constraints which are nor clauses,nor cardinality constraints | 15626 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 913 |
LAUNCH ON wulflinc23 THE 2005-09-23 16:37:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8784 boxname=wulflinc23 idbench=580 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 46da43c96f006f296bc8287cf17c977a /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-momentum2.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-momentum2.opb IDLAUNCH: 8784 /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: 834284 kB Buffers: 14408 kB Cached: 166948 kB SwapCached: 0 kB Active: 134480 kB Inactive: 49796 kB HighTotal: 131008 kB HighFree: 3752 kB LowTotal: 903652 kB LowFree: 830532 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 8 kB Writeback: 0 kB Mapped: 6980 kB Slab: 10456 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 16:39:31 (client local time) WITH STATUS 0 IN 96.3124 SECONDS stats: 8784 7 96.3124 0
c This solver internally uses Chaff 2004.11.15 Simplified s UNKNOWN
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/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21681644 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 373 2 364 364 0 9 0 [pid=8624] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-momentum2.opb [startup+10.0018 s] Raw data (loadavg): 0.95 0.94 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 3387 0 0 0 991 7 0 0 25 0 1 0 21681644 11878400 2541 4294967295 134512640 135987407 3221224560 3221221952 134615172 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 2900 2541 364 364 0 2536 0 [pid=8624] vsize: 11600 Current children cumulated CPU time (s) 9.98 Current children cumulated vsize (Kb) 11600 [startup+20.0024 s] Raw data (loadavg): 0.96 0.94 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 26990 0 0 0 1939 57 0 0 25 0 1 0 21681644 84508672 15720 4294967295 134512640 135987407 3221224560 3221208496 134878060 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8624/statm): 20632 15720 364 364 0 20268 0 [pid=8624] vsize: 82528 Current children cumulated CPU time (s) 19.96 Current children cumulated vsize (Kb) 82528 [startup+30.002 s] Raw data (loadavg): 0.96 0.94 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 53425 0 0 0 2874 121 0 0 25 0 1 0 21681644 160841728 30896 4294967295 134512640 135987407 3221224560 3221209168 134878060 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 39268 30896 364 364 0 38904 0 [pid=8624] vsize: 157072 Current children cumulated CPU time (s) 29.95 Current children cumulated vsize (Kb) 157072 [startup+40.0027 s] Raw data (loadavg): 0.97 0.94 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 92345 0 0 0 3787 206 0 0 25 0 1 0 21681644 274731008 47572 4294967295 134512640 135987407 3221224560 3221208112 134856702 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 67073 47572 364 364 0 66709 0 [pid=8624] vsize: 268292 Current children cumulated CPU time (s) 39.93 Current children cumulated vsize (Kb) 268292 [startup+50.0033 s] Raw data (loadavg): 0.97 0.94 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 106854 0 0 0 4753 239 0 0 25 0 1 0 21681644 314695680 61804 4294967295 134512640 135987407 3221224560 3221208892 134637015 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 76830 61804 364 364 0 76466 0 [pid=8624] vsize: 307320 Current children cumulated CPU time (s) 49.92 Current children cumulated vsize (Kb) 307320 [startup+60.003 s] Raw data (loadavg): 0.98 0.94 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 147134 0 0 0 5671 321 0 0 25 0 1 0 21681644 437329920 82429 4294967295 134512640 135987407 3221224560 3221208096 134866032 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 106770 82429 364 364 0 106406 0 [pid=8624] vsize: 427080 Current children cumulated CPU time (s) 59.92 Current children cumulated vsize (Kb) 427080 [startup+70.0346 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 185220 0 0 0 6585 406 0 0 25 0 1 0 21681644 544890880 95685 4294967295 134512640 135987407 3221224560 3221209220 134641750 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 133030 95685 364 364 0 132666 0 [pid=8624] vsize: 532120 Current children cumulated CPU time (s) 69.91 Current children cumulated vsize (Kb) 532120 [startup+80.0352 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 197955 0 0 0 7552 438 0 0 25 0 1 0 21681644 583831552 108175 4294967295 134512640 135987407 3221224560 3221207940 134639876 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 142537 108175 364 364 0 142173 0 [pid=8624] vsize: 570148 Current children cumulated CPU time (s) 79.9 Current children cumulated vsize (Kb) 570148 [startup+90.0359 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) R 8623 8624 4060 0 -1 0 213396 0 0 0 8519 472 0 0 25 0 1 0 21681644 590360576 123321 4294967295 134512640 135987407 3221224560 3221209312 134887273 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8624/statm): 144131 123321 364 364 0 143767 0 [pid=8624] vsize: 576524 Current children cumulated CPU time (s) 89.91 Current children cumulated vsize (Kb) 576524 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+96.1243 s] Raw data (loadavg): 0.99 0.95 0.92 1/55 8624 Raw data (/proc/8624/stat): 8624 (pb2sat) T 8623 8624 4060 0 -1 0 259527 0 0 0 9033 560 0 0 25 0 1 0 21681644 943812608 167926 4294967295 134512640 135987407 3221224560 3221208844 135635874 0 0 5 16384 3222434794 0 0 17 1 0 0 Raw data (/proc/8624/statm): 230423 167926 364 364 0 230059 0 [pid=8624] vsize: 921692 Current children cumulated CPU time (s) 95.93 Current children cumulated vsize (Kb) 921692 Sending SIGTERM to -8624 Sleeping 2 seconds Sending SIGKILL to -8624 One traced child (pid=8624) ended because it received signal 9 (SIGKILL) All traced children have exited ! Game is over. Child ended because it received signal 9 (SIGKILL) Real time (s): 98.4722 CPU time (s): 96.3124 CPU user time (s): 90.3653 CPU system time (s): 5.9471 CPU usage (%): 97.8067 Max. virtual memory (cumulated for all children) (Kb): 921692
ERROR: no interpretation found !