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

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-misc07.opb
MD5SUMb95827c7e083aae37933a3b226b8189b
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1076618240
Optimality of the best value was proved NO
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1073741824
Number of bits of the biggest number in a constraint 31
Biggest sum of numbers in a constraint 3287948287
Number of bits of the biggest sum of numbers32
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.12
Number of variables290
Total number of constraints471
Number of constraints which are clauses127
Number of constraints which are cardinality constraints (but not clauses)272
Number of constraints which are nor clauses,nor cardinality constraints72
Minimum length of a constraint1
Maximum length of a constraint263

Trace number 4534

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-19 18:04:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2988 boxname=wulflinc5 idbench=644 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b95827c7e083aae37933a3b226b8189b  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-misc07.opb
IDLAUNCH: 2988
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        888124 kB
Buffers:         35608 kB
Cached:          86828 kB
SwapCached:        780 kB
Active:          73272 kB
Inactive:        51888 kB
HighTotal:      131008 kB
HighFree:        47432 kB
LowTotal:       903652 kB
LowFree:        840692 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15768 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:24:58 (client local time) WITH STATUS 10 IN 1209.53 SECONDS
stats: 2988 7 1209.53 10

Solver Data

c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1708   maxlim: 1073742847   bits: 32/31
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25851    84536 |    8617       0        0     nan |  0.000 % |
c |       104 |   25851    84536 |    9478     104     7124    68.5 |  2.893 % |
c |       256 |   25851    84536 |   10426     256    17140    67.0 |  2.893 % |
c ==============================================================================
c Found solution: 1079690240
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       296 |   25863    84565 |    8621     295    19414    65.8 |  2.893 % |
c ==============================================================================
c Found solution: 1078323200
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       323 |   25870    84582 |    8623     321    21042    65.6 |  2.893 % |
c ==============================================================================
c Found solution: 1078266880
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       372 |   25894    84635 |    8631     370    28469    76.9 |  2.893 % |
c |       472 |   25894    84635 |    9494     470    29235    62.2 |  3.011 % |
c ==============================================================================
c Found solution: 1077698560
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       494 |   25910    84673 |    8636     492    29561    60.1 |  3.011 % |
c ==============================================================================
c Found solution: 1077314560
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       517 |   25929    84717 |    8643     515    30376    59.0 |  3.011 % |
c |       618 |   25922    84702 |    9507     615    41587    67.6 |  3.063 % |
c |       769 |   25911    84678 |   10458     765    49337    64.5 |  3.106 % |
c |       995 |   25911    84678 |   11503     991    56584    57.1 |  3.106 % |
c |      1333 |   25911    84678 |   12654    1329   112538    84.7 |  3.106 % |
c |      1840 |   25911    84678 |   13919    1836   148255    80.7 |  3.106 % |
c |      2600 |   25911    84678 |   15311    2596   244986    94.4 |  3.106 % |
c |      3739 |   25911    84678 |   16842    3735   348506    93.3 |  3.106 % |
c |      5448 |   25890    84603 |   18527    5440   514853    94.6 |  3.120 % |
c |      8010 |   25879    84579 |   20379    8001   765920    95.7 |  3.163 % |
c ==============================================================================
c Found solution: 1077242880
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10195 |   25827    84467 |    8609   10176  1004432    98.7 |  3.163 % |
c |     10297 |   25816    84443 |    9469    5189   444650    85.7 |  3.516 % |
c |     10447 |   25816    84443 |   10416    5339   462777    86.7 |  3.516 % |
c |     10674 |   25805    84419 |   11458    5564   476714    85.7 |  3.559 % |
c |     11012 |   25805    84419 |   12604    5902   500179    84.7 |  3.559 % |
c |     11520 |   25805    84419 |   13864    6410   561591    87.6 |  3.559 % |
c |     12280 |   25805    84419 |   15251    7170   618280    86.2 |  3.559 % |
c ==============================================================================
c Found solution: 1077038080
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12859 |   25826    84466 |    8608    7749   708816    91.5 |  3.559 % |
c |     12959 |   25826    84466 |    9468    7849   712677    90.8 |  3.569 % |
c ==============================================================================
c Found solution: 1076966400
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13059 |   25848    84516 |    8616    7949   721699    90.8 |  3.569 % |
c |     13162 |   25841    84501 |    9477    8051   726099    90.2 |  3.608 % |
c |     13312 |   25841    84501 |   10425    8201   733729    89.5 |  3.608 % |
c |     13537 |   25826    84448 |   11467    8424   754034    89.5 |  3.622 % |
c |     13876 |   25826    84448 |   12614    8763   772627    88.2 |  3.622 % |
c |     14382 |   25778    84276 |   13876    9260   841268    90.8 |  3.650 % |
c |     15141 |   25751    84181 |   15263   10017   958101    95.6 |  3.679 % |
c |     16281 |   25700    84002 |   16790   11154  1049169    94.1 |  3.736 % |
c |     17990 |   25700    84002 |   18469   12863  1231456    95.7 |  3.736 % |
c |     20553 |   25672    83912 |   20316   15417  1531371    99.3 |  3.779 % |
c |     24399 |   25610    83711 |   22347   19256  1962822   101.9 |  3.893 % |
c ==============================================================================
c Found solution: 1076894720
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28190 |   25507    83322 |    8502   11546   969479    84.0 |  3.893 % |
c |     28290 |   25507    83322 |    9352    5873   358661    61.1 |  4.089 % |
c |     28441 |   25494    83292 |   10287    6023   366709    60.9 |  4.132 % |
c |     28666 |   25487    83277 |   11316    6247   377997    60.5 |  4.161 % |
c |     29005 |   25457    83210 |   12447    6582   419453    63.7 |  4.289 % |
c |     29511 |   25429    83148 |   13692    7085   466980    65.9 |  4.403 % |
c |     30271 |   25429    83148 |   15061    7845   576063    73.4 |  4.403 % |
c |     31411 |   25396    83075 |   16567    8979   701551    78.1 |  4.545 % |
c |     33120 |   25396    83075 |   18224   10688   814670    76.2 |  4.545 % |
c |     35682 |   25364    82976 |   20047   13245  1087489    82.1 |  4.602 % |
c |     39526 |   25349    82943 |   22051   17087  1405644    82.3 |  4.659 % |
c |     45293 |   25336    82913 |   24257   22851  2037510    89.2 |  4.702 % |
c ==============================================================================
c Found solution: 1076874240
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52953 |   25322    82886 |    8440   17704  1479433    83.6 |  4.702 % |
c |     53054 |   25322    82886 |    9284    4527   245352    54.2 |  4.827 % |
c |     53204 |   25322    82886 |   10212    4677   262079    56.0 |  4.827 % |
c |     53429 |   25322    82886 |   11233    4902   294471    60.1 |  4.827 % |
c |     53770 |   25311    82862 |   12357    5239   313658    59.9 |  4.870 % |
c |     54278 |   25311    82862 |   13592    5747   374383    65.1 |  4.870 % |
c ==============================================================================
c Found solution: 1076782080
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54685 |   25331    82909 |    8443    6154   409485    66.5 |  4.870 % |
c |     54785 |   25331    82909 |    9287    6254   428634    68.5 |  4.878 % |
c |     54935 |   25289    82761 |   10216    6397   431936    67.5 |  4.921 % |
c |     55160 |   25289    82761 |   11237    6622   466517    70.4 |  4.921 % |
c |     55499 |   25289    82761 |   12361    6961   487416    70.0 |  4.921 % |
c |     56006 |   25289    82761 |   13597    7468   532027    71.2 |  4.921 % |
c |     56766 |   25289    82761 |   14957    8228   668807    81.3 |  4.921 % |
c |     57905 |   25258    82689 |   16453    9362   742735    79.3 |  5.049 % |
c |     59615 |   25258    82689 |   18098   11072  1088873    98.3 |  5.049 % |
c |     62177 |   25247    82665 |   19908   13633  1412537   103.6 |  5.092 % |
c |     66022 |   25247    82665 |   21898   17478  2033583   116.4 |  5.092 % |
c |     71788 |   25203    82569 |   24088   23235  2733119   117.6 |  5.262 % |
c ==============================================================================
c Found solution: 1076761600
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74726 |   25195    82553 |    8398   13734  1260018    91.7 |  5.262 % |
c |     74826 |   25195    82553 |    9237    6967   453239    65.1 |  5.385 % |
c ==============================================================================
c Found solution: 1076751360
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74874 |   25212    82593 |    8404    7015   459095    65.4 |  5.385 % |
c |     74975 |   25212    82593 |    9244    7116   477340    67.1 |  5.394 % |
c |     75125 |   25212    82593 |   10168    7266   494117    68.0 |  5.394 % |
c |     75350 |   25212    82593 |   11185    7491   522357    69.7 |  5.394 % |
c |     75688 |   25197    82540 |   12304    7825   538749    68.8 |  5.408 % |
c |     76194 |   25197    82540 |   13534    8331   606164    72.8 |  5.408 % |
c |     76954 |   25197    82540 |   14888    9091   654969    72.0 |  5.408 % |
c ==============================================================================
c Found solution: 1076674560
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77808 |   25215    82581 |    8405    9945   737772    74.2 |  5.408 % |
c |     77909 |   25215    82581 |    9245    5074   240734    47.4 |  5.417 % |
c |     78063 |   25215    82581 |   10170    5228   257316    49.2 |  5.417 % |
c |     78289 |   25215    82581 |   11187    5454   294967    54.1 |  5.417 % |
c |     78627 |   25181    82505 |   12305    5787   344344    59.5 |  5.559 % |
c |     79135 |   25136    82350 |   13536    6289   388408    61.8 |  5.630 % |
c |     79895 |   25119    82312 |   14889    7046   480518    68.2 |  5.701 % |
c |     81034 |   25076    82177 |   16378    8173   542345    66.4 |  5.786 % |
c |     82746 |   25076    82177 |   18016    9885   688880    69.7 |  5.786 % |
c |     85308 |   25003    81922 |   19818   12441   892373    71.7 |  5.913 % |
c |     89152 |   25003    81922 |   21800   16285  1441242    88.5 |  5.913 % |
c |     94918 |   24935    81769 |   23980   22039  2177928    98.8 |  6.183 % |
c |    103571 |   24896    81636 |   26378   18314  1491054    81.4 |  6.254 % |
c |    116545 |   24814    81440 |   29016   17743  1495439    84.3 |  6.580 % |
c |    136006 |   24799    81407 |   31917   21079  1891760    89.7 |  6.636 % |
c |    165198 |   24688    81017 |   35109   33834  3143968    92.9 |  6.807 % |
c |    208987 |   24673    80984 |   38620   19203  1780897    92.7 |  6.863 % |
c ==============================================================================
c Found solution: 1076618240
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    253521 |   24607    80838 |    8202   18865  1615533    85.6 |  6.863 % |
c |    253621 |   24607    80838 |    9022    4817   175033    36.3 |  7.239 % |
c |    253771 |   24512    80515 |    9924    4961   179668    36.2 |  7.409 % |
c |    253997 |   24503    80484 |   10916    5186   188074    36.3 |  7.423 % |
c |    254338 |   24503    80484 |   12008    5527   210289    38.0 |  7.423 % |
c |    254844 |   24503    80484 |   13209    6033   293382    48.6 |  7.423 % |
c |    255604 |   24482    80409 |   14530    6788   345575    50.9 |  7.437 % |
c |    256744 |   24423    80204 |   15983    7921   446794    56.4 |  7.536 % |
c |    258452 |   24423    80204 |   17581    9629   603606    62.7 |  7.537 % |
c |    261014 |   24412    80180 |   19339   12190   855267    70.2 |  7.579 % |
c |    264859 |   24395    80142 |   21273   16034  1234638    77.0 |  7.650 % |
c |    270626 |   24377    80103 |   23401   21798  1861692    85.4 |  7.721 % |
c |    279276 |   24377    80103 |   25741   18005  1530883    85.0 |  7.721 % |
c |    292253 |   24377    80103 |   28315   16155  1842790   114.1 |  7.721 % |
c |    311714 |   24362    80062 |   31147   20479  1375415    67.2 |  7.763 % |
c |    340906 |   24340    80013 |   34261   16236  1091140    67.2 |  7.862 % |
c |    384695 |   24340    80013 |   37687   19232  1909595    99.3 |  7.862 % |

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/19222/stat): 19222 (minisat+_script) R 19221 19222 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793693377 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/19222/statm): 174 3 169 147 0 27 0
[pid=19222] 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=19223
New process pid=19224
New process pid=19225
execve syscall for /bin/sed executable
One traced child (pid=19224) 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=19225) exited with status: 0
One traced child (pid=19223) exited with status: 0
New process pid=19226
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-misc07.opb

[startup+10.003 s]
Raw data (loadavg): 0.87 0.94 0.87 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 1360 0 0 0 983 5 0 0 25 0 1 0 1793693382 5623808 1265 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 1373 1265 145 145 0 1228 0
[pid=19226] vsize: 5492
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 7616

[startup+20.0038 s]
Raw data (loadavg): 0.89 0.94 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 2192 0 0 0 1970 11 0 0 25 0 1 0 1793693382 9048064 2097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 2209 2097 145 145 0 2064 0
[pid=19226] vsize: 8836
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 10960

[startup+30.0046 s]
Raw data (loadavg): 0.90 0.94 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 2295 0 0 0 2967 12 0 0 25 0 1 0 1793693382 9461760 2200 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 2310 2200 145 145 0 2165 0
[pid=19226] vsize: 9240
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 11364

[startup+40.0053 s]
Raw data (loadavg): 0.92 0.94 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3018 0 0 0 3955 18 0 0 25 0 1 0 1793693382 12468224 2923 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3044 2923 145 145 0 2899 0
[pid=19226] vsize: 12176
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 14300

[startup+50.0061 s]
Raw data (loadavg): 0.93 0.94 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3502 0 0 0 4945 23 0 0 25 0 1 0 1793693382 14434304 3407 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3524 3407 145 145 0 3379 0
[pid=19226] vsize: 14096
Current children cumulated CPU time (s) 49.68
Current children cumulated vsize (Kb) 16220

[startup+60.0068 s]
Raw data (loadavg): 0.94 0.95 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3696 0 0 0 5943 24 0 0 25 0 1 0 1793693382 15220736 3601 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3716 3601 145 145 0 3571 0
[pid=19226] vsize: 14864
Current children cumulated CPU time (s) 59.67
Current children cumulated vsize (Kb) 16988

[startup+70.0076 s]
Raw data (loadavg): 0.95 0.95 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3696 0 0 0 6943 24 0 0 25 0 1 0 1793693382 15220736 3601 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3716 3601 145 145 0 3571 0
[pid=19226] vsize: 14864
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 16988

[startup+80.0123 s]
Raw data (loadavg): 0.96 0.95 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3696 0 0 0 7943 25 0 0 25 0 1 0 1793693382 15220736 3601 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3716 3601 145 145 0 3571 0
[pid=19226] vsize: 14864
Current children cumulated CPU time (s) 79.68
Current children cumulated vsize (Kb) 16988

[startup+90.0131 s]
Raw data (loadavg): 0.96 0.95 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3696 0 0 0 8943 25 0 0 25 0 1 0 1793693382 15220736 3601 4294967295 134512640 135094434 3221224432 3221223088 134557771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3716 3601 145 145 0 3571 0
[pid=19226] vsize: 14864
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 16988

[startup+100.014 s]
Raw data (loadavg): 0.97 0.95 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3773 0 0 0 9943 25 0 0 25 0 1 0 1793693382 15523840 3678 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3790 3678 145 145 0 3645 0
[pid=19226] vsize: 15160
Current children cumulated CPU time (s) 99.68
Current children cumulated vsize (Kb) 17284

[startup+110.015 s]
Raw data (loadavg): 0.97 0.95 0.88 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3773 0 0 0 10943 25 0 0 25 0 1 0 1793693382 15523840 3678 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3790 3678 145 145 0 3645 0
[pid=19226] vsize: 15160
Current children cumulated CPU time (s) 109.68
Current children cumulated vsize (Kb) 17284

[startup+120.016 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3773 0 0 0 11943 25 0 0 25 0 1 0 1793693382 15523840 3678 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3790 3678 145 145 0 3645 0
[pid=19226] vsize: 15160
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 17284

[startup+130.016 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3773 0 0 0 12943 25 0 0 25 0 1 0 1793693382 15523840 3678 4294967295 134512640 135094434 3221224432 3221223056 134562101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 3790 3678 145 145 0 3645 0
[pid=19226] vsize: 15160
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 17284

[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 3773 0 0 0 13943 26 0 0 25 0 1 0 1793693382 15523840 3678 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19226/statm): 3790 3678 145 145 0 3645 0
[pid=19226] vsize: 15160
Current children cumulated CPU time (s) 139.69
Current children cumulated vsize (Kb) 17284

[startup+150.019 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4259 0 0 0 14931 30 0 0 25 0 1 0 1793693382 17514496 4164 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19226/statm): 4276 4164 145 145 0 4131 0
[pid=19226] vsize: 17104
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 19228

[startup+160.02 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 15927 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 19940

[startup+170.02 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 16927 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 169.59
Current children cumulated vsize (Kb) 19940

[startup+180.021 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 17927 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 179.59
Current children cumulated vsize (Kb) 19940

[startup+190.022 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 18927 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 189.59
Current children cumulated vsize (Kb) 19940

[startup+200.023 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 19927 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 199.59
Current children cumulated vsize (Kb) 19940

[startup+210.023 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 20928 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 209.6
Current children cumulated vsize (Kb) 19940

[startup+220.024 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 21928 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 219.6
Current children cumulated vsize (Kb) 19940

[startup+230.025 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 22928 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223104 134556493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 229.6
Current children cumulated vsize (Kb) 19940

[startup+240.026 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 23928 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 239.6
Current children cumulated vsize (Kb) 19940

[startup+250.027 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4437 0 0 0 24928 32 0 0 25 0 1 0 1793693382 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4342 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 249.6
Current children cumulated vsize (Kb) 19940

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4438 0 0 0 25928 32 0 0 25 0 1 0 1793693382 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4343 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 19940

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4438 0 0 0 26929 32 0 0 25 0 1 0 1793693382 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4343 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 269.61
Current children cumulated vsize (Kb) 19940

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4438 0 0 0 27929 33 0 0 25 0 1 0 1793693382 18243584 4343 4294967295 134512640 135094434 3221224432 3221223104 134555802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4343 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 279.62
Current children cumulated vsize (Kb) 19940

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4438 0 0 0 28929 33 0 0 25 0 1 0 1793693382 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4454 4343 145 145 0 4309 0
[pid=19226] vsize: 17816
Current children cumulated CPU time (s) 289.62
Current children cumulated vsize (Kb) 19940

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4517 0 0 0 29928 33 0 0 25 0 1 0 1793693382 18558976 4422 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19226/statm): 4531 4422 145 145 0 4386 0
[pid=19226] vsize: 18124
Current children cumulated CPU time (s) 299.61
Current children cumulated vsize (Kb) 20248

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4923 0 0 0 30920 36 0 0 25 0 1 0 1793693382 20209664 4828 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4934 4828 145 145 0 4789 0
[pid=19226] vsize: 19736
Current children cumulated CPU time (s) 309.56
Current children cumulated vsize (Kb) 21860

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4923 0 0 0 31920 36 0 0 25 0 1 0 1793693382 20209664 4828 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4934 4828 145 145 0 4789 0
[pid=19226] vsize: 19736
Current children cumulated CPU time (s) 319.56
Current children cumulated vsize (Kb) 21860

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4925 0 0 0 32920 36 0 0 25 0 1 0 1793693382 20217856 4830 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4936 4830 145 145 0 4791 0
[pid=19226] vsize: 19744
Current children cumulated CPU time (s) 329.56
Current children cumulated vsize (Kb) 21868

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4943 0 0 0 33920 37 0 0 25 0 1 0 1793693382 20299776 4848 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4956 4848 145 145 0 4811 0
[pid=19226] vsize: 19824
Current children cumulated CPU time (s) 339.57
Current children cumulated vsize (Kb) 21948

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 4952 0 0 0 34920 37 0 0 25 0 1 0 1793693382 20336640 4857 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 4965 4857 145 145 0 4820 0
[pid=19226] vsize: 19860
Current children cumulated CPU time (s) 349.57
Current children cumulated vsize (Kb) 21984

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5090 0 0 0 35918 38 0 0 25 0 1 0 1793693382 21028864 4995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5134 4995 145 145 0 4989 0
[pid=19226] vsize: 20536
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 22660

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5090 0 0 0 36918 38 0 0 25 0 1 0 1793693382 21028864 4995 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5134 4995 145 145 0 4989 0
[pid=19226] vsize: 20536
Current children cumulated CPU time (s) 369.56
Current children cumulated vsize (Kb) 22660

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5090 0 0 0 37918 38 0 0 25 0 1 0 1793693382 21028864 4995 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5134 4995 145 145 0 4989 0
[pid=19226] vsize: 20536
Current children cumulated CPU time (s) 379.56
Current children cumulated vsize (Kb) 22660

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5090 0 0 0 38918 38 0 0 25 0 1 0 1793693382 21028864 4995 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5134 4995 145 145 0 4989 0
[pid=19226] vsize: 20536
Current children cumulated CPU time (s) 389.56
Current children cumulated vsize (Kb) 22660

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5128 0 0 0 39918 38 0 0 25 0 1 0 1793693382 21241856 5033 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5186 5033 145 145 0 5041 0
[pid=19226] vsize: 20744
Current children cumulated CPU time (s) 399.56
Current children cumulated vsize (Kb) 22868

[startup+410.037 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5135 0 0 0 40919 38 0 0 25 0 1 0 1793693382 21274624 5040 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5194 5040 145 145 0 5049 0
[pid=19226] vsize: 20776
Current children cumulated CPU time (s) 409.57
Current children cumulated vsize (Kb) 22900

[startup+420.038 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5136 0 0 0 41919 38 0 0 25 0 1 0 1793693382 21274624 5041 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5194 5041 145 145 0 5049 0
[pid=19226] vsize: 20776
Current children cumulated CPU time (s) 419.57
Current children cumulated vsize (Kb) 22900

[startup+430.039 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5601 0 0 0 42911 42 0 0 25 0 1 0 1793693382 23179264 5506 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5659 5506 145 145 0 5514 0
[pid=19226] vsize: 22636
Current children cumulated CPU time (s) 429.53
Current children cumulated vsize (Kb) 24760

[startup+440.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5601 0 0 0 43911 42 0 0 25 0 1 0 1793693382 23179264 5506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5659 5506 145 145 0 5514 0
[pid=19226] vsize: 22636
Current children cumulated CPU time (s) 439.53
Current children cumulated vsize (Kb) 24760

[startup+450.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5601 0 0 0 44911 42 0 0 25 0 1 0 1793693382 23179264 5506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5659 5506 145 145 0 5514 0
[pid=19226] vsize: 22636
Current children cumulated CPU time (s) 449.53
Current children cumulated vsize (Kb) 24760

[startup+460.041 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5601 0 0 0 45911 42 0 0 25 0 1 0 1793693382 23179264 5506 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5659 5506 145 145 0 5514 0
[pid=19226] vsize: 22636
Current children cumulated CPU time (s) 459.53
Current children cumulated vsize (Kb) 24760

[startup+470.042 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 5929 0 0 0 46905 44 0 0 25 0 1 0 1793693382 24522752 5834 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 5987 5834 145 145 0 5842 0
[pid=19226] vsize: 23948
Current children cumulated CPU time (s) 469.49
Current children cumulated vsize (Kb) 26072

[startup+480.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6303 0 0 0 47898 47 0 0 25 0 1 0 1793693382 26054656 6208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6361 6208 145 145 0 6216 0
[pid=19226] vsize: 25444
Current children cumulated CPU time (s) 479.45
Current children cumulated vsize (Kb) 27568

[startup+490.044 s]
Raw data (loadavg): 1.10 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 48897 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 489.45
Current children cumulated vsize (Kb) 27840

[startup+500.044 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 49898 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 499.46
Current children cumulated vsize (Kb) 27840

[startup+510.045 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 50898 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 509.46
Current children cumulated vsize (Kb) 27840

[startup+520.046 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 51898 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 519.46
Current children cumulated vsize (Kb) 27840

[startup+530.047 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 52898 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 529.46
Current children cumulated vsize (Kb) 27840

[startup+540.047 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 53898 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 539.46
Current children cumulated vsize (Kb) 27840

[startup+550.048 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 54899 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 549.47
Current children cumulated vsize (Kb) 27840

[startup+560.048 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 55899 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 559.47
Current children cumulated vsize (Kb) 27840

[startup+570.049 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 56899 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 569.47
Current children cumulated vsize (Kb) 27840

[startup+580.049 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 57899 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 579.47
Current children cumulated vsize (Kb) 27840

[startup+590.05 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6371 0 0 0 58900 48 0 0 25 0 1 0 1793693382 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6276 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 589.48
Current children cumulated vsize (Kb) 27840

[startup+600.051 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6372 0 0 0 59900 48 0 0 25 0 1 0 1793693382 26333184 6277 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6277 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 599.48
Current children cumulated vsize (Kb) 27840

[startup+610.051 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 60900 48 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 609.48
Current children cumulated vsize (Kb) 27840

[startup+620.052 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 61900 48 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 619.48
Current children cumulated vsize (Kb) 27840

[startup+630.052 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 62900 48 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 629.48
Current children cumulated vsize (Kb) 27840

[startup+640.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 63900 48 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 639.48
Current children cumulated vsize (Kb) 27840

[startup+650.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 64900 49 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 649.49
Current children cumulated vsize (Kb) 27840

[startup+660.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 65900 49 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 659.49
Current children cumulated vsize (Kb) 27840

[startup+670.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 66900 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221222896 134781514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 669.5
Current children cumulated vsize (Kb) 27840

[startup+680.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 67899 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 679.49
Current children cumulated vsize (Kb) 27840

[startup+690.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 68900 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 689.5
Current children cumulated vsize (Kb) 27840

[startup+700.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 69900 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 699.5
Current children cumulated vsize (Kb) 27840

[startup+710.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 70900 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 709.5
Current children cumulated vsize (Kb) 27840

[startup+720.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 71900 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 719.5
Current children cumulated vsize (Kb) 27840

[startup+730.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6373 0 0 0 72900 50 0 0 25 0 1 0 1793693382 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6278 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 729.5
Current children cumulated vsize (Kb) 27840

[startup+740.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6374 0 0 0 73900 50 0 0 25 0 1 0 1793693382 26333184 6279 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6279 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 739.5
Current children cumulated vsize (Kb) 27840

[startup+750.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6375 0 0 0 74900 50 0 0 25 0 1 0 1793693382 26333184 6280 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6280 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 749.5
Current children cumulated vsize (Kb) 27840

[startup+760.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 75900 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223024 134779266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 759.51
Current children cumulated vsize (Kb) 27840

[startup+770.062 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 76901 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 769.52
Current children cumulated vsize (Kb) 27840

[startup+780.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 77901 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 779.52
Current children cumulated vsize (Kb) 27840

[startup+790.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 78901 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 789.52
Current children cumulated vsize (Kb) 27840

[startup+800.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 79901 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 799.52
Current children cumulated vsize (Kb) 27840

[startup+810.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 80901 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 809.52
Current children cumulated vsize (Kb) 27840

[startup+820.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 81902 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 819.53
Current children cumulated vsize (Kb) 27840

[startup+830.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6376 0 0 0 82901 51 0 0 25 0 1 0 1793693382 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6281 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 829.52
Current children cumulated vsize (Kb) 27840

[startup+840.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6378 0 0 0 83902 51 0 0 25 0 1 0 1793693382 26333184 6283 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6283 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 839.53
Current children cumulated vsize (Kb) 27840

[startup+850.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6378 0 0 0 84902 51 0 0 25 0 1 0 1793693382 26333184 6283 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6283 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 849.53
Current children cumulated vsize (Kb) 27840

[startup+860.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6378 0 0 0 85902 51 0 0 25 0 1 0 1793693382 26333184 6283 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6283 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 859.53
Current children cumulated vsize (Kb) 27840

[startup+870.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6379 0 0 0 86902 51 0 0 25 0 1 0 1793693382 26333184 6284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6284 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 869.53
Current children cumulated vsize (Kb) 27840

[startup+880.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6382 0 0 0 87902 51 0 0 25 0 1 0 1793693382 26333184 6287 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6287 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 879.53
Current children cumulated vsize (Kb) 27840

[startup+890.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6382 0 0 0 88903 51 0 0 25 0 1 0 1793693382 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6287 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 889.54
Current children cumulated vsize (Kb) 27840

[startup+900.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6382 0 0 0 89903 51 0 0 25 0 1 0 1793693382 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6287 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 899.54
Current children cumulated vsize (Kb) 27840

[startup+910.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6382 0 0 0 90903 51 0 0 25 0 1 0 1793693382 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6287 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 909.54
Current children cumulated vsize (Kb) 27840

[startup+920.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6382 0 0 0 91903 51 0 0 25 0 1 0 1793693382 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6287 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 919.54
Current children cumulated vsize (Kb) 27840

[startup+930.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6382 0 0 0 92903 51 0 0 25 0 1 0 1793693382 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6429 6287 145 145 0 6284 0
[pid=19226] vsize: 25716
Current children cumulated CPU time (s) 929.54
Current children cumulated vsize (Kb) 27840

[startup+940.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6388 0 0 0 93904 51 0 0 25 0 1 0 1793693382 26378240 6293 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6440 6293 145 145 0 6295 0
[pid=19226] vsize: 25760
Current children cumulated CPU time (s) 939.55
Current children cumulated vsize (Kb) 27884

[startup+950.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 94904 51 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 949.55
Current children cumulated vsize (Kb) 27916

[startup+960.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 95904 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 959.56
Current children cumulated vsize (Kb) 27916

[startup+970.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 96904 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 969.56
Current children cumulated vsize (Kb) 27916

[startup+980.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 97904 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 979.56
Current children cumulated vsize (Kb) 27916

[startup+990.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 98904 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 989.56
Current children cumulated vsize (Kb) 27916

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 99904 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 999.56
Current children cumulated vsize (Kb) 27916

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 100904 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1009.56
Current children cumulated vsize (Kb) 27916

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 101905 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1019.57
Current children cumulated vsize (Kb) 27916

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 102905 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1029.57
Current children cumulated vsize (Kb) 27916

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 103905 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1039.57
Current children cumulated vsize (Kb) 27916

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 104905 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1049.57
Current children cumulated vsize (Kb) 27916

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 105905 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1059.57
Current children cumulated vsize (Kb) 27916

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 106906 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1069.58
Current children cumulated vsize (Kb) 27916

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6395 0 0 0 107906 52 0 0 25 0 1 0 1793693382 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6448 6300 145 145 0 6303 0
[pid=19226] vsize: 25792
Current children cumulated CPU time (s) 1079.58
Current children cumulated vsize (Kb) 27916

[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6495 0 0 0 108904 53 0 0 25 0 1 0 1793693382 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6548 6400 145 145 0 6403 0
[pid=19226] vsize: 26192
Current children cumulated CPU time (s) 1089.57
Current children cumulated vsize (Kb) 28316

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6495 0 0 0 109904 53 0 0 25 0 1 0 1793693382 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19226/statm): 6548 6400 145 145 0 6403 0
[pid=19226] vsize: 26192
Current children cumulated CPU time (s) 1099.57
Current children cumulated vsize (Kb) 28316

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6495 0 0 0 110903 53 0 0 25 0 1 0 1793693382 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6548 6400 145 145 0 6403 0
[pid=19226] vsize: 26192
Current children cumulated CPU time (s) 1109.56
Current children cumulated vsize (Kb) 28316

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6495 0 0 0 111903 53 0 0 25 0 1 0 1793693382 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6548 6400 145 145 0 6403 0
[pid=19226] vsize: 26192
Current children cumulated CPU time (s) 1119.56
Current children cumulated vsize (Kb) 28316

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6495 0 0 0 112903 53 0 0 25 0 1 0 1793693382 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6548 6400 145 145 0 6403 0
[pid=19226] vsize: 26192
Current children cumulated CPU time (s) 1129.56
Current children cumulated vsize (Kb) 28316

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6506 0 0 0 113903 53 0 0 25 0 1 0 1793693382 26886144 6411 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6564 6411 145 145 0 6419 0
[pid=19226] vsize: 26256
Current children cumulated CPU time (s) 1139.56
Current children cumulated vsize (Kb) 28380

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6511 0 0 0 114903 53 0 0 25 0 1 0 1793693382 26918912 6416 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6572 6416 145 145 0 6427 0
[pid=19226] vsize: 26288
Current children cumulated CPU time (s) 1149.56
Current children cumulated vsize (Kb) 28412

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6511 0 0 0 115904 53 0 0 25 0 1 0 1793693382 26918912 6416 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6572 6416 145 145 0 6427 0
[pid=19226] vsize: 26288
Current children cumulated CPU time (s) 1159.57
Current children cumulated vsize (Kb) 28412

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 6787 0 0 0 116898 55 0 0 25 0 1 0 1793693382 28049408 6692 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 6848 6692 145 145 0 6703 0
[pid=19226] vsize: 27392
Current children cumulated CPU time (s) 1169.53
Current children cumulated vsize (Kb) 29516

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 7173 0 0 0 117892 58 0 0 25 0 1 0 1793693382 29634560 7078 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 7235 7078 145 145 0 7090 0
[pid=19226] vsize: 28940
Current children cumulated CPU time (s) 1179.5
Current children cumulated vsize (Kb) 31064

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 7196 0 0 0 118891 58 0 0 25 0 1 0 1793693382 29732864 7101 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 7259 7101 145 145 0 7114 0
[pid=19226] vsize: 29036
Current children cumulated CPU time (s) 1189.49
Current children cumulated vsize (Kb) 31160

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 7196 0 0 0 119892 58 0 0 25 0 1 0 1793693382 29732864 7101 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 7259 7101 145 145 0 7114 0
[pid=19226] vsize: 29036
Current children cumulated CPU time (s) 1199.5
Current children cumulated vsize (Kb) 31160

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 7196 0 0 0 120892 58 0 0 25 0 1 0 1793693382 29732864 7101 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 7259 7101 145 145 0 7114 0
[pid=19226] vsize: 29036
Current children cumulated CPU time (s) 1209.5
Current children cumulated vsize (Kb) 31160



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 19226
Raw data (/proc/19222/stat): 19222 (minisat+_script) S 19221 19222 824 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793693377 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/19222/statm): 531 226 485 147 0 384 0
[pid=19222] vsize: 2124
Raw data (/proc/19226/stat): 19226 (minisat+_64-bit) R 19222 19222 824 0 -1 0 7196 0 0 0 120892 58 0 0 25 0 1 0 1793693382 29732864 7101 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19226/statm): 7259 7101 145 145 0 7114 0
[pid=19226] vsize: 29036
Current children cumulated CPU time (s) 1209.5
Current children cumulated vsize (Kb) 31160

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.53
CPU user time (s): 1208.93
CPU system time (s): 0.599908
CPU usage (%): 99.9517
Max. virtual memory (cumulated for all children) (Kb): 31160

Verifier Data

ERROR: no interpretation found !