Name | submitted/manquinho/primes-dimacs-cnf/normalized-par16-5.opb |
MD5SUM | 373fd65e1136c6c0b1070f70c39b678a |
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 | 5.03523 |
Number of variables | 2030 |
Total number of constraints | 4373 |
Number of constraints which are clauses | 4373 |
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 wulflinc18 THE 2005-09-23 14:53:13 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8393 boxname=wulflinc18 idbench=189 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 373fd65e1136c6c0b1070f70c39b678a /oldhome/oroussel/tmp/wulflinc18/normalized-par16-5.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc18/normalized-par16-5.opb IDLAUNCH: 8393 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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.061 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: 938744 kB Buffers: 14212 kB Cached: 62424 kB SwapCached: 0 kB Active: 45252 kB Inactive: 34268 kB HighTotal: 131008 kB HighFree: 64260 kB LowTotal: 903652 kB LowFree: 874484 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6976 kB Slab: 10868 kB Committed_AS: 63620 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 14:56:44 (client local time) WITH STATUS 1 IN 209.689 SECONDS stats: 8393 7 209.689 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/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21058587 1527808 2 4294967295 134512640 135987407 3221224576 3221224576 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 373 2 364 364 0 9 0 [pid=6327] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-par16-5.opb [startup+10.0024 s] Raw data (loadavg): 0.93 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 16887 0 0 0 941 43 0 0 25 0 1 0 21058587 51609600 11347 4294967295 134512640 135987407 3221224576 3220971784 135488035 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 12600 11347 364 364 0 12236 0 [pid=6327] vsize: 50400 Current children cumulated CPU time (s) 9.84 Current children cumulated vsize (Kb) 50400 [startup+20.0033 s] Raw data (loadavg): 0.94 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 52925 0 0 0 1860 122 0 0 25 0 1 0 21058587 181088256 30688 4294967295 134512640 135987407 3221224576 3221169320 135499869 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 44211 30688 364 364 0 43847 0 [pid=6327] vsize: 176844 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 176844 [startup+30.0043 s] Raw data (loadavg): 0.95 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 74094 0 0 0 2813 167 0 0 25 0 1 0 21058587 280780800 51544 4294967295 134512640 135987407 3221224576 3220750368 134856696 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 68550 51544 364 364 0 68186 0 [pid=6327] vsize: 274200 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 274200 [startup+40.0052 s] Raw data (loadavg): 0.95 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 112765 0 0 0 3730 247 0 0 25 0 1 0 21058587 368955392 68129 4294967295 134512640 135987407 3221224576 3221058672 134560572 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 90077 68129 364 364 0 89713 0 [pid=6327] vsize: 360308 Current children cumulated CPU time (s) 39.77 Current children cumulated vsize (Kb) 360308 [startup+50.0061 s] Raw data (loadavg): 0.96 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 130993 0 0 0 4686 287 0 0 25 0 1 0 21058587 392474624 86138 4294967295 134512640 135987407 3221224576 3221115212 135499900 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 95819 86138 364 364 0 95455 0 [pid=6327] vsize: 383276 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 383276 [startup+60.007 s] Raw data (loadavg): 0.97 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 138859 0 0 0 5667 305 0 0 25 0 1 0 21058587 414265344 91063 4294967295 134512640 135987407 3221224576 3221223136 134812018 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 101139 91063 364 364 0 100775 0 [pid=6327] vsize: 404556 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 404556 [startup+70.008 s] Raw data (loadavg): 0.97 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 140297 0 0 0 6663 308 0 0 25 0 1 0 21058587 419393536 92174 4294967295 134512640 135987407 3221224576 3221223136 134811807 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 102391 92174 364 364 0 102027 0 [pid=6327] vsize: 409564 Current children cumulated CPU time (s) 69.71 Current children cumulated vsize (Kb) 409564 [startup+80.0089 s] Raw data (loadavg): 0.98 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 140970 0 0 0 7661 310 0 0 25 0 1 0 21058587 421367808 92426 4294967295 134512640 135987407 3221224576 3221223136 134812053 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 102873 92426 364 364 0 102509 0 [pid=6327] vsize: 411492 Current children cumulated CPU time (s) 79.71 Current children cumulated vsize (Kb) 411492 [startup+90.0098 s] Raw data (loadavg): 0.98 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 142367 0 0 0 8659 312 0 0 25 0 1 0 21058587 425402368 93199 4294967295 134512640 135987407 3221224576 3221223296 134789985 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 103858 93199 364 364 0 103494 0 [pid=6327] vsize: 415432 Current children cumulated CPU time (s) 89.71 Current children cumulated vsize (Kb) 415432 [startup+100.01 s] Raw data (loadavg): 0.98 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 142791 0 0 0 9657 313 0 0 25 0 1 0 21058587 426450944 93364 4294967295 134512640 135987407 3221224576 3221223264 134824261 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 104114 93364 364 364 0 103750 0 [pid=6327] vsize: 416456 Current children cumulated CPU time (s) 99.7 Current children cumulated vsize (Kb) 416456 [startup+110.011 s] Raw data (loadavg): 0.98 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 142988 0 0 0 10656 314 0 0 25 0 1 0 21058587 427388928 93561 4294967295 134512640 135987407 3221224576 3221223136 134811839 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 104343 93561 364 364 0 103979 0 [pid=6327] vsize: 417372 Current children cumulated CPU time (s) 109.7 Current children cumulated vsize (Kb) 417372 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 143133 0 0 0 11652 315 0 0 25 0 1 0 21058587 427819008 93673 4294967295 134512640 135987407 3221224576 3221223136 134811770 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 104448 93673 364 364 0 104084 0 [pid=6327] vsize: 417792 Current children cumulated CPU time (s) 119.67 Current children cumulated vsize (Kb) 417792 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 143442 0 0 0 12648 317 0 0 25 0 1 0 21058587 428814336 93917 4294967295 134512640 135987407 3221224576 3221223136 134811964 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 104691 93917 364 364 0 104327 0 [pid=6327] vsize: 418764 Current children cumulated CPU time (s) 129.65 Current children cumulated vsize (Kb) 418764 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 171423 0 0 0 13564 392 0 0 25 0 1 0 21058587 543031296 121898 4294967295 134512640 135987407 3221224576 3221223136 134893305 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 132576 121898 364 364 0 132212 0 [pid=6327] vsize: 530304 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 530304 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 211667 0 0 0 14476 474 0 0 25 0 1 0 21058587 749981696 161067 4294967295 134512640 135987407 3221224576 3220666368 134856487 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 183101 161067 364 364 0 182737 0 [pid=6327] vsize: 732404 Current children cumulated CPU time (s) 149.5 Current children cumulated vsize (Kb) 732404 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 247228 0 0 0 15396 554 0 0 25 0 1 0 21058587 787722240 153404 4294967295 134512640 135987407 3221224576 3221185376 134876866 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 192315 153404 364 364 0 191951 0 [pid=6327] vsize: 769260 Current children cumulated CPU time (s) 159.5 Current children cumulated vsize (Kb) 769260 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 256740 0 0 0 16373 577 0 0 25 0 1 0 21058587 787722240 162694 4294967295 134512640 135987407 3221224576 3220637456 134931301 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 192315 162694 364 364 0 191951 0 [pid=6327] vsize: 769260 Current children cumulated CPU time (s) 169.5 Current children cumulated vsize (Kb) 769260 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 266344 0 0 0 17353 597 0 0 25 0 1 0 21058587 787722240 172075 4294967295 134512640 135987407 3221224576 3221189520 134856505 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/6327/statm): 192315 172075 364 364 0 191951 0 [pid=6327] vsize: 769260 Current children cumulated CPU time (s) 179.5 Current children cumulated vsize (Kb) 769260 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 277092 0 0 0 18332 618 0 0 25 0 1 0 21058587 793804800 182608 4294967295 134512640 135987407 3221224576 3220727104 134854956 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/6327/statm): 193800 182609 364 364 0 193436 0 [pid=6327] vsize: 775200 Current children cumulated CPU time (s) 189.5 Current children cumulated vsize (Kb) 775200 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 291502 0 0 0 19295 653 0 0 25 0 1 0 21058587 816107520 196810 4294967295 134512640 135987407 3221224576 3221012976 134887887 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/6327/statm): 199245 196810 364 364 0 198881 0 [pid=6327] vsize: 796980 Current children cumulated CPU time (s) 199.48 Current children cumulated vsize (Kb) 796980 [startup+210.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/55 6327 Raw data (/proc/6327/stat): 6327 (pb2sat) R 6326 6327 4060 0 -1 0 293371 0 0 0 20271 679 0 0 25 0 1 0 21058587 377552896 91725 4294967295 134512640 135987407 3221224576 3221223432 135544177 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/6327/statm): 92176 91725 364 364 0 91812 0 [pid=6327] vsize: 368704 Current children cumulated CPU time (s) 209.5 Current children cumulated vsize (Kb) 368704 One traced child (pid=6327) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 210.229 CPU time (s): 209.689 CPU user time (s): 202.712 CPU system time (s): 6.97694 CPU usage (%): 99.7434 Max. virtual memory (cumulated for all children) (Kb): 796980
ERROR: no interpretation found !