Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-fast0507.opb |
MD5SUM | 38504d32a17a57a658eee171614b901e |
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.29 |
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 wulflinc30 THE 2005-09-23 18:04:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9152 boxname=wulflinc30 idbench=948 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 38504d32a17a57a658eee171614b901e /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 9152 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 922884 kB Buffers: 12640 kB Cached: 81608 kB SwapCached: 0 kB Active: 54000 kB Inactive: 43140 kB HighTotal: 131008 kB HighFree: 45416 kB LowTotal: 903652 kB LowFree: 877468 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 9020 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 18:08:48 (client local time) WITH STATUS 1 IN 235.408 SECONDS stats: 9152 7 235.408 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/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22169141 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 373 2 364 364 0 9 0 [pid=10684] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-fast0507.opb [startup+10.0024 s] Raw data (loadavg): 0.93 0.95 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 2139 0 0 0 991 7 0 0 25 0 1 0 22169141 8556544 1459 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 2089 1459 364 364 0 1725 0 [pid=10684] vsize: 8356 Current children cumulated CPU time (s) 9.98 Current children cumulated vsize (Kb) 8356 [startup+20.0032 s] Raw data (loadavg): 0.94 0.95 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 2773 0 0 0 1989 9 0 0 25 0 1 0 22169141 10043392 2082 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 2452 2082 364 364 0 2088 0 [pid=10684] vsize: 9808 Current children cumulated CPU time (s) 19.98 Current children cumulated vsize (Kb) 9808 [startup+30.004 s] Raw data (loadavg): 0.95 0.95 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 4222 0 0 0 2987 11 0 0 25 0 1 0 22169141 15224832 2786 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 3717 2786 364 364 0 3353 0 [pid=10684] vsize: 14868 Current children cumulated CPU time (s) 29.98 Current children cumulated vsize (Kb) 14868 [startup+40.0048 s] Raw data (loadavg): 0.96 0.95 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 4507 0 0 0 3986 11 0 0 25 0 1 0 22169141 15900672 3065 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 3882 3065 364 364 0 3518 0 [pid=10684] vsize: 15528 Current children cumulated CPU time (s) 39.97 Current children cumulated vsize (Kb) 15528 [startup+50.0056 s] Raw data (loadavg): 0.96 0.95 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 4781 0 0 0 4986 12 0 0 25 0 1 0 22169141 16576512 3335 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 4047 3335 364 364 0 3683 0 [pid=10684] vsize: 16188 Current children cumulated CPU time (s) 49.98 Current children cumulated vsize (Kb) 16188 [startup+60.0054 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 5017 0 0 0 5985 13 0 0 25 0 1 0 22169141 17252352 3567 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 4212 3567 364 364 0 3848 0 [pid=10684] vsize: 16848 Current children cumulated CPU time (s) 59.98 Current children cumulated vsize (Kb) 16848 [startup+70.0053 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 5231 0 0 0 6984 13 0 0 25 0 1 0 22169141 17793024 3778 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 4344 3778 364 364 0 3980 0 [pid=10684] vsize: 17376 Current children cumulated CPU time (s) 69.97 Current children cumulated vsize (Kb) 17376 [startup+80.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 10684 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 5429 0 0 0 7984 14 0 0 25 0 1 0 22169141 18198528 3972 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 4443 3972 364 364 0 4079 0 [pid=10684] vsize: 17772 Current children cumulated CPU time (s) 79.98 Current children cumulated vsize (Kb) 17772 [startup+90.0069 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 5614 0 0 0 8983 15 0 0 25 0 1 0 22169141 18739200 4154 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 4575 4154 364 364 0 4211 0 [pid=10684] vsize: 18300 Current children cumulated CPU time (s) 89.98 Current children cumulated vsize (Kb) 18300 [startup+100.008 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 5792 0 0 0 9982 15 0 0 25 0 1 0 22169141 19144704 4329 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 4674 4329 364 364 0 4310 0 [pid=10684] 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.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 6594 0 0 0 10978 19 0 0 25 0 1 0 22169141 22274048 5130 4294967295 134512640 135987407 3221224560 3221221792 135486760 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 5438 5130 364 364 0 5074 0 [pid=10684] vsize: 21752 Current children cumulated CPU time (s) 109.97 Current children cumulated vsize (Kb) 21752 [startup+120.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 6796 0 0 0 11973 23 0 0 25 0 1 0 22169141 23199744 5332 4294967295 134512640 135987407 3221224560 3221221856 134639223 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 5664 5332 364 364 0 5300 0 [pid=10684] vsize: 22656 Current children cumulated CPU time (s) 119.96 Current children cumulated vsize (Kb) 22656 [startup+130.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 6952 0 0 0 12969 25 0 0 25 0 1 0 22169141 24260608 5488 4294967295 134512640 135987407 3221224560 3221222032 134610777 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 5923 5488 364 364 0 5559 0 [pid=10684] vsize: 23692 Current children cumulated CPU time (s) 129.94 Current children cumulated vsize (Kb) 23692 [startup+140.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 48587 0 0 0 13869 122 0 0 25 0 1 0 22169141 164843520 32043 4294967295 134512640 135987407 3221224560 3213379584 134861966 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 40245 32043 364 364 0 39881 0 [pid=10684] vsize: 160980 Current children cumulated CPU time (s) 139.91 Current children cumulated vsize (Kb) 160980 [startup+150.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 76020 0 0 0 14803 186 0 0 25 0 1 0 22169141 239226880 53102 4294967295 134512640 135987407 3221224560 3219341008 134558820 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 58405 53102 364 364 0 58041 0 [pid=10684] vsize: 233620 Current children cumulated CPU time (s) 149.89 Current children cumulated vsize (Kb) 233620 [startup+160.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 117660 0 0 0 15707 278 0 0 25 0 1 0 22169141 402898944 72544 4294967295 134512640 135987407 3221224560 3204307808 134877726 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 98364 72544 364 364 0 98000 0 [pid=10684] vsize: 393456 Current children cumulated CPU time (s) 159.85 Current children cumulated vsize (Kb) 393456 [startup+170.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 137991 0 0 0 16656 327 0 0 25 0 1 0 22169141 429256704 92629 4294967295 134512640 135987407 3221224560 3201485168 134878078 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 104799 92629 364 364 0 104435 0 [pid=10684] vsize: 419196 Current children cumulated CPU time (s) 169.83 Current children cumulated vsize (Kb) 419196 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 181962 0 0 0 17560 418 0 0 25 0 1 0 22169141 568147968 116994 4294967295 134512640 135987407 3221224560 3212762880 134854956 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 138708 116994 364 364 0 138344 0 [pid=10684] vsize: 554832 Current children cumulated CPU time (s) 179.78 Current children cumulated vsize (Kb) 554832 [startup+190.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 221295 0 0 0 18469 508 0 0 25 0 1 0 22169141 721424384 131577 4294967295 134512640 135987407 3221224560 3216471680 134877726 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 176129 131577 364 364 0 175765 0 [pid=10684] vsize: 704516 Current children cumulated CPU time (s) 189.77 Current children cumulated vsize (Kb) 704516 [startup+200.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 241005 0 0 0 19421 554 0 0 25 0 1 0 22169141 746835968 151054 4294967295 134512640 135987407 3221224560 3221212096 135477294 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 182333 151054 364 364 0 181969 0 [pid=10684] vsize: 729332 Current children cumulated CPU time (s) 199.75 Current children cumulated vsize (Kb) 729332 [startup+210.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 260641 0 0 0 20373 600 0 0 25 0 1 0 22169141 773328896 170444 4294967295 134512640 135987407 3221224560 3205900352 134887919 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 188801 170444 364 364 0 188437 0 [pid=10684] vsize: 755204 Current children cumulated CPU time (s) 209.73 Current children cumulated vsize (Kb) 755204 [startup+220.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 276476 0 0 0 21335 636 0 0 25 0 1 0 22169141 843530240 186095 4294967295 134512640 135987407 3221224560 3214493728 135477294 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 205940 186095 364 364 0 205576 0 [pid=10684] vsize: 823760 Current children cumulated CPU time (s) 219.71 Current children cumulated vsize (Kb) 823760 [startup+230.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10686 Raw data (/proc/10684/stat): 10684 (pb2sat) R 10683 10684 4004 0 -1 0 289857 0 0 0 22300 669 0 0 25 0 1 0 22169141 865153024 199088 4294967295 134512640 135987407 3221224560 3221223300 135478497 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10684/statm): 211219 199088 364 364 0 210855 0 [pid=10684] vsize: 844876 Current children cumulated CPU time (s) 229.69 Current children cumulated vsize (Kb) 844876 One traced child (pid=10684) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 235.732 CPU time (s): 235.408 CPU user time (s): 228.31 CPU system time (s): 7.09792 CPU usage (%): 99.8628 Max. virtual memory (cumulated for all children) (Kb): 844876
ERROR: no interpretation found !