Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-2.opb |
MD5SUM | 270e069f649d19b0da4e4d23c0e1ebfc |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -33 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 760 |
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 | 760 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 760 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.03 |
Number of variables | 760 |
Total number of constraints | 41263 |
Number of constraints which are clauses | 41263 |
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 wulflinc1 THE 2005-09-18 18:44:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2696 boxname=wulflinc1 idbench=352 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 270e069f649d19b0da4e4d23c0e1ebfc /oldhome/oroussel/tmp/wulflinc1/normalized-frb40-19-2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-frb40-19-2.opb IDLAUNCH: 2696 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 880652 kB Buffers: 37924 kB Cached: 86084 kB SwapCached: 908 kB Active: 96028 kB Inactive: 30824 kB HighTotal: 131008 kB HighFree: 48888 kB LowTotal: 903652 kB LowFree: 831764 kB SwapTotal: 2097136 kB SwapFree: 2095620 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5992 kB Slab: 21452 kB Committed_AS: 93132 kB PageTables: 344 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 19:04:58 (client local time) WITH STATUS 10 IN 1209.32 SECONDS stats: 2696 7 1209.32 10
c Parsing PB file... c Converting 41263 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 | 41263 82526 | 13754 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost:35010 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 77411 167438 | 25803 0 0 nan | 0.000 % | c | 100 | 77197 167004 | 28383 85 1743 20.5 | 0.449 % | c | 250 | 76777 166128 | 31221 216 3076 14.2 | 1.370 % | c | 475 | 75681 163748 | 34343 367 7270 19.8 | 3.965 % | c | 812 | 74772 161767 | 37778 638 10625 16.7 | 6.213 % | c | 1318 | 72216 156098 | 41555 971 15210 15.7 | 12.362 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1358 | 71957 155524 | 23985 1000 15644 15.6 | 12.362 % | c | 1458 | 71484 154445 | 26383 1077 16216 15.1 | 14.235 % | c | 1609 | 70637 152550 | 29021 1185 17694 14.9 | 16.491 % | c | 1834 | 69903 150904 | 31924 1355 19103 14.1 | 18.302 % | c | 2171 | 68629 148052 | 35116 1633 21862 13.4 | 21.386 % | c | 2677 | 66555 143323 | 38628 2003 25849 12.9 | 26.681 % | c | 3436 | 63907 137250 | 42490 2573 35121 13.6 | 33.519 % | c | 4575 | 60641 129717 | 46739 3414 45806 13.4 | 42.032 % | c | 6284 | 58132 123765 | 51413 4758 70644 14.8 | 48.684 % | c ============================================================================== c [1mFound solution: -32[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6893 | 57499 122346 | 19166 5251 79403 15.1 | 48.684 % | c | 6993 | 57374 122059 | 21082 5340 80419 15.1 | 50.986 % | c | 7143 | 57174 121601 | 23190 5476 83135 15.2 | 51.497 % | c | 7368 | 57124 121493 | 25509 5691 90616 15.9 | 51.614 % | c | 7705 | 56450 119888 | 28060 5895 93895 15.9 | 53.460 % | c | 8211 | 55724 118204 | 30867 6317 101819 16.1 | 55.371 % | c | 8970 | 54430 115147 | 33953 6865 120056 17.5 | 58.891 % | c | 10109 | 53229 112295 | 37349 7784 156050 20.0 | 62.178 % | c | 11817 | 51998 109354 | 41084 9200 202992 22.1 | 65.558 % | c | 14379 | 50235 105114 | 45192 10981 295829 26.9 | 70.406 % | c ============================================================================== c [1mFound solution: -33[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15965 | 49478 103359 | 16492 12311 371372 30.2 | 70.406 % | c | 16066 | 49478 103359 | 18141 12412 374678 30.2 | 72.440 % | c | 16216 | 49424 103225 | 19955 12525 376566 30.1 | 72.597 % | c | 16441 | 49285 102876 | 21950 12651 381138 30.1 | 72.991 % | c | 16778 | 49212 102697 | 24145 12924 395334 30.6 | 73.204 % | c | 17285 | 49156 102561 | 26560 13400 438885 32.8 | 73.360 % | c | 18044 | 48324 100548 | 29216 13832 461348 33.4 | 75.707 % | c | 19183 | 48201 100261 | 32138 14905 550058 36.9 | 76.033 % | c | 20891 | 47874 99472 | 35352 16285 636889 39.1 | 76.957 % | c | 23453 | 47628 98870 | 38887 18649 839926 45.0 | 77.656 % | c ============================================================================== c [1mFound solution: -34[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25038 | 47524 98566 | 15841 20184 980752 48.6 | 77.656 % | c | 25139 | 47524 98566 | 17425 20285 983661 48.5 | 77.940 % | c | 25289 | 47524 98566 | 19167 20435 990976 48.5 | 77.939 % | c | 25514 | 47524 98566 | 21084 20660 1005617 48.7 | 77.939 % | c | 25851 | 47524 98566 | 23192 20997 1026282 48.9 | 77.939 % | c | 26358 | 47524 98566 | 25512 21504 1055909 49.1 | 77.940 % | c | 27118 | 47524 98566 | 28063 22264 1120991 50.3 | 77.939 % | c | 28258 | 47202 97772 | 30869 23237 1219781 52.5 | 78.852 % | c | 29966 | 47191 97747 | 33956 24941 1366171 54.8 | 78.880 % | c | 32528 | 47072 97453 | 37352 27423 1611937 58.8 | 79.221 % | c | 36372 | 47072 97453 | 41087 31267 2099445 67.1 | 79.221 % | c | 42138 | 46746 96661 | 45196 36763 2600401 70.7 | 80.142 % | c ============================================================================== c [1mFound solution: -35[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46022 | 46748 96684 | 15582 40621 3011087 74.1 | 80.142 % | c | 46122 | 46748 96684 | 17140 18203 1211729 66.6 | 80.221 % | c | 46272 | 46748 96684 | 18854 18353 1218705 66.4 | 80.221 % | c | 46497 | 46714 96607 | 20739 18539 1230555 66.4 | 80.297 % | c | 46834 | 46703 96582 | 22813 18867 1250274 66.3 | 80.325 % | c | 47340 | 46651 96453 | 25094 19368 1284175 66.3 | 80.473 % | c | 48100 | 46472 96017 | 27604 20063 1320976 65.8 | 80.974 % | c | 49239 | 46437 95936 | 30364 21181 1424831 67.3 | 81.066 % | c | 50947 | 46434 95929 | 33401 22886 1532403 67.0 | 81.074 % | c | 53509 | 46389 95814 | 36741 25444 1762687 69.3 | 81.214 % | c | 57353 | 46351 95720 | 40415 29177 2121672 72.7 | 81.326 % | c | 63119 | 46102 95119 | 44457 34489 2610152 75.7 | 82.030 % | c | 71769 | 46087 95084 | 48902 43071 3470985 80.6 | 82.070 % | c | 84743 | 46022 94925 | 53793 55928 4763761 85.2 | 82.259 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 91656 | 46006 94872 | 15335 62707 5469040 87.2 | 82.259 % | c | 91756 | 46006 94872 | 16868 20099 1258236 62.6 | 82.312 % | c | 91906 | 46004 94868 | 18555 20247 1269896 62.7 | 82.316 % | c | 92131 | 45981 94815 | 20410 20467 1286191 62.8 | 82.376 % | c | 92469 | 45978 94808 | 22451 20801 1325256 63.7 | 82.384 % | c | 92975 | 45956 94754 | 24697 21154 1350045 63.8 | 82.448 % | c | 93735 | 45891 94586 | 27166 21886 1408143 64.3 | 82.640 % | c | 94874 | 45891 94586 | 29883 23025 1506974 65.4 | 82.640 % | c | 96582 | 45850 94484 | 32871 24718 1656829 67.0 | 82.756 % | c | 99144 | 45850 94484 | 36159 27280 1890855 69.3 | 82.756 % | c | 102988 | 45767 94285 | 39775 31063 2199681 70.8 | 82.989 % | c | 108754 | 45767 94285 | 43752 36829 2758646 74.9 | 82.988 % | c | 117404 | 45755 94257 | 48127 45475 3584527 78.8 | 83.021 % | c | 130378 | 45713 94155 | 52940 58391 4806838 82.3 | 83.141 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 136420 | 45733 94207 | 15244 64433 5331404 82.7 | 83.141 % | c | 136520 | 45733 94207 | 16768 20826 1132496 54.4 | 83.107 % | c | 136670 | 45733 94207 | 18445 20976 1139985 54.3 | 83.107 % | c | 136895 | 45733 94207 | 20289 21201 1153537 54.4 | 83.107 % | c | 137232 | 45733 94207 | 22318 21538 1169510 54.3 | 83.107 % | c | 137738 | 45733 94207 | 24550 22044 1213136 55.0 | 83.107 % | c | 138497 | 45733 94207 | 27005 22803 1266674 55.5 | 83.108 % | c | 139636 | 45733 94207 | 29706 23942 1351252 56.4 | 83.107 % | c | 141344 | 45733 94207 | 32676 25650 1504180 58.6 | 83.107 % | c | 143906 | 45733 94207 | 35944 28212 1667932 59.1 | 83.107 % | c | 147751 | 45733 94207 | 39539 32057 2014186 62.8 | 83.107 % | c | 153517 | 45733 94207 | 43492 37823 2552526 67.5 | 83.107 % | c | 162166 | 45681 94069 | 47842 46460 3249653 69.9 | 83.271 % | c | 175140 | 45681 94069 | 52626 59434 4360949 73.4 | 83.271 % | c | 194601 | 45651 93995 | 57889 24662 1331831 54.0 | 83.359 % | c | 223793 | 45636 93958 | 63677 53847 4465405 82.9 | 83.403 % | c | 267582 | 45636 93958 | 70045 31596 1238437 39.2 | 83.403 % | c | 333266 | 45616 93912 | 77050 24572 866247 35.3 | 83.455 % | c | 431792 | 45563 93787 | 84755 42419 1615243 38.1 | 83.599 % | c c *** TERMINATED *** s SATISFIABLE v -C760 -C759 -C758 -C757 -C756 -C755 -C754 C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 C631 -C630 -C629 -C628 -C627 C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 C480 -C479 -C478 -C477 -C476 C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 C451 -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 -C7
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/27181/stat): 27181 (minisat+_script) R 27180 27181 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1728431273 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/27181/statm): 174 3 169 147 0 27 0 [pid=27181] 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=27182 New process pid=27183 New process pid=27184 execve syscall for /bin/sed executable One traced child (pid=27183) 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=27184) exited with status: 0 One traced child (pid=27182) exited with status: 0 New process pid=27185 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-frb40-19-2.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 2879 0 0 0 974 12 0 0 25 0 1 0 1728431278 12726272 2866 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 3107 2866 145 145 0 2962 0 [pid=27185] vsize: 12428 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 14552 [startup+20.0053 s] Raw data (loadavg): 0.94 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 2879 0 0 0 1973 12 0 0 25 0 1 0 1728431278 12726272 2866 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 3107 2866 145 145 0 2962 0 [pid=27185] vsize: 12428 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 14552 [startup+30.0071 s] Raw data (loadavg): 0.95 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 2940 0 0 0 2972 13 0 0 25 0 1 0 1728431278 12976128 2927 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 3168 2927 145 145 0 3023 0 [pid=27185] vsize: 12672 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 14796 [startup+40.0079 s] Raw data (loadavg): 0.96 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 3198 0 0 0 3967 14 0 0 25 0 1 0 1728431278 14049280 3185 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 3430 3185 145 145 0 3285 0 [pid=27185] vsize: 13720 Current children cumulated CPU time (s) 39.83 Current children cumulated vsize (Kb) 15844 [startup+50.0087 s] Raw data (loadavg): 0.96 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 3609 0 0 0 4960 17 0 0 25 0 1 0 1728431278 15876096 3596 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 3876 3596 145 145 0 3731 0 [pid=27185] vsize: 15504 Current children cumulated CPU time (s) 49.79 Current children cumulated vsize (Kb) 17628 [startup+60.0095 s] Raw data (loadavg): 0.97 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 4231 0 0 0 5950 21 0 0 25 0 1 0 1728431278 18399232 4218 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 4492 4218 145 145 0 4347 0 [pid=27185] vsize: 17968 Current children cumulated CPU time (s) 59.73 Current children cumulated vsize (Kb) 20092 [startup+70.0102 s] Raw data (loadavg): 0.97 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 4852 0 0 0 6938 26 0 0 25 0 1 0 1728431278 20922368 4839 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 5108 4839 145 145 0 4963 0 [pid=27185] vsize: 20432 Current children cumulated CPU time (s) 69.66 Current children cumulated vsize (Kb) 22556 [startup+80.011 s] Raw data (loadavg): 0.98 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 5328 0 0 0 7928 30 0 0 25 0 1 0 1728431278 22986752 5315 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 5612 5315 145 145 0 5467 0 [pid=27185] vsize: 22448 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 24572 [startup+90.0118 s] Raw data (loadavg): 0.98 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 5832 0 0 0 8920 34 0 0 25 0 1 0 1728431278 25030656 5819 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 6111 5819 145 145 0 5966 0 [pid=27185] vsize: 24444 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 26568 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 9913 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0 [pid=27185] vsize: 25772 Current children cumulated CPU time (s) 99.52 Current children cumulated vsize (Kb) 27896 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 10914 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0 [pid=27185] vsize: 25772 Current children cumulated CPU time (s) 109.53 Current children cumulated vsize (Kb) 27896 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 11914 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0 [pid=27185] vsize: 25772 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 27896 [startup+130.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 12914 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0 [pid=27185] vsize: 25772 Current children cumulated CPU time (s) 129.53 Current children cumulated vsize (Kb) 27896 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6334 0 0 0 13911 38 0 0 25 0 1 0 1728431278 27078656 6321 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 6611 6321 145 145 0 6466 0 [pid=27185] vsize: 26444 Current children cumulated CPU time (s) 139.51 Current children cumulated vsize (Kb) 28568 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6821 0 0 0 14902 42 0 0 25 0 1 0 1728431278 29061120 6808 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 7095 6808 145 145 0 6950 0 [pid=27185] vsize: 28380 Current children cumulated CPU time (s) 149.46 Current children cumulated vsize (Kb) 30504 [startup+160.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 7200 0 0 0 15893 45 0 0 25 0 1 0 1728431278 30597120 7187 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 7470 7187 145 145 0 7325 0 [pid=27185] vsize: 29880 Current children cumulated CPU time (s) 159.4 Current children cumulated vsize (Kb) 32004 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 7573 0 0 0 16886 47 0 0 25 0 1 0 1728431278 32112640 7560 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 7840 7560 145 145 0 7695 0 [pid=27185] vsize: 31360 Current children cumulated CPU time (s) 169.35 Current children cumulated vsize (Kb) 33484 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 7903 0 0 0 17882 49 0 0 25 0 1 0 1728431278 33452032 7890 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 8167 7890 145 145 0 8022 0 [pid=27185] vsize: 32668 Current children cumulated CPU time (s) 179.33 Current children cumulated vsize (Kb) 34792 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8259 0 0 0 18876 52 0 0 25 0 1 0 1728431278 34893824 8246 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 8519 8246 145 145 0 8374 0 [pid=27185] vsize: 34076 Current children cumulated CPU time (s) 189.3 Current children cumulated vsize (Kb) 36200 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8655 0 0 0 19870 55 0 0 25 0 1 0 1728431278 36503552 8642 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 8912 8642 145 145 0 8767 0 [pid=27185] vsize: 35648 Current children cumulated CPU time (s) 199.27 Current children cumulated vsize (Kb) 37772 [startup+210.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 20865 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 209.24 Current children cumulated vsize (Kb) 38772 [startup+220.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 21865 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 219.24 Current children cumulated vsize (Kb) 38772 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 22866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 229.25 Current children cumulated vsize (Kb) 38772 [startup+240.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 23866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 239.25 Current children cumulated vsize (Kb) 38772 [startup+250.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 24866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 249.25 Current children cumulated vsize (Kb) 38772 [startup+260.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 25866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 259.25 Current children cumulated vsize (Kb) 38772 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 26867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 269.26 Current children cumulated vsize (Kb) 38772 [startup+280.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 27867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 279.26 Current children cumulated vsize (Kb) 38772 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 28867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 289.26 Current children cumulated vsize (Kb) 38772 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 29867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 299.26 Current children cumulated vsize (Kb) 38772 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 30867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 309.26 Current children cumulated vsize (Kb) 38772 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 31867 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 319.26 Current children cumulated vsize (Kb) 38772 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 32868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 329.27 Current children cumulated vsize (Kb) 38772 [startup+340.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 33868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 339.27 Current children cumulated vsize (Kb) 38772 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 34868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 349.27 Current children cumulated vsize (Kb) 38772 [startup+360.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 35868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 359.27 Current children cumulated vsize (Kb) 38772 [startup+370.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 36868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 369.27 Current children cumulated vsize (Kb) 38772 [startup+380.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 37869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 379.28 Current children cumulated vsize (Kb) 38772 [startup+390.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 38869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 389.28 Current children cumulated vsize (Kb) 38772 [startup+400.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 39869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 399.28 Current children cumulated vsize (Kb) 38772 [startup+410.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 40869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 409.28 Current children cumulated vsize (Kb) 38772 [startup+420.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8909 0 0 0 41869 57 0 0 25 0 1 0 1728431278 37527552 8896 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9162 8896 145 145 0 9017 0 [pid=27185] vsize: 36648 Current children cumulated CPU time (s) 419.28 Current children cumulated vsize (Kb) 38772 [startup+430.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8912 0 0 0 42870 57 0 0 25 0 1 0 1728431278 37789696 8899 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9226 8899 145 145 0 9081 0 [pid=27185] vsize: 36904 Current children cumulated CPU time (s) 429.29 Current children cumulated vsize (Kb) 39028 [startup+440.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8954 0 0 0 43869 57 0 0 25 0 1 0 1728431278 37949440 8941 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9265 8941 145 145 0 9120 0 [pid=27185] vsize: 37060 Current children cumulated CPU time (s) 439.28 Current children cumulated vsize (Kb) 39184 [startup+450.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9177 0 0 0 44866 59 0 0 25 0 1 0 1728431278 38850560 9164 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9485 9164 145 145 0 9340 0 [pid=27185] vsize: 37940 Current children cumulated CPU time (s) 449.27 Current children cumulated vsize (Kb) 40064 [startup+460.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 45865 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 459.26 Current children cumulated vsize (Kb) 40244 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 46866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 469.27 Current children cumulated vsize (Kb) 40244 [startup+480.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 47866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 479.27 Current children cumulated vsize (Kb) 40244 [startup+490.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 48866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 489.27 Current children cumulated vsize (Kb) 40244 [startup+500.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 49866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 499.27 Current children cumulated vsize (Kb) 40244 [startup+510.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 50867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 509.28 Current children cumulated vsize (Kb) 40244 [startup+520.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 51867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 519.28 Current children cumulated vsize (Kb) 40244 [startup+530.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 52867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 529.28 Current children cumulated vsize (Kb) 40244 [startup+540.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 53867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 539.28 Current children cumulated vsize (Kb) 40244 [startup+550.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 54867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 549.28 Current children cumulated vsize (Kb) 40244 [startup+560.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 55868 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 559.29 Current children cumulated vsize (Kb) 40244 [startup+570.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 56868 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0 [pid=27185] vsize: 38120 Current children cumulated CPU time (s) 569.29 Current children cumulated vsize (Kb) 40244 [startup+580.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9227 0 0 0 57868 59 0 0 25 0 1 0 1728431278 39051264 9214 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9534 9214 145 145 0 9389 0 [pid=27185] vsize: 38136 Current children cumulated CPU time (s) 579.29 Current children cumulated vsize (Kb) 40260 [startup+590.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9365 0 0 0 58865 61 0 0 25 0 1 0 1728431278 39616512 9352 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9672 9352 145 145 0 9527 0 [pid=27185] vsize: 38688 Current children cumulated CPU time (s) 589.28 Current children cumulated vsize (Kb) 40812 [startup+600.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9491 0 0 0 59864 62 0 0 25 0 1 0 1728431278 40124416 9478 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9796 9478 145 145 0 9651 0 [pid=27185] vsize: 39184 Current children cumulated CPU time (s) 599.28 Current children cumulated vsize (Kb) 41308 [startup+610.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9623 0 0 0 60862 63 0 0 25 0 1 0 1728431278 40669184 9610 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 9929 9610 145 145 0 9784 0 [pid=27185] vsize: 39716 Current children cumulated CPU time (s) 609.27 Current children cumulated vsize (Kb) 41840 [startup+620.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9843 0 0 0 61857 64 0 0 25 0 1 0 1728431278 41549824 9830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10144 9830 145 145 0 9999 0 [pid=27185] vsize: 40576 Current children cumulated CPU time (s) 619.23 Current children cumulated vsize (Kb) 42700 [startup+630.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 62855 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 629.23 Current children cumulated vsize (Kb) 43324 [startup+640.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 63855 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 639.23 Current children cumulated vsize (Kb) 43324 [startup+650.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 64855 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223088 134562225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 649.23 Current children cumulated vsize (Kb) 43324 [startup+660.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 65854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 659.22 Current children cumulated vsize (Kb) 43324 [startup+670.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 66854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 669.22 Current children cumulated vsize (Kb) 43324 [startup+680.047 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 67853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 679.21 Current children cumulated vsize (Kb) 43324 [startup+690.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 68853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 689.21 Current children cumulated vsize (Kb) 43324 [startup+700.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 69853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 699.21 Current children cumulated vsize (Kb) 43324 [startup+710.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 70853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 709.21 Current children cumulated vsize (Kb) 43324 [startup+720.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 71854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 719.22 Current children cumulated vsize (Kb) 43324 [startup+730.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 72854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 729.22 Current children cumulated vsize (Kb) 43324 [startup+740.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 73854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 739.22 Current children cumulated vsize (Kb) 43324 [startup+750.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 74854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0 [pid=27185] vsize: 41200 Current children cumulated CPU time (s) 749.22 Current children cumulated vsize (Kb) 43324 [startup+760.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10004 0 0 0 75855 66 0 0 25 0 1 0 1728431278 42254336 9991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10316 9991 145 145 0 10171 0 [pid=27185] vsize: 41264 Current children cumulated CPU time (s) 759.23 Current children cumulated vsize (Kb) 43388 [startup+770.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10004 0 0 0 76855 66 0 0 25 0 1 0 1728431278 42254336 9991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10316 9991 145 145 0 10171 0 [pid=27185] vsize: 41264 Current children cumulated CPU time (s) 769.23 Current children cumulated vsize (Kb) 43388 [startup+780.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10005 0 0 0 77855 66 0 0 25 0 1 0 1728431278 42254336 9992 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10316 9992 145 145 0 10171 0 [pid=27185] vsize: 41264 Current children cumulated CPU time (s) 779.23 Current children cumulated vsize (Kb) 43388 [startup+790.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10005 0 0 0 78855 66 0 0 25 0 1 0 1728431278 42254336 9992 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10316 9992 145 145 0 10171 0 [pid=27185] vsize: 41264 Current children cumulated CPU time (s) 789.23 Current children cumulated vsize (Kb) 43388 [startup+800.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10016 0 0 0 79855 67 0 0 25 0 1 0 1728431278 42319872 10003 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10003 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 799.24 Current children cumulated vsize (Kb) 43452 [startup+810.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10019 0 0 0 80856 67 0 0 25 0 1 0 1728431278 42319872 10006 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10006 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 809.25 Current children cumulated vsize (Kb) 43452 [startup+820.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10022 0 0 0 81856 67 0 0 25 0 1 0 1728431278 42319872 10009 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10009 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 819.25 Current children cumulated vsize (Kb) 43452 [startup+830.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 82856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 829.25 Current children cumulated vsize (Kb) 43452 [startup+840.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 83856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 839.25 Current children cumulated vsize (Kb) 43452 [startup+850.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 84856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 849.25 Current children cumulated vsize (Kb) 43452 [startup+860.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 85856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 859.25 Current children cumulated vsize (Kb) 43452 [startup+870.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 86856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 869.25 Current children cumulated vsize (Kb) 43452 [startup+880.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 87857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 879.26 Current children cumulated vsize (Kb) 43452 [startup+890.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 88857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 889.26 Current children cumulated vsize (Kb) 43452 [startup+900.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 89857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 899.26 Current children cumulated vsize (Kb) 43452 [startup+910.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 90857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 909.26 Current children cumulated vsize (Kb) 43452 [startup+920.064 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 91858 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0 [pid=27185] vsize: 41328 Current children cumulated CPU time (s) 919.27 Current children cumulated vsize (Kb) 43452 [startup+930.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10032 0 0 0 92858 67 0 0 25 0 1 0 1728431278 42385408 10019 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10348 10019 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 929.27 Current children cumulated vsize (Kb) 43516 [startup+940.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10033 0 0 0 93858 67 0 0 25 0 1 0 1728431278 42385408 10020 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10348 10020 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 939.27 Current children cumulated vsize (Kb) 43516 [startup+950.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10034 0 0 0 94858 67 0 0 25 0 1 0 1728431278 42385408 10021 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10348 10021 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 949.27 Current children cumulated vsize (Kb) 43516 [startup+960.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 95858 67 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 959.27 Current children cumulated vsize (Kb) 43516 [startup+970.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27185 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 96859 67 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 969.28 Current children cumulated vsize (Kb) 43516 [startup+980.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 97858 68 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223192 134559613 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 979.28 Current children cumulated vsize (Kb) 43516 [startup+990.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 98857 68 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0 [pid=27185] vsize: 41392 Current children cumulated CPU time (s) 989.27 Current children cumulated vsize (Kb) 43516 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10044 0 0 0 99857 68 0 0 25 0 1 0 1728431278 42450944 10031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10364 10031 145 145 0 10219 0 [pid=27185] vsize: 41456 Current children cumulated CPU time (s) 999.27 Current children cumulated vsize (Kb) 43580 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10044 0 0 0 100857 68 0 0 25 0 1 0 1728431278 42450944 10031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10364 10031 145 145 0 10219 0 [pid=27185] vsize: 41456 Current children cumulated CPU time (s) 1009.27 Current children cumulated vsize (Kb) 43580 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10046 0 0 0 101857 68 0 0 25 0 1 0 1728431278 42450944 10033 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10364 10033 145 145 0 10219 0 [pid=27185] vsize: 41456 Current children cumulated CPU time (s) 1019.27 Current children cumulated vsize (Kb) 43580 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10068 0 0 0 102858 68 0 0 25 0 1 0 1728431278 42647552 10055 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10055 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1029.28 Current children cumulated vsize (Kb) 43772 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10070 0 0 0 103858 68 0 0 25 0 1 0 1728431278 42647552 10057 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10057 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1039.28 Current children cumulated vsize (Kb) 43772 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10074 0 0 0 104858 68 0 0 25 0 1 0 1728431278 42647552 10061 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10061 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1049.28 Current children cumulated vsize (Kb) 43772 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10077 0 0 0 105858 68 0 0 25 0 1 0 1728431278 42647552 10064 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10064 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1059.28 Current children cumulated vsize (Kb) 43772 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 106859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1069.29 Current children cumulated vsize (Kb) 43772 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 107859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1079.29 Current children cumulated vsize (Kb) 43772 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 108859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1089.29 Current children cumulated vsize (Kb) 43772 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 109859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1099.29 Current children cumulated vsize (Kb) 43772 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 110860 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1109.3 Current children cumulated vsize (Kb) 43772 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 111859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1119.29 Current children cumulated vsize (Kb) 43772 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 112859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223120 134555950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1129.29 Current children cumulated vsize (Kb) 43772 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 113860 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1139.3 Current children cumulated vsize (Kb) 43772 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10079 0 0 0 114860 68 0 0 25 0 1 0 1728431278 42647552 10066 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10066 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1149.3 Current children cumulated vsize (Kb) 43772 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10080 0 0 0 115860 68 0 0 25 0 1 0 1728431278 42647552 10067 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10067 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1159.3 Current children cumulated vsize (Kb) 43772 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10093 0 0 0 116860 68 0 0 25 0 1 0 1728431278 42647552 10080 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10080 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1169.3 Current children cumulated vsize (Kb) 43772 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10096 0 0 0 117861 68 0 0 25 0 1 0 1728431278 42647552 10083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10083 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1179.31 Current children cumulated vsize (Kb) 43772 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10097 0 0 0 118861 68 0 0 25 0 1 0 1728431278 42647552 10084 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10412 10084 145 145 0 10267 0 [pid=27185] vsize: 41648 Current children cumulated CPU time (s) 1189.31 Current children cumulated vsize (Kb) 43772 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10099 0 0 0 119861 68 0 0 25 0 1 0 1728431278 42778624 10086 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10444 10086 145 145 0 10299 0 [pid=27185] vsize: 41776 Current children cumulated CPU time (s) 1199.31 Current children cumulated vsize (Kb) 43900 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10099 0 0 0 120861 68 0 0 25 0 1 0 1728431278 42778624 10086 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10444 10086 145 145 0 10299 0 [pid=27185] vsize: 41776 Current children cumulated CPU time (s) 1209.31 Current children cumulated vsize (Kb) 43900 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/58 27187 Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27181/statm): 531 226 485 147 0 384 0 [pid=27181] vsize: 2124 Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10099 0 0 0 120861 68 0 0 25 0 1 0 1728431278 42778624 10086 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27185/statm): 10444 10086 145 145 0 10299 0 [pid=27185] vsize: 41776 Current children cumulated CPU time (s) 1209.31 Current children cumulated vsize (Kb) 43900 Sending SIGTERM to -27181 Sleeping 2 seconds One traced child (pid=27181) ended because it received signal 15 (SIGTERM) One traced child (pid=27185) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.32 CPU user time (s): 1208.62 CPU system time (s): 0.704892 CPU usage (%): 99.935 Max. virtual memory (cumulated for all children) (Kb): 43900
ERROR: no interpretation found !