Name | submitted/manquinho/primes-dimacs-cnf/normalized-par16-2.opb |
MD5SUM | ff021c96fa8729c0ff59034e5dd63ec7 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1015 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 2030 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 2030 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2030 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 42.4355 |
Number of variables | 2030 |
Total number of constraints | 4389 |
Number of constraints which are clauses | 4389 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc29 THE 2005-09-23 15:01:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8431 boxname=wulflinc29 idbench=227 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ff021c96fa8729c0ff59034e5dd63ec7 /oldhome/oroussel/tmp/wulflinc29/normalized-par16-2.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc29/normalized-par16-2.opb IDLAUNCH: 8431 /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: 930340 kB Buffers: 11204 kB Cached: 76176 kB SwapCached: 0 kB Active: 44084 kB Inactive: 46144 kB HighTotal: 131008 kB HighFree: 55328 kB LowTotal: 903652 kB LowFree: 875012 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 36 kB Writeback: 0 kB Mapped: 6972 kB Slab: 8600 kB Committed_AS: 63656 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 15:04:31 (client local time) WITH STATUS 1 IN 184.983 SECONDS stats: 8431 7 184.983 1
c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 1015 c big objective detected c trying from 0 to 511 c trying from 512 to 1014 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/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21068344 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 373 2 364 364 0 9 0 [pid=7590] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-par16-2.opb [startup+10.0024 s] Raw data (loadavg): 0.83 0.90 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 16017 0 0 0 937 46 0 0 25 0 1 0 21068344 50528256 10487 4294967295 134512640 135987407 3221224576 3221068036 135479922 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 12336 10487 364 364 0 11972 0 [pid=7590] vsize: 49344 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 49344 [startup+20.0032 s] Raw data (loadavg): 0.86 0.91 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 52342 0 0 0 1855 126 0 0 25 0 1 0 21068344 180412416 30112 4294967295 134512640 135987407 3221224576 3220865568 134877628 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 44046 30112 364 364 0 43682 0 [pid=7590] vsize: 176184 Current children cumulated CPU time (s) 19.81 Current children cumulated vsize (Kb) 176184 [startup+30.004 s] Raw data (loadavg): 0.88 0.91 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 70491 0 0 0 2810 168 0 0 25 0 1 0 21068344 203796480 48043 4294967295 134512640 135987407 3221224576 3220828704 134878632 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 49755 48043 364 364 0 49391 0 [pid=7590] vsize: 199020 Current children cumulated CPU time (s) 29.78 Current children cumulated vsize (Kb) 199020 [startup+40.0048 s] Raw data (loadavg): 0.90 0.91 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 111214 0 0 0 3718 258 0 0 25 0 1 0 21068344 366927872 66596 4294967295 134512640 135987407 3221224576 3220754016 134854984 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 89582 66596 364 364 0 89218 0 [pid=7590] vsize: 358328 Current children cumulated CPU time (s) 39.76 Current children cumulated vsize (Kb) 358328 [startup+50.0056 s] Raw data (loadavg): 0.91 0.91 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 129206 0 0 0 4677 296 0 0 25 0 1 0 21068344 390176768 84372 4294967295 134512640 135987407 3221224576 3220747792 134640133 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 95258 84372 364 364 0 94894 0 [pid=7590] vsize: 381032 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 381032 [startup+60.0063 s] Raw data (loadavg): 0.93 0.92 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 140202 0 0 0 5652 320 0 0 25 0 1 0 21068344 419098624 92012 4294967295 134512640 135987407 3221224576 3221223136 134811805 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 102319 92012 364 364 0 101955 0 [pid=7590] vsize: 409276 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 409276 [startup+70.0071 s] Raw data (loadavg): 0.94 0.92 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 141005 0 0 0 6649 322 0 0 25 0 1 0 21068344 421482496 92472 4294967295 134512640 135987407 3221224576 3221223136 134811706 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 102901 92472 364 364 0 102537 0 [pid=7590] vsize: 411604 Current children cumulated CPU time (s) 69.71 Current children cumulated vsize (Kb) 411604 [startup+80.0079 s] Raw data (loadavg): 0.95 0.92 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 141845 0 0 0 7647 324 0 0 25 0 1 0 21068344 423723008 92858 4294967295 134512640 135987407 3221224576 3221223136 134811729 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 103448 92858 364 364 0 103084 0 [pid=7590] vsize: 413792 Current children cumulated CPU time (s) 79.71 Current children cumulated vsize (Kb) 413792 [startup+90.0087 s] Raw data (loadavg): 0.95 0.92 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 142500 0 0 0 8645 325 0 0 25 0 1 0 21068344 425299968 93156 4294967295 134512640 135987407 3221224576 3221223008 134788454 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 103833 93156 364 364 0 103469 0 [pid=7590] vsize: 415332 Current children cumulated CPU time (s) 89.7 Current children cumulated vsize (Kb) 415332 [startup+100.008 s] Raw data (loadavg): 0.96 0.92 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 142513 0 0 0 9644 325 0 0 25 0 1 0 21068344 425299968 93169 4294967295 134512640 135987407 3221224576 3221223136 134788799 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 103833 93169 364 364 0 103469 0 [pid=7590] vsize: 415332 Current children cumulated CPU time (s) 99.69 Current children cumulated vsize (Kb) 415332 [startup+110.009 s] Raw data (loadavg): 0.97 0.93 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 142610 0 0 0 10643 326 0 0 25 0 1 0 21068344 425299968 93266 4294967295 134512640 135987407 3221224576 3221223136 134811770 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 103833 93266 364 364 0 103469 0 [pid=7590] vsize: 415332 Current children cumulated CPU time (s) 109.69 Current children cumulated vsize (Kb) 415332 [startup+120.01 s] Raw data (loadavg): 0.97 0.93 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 177889 0 0 0 11543 414 0 0 25 0 1 0 21068344 569794560 128545 4294967295 134512640 135987407 3221224576 3221223264 134886405 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 139110 128545 364 364 0 138746 0 [pid=7590] vsize: 556440 Current children cumulated CPU time (s) 119.57 Current children cumulated vsize (Kb) 556440 [startup+130.01 s] Raw data (loadavg): 0.97 0.93 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 220595 0 0 0 12458 497 0 0 25 0 1 0 21068344 884875264 151657 4294967295 134512640 135987407 3221224576 3220781136 134887487 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 216034 151657 364 364 0 215670 0 [pid=7590] vsize: 864136 Current children cumulated CPU time (s) 129.55 Current children cumulated vsize (Kb) 864136 [startup+140.011 s] Raw data (loadavg): 0.98 0.93 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 247519 0 0 0 13399 555 0 0 25 0 1 0 21068344 784207872 153849 4294967295 134512640 135987407 3221224576 3220908432 134537491 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 191457 153849 364 364 0 191093 0 [pid=7590] vsize: 765828 Current children cumulated CPU time (s) 139.54 Current children cumulated vsize (Kb) 765828 [startup+150.011 s] Raw data (loadavg): 0.98 0.93 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 256987 0 0 0 14380 575 0 0 25 0 1 0 21068344 784207872 163097 4294967295 134512640 135987407 3221224576 3220858676 134637037 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 191457 163097 364 364 0 191093 0 [pid=7590] vsize: 765828 Current children cumulated CPU time (s) 149.55 Current children cumulated vsize (Kb) 765828 [startup+160.012 s] Raw data (loadavg): 0.98 0.94 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 266457 0 0 0 15358 597 0 0 25 0 1 0 21068344 784207872 172347 4294967295 134512640 135987407 3221224576 3221198400 134537491 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 191457 172347 364 364 0 191093 0 [pid=7590] vsize: 765828 Current children cumulated CPU time (s) 159.55 Current children cumulated vsize (Kb) 765828 [startup+170.013 s] Raw data (loadavg): 0.99 0.94 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 277726 0 0 0 16334 621 0 0 25 0 1 0 21068344 792723456 183402 4294967295 134512640 135987407 3221224576 3221069372 135482121 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 193536 183402 364 364 0 193172 0 [pid=7590] vsize: 774144 Current children cumulated CPU time (s) 169.55 Current children cumulated vsize (Kb) 774144 [startup+180.014 s] Raw data (loadavg): 0.99 0.94 0.95 2/55 7590 Raw data (/proc/7590/stat): 7590 (pb2sat) R 7589 7590 4005 0 -1 0 292145 0 0 0 17299 653 0 0 25 0 1 0 21068344 815161344 197613 4294967295 134512640 135987407 3221224576 3221217648 134892445 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7590/statm): 199014 197613 364 364 0 198650 0 [pid=7590] vsize: 796056 Current children cumulated CPU time (s) 179.52 Current children cumulated vsize (Kb) 796056 One traced child (pid=7590) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 185.477 CPU time (s): 184.983 CPU user time (s): 178.05 CPU system time (s): 6.93295 CPU usage (%): 99.7336 Max. virtual memory (cumulated for all children) (Kb): 864136
ERROR: no interpretation found !