Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0201.opb
MD5SUM8c361d02d5162bb0b133ab6ed38f9294
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1523
Optimality of the best value was proved YES
Number of terms in the objective function 201
Biggest coefficient in the objective function 1920
Number of bits for the biggest coefficient in the objective function 11
Sum of the numbers in the objective function 19980
Number of bits of the sum of numbers in the objective function 15
Biggest number in a constraint 1920
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 19980
Number of bits of the biggest sum of numbers15
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark212.013
Number of variables201
Total number of constraints334
Number of constraints which are clauses20
Number of constraints which are cardinality constraints (but not clauses)227
Number of constraints which are nor clauses,nor cardinality constraints87
Minimum length of a constraint1
Maximum length of a constraint67

Trace number 4540

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        840328 kB
Buffers:         35704 kB
Cached:         130064 kB
SwapCached:        696 kB
Active:          75316 kB
Inactive:        93032 kB
HighTotal:      131008 kB
HighFree:        34972 kB
LowTotal:       903652 kB
LowFree:        805356 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5816 kB
Slab:            20252 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:26:03 (client local time) WITH STATUS 10 IN 1209.75 SECONDS
stats: 2996 7 1209.75 10

Solver Data

c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   15
c ---[ 107]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   39
c ---[  88]---> BDD-cost:   42
c ---[  87]---> BDD-cost:   42
c ---[  86]---> BDD-cost:   54
c ---[  85]---> BDD-cost:   73
c ---[  84]---> BDD-cost:   73
c ---[  83]---> BDD-cost:   98
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:  160
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  201
c ---[  76]---> BDD-cost:  128
c ---[  75]---> BDD-cost:  128
c ---[  74]---> BDD-cost:  241
c ---[  73]---> BDD-cost:  150
c ---[  72]---> BDD-cost:  150
c ---[  71]---> BDD-cost:  281
c ---[  70]---> BDD-cost:  172
c ---[  69]---> BDD-cost:  172
c ---[  68]---> BDD-cost:  321
c ---[  67]---> BDD-cost:  194
c ---[  66]---> BDD-cost:  194
c ---[  65]---> BDD-cost:  361
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   11
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11741    34621 |    3913       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 2213
c ---[   0]---> Sorter-cost:21097     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        58 |   58177   143044 |   19392      56      148     2.6 |  0.000 % |
c ==============================================================================
c Found solution: 2087
c ---[   0]---> Sorter-cost:    6     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        88 |   58581   144183 |   19527      81      549     6.8 |  0.000 % |
c |       188 |   58581   144183 |   21479     181     2385    13.2 |  0.542 % |
c ==============================================================================
c Found solution: 2077
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       307 |   58494   144055 |   19498     298     8553    28.7 |  0.542 % |
c |       409 |   57412   141593 |   21447     382     9171    24.0 |  1.991 % |
c |       559 |   54361   134594 |   23592     487     9880    20.3 |  5.933 % |
c ==============================================================================
c Found solution: 2076
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       612 |   54176   134172 |   18058     537    12758    23.8 |  5.933 % |
c |       712 |   53761   133220 |   19863     632    13949    22.1 |  6.753 % |
c |       862 |   53131   131774 |   21850     768    17863    23.3 |  7.596 % |
c ==============================================================================
c Found solution: 2015
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1004 |   53241   132050 |   17747     910    28831    31.7 |  7.596 % |
c |      1106 |   53176   131902 |   19521    1010    30785    30.5 |  7.667 % |
c |      1256 |   53016   131530 |   21473    1157    35572    30.7 |  7.907 % |
c |      1482 |   50129   124875 |   23621    1328    39088    29.4 | 11.871 % |
c ==============================================================================
c Found solution: 2014
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1689 |   50199   125050 |   16733    1535    47004    30.6 | 11.871 % |
c |      1790 |   50164   124959 |   18406    1635    47984    29.3 | 11.926 % |
c |      1941 |   50143   124911 |   20246    1784    49437    27.7 | 12.060 % |
c |      2166 |   48818   121858 |   22271    1852    53041    28.6 | 13.758 % |
c |      2503 |   48818   121858 |   24498    2189    83892    38.3 | 13.758 % |
c |      3010 |   48250   120520 |   26948    2656   108054    40.7 | 14.588 % |
c ==============================================================================
c Found solution: 2008
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3349 |   47655   119142 |   15885    2985   116858    39.1 | 14.588 % |
c |      3450 |   47645   119116 |   17473    3083   122439    39.7 | 15.446 % |
c |      3600 |   47645   119116 |   19220    3233   125119    38.7 | 15.446 % |
c ==============================================================================
c Found solution: 1944
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3684 |   47645   119119 |   15881    3313   128636    38.8 | 15.446 % |
c |      3784 |   47642   119110 |   17469    3408   133871    39.3 | 15.463 % |
c |      3937 |   47525   118845 |   19216    3555   134588    37.9 | 15.628 % |
c |      4162 |   46824   117216 |   21137    3767   144530    38.4 | 16.636 % |
c ==============================================================================
c Found solution: 1924
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4272 |   46828   117225 |   15609    3877   149017    38.4 | 16.636 % |
c |      4376 |   46828   117225 |   17169    3981   153904    38.7 | 16.638 % |
c |      4526 |   46129   115608 |   18886    4104   160348    39.1 | 17.606 % |
c |      4754 |   46129   115608 |   20775    4332   167592    38.7 | 17.606 % |
c |      5092 |   46129   115608 |   22853    4670   179196    38.4 | 17.606 % |
c |      5598 |   46129   115608 |   25138    5176   190777    36.9 | 17.606 % |
c |      6359 |   45838   114933 |   27652    5928   228619    38.6 | 17.997 % |
c ==============================================================================
c Found solution: 1919
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6462 |   45848   114959 |   15282    6027   234251    38.9 | 17.997 % |
c |      6563 |   45848   114959 |   16810    6128   237549    38.8 | 18.005 % |
c |      6715 |   45543   114264 |   18491    6275   247244    39.4 | 18.404 % |
c ==============================================================================
c Found solution: 1918
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6777 |   45548   114281 |   15182    6337   248676    39.2 | 18.404 % |
c |      6880 |   45548   114281 |   16700    6440   251831    39.1 | 18.405 % |
c |      7031 |   45548   114281 |   18370    6591   255386    38.7 | 18.405 % |
c |      7257 |   45484   114134 |   20207    6815   263672    38.7 | 18.488 % |
c ==============================================================================
c Found solution: 1916
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7344 |   45488   114145 |   15162    6902   267676    38.8 | 18.488 % |
c |      7444 |   45488   114145 |   16678    7002   274101    39.1 | 18.490 % |
c |      7594 |   45488   114145 |   18346    7152   280094    39.2 | 18.490 % |
c |      7820 |   45488   114145 |   20180    7378   284897    38.6 | 18.490 % |
c |      8157 |   45484   114137 |   22198    7713   291786    37.8 | 18.498 % |
c ==============================================================================
c Found solution: 1846
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8275 |   45493   114162 |   15164    7831   301898    38.6 | 18.498 % |
c |      8376 |   45493   114162 |   16680    7932   304635    38.4 | 18.498 % |
c |      8526 |   45493   114162 |   18348    8082   310387    38.4 | 18.498 % |
c |      8751 |   45493   114162 |   20183    8307   326338    39.3 | 18.498 % |
c |      9088 |   45493   114162 |   22201    8644   350743    40.6 | 18.498 % |
c |      9595 |   45487   114149 |   24421    9149   378954    41.4 | 18.507 % |
c ==============================================================================
c Found solution: 1843
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9817 |   45493   114164 |   15164    9371   396771    42.3 | 18.507 % |
c |      9917 |   45493   114164 |   16680    9471   405490    42.8 | 18.508 % |
c |     10067 |   45043   113120 |   18348    9590   409422    42.7 | 19.128 % |
c |     10292 |   44860   112696 |   20183    9807   421869    43.0 | 19.384 % |
c |     10629 |   44704   112330 |   22201   10139   441298    43.5 | 19.592 % |
c |     11139 |   44704   112330 |   24421   10649   466222    43.8 | 19.592 % |
c |     11898 |   44680   112268 |   26863   11369   490362    43.1 | 19.626 % |
c |     13040 |   44680   112268 |   29550   12511   608632    48.6 | 19.626 % |
c |     14752 |   44669   112242 |   32505   14218   720930    50.7 | 19.644 % |
c ==============================================================================
c Found solution: 1769
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15639 |   44689   112297 |   14896   15105   787606    52.1 | 19.644 % |
c |     15739 |   44614   112122 |   16385   15204   791922    52.1 | 19.753 % |
c |     15889 |   44609   112109 |   18024   15353   803812    52.4 | 19.762 % |
c |     16116 |   44609   112109 |   19826   15580   814384    52.3 | 19.762 % |
c |     16454 |   44605   112100 |   21809   15917   838394    52.7 | 19.766 % |
c |     16960 |   44590   112061 |   23990   16418   854500    52.0 | 19.792 % |
c |     17719 |   44590   112061 |   26389   17177   917295    53.4 | 19.792 % |
c |     18859 |   44590   112061 |   29028   18317   999570    54.6 | 19.792 % |
c |     20567 |   44590   112061 |   31930   20025  1075528    53.7 | 19.792 % |
c |     23130 |   44178   111114 |   35123   22532  1237111    54.9 | 20.394 % |
c |     26974 |   44157   111063 |   38636   26371  1393049    52.8 | 20.433 % |
c |     32744 |   44139   111013 |   42500   32137  1636168    50.9 | 20.455 % |
c |     41393 |   42971   108270 |   46750   40731  2120834    52.1 | 22.110 % |
c ==============================================================================
c Found solution: 1761
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48818 |   42886   108076 |   14295   48152  2633672    54.7 | 22.110 % |
c |     48918 |   42886   108076 |   15724   17188   786843    45.8 | 22.254 % |
c |     49070 |   42886   108076 |   17296   17340   794497    45.8 | 22.254 % |
c |     49296 |   42886   108076 |   19026   17566   802504    45.7 | 22.254 % |
c |     49635 |   42886   108076 |   20929   17905   826393    46.2 | 22.254 % |
c |     50142 |   42886   108076 |   23022   18412   865716    47.0 | 22.254 % |
c |     50902 |   42878   108060 |   25324   19169   913273    47.6 | 22.271 % |
c ==============================================================================
c Found solution: 1759
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51206 |   42886   108079 |   14295   19473   926514    47.6 | 22.271 % |
c |     51310 |   42803   107886 |   15724    9838   411836    41.9 | 22.392 % |
c |     51460 |   42701   107650 |   17296    9986   422304    42.3 | 22.539 % |
c |     51685 |   42697   107641 |   19026   10209   428287    42.0 | 22.543 % |
c |     52023 |   42432   107026 |   20929   10519   434920    41.3 | 22.898 % |
c |     52529 |   42432   107026 |   23022   11025   448791    40.7 | 22.898 % |
c |     53292 |   42432   107026 |   25324   11788   467859    39.7 | 22.898 % |
c ==============================================================================
c Found solution: 1756
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54231 |   42437   107038 |   14145   12727   559381    44.0 | 22.898 % |
c |     54331 |   42437   107038 |   15559   12827   560789    43.7 | 22.900 % |
c |     54481 |   42437   107038 |   17115   12977   573557    44.2 | 22.900 % |
c |     54706 |   42434   107029 |   18826   13198   579935    43.9 | 22.904 % |
c |     55043 |   42434   107029 |   20709   13535   601435    44.4 | 22.904 % |
c |     55550 |   42434   107029 |   22780   14042   661065    47.1 | 22.904 % |
c |     56309 |   42401   106930 |   25058   14797   680051    46.0 | 22.952 % |
c |     57449 |   42322   106745 |   27564   15935   760344    47.7 | 23.069 % |
c ==============================================================================
c Found solution: 1749
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58385 |   42200   106464 |   14066   16861   826619    49.0 | 23.069 % |
c |     58485 |   42200   106464 |   15472   16961   829910    48.9 | 23.248 % |
c |     58635 |   42200   106464 |   17019   17111   836797    48.9 | 23.248 % |
c |     58860 |   42200   106464 |   18721   17336   867691    50.1 | 23.248 % |
c |     59197 |   42200   106464 |   20594   17673   885830    50.1 | 23.248 % |
c |     59703 |   42200   106464 |   22653   18179   915589    50.4 | 23.249 % |
c |     60462 |   42196   106456 |   24918   18937   964396    50.9 | 23.257 % |
c |     61604 |   42196   106456 |   27410   20079  1033370    51.5 | 23.257 % |
c |     63312 |   42196   106456 |   30151   21787  1114193    51.1 | 23.257 % |
c |     65874 |   42196   106456 |   33166   24349  1253412    51.5 | 23.257 % |
c |     69718 |   42187   106435 |   36483   28190  1394186    49.5 | 23.274 % |
c ==============================================================================
c Found solution: 1743
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72990 |   42189   106437 |   14063   31459  1576631    50.1 | 23.274 % |
c |     73091 |   42189   106437 |   15469   15831   562887    35.6 | 23.281 % |
c |     73241 |   42189   106437 |   17016   15981   566465    35.4 | 23.281 % |
c |     73466 |   42189   106437 |   18717   16206   570598    35.2 | 23.281 % |
c |     73805 |   41908   105779 |   20589   16536   579979    35.1 | 23.705 % |
c |     74311 |   41662   105210 |   22648   17030   627126    36.8 | 24.048 % |
c |     75070 |   41523   104885 |   24913   17781   648143    36.5 | 24.251 % |
c |     76211 |   41523   104885 |   27404   18922   717960    37.9 | 24.251 % |
c |     77919 |   41512   104854 |   30145   20628   782194    37.9 | 24.268 % |
c |     80484 |   41512   104854 |   33159   23193   910444    39.3 | 24.268 % |
c |     84329 |   40399   102256 |   36475   26987  1186359    44.0 | 25.849 % |
c |     90099 |   39769   100788 |   40123   32705  1642873    50.2 | 26.758 % |
c |     98749 |   39730   100682 |   44135   41347  2170899    52.5 | 26.819 % |
c |    111725 |   39713   100639 |   48549   54317  3086904    56.8 | 26.849 % |
c ==============================================================================
c Found solution: 1741
c ---[   0]---> Sorter-cost:    1     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118195 |   39699   100609 |   13233   23258  1388829    59.7 | 26.849 % |
c |    118296 |   39689   100586 |   14556   11727   665419    56.7 | 26.884 % |
c |    118446 |   39679   100560 |   16011   11873   670901    56.5 | 26.902 % |
c |    118671 |   39679   100560 |   17613   12098   687485    56.8 | 26.902 % |
c |    119008 |   39679   100560 |   19374   12435   703065    56.5 | 26.902 % |
c |    119514 |   39679   100560 |   21311   12941   720728    55.7 | 26.902 % |
c ==============================================================================
c Found solution: 1729
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119798 |   39683   100570 |   13227   13225   738497    55.8 | 26.902 % |
c |    119900 |   39683   100570 |   14549   13327   742833    55.7 | 26.902 % |
c |    120052 |   39683   100570 |   16004   13479   752015    55.8 | 26.902 % |
c |    120277 |   39683   100570 |   17605   13704   756186    55.2 | 26.902 % |
c |    120614 |   39683   100570 |   19365   14041   782319    55.7 | 26.902 % |
c |    121120 |   39683   100570 |   21302   14547   817325    56.2 | 26.902 % |
c |    121880 |   39683   100570 |   23432   15307   877308    57.3 | 26.902 % |
c |    123019 |   39659   100511 |   25775   16443   938598    57.1 | 26.937 % |
c |    124729 |   39659   100511 |   28353   18153  1000399    55.1 | 26.937 % |
c ==============================================================================
c Found solution: 1701
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125372 |   39664   100522 |   13221   18796  1039475    55.3 | 26.937 % |
c |    125473 |   39664   100522 |   14543   18897  1043357    55.2 | 26.938 % |
c |    125623 |   39664   100522 |   15997   19047  1048216    55.0 | 26.938 % |
c |    125848 |   39664   100522 |   17597   19272  1057344    54.9 | 26.938 % |
c |    126186 |   39664   100522 |   19356   19610  1080876    55.1 | 26.938 % |
c |    126693 |   39650   100490 |   21292   20114  1106316    55.0 | 26.955 % |
c |    127452 |   39650   100490 |   23421   20873  1170355    56.1 | 26.955 % |
c |    128592 |   39650   100490 |   25763   22013  1242185    56.4 | 26.955 % |
c |    130300 |   39650   100490 |   28340   23721  1375243    58.0 | 26.955 % |
c |    132866 |   39647   100481 |   31174   26285  1590875    60.5 | 26.960 % |
c |    136710 |   39637   100455 |   34291   30126  1822172    60.5 | 26.977 % |
c |    142477 |   39637   100455 |   37721   35893  2196023    61.2 | 26.977 % |
c ==============================================================================
c Found solution: 1696
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    143937 |   39642   100466 |   13214   37353  2277346    61.0 | 26.977 % |
c |    144038 |   39642   100466 |   14535   16962   764796    45.1 | 26.978 % |
c |    144188 |   39642   100466 |   15988   17112   775442    45.3 | 26.978 % |
c |    144413 |   39642   100466 |   17587   17337   780597    45.0 | 26.978 % |
c |    144751 |   39642   100466 |   19346   17675   798050    45.2 | 26.978 % |
c |    145257 |   39642   100466 |   21281   18181   821444    45.2 | 26.978 % |
c |    146016 |   39642   100466 |   23409   18940   863635    45.6 | 26.978 % |
c |    147155 |   39642   100466 |   25750   20079   904913    45.1 | 26.978 % |
c ==============================================================================
c Found solution: 1693
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    148336 |   39644   100469 |   13214   21259   971574    45.7 | 26.978 % |
c |    148436 |   39644   100469 |   14535   10730   315161    29.4 | 26.983 % |
c |    148586 |   39644   100469 |   15988   10880   321998    29.6 | 26.983 % |
c |    148812 |   39644   100469 |   17587   11106   328461    29.6 | 26.983 % |
c |    149149 |   39644   100469 |   19346   11443   344450    30.1 | 26.983 % |
c |    149655 |   39644   100469 |   21281   11949   382445    32.0 | 26.983 % |
c |    150416 |   39644   100469 |   23409   12710   427011    33.6 | 26.983 % |
c |    151555 |   39644   100469 |   25750   13849   492378    35.6 | 26.983 % |
c |    153265 |   39644   100469 |   28325   15559   622810    40.0 | 26.983 % |
c |    155829 |   39632   100439 |   31157   18121   766535    42.3 | 27.004 % |
c |    159673 |   39632   100439 |   34273   21965  1039505    47.3 | 27.005 % |
c |    165445 |   39622   100413 |   37701   27733  1317732    47.5 | 27.022 % |
c ==============================================================================
c Found solution: 1679
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    171269 |   39638   100455 |   13212   33557  1651605    49.2 | 27.022 % |
c |    171371 |   39638   100455 |   14533   16881   647248    38.3 | 27.014 % |
c |    171521 |   39638   100455 |   15986   17031   651040    38.2 | 27.014 % |
c |    171746 |   39638   100455 |   17585   17256   662783    38.4 | 27.014 % |
c |    172085 |   39638   100455 |   19343   17595   685001    38.9 | 27.014 % |
c |    172592 |   39638   100455 |   21278   18102   701598    38.8 | 27.014 % |
c ==============================================================================
c Found solution: 1677
c ---[   0]---> Sorter-cost:    4     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    172877 |   39643   100472 |   13214   18387   719968    39.2 | 27.014 % |
c |    172977 |   39643   100472 |   14535   18487   724554    39.2 | 27.014 % |
c |    173127 |   39643   100472 |   15988   18637   729431    39.1 | 27.014 % |
c |    173352 |   39643   100472 |   17587   18862   740892    39.3 | 27.014 % |
c |    173689 |   39643   100472 |   19346   19199   754655    39.3 | 27.014 % |
c |    174196 |   39643   100472 |   21281   19706   785502    39.9 | 27.014 % |
c |    174955 |   39411    99937 |   23409   20453   819913    40.1 | 27.360 % |
c |    176094 |   39397    99904 |   25750   21590   847207    39.2 | 27.360 % |
c |    177807 |   39249    99557 |   28325   23293   943484    40.5 | 27.572 % |
c |    180369 |   39249    99557 |   31157   25855  1038523    40.2 | 27.572 % |
c |    184213 |   39249    99557 |   34273   29699  1239558    41.7 | 27.572 % |
c ==============================================================================
c Found solution: 1672
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187009 |   39256    99582 |   13085   32495  1391426    42.8 | 27.572 % |
c |    187111 |   39256    99582 |   14393   16350   570794    34.9 | 27.570 % |
c |    187263 |   39256    99582 |   15832   16502   578503    35.1 | 27.570 % |
c |    187490 |   39247    99555 |   17416   16726   588517    35.2 | 27.583 % |
c |    187827 |   39235    99519 |   19157   17060   611560    35.8 | 27.601 % |
c |    188334 |   39235    99519 |   21073   17567   634162    36.1 | 27.601 % |
c |    189094 |   39229    99501 |   23180   18325   668812    36.5 | 27.609 % |
c |    190234 |   39229    99501 |   25498   19465   738337    37.9 | 27.609 % |
c |    191943 |   39223    99483 |   28048   21173   832692    39.3 | 27.618 % |
c |    194505 |   39223    99483 |   30853   23735   931114    39.2 | 27.618 % |
c |    198349 |   39223    99483 |   33939   27579  1169224    42.4 | 27.618 % |
c |    204115 |   39223    99483 |   37333   33345  1491711    44.7 | 27.618 % |
c |    212764 |   39217    99465 |   41066   41992  2071589    49.3 | 27.626 % |
c ==============================================================================
c Found solution: 1665
c ---[   0]---> Sorter-cost:    5     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    214192 |   39225    99484 |   13075   43420  2150246    49.5 | 27.626 % |
c |    214293 |   39225    99484 |   14382   17445   812180    46.6 | 27.625 % |
c |    214443 |   39225    99484 |   15820   17595   819216    46.6 | 27.625 % |
c |    214668 |   39225    99484 |   17402   17820   834210    46.8 | 27.625 % |
c |    215008 |   39203    99433 |   19143   18153   847906    46.7 | 27.655 % |
c |    215515 |   39203    99433 |   21057   18660   879984    47.2 | 27.655 % |
c |    216274 |   39203    99433 |   23163   19419   913894    47.1 | 27.655 % |
c |    217413 |   39203    99433 |   25479   20558   970424    47.2 | 27.655 % |
c |    219121 |   38981    98922 |   28027   22264  1088223    48.9 | 27.945 % |
c |    221684 |   38981    98922 |   30830   24827  1212727    48.8 | 27.945 % |
c |    225528 |   38981    98922 |   33913   28671  1371799    47.8 | 27.945 % |
c |    231294 |   38981    98922 |   37304   34437  1650776    47.9 | 27.945 % |
c ==============================================================================
c Found solution: 1649
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    237485 |   38974    98903 |   12991   40623  1971527    48.5 | 27.945 % |
c |    237586 |   38974    98903 |   14290   17766   648734    36.5 | 27.967 % |
c |    237737 |   38974    98903 |   15719   17917   654797    36.5 | 27.967 % |
c |    237962 |   38974    98903 |   17291   18142   666798    36.8 | 27.967 % |
c |    238301 |   38974    98903 |   19020   18481   684022    37.0 | 27.967 % |
c |    238807 |   38974    98903 |   20922   18987   707043    37.2 | 27.967 % |
c |    239566 |   38942    98829 |   23014   19745   747250    37.8 | 28.010 % |
c |    240705 |   38942    98829 |   25315   20884   807899    38.7 | 28.010 % |
c |    242413 |   38942    98829 |   27847   22592   913056    40.4 | 28.010 % |
c |    244977 |   38942    98829 |   30632   25156  1061313    42.2 | 28.010 % |
c |    248822 |   38942    98829 |   33695   29001  1230713    42.4 | 28.010 % |
c |    254589 |   38942    98829 |   37064   34768  1572707    45.2 | 28.010 % |
c |    263239 |   38942    98829 |   40771   43418  2149352    49.5 | 28.010 % |
c ==============================================================================
c Found solution: 1644
c ---[   0]---> Sorter-cost:    2     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    264270 |   38947    98840 |   12982   44449  2208838    49.7 | 28.010 % |
c |    264370 |   38947    98840 |   14280   18634   814489    43.7 | 28.011 % |
c |    264521 |   38947    98840 |   15708   18785   819644    43.6 | 28.011 % |
c |    264747 |   38947    98840 |   17279   19011   829567    43.6 | 28.011 % |
c |    265085 |   38947    98840 |   19006   19349   847697    43.8 | 28.011 % |
c |    265593 |   38947    98840 |   20907   19857   867080    43.7 | 28.011 % |
c |    266352 |   38947    98840 |   22998   20616   900910    43.7 | 28.011 % |
c |    267491 |   38947    98840 |   25298   21755   959365    44.1 | 28.011 % |
c |    269199 |   38947    98840 |   27828   23463  1057461    45.1 | 28.011 % |
c |    271762 |   38947    98840 |   30610   26026  1177586    45.2 | 28.011 % |
c |    275607 |   38947    98840 |   33671   29871  1378191    46.1 | 28.011 % |
c |    281374 |   38947    98840 |   37039   35638  1645153    46.2 | 28.011 % |
c ==============================================================================
c Found solution: 1643
c ---[   0]---> Sorter-cost:    3     Base: 5 2 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    289757 |   38952    98852 |   12984   44021  2047298    46.5 | 28.011 % |
c |    289862 |   38748    98381 |   14282   17891   627874    35.1 | 28.297 % |

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/11672/stat): 11672 (minisat+_script) R 11671 11672 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851932777 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/11672/statm): 174 3 169 147 0 27 0
[pid=11672] 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=11673
New process pid=11674
New process pid=11675
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
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
One traced child (pid=11674) exited with status: 0
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=11675) exited with status: 0
One traced child (pid=11673) exited with status: 0
New process pid=11676
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0201.opb

[startup+10.004 s]
Raw data (loadavg): 0.87 0.94 0.87 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2189 0 0 0 977 9 0 0 25 0 1 0 1851932782 9678848 2124 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11676/statm): 2363 2124 145 145 0 2218 0
[pid=11676] vsize: 9452
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 11576

[startup+20.0046 s]
Raw data (loadavg): 0.89 0.94 0.87 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2323 0 0 0 1974 11 0 0 25 0 1 0 1851932782 10227712 2258 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 2497 2258 145 145 0 2352 0
[pid=11676] vsize: 9988
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 12112

[startup+30.0053 s]
Raw data (loadavg): 0.91 0.94 0.87 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2485 0 0 0 2972 11 0 0 25 0 1 0 1851932782 10895360 2420 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 2660 2420 145 145 0 2515 0
[pid=11676] vsize: 10640
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 12764

[startup+40.006 s]
Raw data (loadavg): 0.92 0.94 0.87 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2689 0 0 0 3969 13 0 0 25 0 1 0 1851932782 11730944 2624 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 2864 2624 145 145 0 2719 0
[pid=11676] vsize: 11456
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 13580

[startup+50.0077 s]
Raw data (loadavg): 0.93 0.94 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2900 0 0 0 4965 14 0 0 25 0 1 0 1851932782 12587008 2835 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3073 2835 145 145 0 2928 0
[pid=11676] vsize: 12292
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 14416

[startup+60.0084 s]
Raw data (loadavg): 0.94 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3059 0 0 0 5961 15 0 0 25 0 1 0 1851932782 13295616 2994 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3246 2994 145 145 0 3101 0
[pid=11676] vsize: 12984
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 15108

[startup+70.009 s]
Raw data (loadavg): 0.95 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3255 0 0 0 6958 17 0 0 25 0 1 0 1851932782 14086144 3190 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3439 3190 145 145 0 3294 0
[pid=11676] vsize: 13756
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 15880

[startup+80.0107 s]
Raw data (loadavg): 0.96 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3423 0 0 0 7955 18 0 0 25 0 1 0 1851932782 14766080 3358 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3605 3358 145 145 0 3460 0
[pid=11676] vsize: 14420
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 16544

[startup+90.0114 s]
Raw data (loadavg): 0.96 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3583 0 0 0 8953 19 0 0 25 0 1 0 1851932782 15409152 3518 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3762 3518 145 145 0 3617 0
[pid=11676] vsize: 15048
Current children cumulated CPU time (s) 89.72
Current children cumulated vsize (Kb) 17172

[startup+100.012 s]
Raw data (loadavg): 0.97 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3689 0 0 0 9950 21 0 0 25 0 1 0 1851932782 15835136 3624 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3866 3624 145 145 0 3721 0
[pid=11676] vsize: 15464
Current children cumulated CPU time (s) 99.71
Current children cumulated vsize (Kb) 17588

[startup+110.013 s]
Raw data (loadavg): 0.97 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3783 0 0 0 10949 21 0 0 25 0 1 0 1851932782 16211968 3718 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 3958 3718 145 145 0 3813 0
[pid=11676] vsize: 15832
Current children cumulated CPU time (s) 109.7
Current children cumulated vsize (Kb) 17956

[startup+120.013 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3901 0 0 0 11947 22 0 0 25 0 1 0 1851932782 16687104 3836 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4074 3836 145 145 0 3929 0
[pid=11676] vsize: 16296
Current children cumulated CPU time (s) 119.69
Current children cumulated vsize (Kb) 18420

[startup+130.014 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4033 0 0 0 12945 23 0 0 25 0 1 0 1851932782 17231872 3968 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4207 3968 145 145 0 4062 0
[pid=11676] vsize: 16828
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 18952

[startup+140.015 s]
Raw data (loadavg): 0.98 0.95 0.88 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4164 0 0 0 13943 24 0 0 25 0 1 0 1851932782 17895424 4099 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4369 4099 145 145 0 4224 0
[pid=11676] vsize: 17476
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 19600

[startup+150.015 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4354 0 0 0 14940 26 0 0 25 0 1 0 1851932782 18657280 4289 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4555 4289 145 145 0 4410 0
[pid=11676] vsize: 18220
Current children cumulated CPU time (s) 149.66
Current children cumulated vsize (Kb) 20344

[startup+160.016 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4477 0 0 0 15938 27 0 0 25 0 1 0 1851932782 19177472 4412 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4682 4412 145 145 0 4537 0
[pid=11676] vsize: 18728
Current children cumulated CPU time (s) 159.65
Current children cumulated vsize (Kb) 20852

[startup+170.017 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4594 0 0 0 16936 27 0 0 25 0 1 0 1851932782 19648512 4529 4294967295 134512640 135094434 3221224432 3221223056 134562110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4797 4529 145 145 0 4652 0
[pid=11676] vsize: 19188
Current children cumulated CPU time (s) 169.63
Current children cumulated vsize (Kb) 21312

[startup+180.017 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4751 0 0 0 17934 28 0 0 25 0 1 0 1851932782 20275200 4686 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 4950 4686 145 145 0 4805 0
[pid=11676] vsize: 19800
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 21924

[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4912 0 0 0 18930 29 0 0 25 0 1 0 1851932782 20926464 4847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5109 4847 145 145 0 4964 0
[pid=11676] vsize: 20436
Current children cumulated CPU time (s) 189.59
Current children cumulated vsize (Kb) 22560

[startup+200.02 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5083 0 0 0 19927 31 0 0 25 0 1 0 1851932782 21630976 5018 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5281 5018 145 145 0 5136 0
[pid=11676] vsize: 21124
Current children cumulated CPU time (s) 199.58
Current children cumulated vsize (Kb) 23248

[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 20926 31 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 209.57
Current children cumulated vsize (Kb) 23632

[startup+220.021 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 21926 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 219.58
Current children cumulated vsize (Kb) 23632

[startup+230.022 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 22926 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 229.58
Current children cumulated vsize (Kb) 23632

[startup+240.023 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 23926 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223056 134557614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 239.58
Current children cumulated vsize (Kb) 23632

[startup+250.023 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 24927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 249.59
Current children cumulated vsize (Kb) 23632

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 25927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 259.59
Current children cumulated vsize (Kb) 23632

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 26927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 269.59
Current children cumulated vsize (Kb) 23632

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 27927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 279.59
Current children cumulated vsize (Kb) 23632

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 28927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 289.59
Current children cumulated vsize (Kb) 23632

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 29928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 299.6
Current children cumulated vsize (Kb) 23632

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 30928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 309.6
Current children cumulated vsize (Kb) 23632

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 31928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 319.6
Current children cumulated vsize (Kb) 23632

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 32928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 329.6
Current children cumulated vsize (Kb) 23632

[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 33928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 339.6
Current children cumulated vsize (Kb) 23632

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 34929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 349.61
Current children cumulated vsize (Kb) 23632

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 35929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 359.61
Current children cumulated vsize (Kb) 23632

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 36929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 369.61
Current children cumulated vsize (Kb) 23632

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 37929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 379.61
Current children cumulated vsize (Kb) 23632

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 38930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 389.62
Current children cumulated vsize (Kb) 23632

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 39930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 399.62
Current children cumulated vsize (Kb) 23632

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 40930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 409.62
Current children cumulated vsize (Kb) 23632

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 41930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0
[pid=11676] vsize: 21508
Current children cumulated CPU time (s) 419.62
Current children cumulated vsize (Kb) 23632

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5217 0 0 0 42930 33 0 0 25 0 1 0 1851932782 22175744 5152 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5414 5152 145 145 0 5269 0
[pid=11676] vsize: 21656
Current children cumulated CPU time (s) 429.63
Current children cumulated vsize (Kb) 23780

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5366 0 0 0 43928 34 0 0 25 0 1 0 1851932782 22806528 5301 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5568 5301 145 145 0 5423 0
[pid=11676] vsize: 22272
Current children cumulated CPU time (s) 439.62
Current children cumulated vsize (Kb) 24396

[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5512 0 0 0 44925 35 0 0 25 0 1 0 1851932782 23412736 5447 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 5716 5447 145 145 0 5571 0
[pid=11676] vsize: 22864
Current children cumulated CPU time (s) 449.6
Current children cumulated vsize (Kb) 24988

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5694 0 0 0 45921 37 0 0 25 0 1 0 1851932782 24150016 5629 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11676/statm): 5896 5629 145 145 0 5751 0
[pid=11676] vsize: 23584
Current children cumulated CPU time (s) 459.58
Current children cumulated vsize (Kb) 25708

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5880 0 0 0 46917 39 0 0 25 0 1 0 1851932782 24903680 5815 4294967295 134512640 135094434 3221224432 3221222912 134780543 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6080 5815 145 145 0 5935 0
[pid=11676] vsize: 24320
Current children cumulated CPU time (s) 469.56
Current children cumulated vsize (Kb) 26444

[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5934 0 0 0 47916 39 0 0 25 0 1 0 1851932782 25120768 5869 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6133 5869 145 145 0 5988 0
[pid=11676] vsize: 24532
Current children cumulated CPU time (s) 479.55
Current children cumulated vsize (Kb) 26656

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5934 0 0 0 48916 39 0 0 25 0 1 0 1851932782 25120768 5869 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6133 5869 145 145 0 5988 0
[pid=11676] vsize: 24532
Current children cumulated CPU time (s) 489.55
Current children cumulated vsize (Kb) 26656

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 49916 39 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 499.55
Current children cumulated vsize (Kb) 26716

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 50915 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 509.55
Current children cumulated vsize (Kb) 26716

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 51915 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 519.55
Current children cumulated vsize (Kb) 26716

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 52915 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 529.55
Current children cumulated vsize (Kb) 26716

[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 53916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 539.56
Current children cumulated vsize (Kb) 26716

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 54916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 549.56
Current children cumulated vsize (Kb) 26716

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 55916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 559.56
Current children cumulated vsize (Kb) 26716

[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 56916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 569.56
Current children cumulated vsize (Kb) 26716

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 57917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 579.57
Current children cumulated vsize (Kb) 26716

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 58917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 589.57
Current children cumulated vsize (Kb) 26716

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 59917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 599.57
Current children cumulated vsize (Kb) 26716

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 60917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 609.57
Current children cumulated vsize (Kb) 26716

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 61917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 619.57
Current children cumulated vsize (Kb) 26716

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 62917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 629.57
Current children cumulated vsize (Kb) 26716

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 63918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 639.58
Current children cumulated vsize (Kb) 26716

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 64918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 649.58
Current children cumulated vsize (Kb) 26716

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 65918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 659.58
Current children cumulated vsize (Kb) 26716

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 66918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 669.58
Current children cumulated vsize (Kb) 26716

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 67918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 679.58
Current children cumulated vsize (Kb) 26716

[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 68919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 689.59
Current children cumulated vsize (Kb) 26716

[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 69919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 699.59
Current children cumulated vsize (Kb) 26716

[startup+710.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 70919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 709.59
Current children cumulated vsize (Kb) 26716

[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 71919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 719.59
Current children cumulated vsize (Kb) 26716

[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 72920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 729.6
Current children cumulated vsize (Kb) 26716

[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 73920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 739.6
Current children cumulated vsize (Kb) 26716

[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 74920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 749.6
Current children cumulated vsize (Kb) 26716

[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 75920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 759.6
Current children cumulated vsize (Kb) 26716

[startup+770.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 76921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 769.61
Current children cumulated vsize (Kb) 26716

[startup+780.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 77921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 779.61
Current children cumulated vsize (Kb) 26716

[startup+790.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 78921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 789.61
Current children cumulated vsize (Kb) 26716

[startup+800.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 79921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 799.61
Current children cumulated vsize (Kb) 26716

[startup+810.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 80922 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 809.62
Current children cumulated vsize (Kb) 26716

[startup+820.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 81922 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223040 134539502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 819.62
Current children cumulated vsize (Kb) 26716

[startup+830.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 82922 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 829.62
Current children cumulated vsize (Kb) 26716

[startup+840.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 83922 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 839.63
Current children cumulated vsize (Kb) 26716

[startup+850.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 84923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 849.64
Current children cumulated vsize (Kb) 26716

[startup+860.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 85923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 859.64
Current children cumulated vsize (Kb) 26716

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 86923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 869.64
Current children cumulated vsize (Kb) 26716

[startup+880.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 87923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 879.64
Current children cumulated vsize (Kb) 26716

[startup+890.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 88923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 889.64
Current children cumulated vsize (Kb) 26716

[startup+900.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 89924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 899.65
Current children cumulated vsize (Kb) 26716

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 90924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 909.65
Current children cumulated vsize (Kb) 26716

[startup+920.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 91924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 919.65
Current children cumulated vsize (Kb) 26716

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 92924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 929.65
Current children cumulated vsize (Kb) 26716

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 93925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 939.66
Current children cumulated vsize (Kb) 26716

[startup+950.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 94925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 949.66
Current children cumulated vsize (Kb) 26716

[startup+960.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 95925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 959.66
Current children cumulated vsize (Kb) 26716

[startup+970.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 96925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 969.66
Current children cumulated vsize (Kb) 26716

[startup+980.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 97926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 979.67
Current children cumulated vsize (Kb) 26716

[startup+990.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 98926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 989.67
Current children cumulated vsize (Kb) 26716

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 99926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 999.67
Current children cumulated vsize (Kb) 26716

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 100926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1009.67
Current children cumulated vsize (Kb) 26716

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 101927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1019.68
Current children cumulated vsize (Kb) 26716

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 102927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1029.68
Current children cumulated vsize (Kb) 26716

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 103927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1039.68
Current children cumulated vsize (Kb) 26716

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 104927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1049.68
Current children cumulated vsize (Kb) 26716

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 105928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1059.69
Current children cumulated vsize (Kb) 26716

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 106928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1069.69
Current children cumulated vsize (Kb) 26716

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 107928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1079.69
Current children cumulated vsize (Kb) 26716

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 108928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1089.69
Current children cumulated vsize (Kb) 26716

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 109928 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1099.69
Current children cumulated vsize (Kb) 26716

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 110929 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1109.7
Current children cumulated vsize (Kb) 26716

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 111929 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1119.7
Current children cumulated vsize (Kb) 26716

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 112929 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1129.7
Current children cumulated vsize (Kb) 26716

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 113930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1139.71
Current children cumulated vsize (Kb) 26716

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 114930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1149.71
Current children cumulated vsize (Kb) 26716

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 115930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1159.71
Current children cumulated vsize (Kb) 26716

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 116930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1169.71
Current children cumulated vsize (Kb) 26716

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 117931 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1179.72
Current children cumulated vsize (Kb) 26716

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 118931 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1189.72
Current children cumulated vsize (Kb) 26716

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 119931 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1199.72
Current children cumulated vsize (Kb) 26716

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 120932 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1209.73
Current children cumulated vsize (Kb) 26716



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 11676
Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11672/statm): 531 226 485 147 0 384 0
[pid=11672] vsize: 2124
Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 120932 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223120 134554682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0
[pid=11676] vsize: 24592
Current children cumulated CPU time (s) 1209.73
Current children cumulated vsize (Kb) 26716

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.75
CPU user time (s): 1209.32
CPU system time (s): 0.424935
CPU usage (%): 99.9697
Max. virtual memory (cumulated for all children) (Kb): 26716

Verifier Data

ERROR: no interpretation found !