Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-1.opb |
MD5SUM | 84d0b0ba659c599a6c66454cd956a06b |
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.04684 |
Number of variables | 450 |
Total number of constraints | 17827 |
Number of constraints which are clauses | 17827 |
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 wulflinc22 THE 2005-05-25 17:05:08 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21896 boxname=wulflinc22 idbench=314 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 84d0b0ba659c599a6c66454cd956a06b /oldhome/oroussel/tmp/wulflinc22/normalized-frb30-15-1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-frb30-15-1.opb IDLAUNCH: 21896 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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.031 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: 615488 kB Buffers: 34996 kB Cached: 361656 kB SwapCached: 400 kB Active: 71936 kB Inactive: 327016 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 615236 kB SwapTotal: 2097892 kB SwapFree: 2096804 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5580 kB Slab: 14640 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 17:20:41 (client local time) WITH STATUS 30 IN 932.548 SECONDS stats: 21896 0 932.548 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17827 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 | 17827 35654 | 5942 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 | 34835 75659 | 11611 0 0 nan | 0.000 % | c | 100 | 34673 75331 | 12772 91 1241 13.6 | 0.760 % | c | 250 | 34372 74694 | 14049 227 3868 17.0 | 2.194 % | c | 475 | 33770 73410 | 15454 390 6617 17.0 | 5.105 % | c | 812 | 32192 69917 | 16999 594 9246 15.6 | 13.274 % | c | 1318 | 30885 66976 | 18699 1025 14636 14.3 | 20.068 % | c | 2077 | 29091 62938 | 20569 1589 22998 14.5 | 29.535 % | 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 | 2290 | 29136 63155 | 9712 1795 26567 14.8 | 29.535 % | c | 2390 | 28918 62661 | 10683 1856 27309 14.7 | 31.219 % | c | 2540 | 28528 61767 | 11751 1959 29052 14.8 | 33.117 % | c | 2765 | 27331 58989 | 12926 2082 31650 15.2 | 39.611 % | c | 3102 | 26489 57001 | 14219 2354 36494 15.5 | 44.301 % | c | 3608 | 25652 55047 | 15641 2750 43545 15.8 | 48.992 % | c | 4367 | 24237 51690 | 17205 3286 60981 18.6 | 57.020 % | c ============================================================================== c [1mFound solution: -24[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5322 | 23486 49866 | 7828 4096 97430 23.8 | 57.020 % | c | 5422 | 23436 49743 | 8610 4190 100261 23.9 | 61.649 % | c | 5572 | 23333 49498 | 9471 4300 105850 24.6 | 62.217 % | c | 5798 | 23169 49105 | 10419 4432 110057 24.8 | 63.156 % | c | 6136 | 23048 48818 | 11460 4735 118374 25.0 | 63.833 % | c ============================================================================== c [1mFound solution: -25[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6546 | 22906 48508 | 7635 5120 134151 26.2 | 63.833 % | c | 6646 | 22828 48319 | 8398 5200 135432 26.0 | 65.208 % | c | 6796 | 22725 48081 | 9238 5333 137158 25.7 | 65.774 % | c | 7021 | 22609 47792 | 10162 5526 146173 26.5 | 66.450 % | c | 7358 | 22317 47103 | 11178 5755 153982 26.8 | 68.114 % | c | 7864 | 21939 46183 | 12296 6101 173024 28.4 | 70.344 % | c | 8623 | 21460 45010 | 13525 6449 192451 29.8 | 73.174 % | c | 9762 | 21006 43926 | 14878 7262 235105 32.4 | 75.792 % | 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 | 10683 | 20998 43864 | 6999 8116 294754 36.3 | 75.792 % | c | 10783 | 20963 43778 | 7698 8195 297213 36.3 | 76.058 % | c | 10934 | 20963 43778 | 8468 8346 305062 36.6 | 76.058 % | c | 11159 | 20963 43778 | 9315 8571 315255 36.8 | 76.058 % | 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 | 11389 | 20967 43804 | 6989 8785 322698 36.7 | 76.058 % | c | 11489 | 20933 43728 | 7687 8859 327407 37.0 | 76.400 % | c | 11639 | 20930 43721 | 8456 9008 331762 36.8 | 76.417 % | c | 11864 | 20930 43721 | 9302 9233 344821 37.3 | 76.417 % | c | 12202 | 20930 43721 | 10232 9571 356569 37.3 | 76.417 % | c | 12708 | 20930 43721 | 11255 10077 385876 38.3 | 76.417 % | c | 13467 | 20831 43489 | 12381 10749 420071 39.1 | 76.979 % | c | 14606 | 20831 43489 | 13619 11888 486952 41.0 | 76.979 % | c | 16315 | 20808 43430 | 14981 13548 605196 44.7 | 77.130 % | c | 18878 | 20663 43086 | 16479 15930 744804 46.8 | 77.951 % | c | 22722 | 20583 42889 | 18127 19676 973894 49.5 | 78.437 % | c | 28488 | 20527 42755 | 19940 25368 1263999 49.8 | 78.756 % | c | 37137 | 20527 42755 | 21934 18260 927635 50.8 | 78.756 % | c | 50111 | 20527 42755 | 24127 31234 1608184 51.5 | 78.756 % | c | 69572 | 20472 42624 | 26540 31866 1272376 39.9 | 79.066 % | 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 | 87300 | 20418 42477 | 6806 29269 1356587 46.3 | 79.066 % | c | 87400 | 20418 42477 | 7486 14434 804584 55.7 | 79.413 % | c | 87550 | 20418 42477 | 8235 14584 808066 55.4 | 79.413 % | c | 87776 | 20418 42477 | 9058 14810 818435 55.3 | 79.413 % | c | 88113 | 20395 42412 | 9964 15143 833712 55.1 | 79.581 % | c | 88621 | 20367 42346 | 10961 15637 854932 54.7 | 79.740 % | c | 89380 | 20367 42346 | 12057 16396 896330 54.7 | 79.740 % | c | 90520 | 20332 42256 | 13262 17507 958188 54.7 | 79.966 % | c | 92228 | 20330 42252 | 14589 19212 1051043 54.7 | 79.975 % | c | 94790 | 20321 42231 | 16048 21737 1203283 55.4 | 80.025 % | c | 98635 | 20321 42231 | 17653 25582 1410295 55.1 | 80.025 % | c | 104403 | 20321 42231 | 19418 17288 716599 41.5 | 80.025 % | c | 113052 | 20260 42081 | 21360 25898 1096992 42.4 | 80.394 % | c | 126026 | 20250 42057 | 23496 22916 651661 28.4 | 80.453 % | c | 145488 | 20249 42054 | 25845 24858 701226 28.2 | 80.461 % | c | 174681 | 20202 41940 | 28430 34645 1648317 47.6 | 80.729 % | c | 218470 | 20172 41868 | 31273 37504 1071129 28.6 | 80.905 % | 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 | 259328 | 20183 41897 | 6727 32816 838031 25.5 | 80.905 % | c | 259428 | 20183 41897 | 7399 16508 354365 21.5 | 80.890 % | c | 259578 | 20183 41897 | 8139 16658 357043 21.4 | 80.890 % | c | 259803 | 20183 41897 | 8953 16883 362276 21.5 | 80.890 % | c | 260141 | 20183 41897 | 9849 17221 370509 21.5 | 80.890 % | c | 260648 | 20156 41830 | 10833 17722 385964 21.8 | 81.057 % | c | 261408 | 20156 41830 | 11917 18482 410658 22.2 | 81.057 % | c | 262547 | 20156 41830 | 13109 19621 439412 22.4 | 81.057 % | c | 264255 | 20156 41830 | 14419 21329 482590 22.6 | 81.057 % | c | 266817 | 20156 41830 | 15861 23891 541150 22.7 | 81.057 % | c | 270661 | 20156 41830 | 17448 14724 273573 18.6 | 81.057 % | c | 276427 | 20156 41830 | 19192 20490 407959 19.9 | 81.057 % | c | 285076 | 20069 41650 | 21112 11273 229439 20.4 | 81.133 % | c | 298050 | 20049 41605 | 23223 24245 809055 33.4 | 81.233 % | c | 317512 | 19928 41349 | 25545 26746 1058371 39.6 | 81.409 % | c | 346704 | 19862 41199 | 28100 19985 476549 23.8 | 81.760 % | c | 390494 | 19677 40823 | 30910 35384 1105188 31.2 | 81.868 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost:16276 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 425189 | 34252 74949 | 11417 31898 911006 28.6 | 81.868 % | c | 425290 | 34252 74949 | 12558 16050 304022 18.9 | 47.829 % | c | 425441 | 34252 74949 | 13814 16201 309026 19.1 | 47.829 % | c | 425666 | 34232 74909 | 15196 16425 314585 19.2 | 47.882 % | c | 426004 | 34232 74909 | 16715 16763 323332 19.3 | 47.882 % | c | 426510 | 34232 74909 | 18387 17269 335565 19.4 | 47.882 % | c | 427269 | 34232 74909 | 20225 18028 360184 20.0 | 47.882 % | c | 428408 | 34230 74905 | 22248 19137 391888 20.5 | 47.886 % | c | 430117 | 34225 74894 | 24473 20843 442862 21.2 | 47.899 % | c | 432680 | 34225 74894 | 26920 23406 518434 22.1 | 47.899 % | c | 436524 | 34127 74674 | 29612 27231 651055 23.9 | 48.175 % | c | 442291 | 33938 74293 | 32574 31785 821921 25.9 | 48.363 % | c | 450940 | 33909 74235 | 35831 40433 1036678 25.6 | 48.438 % | c | 463914 | 33588 73552 | 39414 24437 554602 22.7 | 49.278 % | c | 483375 | 33244 72799 | 43356 43844 1282103 29.2 | 50.249 % | c | 512567 | 33000 72275 | 47691 51376 1520267 29.6 | 50.902 % | c | 556357 | 31874 69857 | 52460 46882 1393857 29.7 | 52.495 % | 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 : 98 c conflicts : 566153 (607 /sec) c decisions : 695343 (746 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 932.238 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.81 0.94 0.92 2/54 6303 Raw data (stat): 6303 (runsolver) R 6302 23310 23309 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840540004 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.0007 s] Raw data (loadavg): 0.84 0.94 0.92 2/55 6307 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.001 s] Raw data (loadavg): 0.86 0.94 0.92 2/55 6307 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0013 s] Raw data (loadavg): 0.88 0.94 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0018 s] Raw data (loadavg): 0.90 0.94 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s] Raw data (loadavg): 0.91 0.94 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.93 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0029 s] Raw data (loadavg): 0.94 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0031 s] Raw data (loadavg): 0.95 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0034 s] Raw data (loadavg): 0.95 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.96 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.97 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.97 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.98 0.95 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+180.002 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+190.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+200.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+210.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+220.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+230.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+240.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+250.003 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+260.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+270.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+280.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+290.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+300.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+310.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+320.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+330.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+340.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+350.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+360.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+370.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+380.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+390.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+400.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+410.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+420.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+430.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+440.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+450.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+460.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+470.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+480.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+490.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+500.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+510.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+520.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+530.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+540.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+550.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+560.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+570.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+580.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+590.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+600.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+610.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+620.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+630.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+640.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+650.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+660.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+670.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+680.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+690.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+700.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+710.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+720.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+730.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+740.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+750.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+760.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+770.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+780.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+790.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+800.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+810.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+820.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+830.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+840.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+850.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+860.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+870.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+880.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+890.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+900.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+910.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+920.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+930.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+932.425 s] Raw data (loadavg): 0.99 0.97 0.92 1/53 6309 Raw data (stat): 6303 (minisat+_script) S 6302 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840540004 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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): 932.424 CPU time (s): 932.548 CPU user time (s): 932.258 CPU system time (s): 0.289955 CPU usage (%): 100.013 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK -30 #### END VERIFIER DATA ####