Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.18 |
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 wulflinc29 THE 2005-09-23 18:24:56 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9213 boxname=wulflinc29 idbench=1009 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-fast0507.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-fast0507.opb IDLAUNCH: 9213 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 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 : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 902056 kB Buffers: 12648 kB Cached: 102272 kB SwapCached: 0 kB Active: 62988 kB Inactive: 54788 kB HighTotal: 131008 kB HighFree: 29148 kB LowTotal: 903652 kB LowFree: 872908 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 9132 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 18:28:46 (client local time) WITH STATUS 1 IN 229.363 SECONDS stats: 9213 7 229.363 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/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22289603 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 373 2 364 364 0 9 0 [pid=10791] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-fast0507.opb [startup+10.0017 s] Raw data (loadavg): 0.93 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 2133 0 0 0 992 5 0 0 25 0 1 0 22289603 8556544 1454 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 2089 1454 364 364 0 1725 0 [pid=10791] vsize: 8356 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 8356 [startup+20.0025 s] Raw data (loadavg): 0.94 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 2879 0 0 0 1991 7 0 0 25 0 1 0 22289603 10313728 2187 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 2518 2187 364 364 0 2154 0 [pid=10791] vsize: 10072 Current children cumulated CPU time (s) 19.98 Current children cumulated vsize (Kb) 10072 [startup+30.0023 s] Raw data (loadavg): 0.95 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 4314 0 0 0 2988 9 0 0 25 0 1 0 22289603 15495168 2876 4294967295 134512640 135987407 3221224560 3221221728 134544693 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 3783 2876 364 364 0 3419 0 [pid=10791] vsize: 15132 Current children cumulated CPU time (s) 29.97 Current children cumulated vsize (Kb) 15132 [startup+40.0021 s] Raw data (loadavg): 0.96 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 4600 0 0 0 3987 11 0 0 25 0 1 0 22289603 16171008 3157 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 3948 3157 364 364 0 3584 0 [pid=10791] vsize: 15792 Current children cumulated CPU time (s) 39.98 Current children cumulated vsize (Kb) 15792 [startup+50.0029 s] Raw data (loadavg): 0.96 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 4863 0 0 0 4986 11 0 0 25 0 1 0 22289603 16846848 3416 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 4113 3416 364 364 0 3749 0 [pid=10791] vsize: 16452 Current children cumulated CPU time (s) 49.97 Current children cumulated vsize (Kb) 16452 [startup+60.0027 s] Raw data (loadavg): 0.97 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 5100 0 0 0 5985 12 0 0 25 0 1 0 22289603 17387520 3649 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 4245 3649 364 364 0 3881 0 [pid=10791] vsize: 16980 Current children cumulated CPU time (s) 59.97 Current children cumulated vsize (Kb) 16980 [startup+70.0034 s] Raw data (loadavg): 0.97 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 5311 0 0 0 6985 12 0 0 25 0 1 0 22289603 17928192 3856 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 4377 3856 364 364 0 4013 0 [pid=10791] vsize: 17508 Current children cumulated CPU time (s) 69.97 Current children cumulated vsize (Kb) 17508 [startup+80.0042 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 5506 0 0 0 7984 13 0 0 25 0 1 0 22289603 18468864 4048 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 4509 4048 364 364 0 4145 0 [pid=10791] vsize: 18036 Current children cumulated CPU time (s) 79.97 Current children cumulated vsize (Kb) 18036 [startup+90.004 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 5689 0 0 0 8984 13 0 0 25 0 1 0 22289603 18874368 4228 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 4608 4228 364 364 0 4244 0 [pid=10791] vsize: 18432 Current children cumulated CPU time (s) 89.97 Current children cumulated vsize (Kb) 18432 [startup+100.005 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 6476 0 0 0 9982 15 0 0 25 0 1 0 22289603 21848064 5012 4294967295 134512640 135987407 3221224560 3221221680 134931275 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 5334 5012 364 364 0 4970 0 [pid=10791] vsize: 21336 Current children cumulated CPU time (s) 99.97 Current children cumulated vsize (Kb) 21336 [startup+110.006 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 6687 0 0 0 10977 20 0 0 25 0 1 0 22289603 22675456 5223 4294967295 134512640 135987407 3221224560 3221221568 134538576 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 5536 5223 364 364 0 5172 0 [pid=10791] vsize: 22144 Current children cumulated CPU time (s) 109.97 Current children cumulated vsize (Kb) 22144 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 6861 0 0 0 11972 23 0 0 25 0 1 0 22289603 24260608 5397 4294967295 134512640 135987407 3221224560 3221221356 135480526 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10791/statm): 5923 5397 364 364 0 5559 0 [pid=10791] vsize: 23692 Current children cumulated CPU time (s) 119.95 Current children cumulated vsize (Kb) 23692 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 26811 0 0 0 12922 70 0 0 25 0 1 0 22289603 93429760 19847 4294967295 134512640 135987407 3221224560 3206811676 135499906 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 22810 19847 364 364 0 22446 0 [pid=10791] vsize: 91240 Current children cumulated CPU time (s) 129.92 Current children cumulated vsize (Kb) 91240 [startup+140.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 64443 0 0 0 13832 156 0 0 25 0 1 0 22289603 222871552 41654 4294967295 134512640 135987407 3221224560 3214670048 134877726 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 54412 41654 364 364 0 54048 0 [pid=10791] vsize: 217648 Current children cumulated CPU time (s) 139.88 Current children cumulated vsize (Kb) 217648 [startup+150.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 97078 0 0 0 14761 223 0 0 25 0 1 0 22289603 306307072 64352 4294967295 134512640 135987407 3221224560 3213234160 134802855 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 74782 64352 364 364 0 74418 0 [pid=10791] vsize: 299128 Current children cumulated CPU time (s) 149.84 Current children cumulated vsize (Kb) 299128 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 127837 0 0 0 15686 295 0 0 25 0 1 0 22289603 416145408 82598 4294967295 134512640 135987407 3221224560 3203080596 135479922 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 101598 82598 364 364 0 101234 0 [pid=10791] vsize: 406392 Current children cumulated CPU time (s) 159.81 Current children cumulated vsize (Kb) 406392 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 156342 0 0 0 16624 355 0 0 25 0 1 0 22289603 597549056 110546 4294967295 134512640 135987407 3221224560 3207610028 135500012 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 145886 110546 364 364 0 145522 0 [pid=10791] vsize: 583544 Current children cumulated CPU time (s) 169.79 Current children cumulated vsize (Kb) 583544 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 214385 0 0 0 17497 478 0 0 25 0 1 0 22289603 680300544 124742 4294967295 134512640 135987407 3221224560 3202840828 135500019 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 166089 124742 364 364 0 165725 0 [pid=10791] vsize: 664356 Current children cumulated CPU time (s) 179.75 Current children cumulated vsize (Kb) 664356 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 231625 0 0 0 18453 520 0 0 25 0 1 0 22289603 734806016 141782 4294967295 134512640 135987407 3221224560 3215940980 134537546 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 179396 141782 364 364 0 179032 0 [pid=10791] vsize: 717584 Current children cumulated CPU time (s) 189.73 Current children cumulated vsize (Kb) 717584 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 251802 0 0 0 19403 568 0 0 25 0 1 0 22289603 760893440 161719 4294967295 134512640 135987407 3221224560 3217808116 134637037 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 185765 161719 364 364 0 185401 0 [pid=10791] vsize: 743060 Current children cumulated CPU time (s) 199.71 Current children cumulated vsize (Kb) 743060 [startup+210.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 270851 0 0 0 20355 613 0 0 25 0 1 0 22289603 836907008 180531 4294967295 134512640 135987407 3221224560 3205349072 134877638 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 204323 180531 364 364 0 203959 0 [pid=10791] vsize: 817292 Current children cumulated CPU time (s) 209.68 Current children cumulated vsize (Kb) 817292 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 10791 Raw data (/proc/10791/stat): 10791 (pb2sat) R 10790 10791 4005 0 -1 0 289654 0 0 0 21309 655 0 0 25 0 1 0 22289603 864886784 199135 4294967295 134512640 135987407 3221224560 3216064448 134855001 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10791/statm): 211154 199135 364 364 0 210790 0 [pid=10791] vsize: 844616 Current children cumulated CPU time (s) 219.64 Current children cumulated vsize (Kb) 844616 One traced child (pid=10791) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 229.722 CPU time (s): 229.363 CPU user time (s): 222.397 CPU system time (s): 6.96594 CPU usage (%): 99.8437 Max. virtual memory (cumulated for all children) (Kb): 844616
ERROR: no interpretation found !