Name | submitted/een/normalized-p0548.opb |
MD5SUM | 422c0da7d5380a26c4dac413428db5c9 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 18745 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 416 |
Biggest coefficient in the objective function | 11000 |
Number of bits for the biggest coefficient in the objective function | 14 |
Sum of the numbers in the objective function | 96797 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 11000 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 96797 |
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 | 1195.1 |
Number of variables | 527 |
Total number of constraints | 156 |
Number of constraints which are clauses | 40 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 116 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 134 |
LAUNCH ON wulflinc14 THE 2005-09-23 15:17:08 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8490 boxname=wulflinc14 idbench=286 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 422c0da7d5380a26c4dac413428db5c9 /oldhome/oroussel/tmp/wulflinc14/normalized-p0548.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc14/normalized-p0548.opb IDLAUNCH: 8490 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.058 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.058 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: 997276 kB Buffers: 1592 kB Cached: 18876 kB SwapCached: 0 kB Active: 16612 kB Inactive: 6696 kB HighTotal: 131008 kB HighFree: 107940 kB LowTotal: 903652 kB LowFree: 889336 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 36 kB Writeback: 0 kB Mapped: 6980 kB Slab: 8348 kB Committed_AS: 63656 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 15:20:23 (client local time) WITH STATUS 1 IN 193.662 SECONDS stats: 8490 7 193.662 1
c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 79460 c small objective detected 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/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21200423 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 373 2 364 364 0 9 0 [pid=7157] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc14/normalized-p0548.opb [startup+10.0015 s] Raw data (loadavg): 0.93 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 28204 0 0 0 930 65 0 0 25 0 1 0 21200423 95293440 16737 4294967295 134512640 135987407 3221224576 3221223264 134812000 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 23265 16737 364 364 0 22901 0 [pid=7157] vsize: 93060 Current children cumulated CPU time (s) 9.95 Current children cumulated vsize (Kb) 93060 [startup+20.0021 s] Raw data (loadavg): 0.94 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 29586 0 0 0 1924 67 0 0 25 0 1 0 21200423 100270080 17628 4294967295 134512640 135987407 3221224576 3221223440 134812647 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 24480 17628 364 364 0 24116 0 [pid=7157] vsize: 97920 Current children cumulated CPU time (s) 19.91 Current children cumulated vsize (Kb) 97920 [startup+30.0028 s] Raw data (loadavg): 0.95 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 29981 0 0 0 2922 69 0 0 25 0 1 0 21200423 101457920 17795 4294967295 134512640 135987407 3221224576 3221223264 134812053 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 24770 17795 364 364 0 24406 0 [pid=7157] vsize: 99080 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 99080 [startup+40.0035 s] Raw data (loadavg): 0.96 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 31033 0 0 0 3915 73 0 0 25 0 1 0 21200423 105357312 18437 4294967295 134512640 135987407 3221224576 3221223264 134812157 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 25722 18437 364 364 0 25358 0 [pid=7157] vsize: 102888 Current children cumulated CPU time (s) 39.88 Current children cumulated vsize (Kb) 102888 [startup+50.0041 s] Raw data (loadavg): 0.96 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 31245 0 0 0 4909 75 0 0 25 0 1 0 21200423 106024960 18583 4294967295 134512640 135987407 3221224576 3221223264 134811775 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 25885 18583 364 364 0 25521 0 [pid=7157] vsize: 103540 Current children cumulated CPU time (s) 49.84 Current children cumulated vsize (Kb) 103540 [startup+60.0038 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 31547 0 0 0 5900 78 0 0 25 0 1 0 21200423 106983424 18753 4294967295 134512640 135987407 3221224576 3221223440 134812696 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 26119 18753 364 364 0 25755 0 [pid=7157] vsize: 104476 Current children cumulated CPU time (s) 59.78 Current children cumulated vsize (Kb) 104476 [startup+70.0045 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 31632 0 0 0 6894 81 0 0 25 0 1 0 21200423 107532288 18838 4294967295 134512640 135987407 3221224576 3221223264 134811839 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 26253 18838 364 364 0 25889 0 [pid=7157] vsize: 105012 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 105012 [startup+80.0042 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 31790 0 0 0 7888 83 0 0 25 0 1 0 21200423 108195840 18963 4294967295 134512640 135987407 3221224576 3221223264 134811805 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 26415 18963 364 364 0 26051 0 [pid=7157] vsize: 105660 Current children cumulated CPU time (s) 79.71 Current children cumulated vsize (Kb) 105660 [startup+90.0049 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 31932 0 0 0 8882 85 0 0 25 0 1 0 21200423 108724224 19039 4294967295 134512640 135987407 3221224576 3221223136 134788496 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 26544 19039 364 364 0 26180 0 [pid=7157] vsize: 106176 Current children cumulated CPU time (s) 89.67 Current children cumulated vsize (Kb) 106176 [startup+100.006 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 55833 0 0 0 9827 138 0 0 25 0 1 0 21200423 186003456 31767 4294967295 134512640 135987407 3221224576 3221128468 134558630 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 45411 31767 364 364 0 45047 0 [pid=7157] vsize: 181644 Current children cumulated CPU time (s) 99.65 Current children cumulated vsize (Kb) 181644 [startup+110.006 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 88114 0 0 0 10761 201 0 0 25 0 1 0 21200423 269856768 54118 4294967295 134512640 135987407 3221224576 3221112664 134537317 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 65883 54118 364 364 0 65519 0 [pid=7157] vsize: 263532 Current children cumulated CPU time (s) 109.62 Current children cumulated vsize (Kb) 263532 [startup+120.007 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 117188 0 0 0 11694 265 0 0 25 0 1 0 21200423 376180736 70703 4294967295 134512640 135987407 3221224576 3221171008 134878060 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 91841 70703 364 364 0 91477 0 [pid=7157] vsize: 367364 Current children cumulated CPU time (s) 119.59 Current children cumulated vsize (Kb) 367364 [startup+130.008 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 136479 0 0 0 12649 308 0 0 25 0 1 0 21200423 401186816 89762 4294967295 134512640 135987407 3221224576 3221211756 135482121 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 97946 89762 364 364 0 97582 0 [pid=7157] vsize: 391784 Current children cumulated CPU time (s) 129.57 Current children cumulated vsize (Kb) 391784 [startup+140.008 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 202070 0 0 0 13512 440 0 0 25 0 1 0 21200423 639410176 111205 4294967295 134512640 135987407 3221224576 3221195632 134537477 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 156106 111205 364 364 0 155742 0 [pid=7157] vsize: 624424 Current children cumulated CPU time (s) 139.52 Current children cumulated vsize (Kb) 624424 [startup+150.009 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 218511 0 0 0 14474 476 0 0 25 0 1 0 21200423 694861824 127451 4294967295 134512640 135987407 3221224576 3221175772 134636997 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 169644 127451 364 364 0 169280 0 [pid=7157] vsize: 678576 Current children cumulated CPU time (s) 149.5 Current children cumulated vsize (Kb) 678576 [startup+160.009 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 237267 0 0 0 15432 516 0 0 25 0 1 0 21200423 719462400 145983 4294967295 134512640 135987407 3221224576 3221180208 134560498 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 175650 145984 364 364 0 175286 0 [pid=7157] vsize: 702600 Current children cumulated CPU time (s) 159.48 Current children cumulated vsize (Kb) 702600 [startup+170.008 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 256022 0 0 0 16389 556 0 0 25 0 1 0 21200423 743792640 164513 4294967295 134512640 135987407 3221224576 3221189632 134560733 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 181590 164514 364 364 0 181226 0 [pid=7157] vsize: 726360 Current children cumulated CPU time (s) 169.45 Current children cumulated vsize (Kb) 726360 [startup+180.008 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 270929 0 0 0 17353 591 0 0 25 0 1 0 21200423 813453312 179240 4294967295 134512640 135987407 3221224576 3221210992 134878666 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7157/statm): 198597 179240 364 364 0 198233 0 [pid=7157] vsize: 794388 Current children cumulated CPU time (s) 179.44 Current children cumulated vsize (Kb) 794388 [startup+190.009 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 7157 Raw data (/proc/7157/stat): 7157 (pb2sat) R 7156 7157 4060 0 -1 0 284707 0 0 0 18321 621 0 0 25 0 1 0 21200423 833290240 192858 4294967295 134512640 135987407 3221224576 3221223256 135477380 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7157/statm): 203440 192858 364 364 0 203076 0 [pid=7157] vsize: 813760 Current children cumulated CPU time (s) 189.42 Current children cumulated vsize (Kb) 813760 One traced child (pid=7157) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 194.245 CPU time (s): 193.662 CPU user time (s): 187.048 CPU system time (s): 6.61399 CPU usage (%): 99.6999 Max. virtual memory (cumulated for all children) (Kb): 813760
ERROR: no interpretation found !