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-2.opb
MD5SUM270e069f649d19b0da4e4d23c0e1ebfc
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 constraints41263
Number of constraints which are clauses41263
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 2290

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        880652 kB
Buffers:         37924 kB
Cached:          86084 kB
SwapCached:        908 kB
Active:          96028 kB
Inactive:        30824 kB
HighTotal:      131008 kB
HighFree:        48888 kB
LowTotal:       903652 kB
LowFree:        831764 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21452 kB
Committed_AS:    93132 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:04:58 (client local time) WITH STATUS 10 IN 1209.32 SECONDS
stats: 2696 7 1209.32 10

Solver Data

c Parsing PB file...
c Converting 41263 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41263    82526 |   13754       0        0     nan |  0.000 % |
c ==============================================================================
c 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 |   77411   167438 |   25803       0        0     nan |  0.000 % |
c |       100 |   77197   167004 |   28383      85     1743    20.5 |  0.449 % |
c |       250 |   76777   166128 |   31221     216     3076    14.2 |  1.370 % |
c |       475 |   75681   163748 |   34343     367     7270    19.8 |  3.965 % |
c |       812 |   74772   161767 |   37778     638    10625    16.7 |  6.213 % |
c |      1318 |   72216   156098 |   41555     971    15210    15.7 | 12.362 % |
c ==============================================================================
c Found solution: -30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1358 |   71957   155524 |   23985    1000    15644    15.6 | 12.362 % |
c |      1458 |   71484   154445 |   26383    1077    16216    15.1 | 14.235 % |
c |      1609 |   70637   152550 |   29021    1185    17694    14.9 | 16.491 % |
c |      1834 |   69903   150904 |   31924    1355    19103    14.1 | 18.302 % |
c |      2171 |   68629   148052 |   35116    1633    21862    13.4 | 21.386 % |
c |      2677 |   66555   143323 |   38628    2003    25849    12.9 | 26.681 % |
c |      3436 |   63907   137250 |   42490    2573    35121    13.6 | 33.519 % |
c |      4575 |   60641   129717 |   46739    3414    45806    13.4 | 42.032 % |
c |      6284 |   58132   123765 |   51413    4758    70644    14.8 | 48.684 % |
c ==============================================================================
c 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 |      6893 |   57499   122346 |   19166    5251    79403    15.1 | 48.684 % |
c |      6993 |   57374   122059 |   21082    5340    80419    15.1 | 50.986 % |
c |      7143 |   57174   121601 |   23190    5476    83135    15.2 | 51.497 % |
c |      7368 |   57124   121493 |   25509    5691    90616    15.9 | 51.614 % |
c |      7705 |   56450   119888 |   28060    5895    93895    15.9 | 53.460 % |
c |      8211 |   55724   118204 |   30867    6317   101819    16.1 | 55.371 % |
c |      8970 |   54430   115147 |   33953    6865   120056    17.5 | 58.891 % |
c |     10109 |   53229   112295 |   37349    7784   156050    20.0 | 62.178 % |
c |     11817 |   51998   109354 |   41084    9200   202992    22.1 | 65.558 % |
c |     14379 |   50235   105114 |   45192   10981   295829    26.9 | 70.406 % |
c ==============================================================================
c 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 |     15965 |   49478   103359 |   16492   12311   371372    30.2 | 70.406 % |
c |     16066 |   49478   103359 |   18141   12412   374678    30.2 | 72.440 % |
c |     16216 |   49424   103225 |   19955   12525   376566    30.1 | 72.597 % |
c |     16441 |   49285   102876 |   21950   12651   381138    30.1 | 72.991 % |
c |     16778 |   49212   102697 |   24145   12924   395334    30.6 | 73.204 % |
c |     17285 |   49156   102561 |   26560   13400   438885    32.8 | 73.360 % |
c |     18044 |   48324   100548 |   29216   13832   461348    33.4 | 75.707 % |
c |     19183 |   48201   100261 |   32138   14905   550058    36.9 | 76.033 % |
c |     20891 |   47874    99472 |   35352   16285   636889    39.1 | 76.957 % |
c |     23453 |   47628    98870 |   38887   18649   839926    45.0 | 77.656 % |
c ==============================================================================
c 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 |     25038 |   47524    98566 |   15841   20184   980752    48.6 | 77.656 % |
c |     25139 |   47524    98566 |   17425   20285   983661    48.5 | 77.940 % |
c |     25289 |   47524    98566 |   19167   20435   990976    48.5 | 77.939 % |
c |     25514 |   47524    98566 |   21084   20660  1005617    48.7 | 77.939 % |
c |     25851 |   47524    98566 |   23192   20997  1026282    48.9 | 77.939 % |
c |     26358 |   47524    98566 |   25512   21504  1055909    49.1 | 77.940 % |
c |     27118 |   47524    98566 |   28063   22264  1120991    50.3 | 77.939 % |
c |     28258 |   47202    97772 |   30869   23237  1219781    52.5 | 78.852 % |
c |     29966 |   47191    97747 |   33956   24941  1366171    54.8 | 78.880 % |
c |     32528 |   47072    97453 |   37352   27423  1611937    58.8 | 79.221 % |
c |     36372 |   47072    97453 |   41087   31267  2099445    67.1 | 79.221 % |
c |     42138 |   46746    96661 |   45196   36763  2600401    70.7 | 80.142 % |
c ==============================================================================
c 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 |     46022 |   46748    96684 |   15582   40621  3011087    74.1 | 80.142 % |
c |     46122 |   46748    96684 |   17140   18203  1211729    66.6 | 80.221 % |
c |     46272 |   46748    96684 |   18854   18353  1218705    66.4 | 80.221 % |
c |     46497 |   46714    96607 |   20739   18539  1230555    66.4 | 80.297 % |
c |     46834 |   46703    96582 |   22813   18867  1250274    66.3 | 80.325 % |
c |     47340 |   46651    96453 |   25094   19368  1284175    66.3 | 80.473 % |
c |     48100 |   46472    96017 |   27604   20063  1320976    65.8 | 80.974 % |
c |     49239 |   46437    95936 |   30364   21181  1424831    67.3 | 81.066 % |
c |     50947 |   46434    95929 |   33401   22886  1532403    67.0 | 81.074 % |
c |     53509 |   46389    95814 |   36741   25444  1762687    69.3 | 81.214 % |
c |     57353 |   46351    95720 |   40415   29177  2121672    72.7 | 81.326 % |
c |     63119 |   46102    95119 |   44457   34489  2610152    75.7 | 82.030 % |
c |     71769 |   46087    95084 |   48902   43071  3470985    80.6 | 82.070 % |
c |     84743 |   46022    94925 |   53793   55928  4763761    85.2 | 82.259 % |
c ==============================================================================
c 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 |     91656 |   46006    94872 |   15335   62707  5469040    87.2 | 82.259 % |
c |     91756 |   46006    94872 |   16868   20099  1258236    62.6 | 82.312 % |
c |     91906 |   46004    94868 |   18555   20247  1269896    62.7 | 82.316 % |
c |     92131 |   45981    94815 |   20410   20467  1286191    62.8 | 82.376 % |
c |     92469 |   45978    94808 |   22451   20801  1325256    63.7 | 82.384 % |
c |     92975 |   45956    94754 |   24697   21154  1350045    63.8 | 82.448 % |
c |     93735 |   45891    94586 |   27166   21886  1408143    64.3 | 82.640 % |
c |     94874 |   45891    94586 |   29883   23025  1506974    65.4 | 82.640 % |
c |     96582 |   45850    94484 |   32871   24718  1656829    67.0 | 82.756 % |
c |     99144 |   45850    94484 |   36159   27280  1890855    69.3 | 82.756 % |
c |    102988 |   45767    94285 |   39775   31063  2199681    70.8 | 82.989 % |
c |    108754 |   45767    94285 |   43752   36829  2758646    74.9 | 82.988 % |
c |    117404 |   45755    94257 |   48127   45475  3584527    78.8 | 83.021 % |
c |    130378 |   45713    94155 |   52940   58391  4806838    82.3 | 83.141 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136420 |   45733    94207 |   15244   64433  5331404    82.7 | 83.141 % |
c |    136520 |   45733    94207 |   16768   20826  1132496    54.4 | 83.107 % |
c |    136670 |   45733    94207 |   18445   20976  1139985    54.3 | 83.107 % |
c |    136895 |   45733    94207 |   20289   21201  1153537    54.4 | 83.107 % |
c |    137232 |   45733    94207 |   22318   21538  1169510    54.3 | 83.107 % |
c |    137738 |   45733    94207 |   24550   22044  1213136    55.0 | 83.107 % |
c |    138497 |   45733    94207 |   27005   22803  1266674    55.5 | 83.108 % |
c |    139636 |   45733    94207 |   29706   23942  1351252    56.4 | 83.107 % |
c |    141344 |   45733    94207 |   32676   25650  1504180    58.6 | 83.107 % |
c |    143906 |   45733    94207 |   35944   28212  1667932    59.1 | 83.107 % |
c |    147751 |   45733    94207 |   39539   32057  2014186    62.8 | 83.107 % |
c |    153517 |   45733    94207 |   43492   37823  2552526    67.5 | 83.107 % |
c |    162166 |   45681    94069 |   47842   46460  3249653    69.9 | 83.271 % |
c |    175140 |   45681    94069 |   52626   59434  4360949    73.4 | 83.271 % |
c |    194601 |   45651    93995 |   57889   24662  1331831    54.0 | 83.359 % |
c |    223793 |   45636    93958 |   63677   53847  4465405    82.9 | 83.403 % |
c |    267582 |   45636    93958 |   70045   31596  1238437    39.2 | 83.403 % |
c |    333266 |   45616    93912 |   77050   24572   866247    35.3 | 83.455 % |
c |    431792 |   45563    93787 |   84755   42419  1615243    38.1 | 83.599 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 C631 -C630 -C629 -C628 -C627 C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 C480 -C479 -C478 -C477 -C476 C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 C231 -C230 -C229 -C228 C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C7

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/27181/stat): 27181 (minisat+_script) R 27180 27181 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1728431273 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27181/statm): 174 3 169 147 0 27 0
[pid=27181] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=27182
New process pid=27183
New process pid=27184
execve syscall for /bin/sed executable
One traced child (pid=27183) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=27184) exited with status: 0
One traced child (pid=27182) exited with status: 0
New process pid=27185
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-frb40-19-2.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 2879 0 0 0 974 12 0 0 25 0 1 0 1728431278 12726272 2866 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 3107 2866 145 145 0 2962 0
[pid=27185] vsize: 12428
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 14552

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 2879 0 0 0 1973 12 0 0 25 0 1 0 1728431278 12726272 2866 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 3107 2866 145 145 0 2962 0
[pid=27185] vsize: 12428
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 14552

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 2940 0 0 0 2972 13 0 0 25 0 1 0 1728431278 12976128 2927 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 3168 2927 145 145 0 3023 0
[pid=27185] vsize: 12672
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 14796

[startup+40.0079 s]
Raw data (loadavg): 0.96 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 3198 0 0 0 3967 14 0 0 25 0 1 0 1728431278 14049280 3185 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 3430 3185 145 145 0 3285 0
[pid=27185] vsize: 13720
Current children cumulated CPU time (s) 39.83
Current children cumulated vsize (Kb) 15844

[startup+50.0087 s]
Raw data (loadavg): 0.96 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 3609 0 0 0 4960 17 0 0 25 0 1 0 1728431278 15876096 3596 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 3876 3596 145 145 0 3731 0
[pid=27185] vsize: 15504
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 17628

[startup+60.0095 s]
Raw data (loadavg): 0.97 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 4231 0 0 0 5950 21 0 0 25 0 1 0 1728431278 18399232 4218 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 4492 4218 145 145 0 4347 0
[pid=27185] vsize: 17968
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 20092

[startup+70.0102 s]
Raw data (loadavg): 0.97 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 4852 0 0 0 6938 26 0 0 25 0 1 0 1728431278 20922368 4839 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 5108 4839 145 145 0 4963 0
[pid=27185] vsize: 20432
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 22556

[startup+80.011 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 5328 0 0 0 7928 30 0 0 25 0 1 0 1728431278 22986752 5315 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 5612 5315 145 145 0 5467 0
[pid=27185] vsize: 22448
Current children cumulated CPU time (s) 79.6
Current children cumulated vsize (Kb) 24572

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 5832 0 0 0 8920 34 0 0 25 0 1 0 1728431278 25030656 5819 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 6111 5819 145 145 0 5966 0
[pid=27185] vsize: 24444
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 26568

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 9913 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0
[pid=27185] vsize: 25772
Current children cumulated CPU time (s) 99.52
Current children cumulated vsize (Kb) 27896

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 10914 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0
[pid=27185] vsize: 25772
Current children cumulated CPU time (s) 109.53
Current children cumulated vsize (Kb) 27896

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 11914 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0
[pid=27185] vsize: 25772
Current children cumulated CPU time (s) 119.53
Current children cumulated vsize (Kb) 27896

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6166 0 0 0 12914 37 0 0 25 0 1 0 1728431278 26390528 6153 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 6443 6153 145 145 0 6298 0
[pid=27185] vsize: 25772
Current children cumulated CPU time (s) 129.53
Current children cumulated vsize (Kb) 27896

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6334 0 0 0 13911 38 0 0 25 0 1 0 1728431278 27078656 6321 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 6611 6321 145 145 0 6466 0
[pid=27185] vsize: 26444
Current children cumulated CPU time (s) 139.51
Current children cumulated vsize (Kb) 28568

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 6821 0 0 0 14902 42 0 0 25 0 1 0 1728431278 29061120 6808 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 7095 6808 145 145 0 6950 0
[pid=27185] vsize: 28380
Current children cumulated CPU time (s) 149.46
Current children cumulated vsize (Kb) 30504

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 7200 0 0 0 15893 45 0 0 25 0 1 0 1728431278 30597120 7187 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 7470 7187 145 145 0 7325 0
[pid=27185] vsize: 29880
Current children cumulated CPU time (s) 159.4
Current children cumulated vsize (Kb) 32004

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 7573 0 0 0 16886 47 0 0 25 0 1 0 1728431278 32112640 7560 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 7840 7560 145 145 0 7695 0
[pid=27185] vsize: 31360
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 33484

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 7903 0 0 0 17882 49 0 0 25 0 1 0 1728431278 33452032 7890 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 8167 7890 145 145 0 8022 0
[pid=27185] vsize: 32668
Current children cumulated CPU time (s) 179.33
Current children cumulated vsize (Kb) 34792

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8259 0 0 0 18876 52 0 0 25 0 1 0 1728431278 34893824 8246 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 8519 8246 145 145 0 8374 0
[pid=27185] vsize: 34076
Current children cumulated CPU time (s) 189.3
Current children cumulated vsize (Kb) 36200

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8655 0 0 0 19870 55 0 0 25 0 1 0 1728431278 36503552 8642 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 8912 8642 145 145 0 8767 0
[pid=27185] vsize: 35648
Current children cumulated CPU time (s) 199.27
Current children cumulated vsize (Kb) 37772

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 20865 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 209.24
Current children cumulated vsize (Kb) 38772

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 21865 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 219.24
Current children cumulated vsize (Kb) 38772

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 22866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 229.25
Current children cumulated vsize (Kb) 38772

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 23866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 239.25
Current children cumulated vsize (Kb) 38772

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 24866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 249.25
Current children cumulated vsize (Kb) 38772

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 25866 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 259.25
Current children cumulated vsize (Kb) 38772

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 26867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 269.26
Current children cumulated vsize (Kb) 38772

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 27867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 279.26
Current children cumulated vsize (Kb) 38772

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 28867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 289.26
Current children cumulated vsize (Kb) 38772

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 29867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 299.26
Current children cumulated vsize (Kb) 38772

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8907 0 0 0 30867 57 0 0 25 0 1 0 1728431278 37527552 8894 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8894 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 309.26
Current children cumulated vsize (Kb) 38772

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 31867 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 319.26
Current children cumulated vsize (Kb) 38772

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 32868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 329.27
Current children cumulated vsize (Kb) 38772

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 33868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 339.27
Current children cumulated vsize (Kb) 38772

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 34868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 349.27
Current children cumulated vsize (Kb) 38772

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 35868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 359.27
Current children cumulated vsize (Kb) 38772

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 36868 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 369.27
Current children cumulated vsize (Kb) 38772

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 37869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 379.28
Current children cumulated vsize (Kb) 38772

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 38869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 389.28
Current children cumulated vsize (Kb) 38772

[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 39869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 399.28
Current children cumulated vsize (Kb) 38772

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8908 0 0 0 40869 57 0 0 25 0 1 0 1728431278 37527552 8895 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8895 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 409.28
Current children cumulated vsize (Kb) 38772

[startup+420.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8909 0 0 0 41869 57 0 0 25 0 1 0 1728431278 37527552 8896 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9162 8896 145 145 0 9017 0
[pid=27185] vsize: 36648
Current children cumulated CPU time (s) 419.28
Current children cumulated vsize (Kb) 38772

[startup+430.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8912 0 0 0 42870 57 0 0 25 0 1 0 1728431278 37789696 8899 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9226 8899 145 145 0 9081 0
[pid=27185] vsize: 36904
Current children cumulated CPU time (s) 429.29
Current children cumulated vsize (Kb) 39028

[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 8954 0 0 0 43869 57 0 0 25 0 1 0 1728431278 37949440 8941 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9265 8941 145 145 0 9120 0
[pid=27185] vsize: 37060
Current children cumulated CPU time (s) 439.28
Current children cumulated vsize (Kb) 39184

[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9177 0 0 0 44866 59 0 0 25 0 1 0 1728431278 38850560 9164 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9485 9164 145 145 0 9340 0
[pid=27185] vsize: 37940
Current children cumulated CPU time (s) 449.27
Current children cumulated vsize (Kb) 40064

[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 45865 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 459.26
Current children cumulated vsize (Kb) 40244

[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 46866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 469.27
Current children cumulated vsize (Kb) 40244

[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 47866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 479.27
Current children cumulated vsize (Kb) 40244

[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 48866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 489.27
Current children cumulated vsize (Kb) 40244

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 49866 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 499.27
Current children cumulated vsize (Kb) 40244

[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 50867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 509.28
Current children cumulated vsize (Kb) 40244

[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 51867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 519.28
Current children cumulated vsize (Kb) 40244

[startup+530.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 52867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 529.28
Current children cumulated vsize (Kb) 40244

[startup+540.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 53867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 539.28
Current children cumulated vsize (Kb) 40244

[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 54867 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 549.28
Current children cumulated vsize (Kb) 40244

[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 55868 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 559.29
Current children cumulated vsize (Kb) 40244

[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9223 0 0 0 56868 59 0 0 25 0 1 0 1728431278 39034880 9210 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9530 9210 145 145 0 9385 0
[pid=27185] vsize: 38120
Current children cumulated CPU time (s) 569.29
Current children cumulated vsize (Kb) 40244

[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9227 0 0 0 57868 59 0 0 25 0 1 0 1728431278 39051264 9214 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9534 9214 145 145 0 9389 0
[pid=27185] vsize: 38136
Current children cumulated CPU time (s) 579.29
Current children cumulated vsize (Kb) 40260

[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9365 0 0 0 58865 61 0 0 25 0 1 0 1728431278 39616512 9352 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9672 9352 145 145 0 9527 0
[pid=27185] vsize: 38688
Current children cumulated CPU time (s) 589.28
Current children cumulated vsize (Kb) 40812

[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9491 0 0 0 59864 62 0 0 25 0 1 0 1728431278 40124416 9478 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9796 9478 145 145 0 9651 0
[pid=27185] vsize: 39184
Current children cumulated CPU time (s) 599.28
Current children cumulated vsize (Kb) 41308

[startup+610.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9623 0 0 0 60862 63 0 0 25 0 1 0 1728431278 40669184 9610 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 9929 9610 145 145 0 9784 0
[pid=27185] vsize: 39716
Current children cumulated CPU time (s) 609.27
Current children cumulated vsize (Kb) 41840

[startup+620.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9843 0 0 0 61857 64 0 0 25 0 1 0 1728431278 41549824 9830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10144 9830 145 145 0 9999 0
[pid=27185] vsize: 40576
Current children cumulated CPU time (s) 619.23
Current children cumulated vsize (Kb) 42700

[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 62855 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 629.23
Current children cumulated vsize (Kb) 43324

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 63855 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 639.23
Current children cumulated vsize (Kb) 43324

[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 64855 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223088 134562225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 649.23
Current children cumulated vsize (Kb) 43324

[startup+660.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 65854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 659.22
Current children cumulated vsize (Kb) 43324

[startup+670.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 66854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 669.22
Current children cumulated vsize (Kb) 43324

[startup+680.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 67853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 679.21
Current children cumulated vsize (Kb) 43324

[startup+690.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 68853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 689.21
Current children cumulated vsize (Kb) 43324

[startup+700.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 69853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 699.21
Current children cumulated vsize (Kb) 43324

[startup+710.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 70853 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 709.21
Current children cumulated vsize (Kb) 43324

[startup+720.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 71854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 719.22
Current children cumulated vsize (Kb) 43324

[startup+730.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 72854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 729.22
Current children cumulated vsize (Kb) 43324

[startup+740.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 73854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 739.22
Current children cumulated vsize (Kb) 43324

[startup+750.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 9994 0 0 0 74854 66 0 0 25 0 1 0 1728431278 42188800 9981 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10300 9981 145 145 0 10155 0
[pid=27185] vsize: 41200
Current children cumulated CPU time (s) 749.22
Current children cumulated vsize (Kb) 43324

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10004 0 0 0 75855 66 0 0 25 0 1 0 1728431278 42254336 9991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10316 9991 145 145 0 10171 0
[pid=27185] vsize: 41264
Current children cumulated CPU time (s) 759.23
Current children cumulated vsize (Kb) 43388

[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10004 0 0 0 76855 66 0 0 25 0 1 0 1728431278 42254336 9991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10316 9991 145 145 0 10171 0
[pid=27185] vsize: 41264
Current children cumulated CPU time (s) 769.23
Current children cumulated vsize (Kb) 43388

[startup+780.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10005 0 0 0 77855 66 0 0 25 0 1 0 1728431278 42254336 9992 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10316 9992 145 145 0 10171 0
[pid=27185] vsize: 41264
Current children cumulated CPU time (s) 779.23
Current children cumulated vsize (Kb) 43388

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10005 0 0 0 78855 66 0 0 25 0 1 0 1728431278 42254336 9992 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10316 9992 145 145 0 10171 0
[pid=27185] vsize: 41264
Current children cumulated CPU time (s) 789.23
Current children cumulated vsize (Kb) 43388

[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10016 0 0 0 79855 67 0 0 25 0 1 0 1728431278 42319872 10003 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10003 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 799.24
Current children cumulated vsize (Kb) 43452

[startup+810.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10019 0 0 0 80856 67 0 0 25 0 1 0 1728431278 42319872 10006 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10006 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 809.25
Current children cumulated vsize (Kb) 43452

[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10022 0 0 0 81856 67 0 0 25 0 1 0 1728431278 42319872 10009 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10009 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 819.25
Current children cumulated vsize (Kb) 43452

[startup+830.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 82856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 829.25
Current children cumulated vsize (Kb) 43452

[startup+840.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 83856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 839.25
Current children cumulated vsize (Kb) 43452

[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 84856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 849.25
Current children cumulated vsize (Kb) 43452

[startup+860.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 85856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 859.25
Current children cumulated vsize (Kb) 43452

[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 86856 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 869.25
Current children cumulated vsize (Kb) 43452

[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 87857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 879.26
Current children cumulated vsize (Kb) 43452

[startup+890.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 88857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 889.26
Current children cumulated vsize (Kb) 43452

[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 89857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 899.26
Current children cumulated vsize (Kb) 43452

[startup+910.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 90857 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 909.26
Current children cumulated vsize (Kb) 43452

[startup+920.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10023 0 0 0 91858 67 0 0 25 0 1 0 1728431278 42319872 10010 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10332 10010 145 145 0 10187 0
[pid=27185] vsize: 41328
Current children cumulated CPU time (s) 919.27
Current children cumulated vsize (Kb) 43452

[startup+930.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10032 0 0 0 92858 67 0 0 25 0 1 0 1728431278 42385408 10019 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10348 10019 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 929.27
Current children cumulated vsize (Kb) 43516

[startup+940.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10033 0 0 0 93858 67 0 0 25 0 1 0 1728431278 42385408 10020 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10348 10020 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 939.27
Current children cumulated vsize (Kb) 43516

[startup+950.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10034 0 0 0 94858 67 0 0 25 0 1 0 1728431278 42385408 10021 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10348 10021 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 949.27
Current children cumulated vsize (Kb) 43516

[startup+960.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 95858 67 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 959.27
Current children cumulated vsize (Kb) 43516

[startup+970.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27185
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 96859 67 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 969.28
Current children cumulated vsize (Kb) 43516

[startup+980.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 97858 68 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223192 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 979.28
Current children cumulated vsize (Kb) 43516

[startup+990.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10035 0 0 0 98857 68 0 0 25 0 1 0 1728431278 42385408 10022 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10348 10022 145 145 0 10203 0
[pid=27185] vsize: 41392
Current children cumulated CPU time (s) 989.27
Current children cumulated vsize (Kb) 43516

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10044 0 0 0 99857 68 0 0 25 0 1 0 1728431278 42450944 10031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10364 10031 145 145 0 10219 0
[pid=27185] vsize: 41456
Current children cumulated CPU time (s) 999.27
Current children cumulated vsize (Kb) 43580

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10044 0 0 0 100857 68 0 0 25 0 1 0 1728431278 42450944 10031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10364 10031 145 145 0 10219 0
[pid=27185] vsize: 41456
Current children cumulated CPU time (s) 1009.27
Current children cumulated vsize (Kb) 43580

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10046 0 0 0 101857 68 0 0 25 0 1 0 1728431278 42450944 10033 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10364 10033 145 145 0 10219 0
[pid=27185] vsize: 41456
Current children cumulated CPU time (s) 1019.27
Current children cumulated vsize (Kb) 43580

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10068 0 0 0 102858 68 0 0 25 0 1 0 1728431278 42647552 10055 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10055 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1029.28
Current children cumulated vsize (Kb) 43772

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10070 0 0 0 103858 68 0 0 25 0 1 0 1728431278 42647552 10057 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10057 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1039.28
Current children cumulated vsize (Kb) 43772

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10074 0 0 0 104858 68 0 0 25 0 1 0 1728431278 42647552 10061 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10061 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1049.28
Current children cumulated vsize (Kb) 43772

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10077 0 0 0 105858 68 0 0 25 0 1 0 1728431278 42647552 10064 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10064 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1059.28
Current children cumulated vsize (Kb) 43772

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 106859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1069.29
Current children cumulated vsize (Kb) 43772

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 107859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1079.29
Current children cumulated vsize (Kb) 43772

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 108859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1089.29
Current children cumulated vsize (Kb) 43772

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 109859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1099.29
Current children cumulated vsize (Kb) 43772

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 110860 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1109.3
Current children cumulated vsize (Kb) 43772

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 111859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1119.29
Current children cumulated vsize (Kb) 43772

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 112859 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223120 134555950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1129.29
Current children cumulated vsize (Kb) 43772

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10078 0 0 0 113860 68 0 0 25 0 1 0 1728431278 42647552 10065 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10065 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1139.3
Current children cumulated vsize (Kb) 43772

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10079 0 0 0 114860 68 0 0 25 0 1 0 1728431278 42647552 10066 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10066 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1149.3
Current children cumulated vsize (Kb) 43772

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10080 0 0 0 115860 68 0 0 25 0 1 0 1728431278 42647552 10067 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10067 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1159.3
Current children cumulated vsize (Kb) 43772

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10093 0 0 0 116860 68 0 0 25 0 1 0 1728431278 42647552 10080 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10080 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1169.3
Current children cumulated vsize (Kb) 43772

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10096 0 0 0 117861 68 0 0 25 0 1 0 1728431278 42647552 10083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10083 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1179.31
Current children cumulated vsize (Kb) 43772

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10097 0 0 0 118861 68 0 0 25 0 1 0 1728431278 42647552 10084 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10412 10084 145 145 0 10267 0
[pid=27185] vsize: 41648
Current children cumulated CPU time (s) 1189.31
Current children cumulated vsize (Kb) 43772

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10099 0 0 0 119861 68 0 0 25 0 1 0 1728431278 42778624 10086 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10444 10086 145 145 0 10299 0
[pid=27185] vsize: 41776
Current children cumulated CPU time (s) 1199.31
Current children cumulated vsize (Kb) 43900

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10099 0 0 0 120861 68 0 0 25 0 1 0 1728431278 42778624 10086 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10444 10086 145 145 0 10299 0
[pid=27185] vsize: 41776
Current children cumulated CPU time (s) 1209.31
Current children cumulated vsize (Kb) 43900



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/58 27187
Raw data (/proc/27181/stat): 27181 (minisat+_script) S 27180 27181 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1728431273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27181/statm): 531 226 485 147 0 384 0
[pid=27181] vsize: 2124
Raw data (/proc/27185/stat): 27185 (minisat+_64-bit) R 27181 27181 17733 0 -1 0 10099 0 0 0 120861 68 0 0 25 0 1 0 1728431278 42778624 10086 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27185/statm): 10444 10086 145 145 0 10299 0
[pid=27185] vsize: 41776
Current children cumulated CPU time (s) 1209.31
Current children cumulated vsize (Kb) 43900

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.32
CPU user time (s): 1208.62
CPU system time (s): 0.704892
CPU usage (%): 99.935
Max. virtual memory (cumulated for all children) (Kb): 43900

Verifier Data

ERROR: no interpretation found !