Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-fast0507.opb |
MD5SUM | 2854384016ebafb26c8bfb47f81aee87 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63009 |
Biggest coefficient in the objective function | 2 |
Number of bits for the biggest coefficient in the objective function | 2 |
Sum of the numbers in the objective function | 122425 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 2 |
Number of bits of the biggest number in a constraint | 2 |
Biggest sum of numbers in a constraint | 122425 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.19 |
Number of variables | 63009 |
Total number of constraints | 63516 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63009 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 7753 |
LAUNCH ON wulflinc9 THE 2005-09-23 16:48:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8829 boxname=wulflinc9 idbench=625 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-fast0507.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-fast0507.opb IDLAUNCH: 8829 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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.053 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: 901576 kB Buffers: 12628 kB Cached: 102836 kB SwapCached: 0 kB Active: 62956 kB Inactive: 55436 kB HighTotal: 131008 kB HighFree: 25004 kB LowTotal: 903652 kB LowFree: 876572 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 9108 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 16:52:34 (client local time) WITH STATUS 1 IN 234.818 SECONDS stats: 8829 7 234.818 1
c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 122425 c big objective detected c trying from 0 to 511 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/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21753371 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 373 2 364 364 0 9 0 [pid=9748] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-fast0507.opb [startup+10.0022 s] Raw data (loadavg): 0.92 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 2127 0 0 0 991 7 0 0 25 0 1 0 21753371 8556544 1448 4294967295 134512640 135987407 3221224560 3221221296 134856445 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 2089 1448 364 364 0 1725 0 [pid=9748] vsize: 8356 Current children cumulated CPU time (s) 9.98 Current children cumulated vsize (Kb) 8356 [startup+20.003 s] Raw data (loadavg): 0.93 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 2776 0 0 0 1988 9 0 0 25 0 1 0 21753371 10043392 2085 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 2452 2085 364 364 0 2088 0 [pid=9748] vsize: 9808 Current children cumulated CPU time (s) 19.97 Current children cumulated vsize (Kb) 9808 [startup+30.0038 s] Raw data (loadavg): 0.94 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 4233 0 0 0 2985 12 0 0 25 0 1 0 21753371 15224832 2797 4294967295 134512640 135987407 3221224560 3221221744 134536160 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 3717 2797 364 364 0 3353 0 [pid=9748] vsize: 14868 Current children cumulated CPU time (s) 29.97 Current children cumulated vsize (Kb) 14868 [startup+40.0045 s] Raw data (loadavg): 0.95 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 4518 0 0 0 3985 12 0 0 25 0 1 0 21753371 15900672 3076 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 3882 3076 364 364 0 3518 0 [pid=9748] vsize: 15528 Current children cumulated CPU time (s) 39.97 Current children cumulated vsize (Kb) 15528 [startup+50.0053 s] Raw data (loadavg): 0.96 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 4786 0 0 0 4984 13 0 0 25 0 1 0 21753371 16576512 3340 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 4047 3340 364 364 0 3683 0 [pid=9748] vsize: 16188 Current children cumulated CPU time (s) 49.97 Current children cumulated vsize (Kb) 16188 [startup+60.0061 s] Raw data (loadavg): 0.96 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 5018 0 0 0 5983 14 0 0 25 0 1 0 21753371 17252352 3568 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 4212 3568 364 364 0 3848 0 [pid=9748] vsize: 16848 Current children cumulated CPU time (s) 59.97 Current children cumulated vsize (Kb) 16848 [startup+70.0059 s] Raw data (loadavg): 0.97 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 5233 0 0 0 6983 15 0 0 25 0 1 0 21753371 17793024 3780 4294967295 134512640 135987407 3221224560 3221221872 134555870 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 4344 3780 364 364 0 3980 0 [pid=9748] vsize: 17376 Current children cumulated CPU time (s) 69.98 Current children cumulated vsize (Kb) 17376 [startup+80.0067 s] Raw data (loadavg): 0.97 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 5433 0 0 0 7982 16 0 0 25 0 1 0 21753371 18333696 3976 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 4476 3976 364 364 0 4112 0 [pid=9748] vsize: 17904 Current children cumulated CPU time (s) 79.98 Current children cumulated vsize (Kb) 17904 [startup+90.0074 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 5621 0 0 0 8981 16 0 0 25 0 1 0 21753371 18739200 4161 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 4575 4161 364 364 0 4211 0 [pid=9748] vsize: 18300 Current children cumulated CPU time (s) 89.97 Current children cumulated vsize (Kb) 18300 [startup+100.007 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 5798 0 0 0 9980 17 0 0 25 0 1 0 21753371 19144704 4335 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 4674 4335 364 364 0 4310 0 [pid=9748] vsize: 18696 Current children cumulated CPU time (s) 99.97 Current children cumulated vsize (Kb) 18696 [startup+110.008 s] Raw data (loadavg): 0.98 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 6604 0 0 0 10976 20 0 0 25 0 1 0 21753371 22274048 5140 4294967295 134512640 135987407 3221224560 3221221756 134535944 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 5438 5140 364 364 0 5074 0 [pid=9748] vsize: 21752 Current children cumulated CPU time (s) 109.96 Current children cumulated vsize (Kb) 21752 [startup+120.009 s] Raw data (loadavg): 0.98 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 6800 0 0 0 11971 24 0 0 25 0 1 0 21753371 23199744 5336 4294967295 134512640 135987407 3221224560 3221221872 134555863 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 5664 5336 364 364 0 5300 0 [pid=9748] vsize: 22656 Current children cumulated CPU time (s) 119.95 Current children cumulated vsize (Kb) 22656 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 6967 0 0 0 12967 26 0 0 25 0 1 0 21753371 24260608 5503 4294967295 134512640 135987407 3221224560 3221221644 134669203 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 5923 5503 364 364 0 5559 0 [pid=9748] vsize: 23692 Current children cumulated CPU time (s) 129.93 Current children cumulated vsize (Kb) 23692 [startup+140.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 49714 0 0 0 13860 127 0 0 25 0 1 0 21753371 166600704 33152 4294967295 134512640 135987407 3221224560 3207022668 135485045 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 40674 33152 364 364 0 40310 0 [pid=9748] vsize: 162696 Current children cumulated CPU time (s) 139.87 Current children cumulated vsize (Kb) 162696 [startup+150.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 79156 0 0 0 14785 200 0 0 25 0 1 0 21753371 313643008 56122 4294967295 134512640 135987407 3221224560 3214428176 134856702 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/9748/statm): 76573 56124 364 364 0 76209 0 [pid=9748] vsize: 306292 Current children cumulated CPU time (s) 149.85 Current children cumulated vsize (Kb) 306292 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 118604 0 0 0 15691 290 0 0 25 0 1 0 21753371 402898944 73488 4294967295 134512640 135987407 3221224560 3221162680 134533885 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 98364 73488 364 364 0 98000 0 [pid=9748] vsize: 393456 Current children cumulated CPU time (s) 159.81 Current children cumulated vsize (Kb) 393456 [startup+170.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 139080 0 0 0 16640 338 0 0 25 0 1 0 21753371 429256704 93718 4294967295 134512640 135987407 3221224560 3221217532 135480735 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 104799 93718 364 364 0 104435 0 [pid=9748] vsize: 419196 Current children cumulated CPU time (s) 169.78 Current children cumulated vsize (Kb) 419196 [startup+180.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 183077 0 0 0 17542 432 0 0 25 0 1 0 21753371 570040320 118092 4294967295 134512640 135987407 3221224560 3206609624 134537317 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 139170 118092 364 364 0 138806 0 [pid=9748] vsize: 556680 Current children cumulated CPU time (s) 179.74 Current children cumulated vsize (Kb) 556680 [startup+190.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 221894 0 0 0 18450 522 0 0 25 0 1 0 21753371 722235392 132165 4294967295 134512640 135987407 3221224560 3212814144 134639904 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 176327 132165 364 364 0 175963 0 [pid=9748] vsize: 705308 Current children cumulated CPU time (s) 189.72 Current children cumulated vsize (Kb) 705308 [startup+200.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 241913 0 0 0 19406 564 0 0 25 0 1 0 21753371 748052480 151946 4294967295 134512640 135987407 3221224560 3215656992 134861966 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 182630 151946 364 364 0 182266 0 [pid=9748] vsize: 730520 Current children cumulated CPU time (s) 199.7 Current children cumulated vsize (Kb) 730520 [startup+210.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 261587 0 0 0 20360 607 0 0 25 0 1 0 21753371 773464064 171389 4294967295 134512640 135987407 3221224560 3220606688 134537472 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 188834 171389 364 364 0 188470 0 [pid=9748] vsize: 755336 Current children cumulated CPU time (s) 209.67 Current children cumulated vsize (Kb) 755336 [startup+220.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 277605 0 0 0 21320 645 0 0 25 0 1 0 21753371 845152256 187215 4294967295 134512640 135987407 3221224560 3218029568 134537491 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 206336 187215 364 364 0 205972 0 [pid=9748] vsize: 825344 Current children cumulated CPU time (s) 219.65 Current children cumulated vsize (Kb) 825344 [startup+230.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 9748 Raw data (/proc/9748/stat): 9748 (pb2sat) R 9747 9748 4060 0 -1 0 289857 0 0 0 22290 672 0 0 25 0 1 0 21753371 865153024 199088 4294967295 134512640 135987407 3221224560 3221223424 134795939 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/9748/statm): 211219 199088 364 364 0 210855 0 [pid=9748] vsize: 844876 Current children cumulated CPU time (s) 229.62 Current children cumulated vsize (Kb) 844876 One traced child (pid=9748) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 235.204 CPU time (s): 234.818 CPU user time (s): 227.683 CPU system time (s): 7.13492 CPU usage (%): 99.8358 Max. virtual memory (cumulated for all children) (Kb): 844876
ERROR: no interpretation found !