Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-4.opb
MD5SUM7731f50c352d2fd7b2fe148b68bfdbab
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.03
Number of variables760
Total number of constraints41605
Number of constraints which are clauses41605
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 2291

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-18 18:45:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2697 boxname=wulflinc20 idbench=353 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7731f50c352d2fd7b2fe148b68bfdbab  /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-4.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-4.opb
IDLAUNCH: 2697
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        910904 kB
Buffers:         35396 kB
Cached:          59244 kB
SwapCached:        832 kB
Active:          67616 kB
Inactive:        29720 kB
HighTotal:      131008 kB
HighFree:        68404 kB
LowTotal:       903652 kB
LowFree:        842500 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20780 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:05:23 (client local time) WITH STATUS 10 IN 1208.95 SECONDS
stats: 2697 7 1208.95 10

Solver Data

c Parsing PB file...
c Converting 41605 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 |   41605    83210 |   13868       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -29
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77753   168122 |   25917       0        0     nan |  0.000 % |
c |       101 |   77380   167357 |   28508      74     1087    14.7 |  0.796 % |
c |       251 |   76935   166400 |   31359     187     2027    10.8 |  1.831 % |
c |       476 |   75593   163504 |   34495     333     4511    13.5 |  4.972 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       781 |   74235   160714 |   24745     565     8133    14.4 |  4.972 % |
c |       881 |   73694   159487 |   27219     640     8842    13.8 | 10.031 % |
c |      1031 |   73182   158344 |   29941     742     9894    13.3 | 11.290 % |
c |      1256 |   71817   155279 |   32935     908    11980    13.2 | 14.690 % |
c |      1593 |   70390   152058 |   36229    1120    14315    12.8 | 18.255 % |
c |      2099 |   68314   147352 |   39852    1473    20259    13.8 | 23.529 % |
c |      2858 |   64983   139810 |   43837    2005    27170    13.6 | 31.922 % |
c |      3997 |   61942   132839 |   48221    2827    38151    13.5 | 39.672 % |
c |      5705 |   57794   123031 |   53043    4147    58590    14.1 | 50.708 % |
c |      8267 |   53937   113879 |   58347    6175   101349    16.4 | 61.198 % |
c |     12111 |   51088   107100 |   64182    9376   209229    22.3 | 68.931 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14510 |   50433   105575 |   16811   11454   342561    29.9 | 68.931 % |
c |     14610 |   50433   105575 |   18492   11554   344419    29.8 | 70.722 % |
c |     14761 |   50433   105575 |   20341   11705   350475    29.9 | 70.722 % |
c |     14986 |   50433   105575 |   22375   11930   361583    30.3 | 70.722 % |
c |     15324 |   50107   104782 |   24612   12183   372190    30.5 | 71.626 % |
c |     15831 |   49933   104364 |   27074   12595   390221    31.0 | 72.104 % |
c |     16590 |   49629   103648 |   29781   13283   428057    32.2 | 72.916 % |
c |     17729 |   48931   101939 |   32759   14235   473128    33.2 | 74.898 % |
c |     19438 |   48867   101783 |   36035   15894   575254    36.2 | 75.083 % |
c |     22000 |   48275   100352 |   39639   18090   716401    39.6 | 76.734 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24883 |   48095    99832 |   16031   20800   934720    44.9 | 76.734 % |
c |     24983 |   47740    98976 |   17634   20624   932425    45.2 | 78.263 % |
c |     25133 |   47740    98976 |   19397   20774   941755    45.3 | 78.263 % |
c |     25358 |   47702    98882 |   21337   20927   950824    45.4 | 78.376 % |
c |     25695 |   47702    98882 |   23470   21264   970411    45.6 | 78.376 % |
c |     26201 |   47700    98878 |   25818   21769  1001975    46.0 | 78.380 % |
c |     26960 |   47487    98334 |   28399   22339  1043094    46.7 | 79.015 % |
c |     28099 |   47449    98246 |   31239   23430  1110397    47.4 | 79.115 % |
c |     29807 |   47449    98246 |   34363   25138  1301421    51.8 | 79.115 % |
c |     32369 |   47408    98151 |   37800   27600  1517138    55.0 | 79.224 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34890 |   47234    97752 |   15744   29984  1760205    58.7 | 79.224 % |
c |     34990 |   47194    97654 |   17318   29906  1761335    58.9 | 79.907 % |
c |     35140 |   47194    97654 |   19050   30056  1774039    59.0 | 79.907 % |
c |     35365 |   47194    97654 |   20955   30281  1792828    59.2 | 79.907 % |
c |     35702 |   47194    97654 |   23050   30618  1825661    59.6 | 79.907 % |
c |     36208 |   47194    97654 |   25355   31124  1860327    59.8 | 79.907 % |
c |     36968 |   47166    97583 |   27891   31860  1920463    60.3 | 79.991 % |
c |     38109 |   47162    97573 |   30680   32897  2012855    61.2 | 80.003 % |
c |     39818 |   47162    97573 |   33748   34606  2163659    62.5 | 80.003 % |
c |     42380 |   47162    97573 |   37123   37168  2449092    65.9 | 80.003 % |
c |     46227 |   47060    97338 |   40835   40876  2850607    69.7 | 80.260 % |
c |     51994 |   46982    97141 |   44919   46508  3471568    74.6 | 80.484 % |
c |     60644 |   46934    97017 |   49411   54952  4522068    82.3 | 80.632 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65436 |   46893    96903 |   15631   59362  5113871    86.1 | 80.632 % |
c |     65536 |   46893    96903 |   17194   18644  1614753    86.6 | 80.749 % |
c |     65686 |   46854    96804 |   18913   18767  1618131    86.2 | 80.869 % |
c |     65911 |   46795    96659 |   20804   18985  1627818    85.7 | 81.042 % |
c |     66248 |   46795    96659 |   22885   19322  1649457    85.4 | 81.042 % |
c |     66756 |   46795    96659 |   25173   19830  1672800    84.4 | 81.042 % |
c |     67518 |   46795    96659 |   27691   20592  1744416    84.7 | 81.042 % |
c |     68657 |   46795    96659 |   30460   21731  1856295    85.4 | 81.042 % |
c |     70366 |   46795    96659 |   33506   23440  1997186    85.2 | 81.042 % |
c |     72928 |   46742    96532 |   36857   25984  2212431    85.1 | 81.190 % |
c |     76774 |   46714    96464 |   40542   29821  2582192    86.6 | 81.266 % |
c |     82540 |   46712    96460 |   44597   35586  3095009    87.0 | 81.270 % |
c |     91190 |   46712    96460 |   49056   44236  3866480    87.4 | 81.270 % |
c |    104165 |   46623    96245 |   53962   57037  4993464    87.5 | 81.522 % |
c |    123626 |   46580    96146 |   59358   20979  1569020    74.8 | 81.634 % |
c |    152819 |   46485    95911 |   65294   50114  4321342    86.2 | 81.914 % |
c |    196609 |   46391    95677 |   71824   26970  1175384    43.6 | 82.190 % |
c |    262293 |   46384    95660 |   79006   92651  5737328    61.9 | 82.211 % |
c |    360821 |   46278    95411 |   86907   25024  2605510   104.1 | 82.491 % |
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 -C

Watcher Data

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/13295/stat): 13295 (minisat+_script) R 13294 13295 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843517031 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13295/statm): 174 3 169 147 0 27 0
[pid=13295] 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=13296
New process pid=13297
New process pid=13298
execve syscall for /bin/sed executable
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
One traced child (pid=13297) exited with status: 0
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=13298) exited with status: 0
One traced child (pid=13296) exited with status: 0
New process pid=13299
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-4.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 2875 0 0 0 973 14 0 0 25 0 1 0 1843517036 12709888 2862 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 3103 2862 145 145 0 2958 0
[pid=13299] vsize: 12412
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 14536

[startup+20.0058 s]
Raw data (loadavg): 0.94 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 2875 0 0 0 1972 14 0 0 25 0 1 0 1843517036 12709888 2862 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 3103 2862 145 145 0 2958 0
[pid=13299] vsize: 12412
Current children cumulated CPU time (s) 19.88
Current children cumulated vsize (Kb) 14536

[startup+30.0065 s]
Raw data (loadavg): 0.95 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 2914 0 0 0 2971 15 0 0 25 0 1 0 1843517036 12869632 2901 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 3142 2901 145 145 0 2997 0
[pid=13299] vsize: 12568
Current children cumulated CPU time (s) 29.88
Current children cumulated vsize (Kb) 14692

[startup+40.0072 s]
Raw data (loadavg): 0.95 0.97 0.97 1/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) T 13295 13295 2660 0 -1 0 3247 0 0 0 3965 18 0 0 25 0 1 0 1843517036 14340096 3234 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13299/statm): 3501 3234 145 145 0 3356 0
[pid=13299] vsize: 14004
Current children cumulated CPU time (s) 39.85
Current children cumulated vsize (Kb) 16128

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 3657 0 0 0 4959 20 0 0 25 0 1 0 1843517036 16064512 3644 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 3922 3644 145 145 0 3777 0
[pid=13299] vsize: 15688
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 17812

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 4163 0 0 0 5950 24 0 0 25 0 1 0 1843517036 18112512 4150 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 4422 4150 145 145 0 4277 0
[pid=13299] vsize: 17688
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 19812

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 4704 0 0 0 6941 27 0 0 25 0 1 0 1843517036 20307968 4691 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 4958 4691 145 145 0 4813 0
[pid=13299] vsize: 19832
Current children cumulated CPU time (s) 69.7
Current children cumulated vsize (Kb) 21956

[startup+80.0101 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 5204 0 0 0 7930 31 0 0 25 0 1 0 1843517036 22470656 5191 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 5486 5191 145 145 0 5341 0
[pid=13299] vsize: 21944
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 24068

[startup+90.0108 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 5742 0 0 0 8921 36 0 0 25 0 1 0 1843517036 24657920 5729 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 6020 5729 145 145 0 5875 0
[pid=13299] vsize: 24080
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 26204

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 6198 0 0 0 9912 39 0 0 25 0 1 0 1843517036 26513408 6185 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 6473 6185 145 145 0 6328 0
[pid=13299] vsize: 25892
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 28016

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 6637 0 0 0 10903 42 0 0 25 0 1 0 1843517036 28295168 6624 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 6908 6624 145 145 0 6763 0
[pid=13299] vsize: 27632
Current children cumulated CPU time (s) 109.47
Current children cumulated vsize (Kb) 29756

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 7110 0 0 0 11895 44 0 0 25 0 1 0 1843517036 30220288 7097 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 7378 7097 145 145 0 7233 0
[pid=13299] vsize: 29512
Current children cumulated CPU time (s) 119.41
Current children cumulated vsize (Kb) 31636

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 7578 0 0 0 12888 47 0 0 25 0 1 0 1843517036 32120832 7565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 7842 7565 145 145 0 7697 0
[pid=13299] vsize: 31368
Current children cumulated CPU time (s) 129.37
Current children cumulated vsize (Kb) 33492

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8010 0 0 0 13881 51 0 0 25 0 1 0 1843517036 33878016 7997 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8271 7997 145 145 0 8126 0
[pid=13299] vsize: 33084
Current children cumulated CPU time (s) 139.34
Current children cumulated vsize (Kb) 35208

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8451 0 0 0 14872 55 0 0 25 0 1 0 1843517036 35672064 8438 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8709 8438 145 145 0 8564 0
[pid=13299] vsize: 34836
Current children cumulated CPU time (s) 149.29
Current children cumulated vsize (Kb) 36960

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 15871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 159.29
Current children cumulated vsize (Kb) 37200

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 16871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 169.29
Current children cumulated vsize (Kb) 37200

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 17871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 179.29
Current children cumulated vsize (Kb) 37200

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 18871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 189.29
Current children cumulated vsize (Kb) 37200

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 19871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 199.29
Current children cumulated vsize (Kb) 37200

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 20871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 209.29
Current children cumulated vsize (Kb) 37200

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 21871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 219.29
Current children cumulated vsize (Kb) 37200

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 22871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 229.29
Current children cumulated vsize (Kb) 37200

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8511 0 0 0 23871 56 0 0 25 0 1 0 1843517036 35917824 8498 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8769 8498 145 145 0 8624 0
[pid=13299] vsize: 35076
Current children cumulated CPU time (s) 239.29
Current children cumulated vsize (Kb) 37200

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 8711 0 0 0 24869 58 0 0 25 0 1 0 1843517036 36741120 8698 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 8970 8698 145 145 0 8825 0
[pid=13299] vsize: 35880
Current children cumulated CPU time (s) 249.29
Current children cumulated vsize (Kb) 38004

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 9074 0 0 0 25862 61 0 0 25 0 1 0 1843517036 38215680 9061 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 9330 9061 145 145 0 9185 0
[pid=13299] vsize: 37320
Current children cumulated CPU time (s) 259.25
Current children cumulated vsize (Kb) 39444

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 9416 0 0 0 26856 63 0 0 25 0 1 0 1843517036 39866368 9403 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 9733 9403 145 145 0 9588 0
[pid=13299] vsize: 38932
Current children cumulated CPU time (s) 269.21
Current children cumulated vsize (Kb) 41056

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 9789 0 0 0 27850 65 0 0 25 0 1 0 1843517036 41385984 9776 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10104 9776 145 145 0 9959 0
[pid=13299] vsize: 40416
Current children cumulated CPU time (s) 279.17
Current children cumulated vsize (Kb) 42540

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10148 0 0 0 28844 68 0 0 25 0 1 0 1843517036 42848256 10135 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10461 10135 145 145 0 10316 0
[pid=13299] vsize: 41844
Current children cumulated CPU time (s) 289.14
Current children cumulated vsize (Kb) 43968

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10463 0 0 0 29838 70 0 0 25 0 1 0 1843517036 44134400 10450 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10775 10450 145 145 0 10630 0
[pid=13299] vsize: 43100
Current children cumulated CPU time (s) 299.1
Current children cumulated vsize (Kb) 45224

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 30834 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 309.08
Current children cumulated vsize (Kb) 45912

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 31834 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 319.08
Current children cumulated vsize (Kb) 45912

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 32834 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223120 134555953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 329.08
Current children cumulated vsize (Kb) 45912

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 33834 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 339.08
Current children cumulated vsize (Kb) 45912

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 34835 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 349.09
Current children cumulated vsize (Kb) 45912

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 35835 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 359.09
Current children cumulated vsize (Kb) 45912

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 36835 72 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 369.09
Current children cumulated vsize (Kb) 45912

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 37835 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 379.1
Current children cumulated vsize (Kb) 45912

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 38835 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 389.1
Current children cumulated vsize (Kb) 45912

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 39835 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 399.1
Current children cumulated vsize (Kb) 45912

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 40835 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 409.1
Current children cumulated vsize (Kb) 45912

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 41835 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 419.1
Current children cumulated vsize (Kb) 45912

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 42836 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 429.11
Current children cumulated vsize (Kb) 45912

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10636 0 0 0 43836 73 0 0 25 0 1 0 1843517036 44838912 10623 4294967295 134512640 135094434 3221224448 3221223060 134563080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10623 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 439.11
Current children cumulated vsize (Kb) 45912

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10637 0 0 0 44836 73 0 0 25 0 1 0 1843517036 44838912 10624 4294967295 134512640 135094434 3221224448 3221223040 134557196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10624 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 449.11
Current children cumulated vsize (Kb) 45912

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10640 0 0 0 45836 73 0 0 25 0 1 0 1843517036 44838912 10627 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10627 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 459.11
Current children cumulated vsize (Kb) 45912

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10642 0 0 0 46836 73 0 0 25 0 1 0 1843517036 44838912 10629 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10629 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 469.11
Current children cumulated vsize (Kb) 45912

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10644 0 0 0 47837 73 0 0 25 0 1 0 1843517036 44838912 10631 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10631 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 479.12
Current children cumulated vsize (Kb) 45912

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10647 0 0 0 48837 73 0 0 25 0 1 0 1843517036 44838912 10634 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10634 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 489.12
Current children cumulated vsize (Kb) 45912

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 49837 73 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 499.12
Current children cumulated vsize (Kb) 45912

[startup+510.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 50837 73 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223040 134557117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 509.12
Current children cumulated vsize (Kb) 45912

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 51837 73 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 519.12
Current children cumulated vsize (Kb) 45912

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 52837 73 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 529.12
Current children cumulated vsize (Kb) 45912

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 53837 73 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 539.12
Current children cumulated vsize (Kb) 45912

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 54837 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 549.13
Current children cumulated vsize (Kb) 45912

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 55838 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 559.14
Current children cumulated vsize (Kb) 45912

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 56838 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 569.14
Current children cumulated vsize (Kb) 45912

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 57838 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 579.14
Current children cumulated vsize (Kb) 45912

[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 58838 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 589.14
Current children cumulated vsize (Kb) 45912

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 59838 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 599.14
Current children cumulated vsize (Kb) 45912

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 60839 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 609.15
Current children cumulated vsize (Kb) 45912

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 61839 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 619.15
Current children cumulated vsize (Kb) 45912

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 62839 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 629.15
Current children cumulated vsize (Kb) 45912

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 63839 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 639.15
Current children cumulated vsize (Kb) 45912

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 64839 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223120 134556533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 649.15
Current children cumulated vsize (Kb) 45912

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 65840 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 659.16
Current children cumulated vsize (Kb) 45912

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 66840 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 669.16
Current children cumulated vsize (Kb) 45912

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 67840 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 679.16
Current children cumulated vsize (Kb) 45912

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 68840 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223120 134556487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 689.16
Current children cumulated vsize (Kb) 45912

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10648 0 0 0 69841 74 0 0 25 0 1 0 1843517036 44838912 10635 4294967295 134512640 135094434 3221224448 3221223072 134562106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10635 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 699.17
Current children cumulated vsize (Kb) 45912

[startup+710.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10650 0 0 0 70841 74 0 0 25 0 1 0 1843517036 44838912 10637 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10637 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 709.17
Current children cumulated vsize (Kb) 45912

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10652 0 0 0 71841 74 0 0 25 0 1 0 1843517036 44838912 10639 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10639 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 719.17
Current children cumulated vsize (Kb) 45912

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10655 0 0 0 72840 74 0 0 25 0 1 0 1843517036 44838912 10642 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 10947 10642 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 729.16
Current children cumulated vsize (Kb) 45912

[startup+740.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10657 0 0 0 73840 75 0 0 25 0 1 0 1843517036 44838912 10644 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 10947 10644 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 739.17
Current children cumulated vsize (Kb) 45912

[startup+750.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10660 0 0 0 74838 75 0 0 25 0 1 0 1843517036 44838912 10647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13299/statm): 10947 10647 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 749.15
Current children cumulated vsize (Kb) 45912

[startup+760.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10662 0 0 0 75838 75 0 0 25 0 1 0 1843517036 44838912 10649 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10649 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 759.15
Current children cumulated vsize (Kb) 45912

[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10662 0 0 0 76838 75 0 0 25 0 1 0 1843517036 44838912 10649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10649 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 769.15
Current children cumulated vsize (Kb) 45912

[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 77839 75 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 779.16
Current children cumulated vsize (Kb) 45912

[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 78839 75 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 789.16
Current children cumulated vsize (Kb) 45912

[startup+800.074 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 79839 75 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 799.16
Current children cumulated vsize (Kb) 45912

[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 80840 75 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 809.17
Current children cumulated vsize (Kb) 45912

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 81840 75 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 819.17
Current children cumulated vsize (Kb) 45912

[startup+830.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 82840 75 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 829.17
Current children cumulated vsize (Kb) 45912

[startup+840.077 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 83840 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 839.18
Current children cumulated vsize (Kb) 45912

[startup+850.078 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 84840 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 849.18
Current children cumulated vsize (Kb) 45912

[startup+860.078 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 85840 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 859.18
Current children cumulated vsize (Kb) 45912

[startup+870.079 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 86841 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 869.19
Current children cumulated vsize (Kb) 45912

[startup+880.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 87841 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 879.19
Current children cumulated vsize (Kb) 45912

[startup+890.081 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 88841 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 889.19
Current children cumulated vsize (Kb) 45912

[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 89841 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 899.19
Current children cumulated vsize (Kb) 45912

[startup+910.083 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 90841 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 909.19
Current children cumulated vsize (Kb) 45912

[startup+920.084 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 91842 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 919.2
Current children cumulated vsize (Kb) 45912

[startup+930.085 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 92842 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 929.2
Current children cumulated vsize (Kb) 45912

[startup+940.085 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 93842 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 939.2
Current children cumulated vsize (Kb) 45912

[startup+950.086 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 10663 0 0 0 94842 76 0 0 25 0 1 0 1843517036 44838912 10650 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 10947 10650 145 145 0 10802 0
[pid=13299] vsize: 43788
Current children cumulated CPU time (s) 949.2
Current children cumulated vsize (Kb) 45912

[startup+960.088 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) T 13295 13295 2660 0 -1 0 10962 0 0 0 95837 78 0 0 25 0 1 0 1843517036 46063616 10949 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13299/statm): 11246 10949 145 145 0 11101 0
[pid=13299] vsize: 44984
Current children cumulated CPU time (s) 959.17
Current children cumulated vsize (Kb) 47108

[startup+970.088 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 11297 0 0 0 96831 81 0 0 25 0 1 0 1843517036 47435776 11284 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 11581 11284 145 145 0 11436 0
[pid=13299] vsize: 46324
Current children cumulated CPU time (s) 969.14
Current children cumulated vsize (Kb) 48448

[startup+980.089 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 11623 0 0 0 97825 83 0 0 25 0 1 0 1843517036 48771072 11610 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 11907 11610 145 145 0 11762 0
[pid=13299] vsize: 47628
Current children cumulated CPU time (s) 979.1
Current children cumulated vsize (Kb) 49752

[startup+990.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 11922 0 0 0 98820 86 0 0 25 0 1 0 1843517036 50008064 11909 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12209 11909 145 145 0 12064 0
[pid=13299] vsize: 48836
Current children cumulated CPU time (s) 989.08
Current children cumulated vsize (Kb) 50960

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12227 0 0 0 99814 89 0 0 25 0 1 0 1843517036 51249152 12214 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12512 12214 145 145 0 12367 0
[pid=13299] vsize: 50048
Current children cumulated CPU time (s) 999.05
Current children cumulated vsize (Kb) 52172

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12512 0 0 0 100810 91 0 0 25 0 1 0 1843517036 52420608 12499 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12798 12499 145 145 0 12653 0
[pid=13299] vsize: 51192
Current children cumulated CPU time (s) 1009.03
Current children cumulated vsize (Kb) 53316

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 101809 91 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1019.02
Current children cumulated vsize (Kb) 53668

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 102809 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1029.03
Current children cumulated vsize (Kb) 53668

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 103808 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1039.02
Current children cumulated vsize (Kb) 53668

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 104809 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223040 134557435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1049.03
Current children cumulated vsize (Kb) 53668

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 105809 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1059.03
Current children cumulated vsize (Kb) 53668

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 106809 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1069.03
Current children cumulated vsize (Kb) 53668

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 107809 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1079.03
Current children cumulated vsize (Kb) 53668

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 108810 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1089.04
Current children cumulated vsize (Kb) 53668

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 109810 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1099.04
Current children cumulated vsize (Kb) 53668

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 110810 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1109.04
Current children cumulated vsize (Kb) 53668

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12600 0 0 0 111810 92 0 0 25 0 1 0 1843517036 52781056 12587 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12587 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1119.04
Current children cumulated vsize (Kb) 53668

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12601 0 0 0 112810 92 0 0 25 0 1 0 1843517036 52781056 12588 4294967295 134512640 135094434 3221224448 3221223120 134556329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12588 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1129.04
Current children cumulated vsize (Kb) 53668

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12601 0 0 0 113810 92 0 0 25 0 1 0 1843517036 52781056 12588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12588 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1139.04
Current children cumulated vsize (Kb) 53668

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12601 0 0 0 114811 92 0 0 25 0 1 0 1843517036 52781056 12588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12588 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1149.05
Current children cumulated vsize (Kb) 53668

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12601 0 0 0 115811 92 0 0 25 0 1 0 1843517036 52781056 12588 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12588 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1159.05
Current children cumulated vsize (Kb) 53668

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12601 0 0 0 116811 92 0 0 25 0 1 0 1843517036 52781056 12588 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 12886 12588 145 145 0 12741 0
[pid=13299] vsize: 51544
Current children cumulated CPU time (s) 1169.05
Current children cumulated vsize (Kb) 53668

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 12881 0 0 0 117806 95 0 0 25 0 1 0 1843517036 53927936 12868 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 13166 12868 145 145 0 13021 0
[pid=13299] vsize: 52664
Current children cumulated CPU time (s) 1179.03
Current children cumulated vsize (Kb) 54788

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 13249 0 0 0 118799 98 0 0 25 0 1 0 1843517036 55439360 13236 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 13535 13236 145 145 0 13390 0
[pid=13299] vsize: 54140
Current children cumulated CPU time (s) 1188.99
Current children cumulated vsize (Kb) 56264

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 13580 0 0 0 119794 100 0 0 25 0 1 0 1843517036 56799232 13567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 13867 13567 145 145 0 13722 0
[pid=13299] vsize: 55468
Current children cumulated CPU time (s) 1198.96
Current children cumulated vsize (Kb) 57592

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 13846 0 0 0 120789 102 0 0 25 0 1 0 1843517036 57876480 13833 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 14130 13833 145 145 0 13985 0
[pid=13299] vsize: 56520
Current children cumulated CPU time (s) 1208.93
Current children cumulated vsize (Kb) 58644



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13299
Raw data (/proc/13295/stat): 13295 (minisat+_script) S 13294 13295 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843517031 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13295/statm): 531 226 485 147 0 384 0
[pid=13295] vsize: 2124
Raw data (/proc/13299/stat): 13299 (minisat+_64-bit) R 13295 13295 2660 0 -1 0 13846 0 0 0 120789 102 0 0 25 0 1 0 1843517036 57876480 13833 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13299/statm): 14130 13833 145 145 0 13985 0
[pid=13299] vsize: 56520
Current children cumulated CPU time (s) 1208.93
Current children cumulated vsize (Kb) 58644

Sending SIGTERM to -13295
Sleeping 2 seconds
One traced child (pid=13295) ended because it received signal 15 (SIGTERM)
One traced child (pid=13299) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.95
CPU user time (s): 1207.9
CPU system time (s): 1.04984
CPU usage (%): 99.9015
Max. virtual memory (cumulated for all children) (Kb): 58644

Verifier Data

ERROR: no interpretation found !