Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-5.opb |
MD5SUM | 00a81d808a7a59d6e11f17e19e68d826 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -30 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 450 |
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 | 450 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 450 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04884 |
Number of variables | 450 |
Total number of constraints | 17794 |
Number of constraints which are clauses | 17794 |
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 | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc1 THE 2005-05-25 17:07:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21900 boxname=wulflinc1 idbench=318 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 00a81d808a7a59d6e11f17e19e68d826 /oldhome/oroussel/tmp/wulflinc1/normalized-frb30-15-5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-frb30-15-5.opb IDLAUNCH: 21900 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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.053 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: 612896 kB Buffers: 35456 kB Cached: 356668 kB SwapCached: 3976 kB Active: 79480 kB Inactive: 319556 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 612644 kB SwapTotal: 2097136 kB SwapFree: 2092844 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6968 kB Slab: 17020 kB Committed_AS: 92684 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:10:40 (client local time) WITH STATUS 30 IN 171.55 SECONDS stats: 21900 0 171.55 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17794 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17794 35588 | 5931 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -22[0m c ---[ 0]---> Sorter-cost:16912 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 34802 75593 | 11600 0 0 nan | 0.000 % | c | 100 | 34555 75082 | 12760 84 563 6.7 | 1.179 % | c | 250 | 33868 73599 | 14036 182 1409 7.7 | 4.575 % | c | 475 | 33293 72348 | 15439 361 4402 12.2 | 7.461 % | c | 812 | 32099 69706 | 16983 623 7299 11.7 | 13.625 % | c | 1318 | 30542 66231 | 18681 1026 11447 11.2 | 21.768 % | c | 2077 | 28055 60546 | 20550 1550 20019 12.9 | 35.084 % | c | 3216 | 25883 55479 | 22605 2330 33904 14.6 | 47.119 % | c ============================================================================== c [1mFound solution: -23[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3418 | 25783 55330 | 8594 2508 37255 14.9 | 47.119 % | c | 3518 | 25667 55054 | 9453 2597 38818 14.9 | 48.756 % | c | 3668 | 25620 54943 | 10398 2740 41433 15.1 | 49.026 % | c | 3893 | 25347 54298 | 11438 2928 46237 15.8 | 50.576 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4124 | 25176 53901 | 8392 3128 49826 15.9 | 50.576 % | c | 4225 | 24881 53213 | 9231 3212 51047 15.9 | 53.265 % | c | 4375 | 24356 51964 | 10154 3223 52127 16.2 | 56.273 % | c | 4600 | 23882 50842 | 11169 3302 54080 16.4 | 58.934 % | c | 4937 | 23389 49655 | 12286 3569 61701 17.3 | 61.756 % | c | 5443 | 22849 48372 | 13515 3965 74891 18.9 | 64.848 % | c | 6202 | 22592 47757 | 14866 4637 95068 20.5 | 66.284 % | c | 7342 | 22346 47158 | 16353 5705 144892 25.4 | 67.746 % | c | 9050 | 22090 46543 | 17988 7284 217107 29.8 | 69.207 % | c | 11612 | 21844 45943 | 19787 9771 372379 38.1 | 70.643 % | c | 15457 | 21655 45496 | 21766 13383 623366 46.6 | 71.725 % | c | 21224 | 21372 44811 | 23943 18951 984412 51.9 | 73.372 % | c ============================================================================== c [1mFound solution: -27[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26066 | 21193 44399 | 7064 23613 1307116 55.4 | 73.372 % | c | 26166 | 21193 44399 | 7770 11907 597346 50.2 | 74.606 % | c | 26316 | 21167 44337 | 8547 12041 602393 50.0 | 74.757 % | c | 26542 | 21167 44337 | 9402 12267 610860 49.8 | 74.757 % | c ============================================================================== c [1mFound solution: -28[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26715 | 21158 44290 | 7052 12438 619287 49.8 | 74.757 % | c | 26815 | 21158 44290 | 7757 12538 623239 49.7 | 74.820 % | c | 26965 | 21158 44290 | 8532 12688 628883 49.6 | 74.820 % | c | 27190 | 21158 44290 | 9386 12913 639459 49.5 | 74.820 % | c | 27527 | 21158 44290 | 10324 13250 655887 49.5 | 74.820 % | c | 28033 | 21158 44290 | 11357 13756 682076 49.6 | 74.820 % | c | 28792 | 21150 44272 | 12493 14511 718628 49.5 | 74.862 % | c | 29932 | 21143 44255 | 13742 15649 781893 50.0 | 74.904 % | c | 31640 | 21087 44120 | 15116 17285 872061 50.5 | 75.223 % | c | 34203 | 20937 43767 | 16628 19687 1017745 51.7 | 76.061 % | c | 38047 | 20765 43355 | 18291 23469 1249644 53.2 | 77.050 % | c | 43813 | 20741 43298 | 20120 14828 600488 40.5 | 77.184 % | c | 52463 | 20741 43298 | 22132 23478 924084 39.4 | 77.185 % | c | 65437 | 20727 43264 | 24345 20053 535668 26.7 | 77.268 % | c | 84898 | 20692 43186 | 26779 20388 496597 24.4 | 77.445 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90372 | 20701 43213 | 6900 25859 654515 25.3 | 77.445 % | c | 90472 | 20701 43213 | 7590 13030 285934 21.9 | 77.454 % | c | 90622 | 20674 43140 | 8349 13177 288840 21.9 | 77.646 % | c | 90847 | 20674 43140 | 9183 13402 293530 21.9 | 77.646 % | c | 91184 | 20674 43140 | 10102 13739 298910 21.8 | 77.646 % | c | 91690 | 20674 43140 | 11112 14245 308722 21.7 | 77.646 % | c | 92451 | 20674 43140 | 12223 15006 320094 21.3 | 77.646 % | c | 93590 | 20674 43140 | 13446 16145 350318 21.7 | 77.646 % | c | 95298 | 20641 43065 | 14790 17849 400355 22.4 | 77.822 % | c | 97860 | 20641 43065 | 16269 20411 461070 22.6 | 77.822 % | c | 101706 | 20603 42971 | 17896 24246 583457 24.1 | 78.056 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104199 | 20595 42933 | 6865 26728 644312 24.1 | 78.056 % | c | 104300 | 20595 42933 | 7551 13465 297891 22.1 | 78.118 % | c | 104451 | 20595 42933 | 8306 13616 301225 22.1 | 78.118 % | c | 104676 | 20595 42933 | 9137 13841 305817 22.1 | 78.118 % | c | 105014 | 20567 42863 | 10051 14126 312264 22.1 | 78.294 % | c | 105520 | 20567 42863 | 11056 14632 321076 21.9 | 78.294 % | c | 106280 | 20562 42850 | 12161 15391 334902 21.8 | 78.327 % | c | 107419 | 20362 42389 | 13377 7434 137717 18.5 | 79.122 % | c | 109127 | 20331 42310 | 14715 9132 223483 24.5 | 79.314 % | c | 111689 | 20243 42100 | 16187 11666 314439 27.0 | 79.816 % | c | 115533 | 20243 42100 | 17806 15510 406098 26.2 | 79.816 % | c | 121300 | 20058 41689 | 19586 14339 350749 24.5 | 80.335 % | c ============================================================================== c [1mOptimal solution: -30[0m s OPTIMUM FOUND v -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 C410 -C409 -C408 -C407 -C406 -C405 C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 C319 -C318 -C317 -C316 -C315 -C314 C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 C245 -C244 -C243 -C242 -C241 C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 C213 -C212 -C211 -C210 C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 C140 -C139 -C138 -C137 -C136 -C135 -C134 C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 C77 -C76 -C75 -C74 C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 -C62 -C61 -C60 -C59 -C58 -C57 -C56 -C55 -C54 -C53 -C52 -C51 C50 -C49 -C48 -C47 -C46 -C45 -C44 -C43 -C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 -C34 -C33 C32 -C31 -C30 -C29 -C28 -C27 -C26 -C25 -C24 C23 -C22 -C21 -C20 -C19 -C18 -C17 -C16 -C15 -C14 -C13 -C12 -C11 -C10 -C9 -C8 -C7 -C6 -C5 -C4 -C3 -C2 C1 c _______________________________________________________________________________ c c restarts : 67 c conflicts : 129853 (758 /sec) c decisions : 192464 (1123 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 171.398 s c _______________________________________________________________________________ #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.94 0.95 2/55 24315 Raw data (stat): 24315 (runsolver) R 24314 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 725479128 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.001 s] Raw data (loadavg): 0.93 0.94 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0017 s] Raw data (loadavg): 0.94 0.94 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0025 s] Raw data (loadavg): 0.95 0.94 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0022 s] Raw data (loadavg): 0.95 0.94 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0021 s] Raw data (loadavg): 0.96 0.94 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0019 s] Raw data (loadavg): 0.97 0.94 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0026 s] Raw data (loadavg): 0.97 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0034 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0032 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.004 s] Raw data (loadavg): 0.98 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.005 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.005 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.005 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.005 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.005 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.005 s] Raw data (loadavg): 0.99 0.95 0.95 2/56 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+171.541 s] Raw data (loadavg): 0.99 0.96 0.95 1/54 24319 Raw data (stat): 24315 (minisat+_script) S 24314 8378 8377 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 725479128 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 171.541 CPU time (s): 171.55 CPU user time (s): 171.41 CPU system time (s): 0.139978 CPU usage (%): 100.005 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK -30 #### END VERIFIER DATA ####