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/miplib/normalized-mps-v2-20-10-misc07.opb
MD5SUMf204f0495d2a5caf7ce1d50b166e58a2
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.14
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 3871

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-19 03:11:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2867 boxname=wulflinc4 idbench=523 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f204f0495d2a5caf7ce1d50b166e58a2  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-misc07.opb
IDLAUNCH: 2867
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        911676 kB
Buffers:         31736 kB
Cached:          65852 kB
SwapCached:        944 kB
Active:          53652 kB
Inactive:        46576 kB
HighTotal:      131008 kB
HighFree:        62244 kB
LowTotal:       903652 kB
LowFree:        849432 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            16972 kB
Committed_AS:    72324 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:31:11 (client local time) WITH STATUS 10 IN 1209.59 SECONDS
stats: 2867 7 1209.59 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/30045/stat): 30045 (minisat+_script) R 30044 30045 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788310575 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/30045/statm): 174 3 169 147 0 27 0
[pid=30045] 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=30046
New process pid=30047
New process pid=30048
execve syscall for /bin/sed executable
One traced child (pid=30047) 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=30048) exited with status: 0
One traced child (pid=30046) exited with status: 0
New process pid=30049
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-misc07.opb

[startup+10.0031 s]
Raw data (loadavg): 1.02 1.04 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 1362 0 0 0 982 5 0 0 25 0 1 0 1788310580 5632000 1267 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 1375 1267 145 145 0 1230 0
[pid=30049] vsize: 5500
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 7624

[startup+20.0039 s]
Raw data (loadavg): 1.02 1.04 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 2192 0 0 0 1970 11 0 0 25 0 1 0 1788310580 9048064 2097 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 2209 2097 145 145 0 2064 0
[pid=30049] vsize: 8836
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 10960

[startup+30.0048 s]
Raw data (loadavg): 1.02 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 2298 0 0 0 2966 12 0 0 25 0 1 0 1788310580 9474048 2203 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30049/statm): 2313 2203 145 145 0 2168 0
[pid=30049] vsize: 9252
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 11376

[startup+40.0066 s]
Raw data (loadavg): 1.01 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3018 0 0 0 3952 19 0 0 25 0 1 0 1788310580 12468224 2923 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3044 2923 145 145 0 2899 0
[pid=30049] vsize: 12176
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 14300

[startup+50.0074 s]
Raw data (loadavg): 1.01 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3508 0 0 0 4945 21 0 0 25 0 1 0 1788310580 14458880 3413 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3530 3413 145 145 0 3385 0
[pid=30049] vsize: 14120
Current children cumulated CPU time (s) 49.66
Current children cumulated vsize (Kb) 16244

[startup+60.0083 s]
Raw data (loadavg): 1.01 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3696 0 0 0 5942 23 0 0 25 0 1 0 1788310580 15220736 3601 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3716 3601 145 145 0 3571 0
[pid=30049] vsize: 14864
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 16988

[startup+70.0091 s]
Raw data (loadavg): 1.01 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3696 0 0 0 6941 23 0 0 25 0 1 0 1788310580 15220736 3601 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3716 3601 145 145 0 3571 0
[pid=30049] vsize: 14864
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 16988

[startup+80.0099 s]
Raw data (loadavg): 1.00 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3696 0 0 0 7941 23 0 0 25 0 1 0 1788310580 15220736 3601 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3716 3601 145 145 0 3571 0
[pid=30049] vsize: 14864
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 16988

[startup+90.0108 s]
Raw data (loadavg): 1.00 1.03 0.86 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3696 0 0 0 8942 23 0 0 25 0 1 0 1788310580 15220736 3601 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3716 3601 145 145 0 3571 0
[pid=30049] vsize: 14864
Current children cumulated CPU time (s) 89.65
Current children cumulated vsize (Kb) 16988

[startup+100.012 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3773 0 0 0 9941 24 0 0 25 0 1 0 1788310580 15523840 3678 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3790 3678 145 145 0 3645 0
[pid=30049] vsize: 15160
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 17284

[startup+110.012 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3773 0 0 0 10941 24 0 0 25 0 1 0 1788310580 15523840 3678 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3790 3678 145 145 0 3645 0
[pid=30049] vsize: 15160
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 17284

[startup+120.013 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3773 0 0 0 11941 24 0 0 25 0 1 0 1788310580 15523840 3678 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3790 3678 145 145 0 3645 0
[pid=30049] vsize: 15160
Current children cumulated CPU time (s) 119.65
Current children cumulated vsize (Kb) 17284

[startup+130.014 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3773 0 0 0 12941 24 0 0 25 0 1 0 1788310580 15523840 3678 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3790 3678 145 145 0 3645 0
[pid=30049] vsize: 15160
Current children cumulated CPU time (s) 129.65
Current children cumulated vsize (Kb) 17284

[startup+140.015 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 3773 0 0 0 13941 24 0 0 25 0 1 0 1788310580 15523840 3678 4294967295 134512640 135094434 3221224432 3221223056 134562122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 3790 3678 145 145 0 3645 0
[pid=30049] vsize: 15160
Current children cumulated CPU time (s) 139.65
Current children cumulated vsize (Kb) 17284

[startup+150.016 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4271 0 0 0 14933 27 0 0 25 0 1 0 1788310580 17563648 4176 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4288 4176 145 145 0 4143 0
[pid=30049] vsize: 17152
Current children cumulated CPU time (s) 149.6
Current children cumulated vsize (Kb) 19276

[startup+160.017 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 15930 28 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 159.58
Current children cumulated vsize (Kb) 19940

[startup+170.018 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 16930 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223024 134551883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 169.59
Current children cumulated vsize (Kb) 19940

[startup+180.017 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 17930 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 179.59
Current children cumulated vsize (Kb) 19940

[startup+190.019 s]
Raw data (loadavg): 1.00 1.02 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 18930 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 189.59
Current children cumulated vsize (Kb) 19940

[startup+200.02 s]
Raw data (loadavg): 1.00 1.01 0.87 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 19930 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 199.59
Current children cumulated vsize (Kb) 19940

[startup+210.02 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 20931 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 209.6
Current children cumulated vsize (Kb) 19940

[startup+220.021 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 21931 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 219.6
Current children cumulated vsize (Kb) 19940

[startup+230.022 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 22931 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 229.6
Current children cumulated vsize (Kb) 19940

[startup+240.022 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4437 0 0 0 23931 29 0 0 25 0 1 0 1788310580 18243584 4342 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4342 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 239.6
Current children cumulated vsize (Kb) 19940

[startup+250.023 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4438 0 0 0 24931 29 0 0 25 0 1 0 1788310580 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4343 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 249.6
Current children cumulated vsize (Kb) 19940

[startup+260.024 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4438 0 0 0 25931 29 0 0 25 0 1 0 1788310580 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4343 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 19940

[startup+270.025 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4438 0 0 0 26932 29 0 0 25 0 1 0 1788310580 18243584 4343 4294967295 134512640 135094434 3221224432 3221223024 134557253 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4343 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 269.61
Current children cumulated vsize (Kb) 19940

[startup+280.026 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4438 0 0 0 27932 29 0 0 25 0 1 0 1788310580 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4343 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 279.61
Current children cumulated vsize (Kb) 19940

[startup+290.028 s]
Raw data (loadavg): 1.00 1.01 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4438 0 0 0 28932 29 0 0 25 0 1 0 1788310580 18243584 4343 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4454 4343 145 145 0 4309 0
[pid=30049] vsize: 17816
Current children cumulated CPU time (s) 289.61
Current children cumulated vsize (Kb) 19940

[startup+300.028 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4579 0 0 0 29930 30 0 0 25 0 1 0 1788310580 18812928 4484 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4593 4484 145 145 0 4448 0
[pid=30049] vsize: 18372
Current children cumulated CPU time (s) 299.6
Current children cumulated vsize (Kb) 20496

[startup+310.029 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4923 0 0 0 30925 33 0 0 25 0 1 0 1788310580 20209664 4828 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4934 4828 145 145 0 4789 0
[pid=30049] vsize: 19736
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 21860

[startup+320.03 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4923 0 0 0 31925 33 0 0 25 0 1 0 1788310580 20209664 4828 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4934 4828 145 145 0 4789 0
[pid=30049] vsize: 19736
Current children cumulated CPU time (s) 319.58
Current children cumulated vsize (Kb) 21860

[startup+330.031 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4928 0 0 0 32925 33 0 0 25 0 1 0 1788310580 20234240 4833 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4940 4833 145 145 0 4795 0
[pid=30049] vsize: 19760
Current children cumulated CPU time (s) 329.58
Current children cumulated vsize (Kb) 21884

[startup+340.032 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4943 0 0 0 33925 33 0 0 25 0 1 0 1788310580 20299776 4848 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4956 4848 145 145 0 4811 0
[pid=30049] vsize: 19824
Current children cumulated CPU time (s) 339.58
Current children cumulated vsize (Kb) 21948

[startup+350.033 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 4952 0 0 0 34925 33 0 0 25 0 1 0 1788310580 20336640 4857 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 4965 4857 145 145 0 4820 0
[pid=30049] vsize: 19860
Current children cumulated CPU time (s) 349.58
Current children cumulated vsize (Kb) 21984

[startup+360.033 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5090 0 0 0 35923 34 0 0 25 0 1 0 1788310580 21028864 4995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5134 4995 145 145 0 4989 0
[pid=30049] vsize: 20536
Current children cumulated CPU time (s) 359.57
Current children cumulated vsize (Kb) 22660

[startup+370.034 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5090 0 0 0 36923 34 0 0 25 0 1 0 1788310580 21028864 4995 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5134 4995 145 145 0 4989 0
[pid=30049] vsize: 20536
Current children cumulated CPU time (s) 369.57
Current children cumulated vsize (Kb) 22660

[startup+380.035 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5090 0 0 0 37923 34 0 0 25 0 1 0 1788310580 21028864 4995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5134 4995 145 145 0 4989 0
[pid=30049] vsize: 20536
Current children cumulated CPU time (s) 379.57
Current children cumulated vsize (Kb) 22660

[startup+390.036 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5099 0 0 0 38924 34 0 0 25 0 1 0 1788310580 21078016 5004 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5146 5004 145 145 0 5001 0
[pid=30049] vsize: 20584
Current children cumulated CPU time (s) 389.58
Current children cumulated vsize (Kb) 22708

[startup+400.037 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5134 0 0 0 39924 34 0 0 25 0 1 0 1788310580 21274624 5039 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5194 5039 145 145 0 5049 0
[pid=30049] vsize: 20776
Current children cumulated CPU time (s) 399.58
Current children cumulated vsize (Kb) 22900

[startup+410.038 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5135 0 0 0 40924 34 0 0 25 0 1 0 1788310580 21274624 5040 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5194 5040 145 145 0 5049 0
[pid=30049] vsize: 20776
Current children cumulated CPU time (s) 409.58
Current children cumulated vsize (Kb) 22900

[startup+420.038 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5157 0 0 0 41924 35 0 0 25 0 1 0 1788310580 21360640 5062 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5215 5062 145 145 0 5070 0
[pid=30049] vsize: 20860
Current children cumulated CPU time (s) 419.59
Current children cumulated vsize (Kb) 22984

[startup+430.039 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5601 0 0 0 42916 38 0 0 25 0 1 0 1788310580 23179264 5506 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5659 5506 145 145 0 5514 0
[pid=30049] vsize: 22636
Current children cumulated CPU time (s) 429.54
Current children cumulated vsize (Kb) 24760

[startup+440.04 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5601 0 0 0 43916 38 0 0 25 0 1 0 1788310580 23179264 5506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5659 5506 145 145 0 5514 0
[pid=30049] vsize: 22636
Current children cumulated CPU time (s) 439.54
Current children cumulated vsize (Kb) 24760

[startup+450.041 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5601 0 0 0 44916 38 0 0 25 0 1 0 1788310580 23179264 5506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5659 5506 145 145 0 5514 0
[pid=30049] vsize: 22636
Current children cumulated CPU time (s) 449.54
Current children cumulated vsize (Kb) 24760

[startup+460.042 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5601 0 0 0 45917 39 0 0 25 0 1 0 1788310580 23179264 5506 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 5659 5506 145 145 0 5514 0
[pid=30049] vsize: 22636
Current children cumulated CPU time (s) 459.56
Current children cumulated vsize (Kb) 24760

[startup+470.043 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 5996 0 0 0 46911 41 0 0 25 0 1 0 1788310580 24797184 5901 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6054 5901 145 145 0 5909 0
[pid=30049] vsize: 24216
Current children cumulated CPU time (s) 469.52
Current children cumulated vsize (Kb) 26340

[startup+480.043 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 47903 45 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 479.48
Current children cumulated vsize (Kb) 27840

[startup+490.044 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 48902 46 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 489.48
Current children cumulated vsize (Kb) 27840

[startup+500.046 s]
Raw data (loadavg): 1.00 1.00 0.90 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 49902 46 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223156 134558440 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 499.48
Current children cumulated vsize (Kb) 27840

[startup+510.046 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 50902 46 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 509.48
Current children cumulated vsize (Kb) 27840

[startup+520.047 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 51902 46 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 519.48
Current children cumulated vsize (Kb) 27840

[startup+530.048 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 52902 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 529.49
Current children cumulated vsize (Kb) 27840

[startup+540.049 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 53901 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 539.48
Current children cumulated vsize (Kb) 27840

[startup+550.049 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 54902 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 549.49
Current children cumulated vsize (Kb) 27840

[startup+560.05 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 55902 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 559.49
Current children cumulated vsize (Kb) 27840

[startup+570.051 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 56902 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 569.49
Current children cumulated vsize (Kb) 27840

[startup+580.052 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 57902 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 579.49
Current children cumulated vsize (Kb) 27840

[startup+590.054 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6371 0 0 0 58902 47 0 0 25 0 1 0 1788310580 26333184 6276 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6276 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 589.49
Current children cumulated vsize (Kb) 27840

[startup+600.055 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6372 0 0 0 59902 47 0 0 25 0 1 0 1788310580 26333184 6277 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6277 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 599.49
Current children cumulated vsize (Kb) 27840

[startup+610.056 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 60903 47 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221222896 134781514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 609.5
Current children cumulated vsize (Kb) 27840

[startup+620.056 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 61903 47 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 619.5
Current children cumulated vsize (Kb) 27840

[startup+630.056 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 62903 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 629.51
Current children cumulated vsize (Kb) 27840

[startup+640.057 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 63903 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 639.51
Current children cumulated vsize (Kb) 27840

[startup+650.058 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 64903 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 649.51
Current children cumulated vsize (Kb) 27840

[startup+660.058 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 65904 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 659.52
Current children cumulated vsize (Kb) 27840

[startup+670.059 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 66904 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 669.52
Current children cumulated vsize (Kb) 27840

[startup+680.059 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 67903 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221222976 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 679.51
Current children cumulated vsize (Kb) 27840

[startup+690.06 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 68903 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 689.51
Current children cumulated vsize (Kb) 27840

[startup+700.061 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 69904 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 699.52
Current children cumulated vsize (Kb) 27840

[startup+710.062 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 70904 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 709.52
Current children cumulated vsize (Kb) 27840

[startup+720.064 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 71904 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 719.52
Current children cumulated vsize (Kb) 27840

[startup+730.065 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6373 0 0 0 72904 48 0 0 25 0 1 0 1788310580 26333184 6278 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6278 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 729.52
Current children cumulated vsize (Kb) 27840

[startup+740.066 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6374 0 0 0 73904 48 0 0 25 0 1 0 1788310580 26333184 6279 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6279 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 739.52
Current children cumulated vsize (Kb) 27840

[startup+750.066 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 74905 48 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 749.53
Current children cumulated vsize (Kb) 27840

[startup+760.067 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 75905 48 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 759.53
Current children cumulated vsize (Kb) 27840

[startup+770.068 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 76905 48 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 769.53
Current children cumulated vsize (Kb) 27840

[startup+780.07 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 77905 49 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 779.54
Current children cumulated vsize (Kb) 27840

[startup+790.072 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 78905 49 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 789.54
Current children cumulated vsize (Kb) 27840

[startup+800.073 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 79906 49 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 799.55
Current children cumulated vsize (Kb) 27840

[startup+810.073 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 80906 49 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 809.55
Current children cumulated vsize (Kb) 27840

[startup+820.074 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 81906 49 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 819.55
Current children cumulated vsize (Kb) 27840

[startup+830.075 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6376 0 0 0 82906 49 0 0 25 0 1 0 1788310580 26333184 6281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6281 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 829.55
Current children cumulated vsize (Kb) 27840

[startup+840.077 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6378 0 0 0 83907 49 0 0 25 0 1 0 1788310580 26333184 6283 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6283 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 839.56
Current children cumulated vsize (Kb) 27840

[startup+850.078 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6378 0 0 0 84907 49 0 0 25 0 1 0 1788310580 26333184 6283 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6283 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 849.56
Current children cumulated vsize (Kb) 27840

[startup+860.079 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6378 0 0 0 85907 49 0 0 25 0 1 0 1788310580 26333184 6283 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6283 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 859.56
Current children cumulated vsize (Kb) 27840

[startup+870.079 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 86907 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 869.56
Current children cumulated vsize (Kb) 27840

[startup+880.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 87908 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 879.57
Current children cumulated vsize (Kb) 27840

[startup+890.081 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 88907 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 889.56
Current children cumulated vsize (Kb) 27840

[startup+900.082 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 89908 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 899.57
Current children cumulated vsize (Kb) 27840

[startup+910.083 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 90908 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 909.57
Current children cumulated vsize (Kb) 27840

[startup+920.084 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 91908 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 919.57
Current children cumulated vsize (Kb) 27840

[startup+930.085 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6382 0 0 0 92909 49 0 0 25 0 1 0 1788310580 26333184 6287 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6429 6287 145 145 0 6284 0
[pid=30049] vsize: 25716
Current children cumulated CPU time (s) 929.58
Current children cumulated vsize (Kb) 27840

[startup+940.085 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6389 0 0 0 93909 49 0 0 25 0 1 0 1788310580 26378240 6294 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6440 6294 145 145 0 6295 0
[pid=30049] vsize: 25760
Current children cumulated CPU time (s) 939.58
Current children cumulated vsize (Kb) 27884

[startup+950.086 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 94909 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 949.58
Current children cumulated vsize (Kb) 27916

[startup+960.087 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 95909 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 959.58
Current children cumulated vsize (Kb) 27916

[startup+970.088 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 96909 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 969.58
Current children cumulated vsize (Kb) 27916

[startup+980.089 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 97910 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 979.59
Current children cumulated vsize (Kb) 27916

[startup+990.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 98910 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 989.59
Current children cumulated vsize (Kb) 27916

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 99910 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 999.59
Current children cumulated vsize (Kb) 27916

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 100910 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1009.59
Current children cumulated vsize (Kb) 27916

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 101911 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1019.6
Current children cumulated vsize (Kb) 27916

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 102911 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1029.6
Current children cumulated vsize (Kb) 27916

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 103911 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1039.6
Current children cumulated vsize (Kb) 27916

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 104911 49 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1049.6
Current children cumulated vsize (Kb) 27916

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 105911 50 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1059.61
Current children cumulated vsize (Kb) 27916

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6395 0 0 0 106911 50 0 0 25 0 1 0 1788310580 26411008 6300 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6448 6300 145 145 0 6303 0
[pid=30049] vsize: 25792
Current children cumulated CPU time (s) 1069.61
Current children cumulated vsize (Kb) 27916

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6462 0 0 0 107910 51 0 0 25 0 1 0 1788310580 26685440 6367 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6515 6367 145 145 0 6370 0
[pid=30049] vsize: 26060
Current children cumulated CPU time (s) 1079.61
Current children cumulated vsize (Kb) 28184

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6495 0 0 0 108908 52 0 0 25 0 1 0 1788310580 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6548 6400 145 145 0 6403 0
[pid=30049] vsize: 26192
Current children cumulated CPU time (s) 1089.6
Current children cumulated vsize (Kb) 28316

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6495 0 0 0 109908 52 0 0 25 0 1 0 1788310580 26820608 6400 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6548 6400 145 145 0 6403 0
[pid=30049] vsize: 26192
Current children cumulated CPU time (s) 1099.6
Current children cumulated vsize (Kb) 28316

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6495 0 0 0 110908 53 0 0 25 0 1 0 1788310580 26820608 6400 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6548 6400 145 145 0 6403 0
[pid=30049] vsize: 26192
Current children cumulated CPU time (s) 1109.61
Current children cumulated vsize (Kb) 28316

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6495 0 0 0 111909 53 0 0 25 0 1 0 1788310580 26820608 6400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6548 6400 145 145 0 6403 0
[pid=30049] vsize: 26192
Current children cumulated CPU time (s) 1119.62
Current children cumulated vsize (Kb) 28316

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6500 0 0 0 112909 53 0 0 25 0 1 0 1788310580 26853376 6405 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6556 6405 145 145 0 6411 0
[pid=30049] vsize: 26224
Current children cumulated CPU time (s) 1129.62
Current children cumulated vsize (Kb) 28348

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6506 0 0 0 113909 53 0 0 25 0 1 0 1788310580 26886144 6411 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6564 6411 145 145 0 6419 0
[pid=30049] vsize: 26256
Current children cumulated CPU time (s) 1139.62
Current children cumulated vsize (Kb) 28380

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6511 0 0 0 114909 53 0 0 25 0 1 0 1788310580 26918912 6416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6572 6416 145 145 0 6427 0
[pid=30049] vsize: 26288
Current children cumulated CPU time (s) 1149.62
Current children cumulated vsize (Kb) 28412

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 6601 0 0 0 115908 54 0 0 25 0 1 0 1788310580 27287552 6506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 6662 6506 145 145 0 6517 0
[pid=30049] vsize: 26648
Current children cumulated CPU time (s) 1159.62
Current children cumulated vsize (Kb) 28772

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 7031 0 0 0 116901 57 0 0 25 0 1 0 1788310580 29052928 6936 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 7093 6936 145 145 0 6948 0
[pid=30049] vsize: 28372
Current children cumulated CPU time (s) 1169.58
Current children cumulated vsize (Kb) 30496

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 7196 0 0 0 117898 57 0 0 25 0 1 0 1788310580 29732864 7101 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 7259 7101 145 145 0 7114 0
[pid=30049] vsize: 29036
Current children cumulated CPU time (s) 1179.55
Current children cumulated vsize (Kb) 31160

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 7196 0 0 0 118898 58 0 0 25 0 1 0 1788310580 29732864 7101 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 7259 7101 145 145 0 7114 0
[pid=30049] vsize: 29036
Current children cumulated CPU time (s) 1189.56
Current children cumulated vsize (Kb) 31160

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 7196 0 0 0 119898 58 0 0 25 0 1 0 1788310580 29732864 7101 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 7259 7101 145 145 0 7114 0
[pid=30049] vsize: 29036
Current children cumulated CPU time (s) 1199.56
Current children cumulated vsize (Kb) 31160

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 7196 0 0 0 120899 58 0 0 25 0 1 0 1788310580 29732864 7101 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 7259 7101 145 145 0 7114 0
[pid=30049] vsize: 29036
Current children cumulated CPU time (s) 1209.57
Current children cumulated vsize (Kb) 31160



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.91 2/57 30049
Raw data (/proc/30045/stat): 30045 (minisat+_script) S 30044 30045 6847 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788310575 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30045/statm): 531 226 485 147 0 384 0
[pid=30045] vsize: 2124
Raw data (/proc/30049/stat): 30049 (minisat+_64-bit) R 30045 30045 6847 0 -1 0 7196 0 0 0 120899 58 0 0 25 0 1 0 1788310580 29732864 7101 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30049/statm): 7259 7101 145 145 0 7114 0
[pid=30049] vsize: 29036
Current children cumulated CPU time (s) 1209.57
Current children cumulated vsize (Kb) 31160

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.59
CPU user time (s): 1208.99
CPU system time (s): 0.595909
CPU usage (%): 99.9552
Max. virtual memory (cumulated for all children) (Kb): 31160

Verifier Data

ERROR: no interpretation found !