Name | submitted/een/normalized-fast0507.opb |
MD5SUM | bc1a4f1c9875fd4d3273e85dcf5e871e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 251 |
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 | 1203.94 |
Number of variables | 63001 |
Total number of constraints | 489 |
Number of constraints which are clauses | 489 |
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 | 2 |
Maximum length of a constraint | 7753 |
LAUNCH ON wulflinc3 THE 2005-09-23 15:14:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8475 boxname=wulflinc3 idbench=271 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: bc1a4f1c9875fd4d3273e85dcf5e871e /oldhome/oroussel/tmp/wulflinc3/normalized-fast0507.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc3/normalized-fast0507.opb IDLAUNCH: 8475 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.228 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.228 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: 935264 kB Buffers: 12288 kB Cached: 69652 kB SwapCached: 0 kB Active: 48268 kB Inactive: 36568 kB HighTotal: 131008 kB HighFree: 57036 kB LowTotal: 903652 kB LowFree: 878228 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6972 kB Slab: 8948 kB Committed_AS: 63656 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 15:18:05 (client local time) WITH STATUS 1 IN 219.301 SECONDS stats: 8475 7 219.301 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/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21202059 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 373 2 364 364 0 9 0 [pid=7389] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-fast0507.opb [startup+10.0018 s] Raw data (loadavg): 0.83 0.94 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 2553 0 0 0 992 7 0 0 25 0 1 0 21202059 9498624 1867 4294967295 134512640 135987407 3221224576 3221221888 134555870 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 2319 1867 364 364 0 1955 0 [pid=7389] vsize: 9276 Current children cumulated CPU time (s) 9.99 Current children cumulated vsize (Kb) 9276 [startup+20.0026 s] Raw data (loadavg): 0.86 0.94 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 3035 0 0 0 1991 8 0 0 25 0 1 0 21202059 10715136 2341 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 2616 2341 364 364 0 2252 0 [pid=7389] vsize: 10464 Current children cumulated CPU time (s) 19.99 Current children cumulated vsize (Kb) 10464 [startup+30.0035 s] Raw data (loadavg): 0.88 0.94 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 4406 0 0 0 2987 12 0 0 25 0 1 0 21202059 15626240 2967 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 3815 2967 364 364 0 3451 0 [pid=7389] vsize: 15260 Current children cumulated CPU time (s) 29.99 Current children cumulated vsize (Kb) 15260 [startup+40.0043 s] Raw data (loadavg): 0.90 0.94 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 4679 0 0 0 3986 13 0 0 25 0 1 0 21202059 16302080 3236 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 3980 3236 364 364 0 3616 0 [pid=7389] vsize: 15920 Current children cumulated CPU time (s) 39.99 Current children cumulated vsize (Kb) 15920 [startup+50.0051 s] Raw data (loadavg): 0.91 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 4931 0 0 0 4985 14 0 0 25 0 1 0 21202059 16977920 3483 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 4145 3483 364 364 0 3781 0 [pid=7389] vsize: 16580 Current children cumulated CPU time (s) 49.99 Current children cumulated vsize (Kb) 16580 [startup+60.006 s] Raw data (loadavg): 0.92 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5154 0 0 0 5984 14 0 0 25 0 1 0 21202059 17518592 3703 4294967295 134512640 135987407 3221224576 3221221888 134555861 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 4277 3703 364 364 0 3913 0 [pid=7389] vsize: 17108 Current children cumulated CPU time (s) 59.98 Current children cumulated vsize (Kb) 17108 [startup+70.0058 s] Raw data (loadavg): 0.94 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5359 0 0 0 6984 15 0 0 25 0 1 0 21202059 18059264 3904 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 4409 3904 364 364 0 4045 0 [pid=7389] vsize: 17636 Current children cumulated CPU time (s) 69.99 Current children cumulated vsize (Kb) 17636 [startup+80.0067 s] Raw data (loadavg): 0.95 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5550 0 0 0 7983 15 0 0 25 0 1 0 21202059 18599936 4092 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 4541 4092 364 364 0 4177 0 [pid=7389] vsize: 18164 Current children cumulated CPU time (s) 79.98 Current children cumulated vsize (Kb) 18164 [startup+90.0065 s] Raw data (loadavg): 0.95 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 5732 0 0 0 8983 16 0 0 25 0 1 0 21202059 19005440 4271 4294967295 134512640 135987407 3221224576 3221221888 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 4640 4271 364 364 0 4276 0 [pid=7389] vsize: 18560 Current children cumulated CPU time (s) 89.99 Current children cumulated vsize (Kb) 18560 [startup+100.007 s] Raw data (loadavg): 0.96 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 6591 0 0 0 9980 18 0 0 25 0 1 0 21202059 22495232 5128 4294967295 134512640 135987407 3221224576 3221221968 134615250 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 5492 5128 364 364 0 5128 0 [pid=7389] vsize: 21968 Current children cumulated CPU time (s) 99.98 Current children cumulated vsize (Kb) 21968 [startup+110.008 s] Raw data (loadavg): 0.97 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 6820 0 0 0 10975 22 0 0 25 0 1 0 21202059 24076288 5357 4294967295 134512640 135987407 3221224576 3221221888 134555870 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 5878 5357 364 364 0 5514 0 [pid=7389] vsize: 23512 Current children cumulated CPU time (s) 109.97 Current children cumulated vsize (Kb) 23512 [startup+120.009 s] Raw data (loadavg): 0.97 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 21543 0 0 0 11936 59 0 0 25 0 1 0 21202059 72876032 17054 4294967295 134512640 135987407 3221224576 3220596816 134856397 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 17792 17054 364 364 0 17428 0 [pid=7389] vsize: 71168 Current children cumulated CPU time (s) 119.95 Current children cumulated vsize (Kb) 71168 [startup+130.01 s] Raw data (loadavg): 0.97 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 55853 0 0 0 12854 137 0 0 25 0 1 0 21202059 177115136 39228 4294967295 134512640 135987407 3221224576 3206232448 134866075 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 43241 39228 364 364 0 42877 0 [pid=7389] vsize: 172964 Current children cumulated CPU time (s) 129.91 Current children cumulated vsize (Kb) 172964 [startup+140.01 s] Raw data (loadavg): 0.98 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 93832 0 0 0 13761 226 0 0 25 0 1 0 21202059 303034368 61140 4294967295 134512640 135987407 3221224576 3203638608 134878060 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 73983 61140 364 364 0 73619 0 [pid=7389] vsize: 295932 Current children cumulated CPU time (s) 139.87 Current children cumulated vsize (Kb) 295932 [startup+150.011 s] Raw data (loadavg): 0.98 0.95 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 123742 0 0 0 14688 297 0 0 25 0 1 0 21202059 409628672 78566 4294967295 134512640 135987407 3221224576 3221200412 135480876 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 100007 78566 364 364 0 99643 0 [pid=7389] vsize: 400028 Current children cumulated CPU time (s) 149.85 Current children cumulated vsize (Kb) 400028 [startup+160.011 s] Raw data (loadavg): 0.98 0.96 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 144750 0 0 0 15636 346 0 0 25 0 1 0 21202059 438284288 99328 4294967295 134512640 135987407 3221224576 3220696676 135478476 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 107003 99328 364 364 0 106639 0 [pid=7389] vsize: 428012 Current children cumulated CPU time (s) 159.82 Current children cumulated vsize (Kb) 428012 [startup+170.011 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 199250 0 0 0 16517 459 0 0 25 0 1 0 21202059 775532544 134231 4294967295 134512640 135987407 3221224576 3215821440 134887487 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 189339 134231 364 364 0 188975 0 [pid=7389] vsize: 757356 Current children cumulated CPU time (s) 169.76 Current children cumulated vsize (Kb) 757356 [startup+180.012 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 226919 0 0 0 17453 522 0 0 25 0 1 0 21202059 728829952 137132 4294967295 134512640 135987407 3221224576 3213542816 134556288 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 177937 137132 364 364 0 177573 0 [pid=7389] vsize: 711748 Current children cumulated CPU time (s) 179.75 Current children cumulated vsize (Kb) 711748 [startup+190.013 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 246925 0 0 0 18404 570 0 0 25 0 1 0 21202059 754647040 156900 4294967295 134512640 135987407 3221224576 3216453712 134640151 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 184240 156900 364 364 0 183876 0 [pid=7389] vsize: 736960 Current children cumulated CPU time (s) 189.74 Current children cumulated vsize (Kb) 736960 [startup+200.014 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 266666 0 0 0 19355 616 0 0 25 0 1 0 21202059 780058624 176408 4294967295 134512640 135987407 3221224576 3220993592 135499909 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 190444 176408 364 364 0 190080 0 [pid=7389] vsize: 761776 Current children cumulated CPU time (s) 199.71 Current children cumulated vsize (Kb) 761776 [startup+210.015 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 7389 Raw data (/proc/7389/stat): 7389 (pb2sat) R 7388 7389 4060 0 -1 0 283399 0 0 0 20313 656 0 0 25 0 1 0 21202059 854855680 192950 4294967295 134512640 135987407 3221224576 3218602256 134854972 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7389/statm): 208705 192950 364 364 0 208341 0 [pid=7389] vsize: 834820 Current children cumulated CPU time (s) 209.69 Current children cumulated vsize (Kb) 834820 One traced child (pid=7389) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 219.639 CPU time (s): 219.301 CPU user time (s): 212.187 CPU system time (s): 7.11392 CPU usage (%): 99.8461 Max. virtual memory (cumulated for all children) (Kb): 834820
ERROR: no interpretation found !