Name | 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 | YES |
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 | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 940.368 |
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 |
LAUNCH ON wulflinc30 THE 2005-09-18 18:33:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2685 boxname=wulflinc30 idbench=341 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 84d0b0ba659c599a6c66454cd956a06b /oldhome/oroussel/tmp/wulflinc30/normalized-frb30-15-1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-frb30-15-1.opb IDLAUNCH: 2685 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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 : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 907576 kB Buffers: 37496 kB Cached: 59432 kB SwapCached: 788 kB Active: 66036 kB Inactive: 33608 kB HighTotal: 131008 kB HighFree: 70756 kB LowTotal: 903652 kB LowFree: 836820 kB SwapTotal: 2097892 kB SwapFree: 2096636 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5732 kB Slab: 21908 kB Committed_AS: 64172 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:49:40 (client local time) WITH STATUS 30 IN 940.368 SECONDS stats: 2685 0 940.368 30
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 (602 /sec) c decisions : 695343 (740 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 939.898 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/13713/stat): 13713 (minisat+_script) R 13712 13713 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843437186 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/13713/statm): 174 3 169 147 0 27 0 [pid=13713] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=13714 New process pid=13715 New process pid=13716 execve syscall for /bin/sed executable One traced child (pid=13715) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=13716) exited with status: 0 One traced child (pid=13714) exited with status: 0 New process pid=13717 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-frb30-15-1.opb [startup+10.0039 s] Raw data (loadavg): 0.93 0.95 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 1517 0 0 0 983 6 0 0 25 0 1 0 1843437191 6815744 1472 4294967295 134512640 135094434 3221224448 3221223040 134557117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13717/statm): 1664 1472 145 145 0 1519 0 [pid=13717] vsize: 6656 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 8780 [startup+20.0056 s] Raw data (loadavg): 0.94 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 2095 0 0 0 1973 11 0 0 25 0 1 0 1843437191 9175040 2050 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 2240 2050 145 145 0 2095 0 [pid=13717] vsize: 8960 Current children cumulated CPU time (s) 19.84 Current children cumulated vsize (Kb) 11084 [startup+30.0064 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 2634 0 0 0 2962 16 0 0 25 0 1 0 1843437191 11419648 2589 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 2788 2589 145 145 0 2643 0 [pid=13717] vsize: 11152 Current children cumulated CPU time (s) 29.78 Current children cumulated vsize (Kb) 13276 [startup+40.0072 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3114 0 0 0 3952 20 0 0 25 0 1 0 1843437191 13361152 3069 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3262 3069 145 145 0 3117 0 [pid=13717] vsize: 13048 Current children cumulated CPU time (s) 39.72 Current children cumulated vsize (Kb) 15172 [startup+50.008 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3293 0 0 0 4949 22 0 0 25 0 1 0 1843437191 14086144 3248 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3439 3248 145 145 0 3294 0 [pid=13717] vsize: 13756 Current children cumulated CPU time (s) 49.71 Current children cumulated vsize (Kb) 15880 [startup+60.0078 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3293 0 0 0 5948 22 0 0 25 0 1 0 1843437191 14086144 3248 4294967295 134512640 135094434 3221224448 3221223120 134556275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3439 3248 145 145 0 3294 0 [pid=13717] vsize: 13756 Current children cumulated CPU time (s) 59.7 Current children cumulated vsize (Kb) 15880 [startup+70.0086 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3408 0 0 0 6947 23 0 0 25 0 1 0 1843437191 14548992 3363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13717/statm): 3552 3363 145 145 0 3407 0 [pid=13717] vsize: 14208 Current children cumulated CPU time (s) 69.7 Current children cumulated vsize (Kb) 16332 [startup+80.0094 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3474 0 0 0 7945 23 0 0 25 0 1 0 1843437191 14942208 3429 4294967295 134512640 135094434 3221224448 3221223120 134556434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3648 3429 145 145 0 3503 0 [pid=13717] vsize: 14592 Current children cumulated CPU time (s) 79.68 Current children cumulated vsize (Kb) 16716 [startup+90.0102 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3474 0 0 0 8946 23 0 0 25 0 1 0 1843437191 14942208 3429 4294967295 134512640 135094434 3221224448 3221223072 134562161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3648 3429 145 145 0 3503 0 [pid=13717] vsize: 14592 Current children cumulated CPU time (s) 89.69 Current children cumulated vsize (Kb) 16716 [startup+100.011 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3488 0 0 0 9946 24 0 0 25 0 1 0 1843437191 15003648 3443 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3663 3443 145 145 0 3518 0 [pid=13717] vsize: 14652 Current children cumulated CPU time (s) 99.7 Current children cumulated vsize (Kb) 16776 [startup+110.012 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3514 0 0 0 10946 24 0 0 25 0 1 0 1843437191 15118336 3469 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3691 3469 145 145 0 3546 0 [pid=13717] vsize: 14764 Current children cumulated CPU time (s) 109.7 Current children cumulated vsize (Kb) 16888 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3514 0 0 0 11946 24 0 0 25 0 1 0 1843437191 15118336 3469 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3691 3469 145 145 0 3546 0 [pid=13717] vsize: 14764 Current children cumulated CPU time (s) 119.7 Current children cumulated vsize (Kb) 16888 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 12946 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 129.7 Current children cumulated vsize (Kb) 16908 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 13946 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 139.7 Current children cumulated vsize (Kb) 16908 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 14946 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 149.7 Current children cumulated vsize (Kb) 16908 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 15946 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 159.7 Current children cumulated vsize (Kb) 16908 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 16946 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 169.7 Current children cumulated vsize (Kb) 16908 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 17947 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 179.71 Current children cumulated vsize (Kb) 16908 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 18947 24 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 189.71 Current children cumulated vsize (Kb) 16908 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 19947 25 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 199.72 Current children cumulated vsize (Kb) 16908 [startup+210.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 20947 25 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 209.72 Current children cumulated vsize (Kb) 16908 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 21947 25 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 219.72 Current children cumulated vsize (Kb) 16908 [startup+230.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 22948 25 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 229.73 Current children cumulated vsize (Kb) 16908 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3519 0 0 0 23948 25 0 0 25 0 1 0 1843437191 15138816 3474 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3696 3474 145 145 0 3551 0 [pid=13717] vsize: 14784 Current children cumulated CPU time (s) 239.73 Current children cumulated vsize (Kb) 16908 [startup+250.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3604 0 0 0 24947 25 0 0 25 0 1 0 1843437191 15495168 3559 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 3783 3559 145 145 0 3638 0 [pid=13717] vsize: 15132 Current children cumulated CPU time (s) 249.72 Current children cumulated vsize (Kb) 17256 [startup+260.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3850 0 0 0 25943 27 0 0 25 0 1 0 1843437191 16551936 3805 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4041 3805 145 145 0 3896 0 [pid=13717] vsize: 16164 Current children cumulated CPU time (s) 259.7 Current children cumulated vsize (Kb) 18288 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3879 0 0 0 26942 27 0 0 25 0 1 0 1843437191 16666624 3834 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4069 3834 145 145 0 3924 0 [pid=13717] vsize: 16276 Current children cumulated CPU time (s) 269.69 Current children cumulated vsize (Kb) 18400 [startup+280.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3887 0 0 0 27943 27 0 0 25 0 1 0 1843437191 16715776 3842 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13717/statm): 4081 3842 145 145 0 3936 0 [pid=13717] vsize: 16324 Current children cumulated CPU time (s) 279.7 Current children cumulated vsize (Kb) 18448 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3890 0 0 0 28942 28 0 0 25 0 1 0 1843437191 16732160 3845 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3845 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 289.7 Current children cumulated vsize (Kb) 18464 [startup+300.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3890 0 0 0 29943 28 0 0 25 0 1 0 1843437191 16732160 3845 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3845 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 299.71 Current children cumulated vsize (Kb) 18464 [startup+310.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3891 0 0 0 30943 28 0 0 25 0 1 0 1843437191 16732160 3846 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3846 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 309.71 Current children cumulated vsize (Kb) 18464 [startup+320.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3892 0 0 0 31943 28 0 0 25 0 1 0 1843437191 16732160 3847 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3847 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 319.71 Current children cumulated vsize (Kb) 18464 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3894 0 0 0 32943 28 0 0 25 0 1 0 1843437191 16732160 3849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3849 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 329.71 Current children cumulated vsize (Kb) 18464 [startup+340.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3894 0 0 0 33943 28 0 0 25 0 1 0 1843437191 16732160 3849 4294967295 134512640 135094434 3221224448 3221223072 134557627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3849 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 339.71 Current children cumulated vsize (Kb) 18464 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3894 0 0 0 34944 28 0 0 25 0 1 0 1843437191 16732160 3849 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3849 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 349.72 Current children cumulated vsize (Kb) 18464 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3895 0 0 0 35944 28 0 0 25 0 1 0 1843437191 16732160 3850 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3850 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 359.72 Current children cumulated vsize (Kb) 18464 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3896 0 0 0 36944 28 0 0 25 0 1 0 1843437191 16732160 3851 4294967295 134512640 135094434 3221224448 3221223136 134554859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3851 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 369.72 Current children cumulated vsize (Kb) 18464 [startup+380.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3896 0 0 0 37944 28 0 0 25 0 1 0 1843437191 16732160 3851 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3851 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 379.72 Current children cumulated vsize (Kb) 18464 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3896 0 0 0 38945 28 0 0 25 0 1 0 1843437191 16732160 3851 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3851 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 389.73 Current children cumulated vsize (Kb) 18464 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3897 0 0 0 39944 28 0 0 25 0 1 0 1843437191 16732160 3852 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3852 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 399.72 Current children cumulated vsize (Kb) 18464 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3897 0 0 0 40945 28 0 0 25 0 1 0 1843437191 16732160 3852 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3852 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 409.73 Current children cumulated vsize (Kb) 18464 [startup+420.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3897 0 0 0 41945 28 0 0 25 0 1 0 1843437191 16732160 3852 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3852 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 419.73 Current children cumulated vsize (Kb) 18464 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3897 0 0 0 42945 28 0 0 25 0 1 0 1843437191 16732160 3852 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3852 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 429.73 Current children cumulated vsize (Kb) 18464 [startup+440.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 43945 28 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 439.73 Current children cumulated vsize (Kb) 18464 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 44946 28 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 449.74 Current children cumulated vsize (Kb) 18464 [startup+460.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 45946 28 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 459.74 Current children cumulated vsize (Kb) 18464 [startup+470.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 46946 28 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 469.74 Current children cumulated vsize (Kb) 18464 [startup+480.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 47946 28 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 479.74 Current children cumulated vsize (Kb) 18464 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 48946 29 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 489.75 Current children cumulated vsize (Kb) 18464 [startup+500.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 49946 29 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 499.75 Current children cumulated vsize (Kb) 18464 [startup+510.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 50947 29 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 509.76 Current children cumulated vsize (Kb) 18464 [startup+520.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 51945 30 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 519.75 Current children cumulated vsize (Kb) 18464 [startup+530.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 52945 30 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 529.75 Current children cumulated vsize (Kb) 18464 [startup+540.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3898 0 0 0 53945 30 0 0 25 0 1 0 1843437191 16732160 3853 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3853 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 539.75 Current children cumulated vsize (Kb) 18464 [startup+550.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3899 0 0 0 54945 31 0 0 25 0 1 0 1843437191 16732160 3854 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3854 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 549.76 Current children cumulated vsize (Kb) 18464 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3899 0 0 0 55945 31 0 0 25 0 1 0 1843437191 16732160 3854 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3854 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 559.76 Current children cumulated vsize (Kb) 18464 [startup+570.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3899 0 0 0 56945 31 0 0 25 0 1 0 1843437191 16732160 3854 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3854 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 569.76 Current children cumulated vsize (Kb) 18464 [startup+580.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3899 0 0 0 57945 31 0 0 25 0 1 0 1843437191 16732160 3854 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3854 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 579.76 Current children cumulated vsize (Kb) 18464 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 3899 0 0 0 58945 31 0 0 25 0 1 0 1843437191 16732160 3854 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4085 3854 145 145 0 3940 0 [pid=13717] vsize: 16340 Current children cumulated CPU time (s) 589.76 Current children cumulated vsize (Kb) 18464 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4236 0 0 0 59945 32 0 0 25 0 1 0 1843437191 18776064 4191 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4584 4191 145 145 0 4439 0 [pid=13717] vsize: 18336 Current children cumulated CPU time (s) 599.77 Current children cumulated vsize (Kb) 20460 [startup+610.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4236 0 0 0 60945 32 0 0 25 0 1 0 1843437191 18776064 4191 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4584 4191 145 145 0 4439 0 [pid=13717] vsize: 18336 Current children cumulated CPU time (s) 609.77 Current children cumulated vsize (Kb) 20460 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4236 0 0 0 61945 32 0 0 25 0 1 0 1843437191 18776064 4191 4294967295 134512640 135094434 3221224448 3221223088 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4584 4191 145 145 0 4439 0 [pid=13717] vsize: 18336 Current children cumulated CPU time (s) 619.77 Current children cumulated vsize (Kb) 20460 [startup+630.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4236 0 0 0 62945 33 0 0 25 0 1 0 1843437191 18776064 4191 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4584 4191 145 145 0 4439 0 [pid=13717] vsize: 18336 Current children cumulated CPU time (s) 629.78 Current children cumulated vsize (Kb) 20460 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4236 0 0 0 63945 33 0 0 25 0 1 0 1843437191 18776064 4191 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4584 4191 145 145 0 4439 0 [pid=13717] vsize: 18336 Current children cumulated CPU time (s) 639.78 Current children cumulated vsize (Kb) 20460 [startup+650.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4236 0 0 0 64945 33 0 0 25 0 1 0 1843437191 18776064 4191 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4584 4191 145 145 0 4439 0 [pid=13717] vsize: 18336 Current children cumulated CPU time (s) 649.78 Current children cumulated vsize (Kb) 20460 [startup+660.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4335 0 0 0 65943 34 0 0 25 0 1 0 1843437191 19161088 4290 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4678 4290 145 145 0 4533 0 [pid=13717] vsize: 18712 Current children cumulated CPU time (s) 659.77 Current children cumulated vsize (Kb) 20836 [startup+670.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4429 0 0 0 66942 35 0 0 25 0 1 0 1843437191 19542016 4384 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4771 4384 145 145 0 4626 0 [pid=13717] vsize: 19084 Current children cumulated CPU time (s) 669.77 Current children cumulated vsize (Kb) 21208 [startup+680.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4429 0 0 0 67942 35 0 0 25 0 1 0 1843437191 19542016 4384 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4771 4384 145 145 0 4626 0 [pid=13717] vsize: 19084 Current children cumulated CPU time (s) 679.77 Current children cumulated vsize (Kb) 21208 [startup+690.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4429 0 0 0 68942 35 0 0 25 0 1 0 1843437191 19542016 4384 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4771 4384 145 145 0 4626 0 [pid=13717] vsize: 19084 Current children cumulated CPU time (s) 689.77 Current children cumulated vsize (Kb) 21208 [startup+700.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4442 0 0 0 69942 36 0 0 25 0 1 0 1843437191 19607552 4397 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4787 4397 145 145 0 4642 0 [pid=13717] vsize: 19148 Current children cumulated CPU time (s) 699.78 Current children cumulated vsize (Kb) 21272 [startup+710.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4442 0 0 0 70942 36 0 0 25 0 1 0 1843437191 19607552 4397 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4787 4397 145 145 0 4642 0 [pid=13717] vsize: 19148 Current children cumulated CPU time (s) 709.78 Current children cumulated vsize (Kb) 21272 [startup+720.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4446 0 0 0 71942 36 0 0 25 0 1 0 1843437191 19623936 4401 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4791 4401 145 145 0 4646 0 [pid=13717] vsize: 19164 Current children cumulated CPU time (s) 719.78 Current children cumulated vsize (Kb) 21288 [startup+730.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4543 0 0 0 72941 36 0 0 25 0 1 0 1843437191 20041728 4498 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 4893 4498 145 145 0 4748 0 [pid=13717] vsize: 19572 Current children cumulated CPU time (s) 729.77 Current children cumulated vsize (Kb) 21696 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4664 0 0 0 73939 38 0 0 25 0 1 0 1843437191 20525056 4619 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5011 4619 145 145 0 4866 0 [pid=13717] vsize: 20044 Current children cumulated CPU time (s) 739.77 Current children cumulated vsize (Kb) 22168 [startup+750.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4760 0 0 0 74937 38 0 0 25 0 1 0 1843437191 20905984 4715 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5104 4715 145 145 0 4959 0 [pid=13717] vsize: 20416 Current children cumulated CPU time (s) 749.75 Current children cumulated vsize (Kb) 22540 [startup+760.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4766 0 0 0 75937 38 0 0 25 0 1 0 1843437191 20942848 4721 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5113 4721 145 145 0 4968 0 [pid=13717] vsize: 20452 Current children cumulated CPU time (s) 759.75 Current children cumulated vsize (Kb) 22576 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4766 0 0 0 76937 38 0 0 25 0 1 0 1843437191 20942848 4721 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5113 4721 145 145 0 4968 0 [pid=13717] vsize: 20452 Current children cumulated CPU time (s) 769.75 Current children cumulated vsize (Kb) 22576 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4766 0 0 0 77938 38 0 0 25 0 1 0 1843437191 20942848 4721 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5113 4721 145 145 0 4968 0 [pid=13717] vsize: 20452 Current children cumulated CPU time (s) 779.76 Current children cumulated vsize (Kb) 22576 [startup+790.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4766 0 0 0 78938 38 0 0 25 0 1 0 1843437191 20942848 4721 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5113 4721 145 145 0 4968 0 [pid=13717] vsize: 20452 Current children cumulated CPU time (s) 789.76 Current children cumulated vsize (Kb) 22576 [startup+800.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4774 0 0 0 79938 39 0 0 25 0 1 0 1843437191 20983808 4729 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5123 4729 145 145 0 4978 0 [pid=13717] vsize: 20492 Current children cumulated CPU time (s) 799.77 Current children cumulated vsize (Kb) 22616 [startup+810.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4835 0 0 0 80937 39 0 0 25 0 1 0 1843437191 21241856 4790 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5186 4790 145 145 0 5041 0 [pid=13717] vsize: 20744 Current children cumulated CPU time (s) 809.76 Current children cumulated vsize (Kb) 22868 [startup+820.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 4967 0 0 0 81935 40 0 0 25 0 1 0 1843437191 21770240 4922 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5315 4922 145 145 0 5170 0 [pid=13717] vsize: 21260 Current children cumulated CPU time (s) 819.75 Current children cumulated vsize (Kb) 23384 [startup+830.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5033 0 0 0 82934 41 0 0 25 0 1 0 1843437191 22036480 4988 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5380 4988 145 145 0 5235 0 [pid=13717] vsize: 21520 Current children cumulated CPU time (s) 829.75 Current children cumulated vsize (Kb) 23644 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5033 0 0 0 83934 41 0 0 25 0 1 0 1843437191 22036480 4988 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5380 4988 145 145 0 5235 0 [pid=13717] vsize: 21520 Current children cumulated CPU time (s) 839.75 Current children cumulated vsize (Kb) 23644 [startup+850.064 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5033 0 0 0 84935 41 0 0 25 0 1 0 1843437191 22036480 4988 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5380 4988 145 145 0 5235 0 [pid=13717] vsize: 21520 Current children cumulated CPU time (s) 849.76 Current children cumulated vsize (Kb) 23644 [startup+860.064 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5041 0 0 0 85934 41 0 0 25 0 1 0 1843437191 22069248 4996 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5388 4996 145 145 0 5243 0 [pid=13717] vsize: 21552 Current children cumulated CPU time (s) 859.75 Current children cumulated vsize (Kb) 23676 [startup+870.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5050 0 0 0 86935 41 0 0 25 0 1 0 1843437191 22118400 5005 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5400 5005 145 145 0 5255 0 [pid=13717] vsize: 21600 Current children cumulated CPU time (s) 869.76 Current children cumulated vsize (Kb) 23724 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5053 0 0 0 87935 41 0 0 25 0 1 0 1843437191 22118400 5008 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5400 5008 145 145 0 5255 0 [pid=13717] vsize: 21600 Current children cumulated CPU time (s) 879.76 Current children cumulated vsize (Kb) 23724 [startup+890.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5070 0 0 0 88935 41 0 0 25 0 1 0 1843437191 22216704 5025 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5424 5025 145 145 0 5279 0 [pid=13717] vsize: 21696 Current children cumulated CPU time (s) 889.76 Current children cumulated vsize (Kb) 23820 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5071 0 0 0 89935 41 0 0 25 0 1 0 1843437191 22216704 5026 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5424 5026 145 145 0 5279 0 [pid=13717] vsize: 21696 Current children cumulated CPU time (s) 899.76 Current children cumulated vsize (Kb) 23820 [startup+910.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5071 0 0 0 90935 41 0 0 25 0 1 0 1843437191 22216704 5026 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5424 5026 145 145 0 5279 0 [pid=13717] vsize: 21696 Current children cumulated CPU time (s) 909.76 Current children cumulated vsize (Kb) 23820 [startup+920.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5077 0 0 0 91936 41 0 0 25 0 1 0 1843437191 22249472 5032 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5432 5032 145 145 0 5287 0 [pid=13717] vsize: 21728 Current children cumulated CPU time (s) 919.77 Current children cumulated vsize (Kb) 23852 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5077 0 0 0 92936 42 0 0 25 0 1 0 1843437191 22249472 5032 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5432 5032 145 145 0 5287 0 [pid=13717] vsize: 21728 Current children cumulated CPU time (s) 929.78 Current children cumulated vsize (Kb) 23852 [startup+940.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 13717 Raw data (/proc/13713/stat): 13713 (minisat+_script) S 13712 13713 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843437186 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13713/statm): 531 226 485 147 0 384 0 [pid=13713] vsize: 2124 Raw data (/proc/13717/stat): 13717 (minisat+_64-bit) R 13713 13713 5245 0 -1 0 5078 0 0 0 93936 42 0 0 25 0 1 0 1843437191 22249472 5033 4294967295 134512640 135094434 3221224448 3221223088 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13717/statm): 5432 5033 145 145 0 5287 0 [pid=13717] vsize: 21728 Current children cumulated CPU time (s) 939.78 Current children cumulated vsize (Kb) 23852 One traced child (pid=13717) exited with status: 30 One traced child (pid=13713) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 940.638 CPU time (s): 940.368 CPU user time (s): 939.92 CPU system time (s): 0.447931 CPU usage (%): 99.9713 Max. virtual memory (cumulated for all children) (Kb): 23852
Verifier: OK -30