Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-momentum3.opb |
MD5SUM | bdf0df6b57384ca8a37c1ce2e87cfc07 |
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 | 67174 |
Biggest coefficient in the objective function | 163840000 |
Number of bits for the biggest coefficient in the objective function | 28 |
Sum of the numbers in the objective function | 1696626095 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 1280000000000000115964116992 |
Number of bits of the biggest number in a constraint | 91 |
Biggest sum of numbers in a constraint | 3721289892401349417752330240 |
Number of bits of the biggest sum of numbers | 92 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 71194 |
Total number of constraints | 70153 |
Number of constraints which are clauses | 6081 |
Number of constraints which are cardinality constraints (but not clauses) | 7185 |
Number of constraints which are nor clauses,nor cardinality constraints | 56887 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 814 |
LAUNCH ON wulflinc4 THE 2005-09-23 18:15:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9169 boxname=wulflinc4 idbench=965 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: bdf0df6b57384ca8a37c1ce2e87cfc07 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-momentum3.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-momentum3.opb IDLAUNCH: 9169 /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: 658176 kB Buffers: 12948 kB Cached: 345276 kB SwapCached: 0 kB Active: 279568 kB Inactive: 81556 kB HighTotal: 131008 kB HighFree: 3780 kB LowTotal: 903652 kB LowFree: 654396 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 20 kB Writeback: 0 kB Mapped: 6980 kB Slab: 9700 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 18:19:35 (client local time) WITH STATUS 1 IN 222.316 SECONDS stats: 9169 7 222.316 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/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 18 0 0 0 0 0 0 0 19 0 1 0 22290848 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 373 2 364 364 0 9 0 [pid=10315] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-momentum3.opb [startup+10.0034 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 2496 0 0 0 992 7 0 0 25 0 1 0 22290848 9367552 1810 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 2287 1810 364 364 0 1923 0 [pid=10315] vsize: 9148 Current children cumulated CPU time (s) 9.99 Current children cumulated vsize (Kb) 9148 [startup+20.0043 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4189 0 0 0 1988 11 0 0 25 0 1 0 22290848 15360000 2755 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 3750 2755 364 364 0 3386 0 [pid=10315] vsize: 15000 Current children cumulated CPU time (s) 19.99 Current children cumulated vsize (Kb) 15000 [startup+30.0052 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4426 0 0 0 2987 11 0 0 25 0 1 0 22290848 15765504 2986 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 3849 2986 364 364 0 3485 0 [pid=10315] vsize: 15396 Current children cumulated CPU time (s) 29.98 Current children cumulated vsize (Kb) 15396 [startup+40.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4693 0 0 0 3986 12 0 0 25 0 1 0 22290848 16441344 3249 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10315/statm): 4014 3249 364 364 0 3650 0 [pid=10315] vsize: 16056 Current children cumulated CPU time (s) 39.98 Current children cumulated vsize (Kb) 16056 [startup+50.0069 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4943 0 0 0 4985 13 0 0 25 0 1 0 22290848 17117184 3495 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 4179 3495 364 364 0 3815 0 [pid=10315] vsize: 16716 Current children cumulated CPU time (s) 49.98 Current children cumulated vsize (Kb) 16716 [startup+60.0077 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5176 0 0 0 5985 13 0 0 25 0 1 0 22290848 17657856 3724 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 4311 3724 364 364 0 3947 0 [pid=10315] vsize: 17244 Current children cumulated CPU time (s) 59.98 Current children cumulated vsize (Kb) 17244 [startup+70.0086 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5390 0 0 0 6985 14 0 0 25 0 1 0 22290848 18198528 3935 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 4443 3935 364 364 0 4079 0 [pid=10315] vsize: 17772 Current children cumulated CPU time (s) 69.99 Current children cumulated vsize (Kb) 17772 [startup+80.0085 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5588 0 0 0 7984 14 0 0 25 0 1 0 22290848 18739200 4129 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 4575 4129 364 364 0 4211 0 [pid=10315] vsize: 18300 Current children cumulated CPU time (s) 79.98 Current children cumulated vsize (Kb) 18300 [startup+90.0093 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5775 0 0 0 8983 15 0 0 25 0 1 0 22290848 19279872 4313 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 4707 4313 364 364 0 4343 0 [pid=10315] vsize: 18828 Current children cumulated CPU time (s) 89.98 Current children cumulated vsize (Kb) 18828 [startup+100.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5949 0 0 0 9983 16 0 0 25 0 1 0 22290848 19685376 4485 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 4806 4485 364 364 0 4442 0 [pid=10315] vsize: 19224 Current children cumulated CPU time (s) 99.99 Current children cumulated vsize (Kb) 19224 [startup+110.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 8316 0 0 0 10976 22 0 0 25 0 1 0 22290848 28831744 5374 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 7039 5374 364 364 0 6675 0 [pid=10315] vsize: 28156 Current children cumulated CPU time (s) 109.98 Current children cumulated vsize (Kb) 28156 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 17395 0 0 0 11952 44 0 0 25 0 1 0 22290848 56791040 10448 4294967295 134512640 135987407 3221224560 3221222028 134609743 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 13865 10448 364 364 0 13501 0 [pid=10315] vsize: 55460 Current children cumulated CPU time (s) 119.96 Current children cumulated vsize (Kb) 55460 [startup+130.011 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 44089 0 0 0 12891 103 0 0 25 0 1 0 22290848 137244672 27482 4294967295 134512640 135987407 3221224560 3220978144 134887305 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 33507 27482 364 364 0 33143 0 [pid=10315] vsize: 134028 Current children cumulated CPU time (s) 129.94 Current children cumulated vsize (Kb) 134028 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 82005 0 0 0 13808 182 0 0 25 0 1 0 22290848 297803776 58546 4294967295 134512640 135987407 3221224560 3220998512 134861431 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 72706 58546 364 364 0 72342 0 [pid=10315] vsize: 290824 Current children cumulated CPU time (s) 139.9 Current children cumulated vsize (Kb) 290824 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 111782 0 0 0 14742 246 0 0 25 0 1 0 22290848 370708480 66610 4294967295 134512640 135987407 3221224560 3221039272 134537317 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 90505 66610 364 364 0 90141 0 [pid=10315] vsize: 362020 Current children cumulated CPU time (s) 149.88 Current children cumulated vsize (Kb) 362020 [startup+160.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 132597 0 0 0 15698 288 0 0 25 0 1 0 22290848 400445440 87184 4294967295 134512640 135987407 3221224560 3221019808 134887887 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 97765 87184 364 364 0 97401 0 [pid=10315] vsize: 391060 Current children cumulated CPU time (s) 159.86 Current children cumulated vsize (Kb) 391060 [startup+170.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 176762 0 0 0 16608 372 0 0 25 0 1 0 22290848 541097984 111734 4294967295 134512640 135987407 3221224560 3221012368 134537352 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 132104 111734 364 364 0 131740 0 [pid=10315] vsize: 528416 Current children cumulated CPU time (s) 169.8 Current children cumulated vsize (Kb) 528416 [startup+180.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 216634 0 0 0 17508 471 0 0 25 0 1 0 22290848 695590912 126845 4294967295 134512640 135987407 3221224560 3221030656 134877726 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 169822 126845 364 364 0 169458 0 [pid=10315] vsize: 679288 Current children cumulated CPU time (s) 179.79 Current children cumulated vsize (Kb) 679288 [startup+190.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 235015 0 0 0 18468 509 0 0 25 0 1 0 22290848 720326656 145003 4294967295 134512640 135987407 3221224560 3221024176 134887887 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10315/statm): 175861 145004 364 364 0 175497 0 [pid=10315] vsize: 703444 Current children cumulated CPU time (s) 189.77 Current children cumulated vsize (Kb) 703444 [startup+200.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 254208 0 0 0 19428 548 0 0 25 0 1 0 22290848 745873408 163965 4294967295 134512640 135987407 3221224560 3220990776 134533885 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10315/statm): 182098 163965 364 364 0 181734 0 [pid=10315] vsize: 728392 Current children cumulated CPU time (s) 199.76 Current children cumulated vsize (Kb) 728392 [startup+210.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 269363 0 0 0 20387 580 0 0 25 0 1 0 22290848 817020928 178940 4294967295 134512640 135987407 3221224560 3220994464 134878060 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10315/statm): 199468 178940 364 364 0 199104 0 [pid=10315] vsize: 797872 Current children cumulated CPU time (s) 209.67 Current children cumulated vsize (Kb) 797872 [startup+220.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10315 Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 280275 0 0 0 21343 618 0 0 25 0 1 0 22290848 473493504 115135 4294967295 134512640 135987407 3221224560 3221223224 135477314 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10315/statm): 115599 115135 364 364 0 115235 0 [pid=10315] vsize: 462396 Current children cumulated CPU time (s) 219.61 Current children cumulated vsize (Kb) 462396 One traced child (pid=10315) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 222.711 CPU time (s): 222.316 CPU user time (s): 215.884 CPU system time (s): 6.43202 CPU usage (%): 99.8227 Max. virtual memory (cumulated for all children) (Kb): 797872
ERROR: no interpretation found !