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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc07.opb
MD5SUM9cc94d1db4d494288ef67a8d5ad5d77e
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1408128
Optimality of the best value was proved NO
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 11486079
Number of bits of the biggest sum of numbers24
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables280
Total number of constraints471
Number of constraints which are clauses127
Number of constraints which are cardinality constraints (but not clauses)272
Number of constraints which are nor clauses,nor cardinality constraints72
Minimum length of a constraint1
Maximum length of a constraint253

Trace number 6095

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        910900 kB
Buffers:         33288 kB
Cached:          60060 kB
SwapCached:        492 kB
Active:          44256 kB
Inactive:        51688 kB
HighTotal:      131008 kB
HighFree:        68712 kB
LowTotal:       903652 kB
LowFree:        842188 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            21996 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:34:55 (client local time) WITH STATUS 10 IN 1209.69 SECONDS
stats: 3251 7 1209.69 10

Solver Data

c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25782    84321 |    8594       0        0     nan |  0.000 % |
c |       104 |   25782    84321 |    9453     104     6117    58.8 |  2.677 % |
c ==============================================================================
c Found solution: 1611648
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       123 |   25795    84354 |    8598     123     6748    54.9 |  2.677 % |
c ==============================================================================
c Found solution: 1508608
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       125 |   25808    84385 |    8602     125     6762    54.1 |  2.677 % |
c |       226 |   25808    84385 |    9462     226    17913    79.3 |  2.700 % |
c |       376 |   25808    84385 |   10408     376    23984    63.8 |  2.700 % |
c |       602 |   25808    84385 |   11449     602    49428    82.1 |  2.700 % |
c |       939 |   25787    84310 |   12594     937    66619    71.1 |  2.715 % |
c |      1446 |   25787    84310 |   13853    1444   118779    82.3 |  2.715 % |
c |      2206 |   25732    84151 |   15238    2192   175466    80.0 |  2.845 % |
c ==============================================================================
c Found solution: 1476608
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2813 |   25675    84026 |    8558    2786   202362    72.6 |  2.845 % |
c |      2914 |   25675    84026 |    9413    2887   216333    74.9 |  3.131 % |
c |      3064 |   25675    84026 |   10355    3037   232590    76.6 |  3.131 % |
c |      3290 |   25651    83953 |   11390    3260   236544    72.6 |  3.189 % |
c |      3628 |   25623    83890 |   12529    3595   279647    77.8 |  3.290 % |
c |      4136 |   25623    83890 |   13782    4103   311959    76.0 |  3.290 % |
c |      4896 |   25623    83890 |   15161    4863   391121    80.4 |  3.290 % |
c |      6037 |   25623    83890 |   16677    6004   489351    81.5 |  3.290 % |
c |      7749 |   25574    83745 |   18344    7708   650986    84.5 |  3.391 % |
c ==============================================================================
c Found solution: 1470848
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8367 |   25534    83606 |    8511    8319   709343    85.3 |  3.391 % |
c |      8467 |   25513    83531 |    9362    8416   712125    84.6 |  3.502 % |
c |      8618 |   25513    83531 |   10298    8567   720411    84.1 |  3.502 % |
c |      8846 |   25513    83531 |   11328    8795   739938    84.1 |  3.502 % |
c |      9183 |   25513    83531 |   12460    9132   783046    85.7 |  3.502 % |
c |      9690 |   25400    83151 |   13707    9625   842609    87.5 |  3.675 % |
c ==============================================================================
c Found solution: 1465728
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10436 |   25402    83160 |    8467   10369   916955    88.4 |  3.675 % |
c |     10536 |   25402    83160 |    9313    5285   386079    73.1 |  3.729 % |
c |     10686 |   25361    83069 |   10245    5426   393377    72.5 |  3.902 % |
c |     10911 |   25361    83069 |   11269    5651   409599    72.5 |  3.902 % |
c |     11249 |   25361    83069 |   12396    5989   450093    75.2 |  3.902 % |
c |     11755 |   25328    82952 |   13636    6486   476029    73.4 |  3.930 % |
c |     12517 |   25328    82952 |   14999    7248   532015    73.4 |  3.930 % |
c |     13656 |   25328    82952 |   16499    8387   624983    74.5 |  3.930 % |
c |     15365 |   25328    82952 |   18149   10096   891959    88.3 |  3.930 % |
c |     17927 |   25321    82937 |   19964   12657  1137466    89.9 |  3.959 % |
c ==============================================================================
c Found solution: 1459328
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18442 |   25337    82974 |    8445   13172  1195556    90.8 |  3.959 % |
c |     18544 |   25337    82974 |    9289    6688   584306    87.4 |  3.969 % |
c |     18698 |   25337    82974 |   10218    6842   607049    88.7 |  3.969 % |
c |     18923 |   25232    82626 |   11240    7056   627855    89.0 |  4.170 % |
c |     19263 |   25187    82494 |   12364    7389   652013    88.2 |  4.285 % |
c |     19770 |   25170    82456 |   13600    7895   721465    91.4 |  4.357 % |
c |     20529 |   25170    82456 |   14960    8654   806216    93.2 |  4.357 % |
c |     21671 |   25127    82305 |   16456    9793   890194    90.9 |  4.443 % |
c ==============================================================================
c Found solution: 1440128
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22665 |   25125    82307 |    8375   10784  1014528    94.1 |  4.443 % |
c |     22765 |   25125    82307 |    9212    5492   368580    67.1 |  4.497 % |
c |     22916 |   25125    82307 |   10133    5643   371798    65.9 |  4.497 % |
c |     23143 |   25114    82283 |   11147    5869   407568    69.4 |  4.540 % |
c |     23480 |   25114    82283 |   12261    6206   427989    69.0 |  4.540 % |
c ==============================================================================
c Found solution: 1429248
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23792 |   25125    82313 |    8375    6518   470528    72.2 |  4.540 % |
c |     23896 |   25125    82313 |    9212    6622   482346    72.8 |  4.550 % |
c |     24046 |   25044    82051 |   10133    6765   493619    73.0 |  4.722 % |
c |     24274 |   24863    81448 |   11147    6973   507046    72.7 |  5.038 % |
c |     24613 |   24844    81404 |   12261    7307   529616    72.5 |  5.110 % |
c |     25119 |   24844    81404 |   13488    7813   610135    78.1 |  5.110 % |
c |     25880 |   24844    81404 |   14836    8574   646861    75.4 |  5.110 % |
c |     27022 |   24824    81360 |   16320    9711   732271    75.4 |  5.196 % |
c |     28734 |   24824    81360 |   17952   11423   891715    78.1 |  5.196 % |
c |     31297 |   24824    81360 |   19747   13986  1292109    92.4 |  5.196 % |
c |     35141 |   24802    81312 |   21722   17826  1712988    96.1 |  5.282 % |
c |     40907 |   24784    81273 |   23894   23589  2293176    97.2 |  5.354 % |
c |     49556 |   24773    81249 |   26284   20011  2092469   104.6 |  5.397 % |
c |     62530 |   24740    81132 |   28912   19252  1361391    70.7 |  5.426 % |
c |     81991 |   24660    80889 |   31804   23203  1916008    82.6 |  5.641 % |
c ==============================================================================
c Found solution: 1419008
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86665 |   24652    80876 |    8217   27873  2312061    82.9 |  5.641 % |
c |     86765 |   24652    80876 |    9038    7069   359139    50.8 |  5.734 % |
c |     86915 |   24589    80694 |    9942    7212   361365    50.1 |  5.906 % |
c |     87140 |   24589    80694 |   10936    7437   379936    51.1 |  5.906 % |
c |     87478 |   24543    80590 |   12030    7770   392965    50.6 |  6.121 % |
c |     87985 |   24543    80590 |   13233    8277   449311    54.3 |  6.121 % |
c |     88744 |   24543    80590 |   14556    9036   528727    58.5 |  6.121 % |
c |     89885 |   24543    80590 |   16012   10177   658551    64.7 |  6.121 % |
c |     91595 |   24543    80590 |   17613   11887   865744    72.8 |  6.121 % |
c |     94157 |   24493    80427 |   19375   14439  1148273    79.5 |  6.221 % |
c |     98002 |   24449    80290 |   21312   18275  1436698    78.6 |  6.322 % |
c |    103768 |   24432    80252 |   23444   12999   898365    69.1 |  6.393 % |
c |    112417 |   24421    80228 |   25788   21646  1813298    83.8 |  6.436 % |
c |    125391 |   24421    80228 |   28367   20828  1681241    80.7 |  6.436 % |
c |    144852 |   24406    80175 |   31204   24623  2133182    86.6 |  6.451 % |
c ==============================================================================
c Found solution: 1415168
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162569 |   24351    80012 |    8117   23650  2252373    95.2 |  6.451 % |
c |    162670 |   24351    80012 |    8928    6014   408136    67.9 |  6.645 % |
c |    162820 |   24351    80012 |    9821    6164   422946    68.6 |  6.645 % |
c |    163045 |   24351    80012 |   10803    6389   443258    69.4 |  6.645 % |
c |    163382 |   24351    80012 |   11884    6726   487694    72.5 |  6.645 % |
c |    163888 |   24351    80012 |   13072    7232   518741    71.7 |  6.645 % |
c |    164651 |   24338    79983 |   14379    7993   606780    75.9 |  6.702 % |
c |    165792 |   24338    79983 |   15817    9134   770652    84.4 |  6.702 % |
c |    167500 |   24338    79983 |   17399   10842   883396    81.5 |  6.702 % |
c |    170062 |   24329    79952 |   19139   13401  1257807    93.9 |  6.716 % |
c |    173906 |   24318    79928 |   21053   17243  1583558    91.8 |  6.759 % |
c |    179672 |   24318    79928 |   23158   11574   882126    76.2 |  6.759 % |
c |    188322 |   24318    79928 |   25474   20224  1960555    96.9 |  6.759 % |
c |    201298 |   24296    79880 |   28022   20015  1816864    90.8 |  6.845 % |
c ==============================================================================
c Found solution: 1408128
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    209149 |   24306    79907 |    8102   27866  2723490    97.7 |  6.845 % |
c |    209250 |   24306    79907 |    8912    7068   466379    66.0 |  6.853 % |
c |    209401 |   24306    79907 |    9803    7219   479276    66.4 |  6.853 % |
c |    209627 |   24306    79907 |   10783    7445   508961    68.4 |  6.853 % |
c |    209967 |   24306    79907 |   11862    7785   532660    68.4 |  6.853 % |
c |    210473 |   24306    79907 |   13048    8291   602654    72.7 |  6.853 % |
c |    211232 |   24241    79734 |   14353    9039   675578    74.7 |  7.067 % |
c |    212372 |   24241    79734 |   15788   10179   812871    79.9 |  7.067 % |
c |    214080 |   24230    79710 |   17367   11884   928908    78.2 |  7.110 % |
c |    216643 |   24224    79690 |   19104   14443  1193339    82.6 |  7.124 % |
c |    220487 |   24224    79690 |   21014   18287  1514845    82.8 |  7.124 % |
c |    226254 |   24224    79690 |   23115   13248  1001035    75.6 |  7.124 % |
c |    234904 |   24224    79690 |   25427   21898  1857367    84.8 |  7.124 % |
c |    247878 |   24201    79627 |   27970   21357  1844939    86.4 |  7.210 % |
c |    267340 |   24011    79030 |   30767   25653  2211361    86.2 |  7.639 % |
c |    296534 |   23994    78992 |   33844   22302  2056277    92.2 |  7.711 % |
c |    340323 |   23969    78936 |   37228   27120  2364139    87.2 |  7.811 % |

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/11346/stat): 11346 (minisat+_script) R 11345 11346 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796976270 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/11346/statm): 174 3 169 147 0 27 0
[pid=11346] 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=11347
New process pid=11348
New process pid=11349
execve syscall for /bin/sed executable
One traced child (pid=11348) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=11349) exited with status: 0
One traced child (pid=11347) exited with status: 0
New process pid=11350
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-misc07.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 1562 0 0 0 978 8 0 0 25 0 1 0 1796976275 6447104 1463 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11350/statm): 1574 1463 145 145 0 1429 0
[pid=11350] vsize: 6296
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 8420

[startup+20.005 s]
Raw data (loadavg): 0.94 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 2119 0 0 0 1970 11 0 0 25 0 1 0 1796976275 8744960 2020 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11350/statm): 2135 2020 145 145 0 1990 0
[pid=11350] vsize: 8540
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 10664

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 2270 0 0 0 2966 13 0 0 25 0 1 0 1796976275 9359360 2171 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11350/statm): 2285 2171 145 145 0 2140 0
[pid=11350] vsize: 9140
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 11264

[startup+40.0066 s]
Raw data (loadavg): 0.96 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 2472 0 0 0 3963 15 0 0 25 0 1 0 1796976275 10178560 2373 4294967295 134512640 135094434 3221224432 3221223104 134556297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11350/statm): 2485 2373 145 145 0 2340 0
[pid=11350] vsize: 9940
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 12064

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 2472 0 0 0 4962 16 0 0 25 0 1 0 1796976275 10178560 2373 4294967295 134512640 135094434 3221224432 3221223024 134557509 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11350/statm): 2485 2373 145 145 0 2340 0
[pid=11350] vsize: 9940
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 12064

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 2666 0 0 0 5958 17 0 0 25 0 1 0 1796976275 10969088 2567 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 2678 2567 145 145 0 2533 0
[pid=11350] vsize: 10712
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 12836

[startup+70.0102 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 3189 0 0 0 6950 22 0 0 25 0 1 0 1796976275 13156352 3090 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11350/statm): 3212 3090 145 145 0 3067 0
[pid=11350] vsize: 12848
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 14972

[startup+80.012 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 3649 0 0 0 7940 26 0 0 25 0 1 0 1796976275 15024128 3550 4294967295 134512640 135094434 3221224432 3221222976 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 3668 3550 145 145 0 3523 0
[pid=11350] vsize: 14672
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 16796

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 3805 0 0 0 8937 28 0 0 25 0 1 0 1796976275 15659008 3706 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 3823 3706 145 145 0 3678 0
[pid=11350] vsize: 15292
Current children cumulated CPU time (s) 89.65
Current children cumulated vsize (Kb) 17416

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 3805 0 0 0 9938 28 0 0 25 0 1 0 1796976275 15659008 3706 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 3823 3706 145 145 0 3678 0
[pid=11350] vsize: 15292
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 17416

[startup+110.013 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 3917 0 0 0 10935 28 0 0 25 0 1 0 1796976275 16125952 3818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 3937 3818 145 145 0 3792 0
[pid=11350] vsize: 15748
Current children cumulated CPU time (s) 109.63
Current children cumulated vsize (Kb) 17872

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4161 0 0 0 11931 31 0 0 25 0 1 0 1796976275 17117184 4062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4062 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 18840

[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4161 0 0 0 12931 31 0 0 25 0 1 0 1796976275 17117184 4062 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4062 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 129.62
Current children cumulated vsize (Kb) 18840

[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4161 0 0 0 13931 31 0 0 25 0 1 0 1796976275 17117184 4062 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4062 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 18840

[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4161 0 0 0 14932 31 0 0 25 0 1 0 1796976275 17117184 4062 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4062 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 149.63
Current children cumulated vsize (Kb) 18840

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 15932 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 159.63
Current children cumulated vsize (Kb) 18840

[startup+170.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 16932 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 169.63
Current children cumulated vsize (Kb) 18840

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 17932 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 179.63
Current children cumulated vsize (Kb) 18840

[startup+190.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 18933 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 189.64
Current children cumulated vsize (Kb) 18840

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 19933 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 199.64
Current children cumulated vsize (Kb) 18840

[startup+210.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 20933 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 209.64
Current children cumulated vsize (Kb) 18840

[startup+220.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 21933 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221222896 134781514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 219.64
Current children cumulated vsize (Kb) 18840

[startup+230.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 22933 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 229.64
Current children cumulated vsize (Kb) 18840

[startup+240.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 23933 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 239.64
Current children cumulated vsize (Kb) 18840

[startup+250.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 24934 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 249.65
Current children cumulated vsize (Kb) 18840

[startup+260.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 25934 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 259.65
Current children cumulated vsize (Kb) 18840

[startup+270.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4164 0 0 0 26934 31 0 0 25 0 1 0 1796976275 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4179 4065 145 145 0 4034 0
[pid=11350] vsize: 16716
Current children cumulated CPU time (s) 269.65
Current children cumulated vsize (Kb) 18840

[startup+280.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4198 0 0 0 27934 31 0 0 25 0 1 0 1796976275 17256448 4099 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4213 4099 145 145 0 4068 0
[pid=11350] vsize: 16852
Current children cumulated CPU time (s) 279.65
Current children cumulated vsize (Kb) 18976

[startup+290.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4200 0 0 0 28934 31 0 0 25 0 1 0 1796976275 17264640 4101 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4215 4101 145 145 0 4070 0
[pid=11350] vsize: 16860
Current children cumulated CPU time (s) 289.65
Current children cumulated vsize (Kb) 18984

[startup+300.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4210 0 0 0 29934 31 0 0 25 0 1 0 1796976275 17305600 4111 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4225 4111 145 145 0 4080 0
[pid=11350] vsize: 16900
Current children cumulated CPU time (s) 299.65
Current children cumulated vsize (Kb) 19024

[startup+310.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) T 11346 11346 8263 0 -1 0 4629 0 0 0 30927 35 0 0 25 0 1 0 1796976275 19021824 4530 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4644 4530 145 145 0 4499 0
[pid=11350] vsize: 18576
Current children cumulated CPU time (s) 309.62
Current children cumulated vsize (Kb) 20700

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4669 0 0 0 31927 35 0 0 25 0 1 0 1796976275 19185664 4570 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4684 4570 145 145 0 4539 0
[pid=11350] vsize: 18736
Current children cumulated CPU time (s) 319.62
Current children cumulated vsize (Kb) 20860

[startup+330.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4669 0 0 0 32927 35 0 0 25 0 1 0 1796976275 19185664 4570 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4684 4570 145 145 0 4539 0
[pid=11350] vsize: 18736
Current children cumulated CPU time (s) 329.62
Current children cumulated vsize (Kb) 20860

[startup+340.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4683 0 0 0 33927 35 0 0 25 0 1 0 1796976275 19247104 4584 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4699 4584 145 145 0 4554 0
[pid=11350] vsize: 18796
Current children cumulated CPU time (s) 339.62
Current children cumulated vsize (Kb) 20920

[startup+350.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4695 0 0 0 34927 35 0 0 25 0 1 0 1796976275 19296256 4596 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4711 4596 145 145 0 4566 0
[pid=11350] vsize: 18844
Current children cumulated CPU time (s) 349.62
Current children cumulated vsize (Kb) 20968

[startup+360.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 4714 0 0 0 35927 35 0 0 25 0 1 0 1796976275 19378176 4615 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 4731 4615 145 145 0 4586 0
[pid=11350] vsize: 18924
Current children cumulated CPU time (s) 359.62
Current children cumulated vsize (Kb) 21048

[startup+370.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 36921 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 369.59
Current children cumulated vsize (Kb) 23004

[startup+380.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 37921 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 379.59
Current children cumulated vsize (Kb) 23004

[startup+390.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 38921 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 389.59
Current children cumulated vsize (Kb) 23004

[startup+400.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 39921 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 399.59
Current children cumulated vsize (Kb) 23004

[startup+410.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 40921 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 409.59
Current children cumulated vsize (Kb) 23004

[startup+420.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 41922 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 419.6
Current children cumulated vsize (Kb) 23004

[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 42922 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 429.6
Current children cumulated vsize (Kb) 23004

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 43922 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 439.6
Current children cumulated vsize (Kb) 23004

[startup+450.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 44922 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 449.6
Current children cumulated vsize (Kb) 23004

[startup+460.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 45923 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 459.61
Current children cumulated vsize (Kb) 23004

[startup+470.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 46923 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 469.61
Current children cumulated vsize (Kb) 23004

[startup+480.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 47923 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 479.61
Current children cumulated vsize (Kb) 23004

[startup+490.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 48923 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 489.61
Current children cumulated vsize (Kb) 23004

[startup+500.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 49923 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 499.61
Current children cumulated vsize (Kb) 23004

[startup+510.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 50924 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 509.62
Current children cumulated vsize (Kb) 23004

[startup+520.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 51924 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 519.62
Current children cumulated vsize (Kb) 23004

[startup+530.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 52924 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 529.62
Current children cumulated vsize (Kb) 23004

[startup+540.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 53924 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 539.62
Current children cumulated vsize (Kb) 23004

[startup+550.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 54924 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 549.62
Current children cumulated vsize (Kb) 23004

[startup+560.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 55924 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 559.62
Current children cumulated vsize (Kb) 23004

[startup+570.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 56925 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 569.63
Current children cumulated vsize (Kb) 23004

[startup+580.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 57925 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 579.63
Current children cumulated vsize (Kb) 23004

[startup+590.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 58925 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 589.63
Current children cumulated vsize (Kb) 23004

[startup+600.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5175 0 0 0 59925 38 0 0 25 0 1 0 1796976275 21381120 5076 4294967295 134512640 135094434 3221224432 3221222896 134780984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5076 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 599.63
Current children cumulated vsize (Kb) 23004

[startup+610.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 60926 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 609.64
Current children cumulated vsize (Kb) 23004

[startup+620.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 61926 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 619.64
Current children cumulated vsize (Kb) 23004

[startup+630.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 62926 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 629.64
Current children cumulated vsize (Kb) 23004

[startup+640.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 63926 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 639.64
Current children cumulated vsize (Kb) 23004

[startup+650.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 64927 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 649.65
Current children cumulated vsize (Kb) 23004

[startup+660.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 65927 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 659.65
Current children cumulated vsize (Kb) 23004

[startup+670.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 66927 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223104 134556507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 669.65
Current children cumulated vsize (Kb) 23004

[startup+680.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 67927 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 679.65
Current children cumulated vsize (Kb) 23004

[startup+690.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 68927 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 689.65
Current children cumulated vsize (Kb) 23004

[startup+700.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5176 0 0 0 69928 38 0 0 25 0 1 0 1796976275 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5220 5077 145 145 0 5075 0
[pid=11350] vsize: 20880
Current children cumulated CPU time (s) 699.66
Current children cumulated vsize (Kb) 23004

[startup+710.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5201 0 0 0 70927 38 0 0 25 0 1 0 1796976275 21483520 5102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5245 5102 145 145 0 5100 0
[pid=11350] vsize: 20980
Current children cumulated CPU time (s) 709.65
Current children cumulated vsize (Kb) 23104

[startup+720.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5237 0 0 0 71927 39 0 0 25 0 1 0 1796976275 21651456 5138 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5286 5138 145 145 0 5141 0
[pid=11350] vsize: 21144
Current children cumulated CPU time (s) 719.66
Current children cumulated vsize (Kb) 23268

[startup+730.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5242 0 0 0 72927 39 0 0 25 0 1 0 1796976275 21684224 5143 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5294 5143 145 145 0 5149 0
[pid=11350] vsize: 21176
Current children cumulated CPU time (s) 729.66
Current children cumulated vsize (Kb) 23300

[startup+740.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5248 0 0 0 73927 39 0 0 25 0 1 0 1796976275 21716992 5149 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5302 5149 145 145 0 5157 0
[pid=11350] vsize: 21208
Current children cumulated CPU time (s) 739.66
Current children cumulated vsize (Kb) 23332

[startup+750.063 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5269 0 0 0 74927 39 0 0 25 0 1 0 1796976275 21815296 5170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5326 5170 145 145 0 5181 0
[pid=11350] vsize: 21304
Current children cumulated CPU time (s) 749.66
Current children cumulated vsize (Kb) 23428

[startup+760.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5301 0 0 0 75927 39 0 0 25 0 1 0 1796976275 21979136 5202 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5366 5202 145 145 0 5221 0
[pid=11350] vsize: 21464
Current children cumulated CPU time (s) 759.66
Current children cumulated vsize (Kb) 23588

[startup+770.065 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5319 0 0 0 76927 39 0 0 25 0 1 0 1796976275 22077440 5220 4294967295 134512640 135094434 3221224432 3221223024 134557363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5390 5220 145 145 0 5245 0
[pid=11350] vsize: 21560
Current children cumulated CPU time (s) 769.66
Current children cumulated vsize (Kb) 23684

[startup+780.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5341 0 0 0 77927 39 0 0 25 0 1 0 1796976275 22208512 5242 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5422 5242 145 145 0 5277 0
[pid=11350] vsize: 21688
Current children cumulated CPU time (s) 779.66
Current children cumulated vsize (Kb) 23812

[startup+790.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5351 0 0 0 78927 39 0 0 25 0 1 0 1796976275 22306816 5252 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5446 5252 145 145 0 5301 0
[pid=11350] vsize: 21784
Current children cumulated CPU time (s) 789.66
Current children cumulated vsize (Kb) 23908

[startup+800.067 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5406 0 0 0 79928 39 0 0 25 0 1 0 1796976275 22536192 5307 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5502 5307 145 145 0 5357 0
[pid=11350] vsize: 22008
Current children cumulated CPU time (s) 799.67
Current children cumulated vsize (Kb) 24132

[startup+810.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5625 0 0 0 80925 40 0 0 25 0 1 0 1796976275 23486464 5526 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5734 5526 145 145 0 5589 0
[pid=11350] vsize: 22936
Current children cumulated CPU time (s) 809.65
Current children cumulated vsize (Kb) 25060

[startup+820.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5760 0 0 0 81923 41 0 0 25 0 1 0 1796976275 24068096 5661 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5876 5661 145 145 0 5731 0
[pid=11350] vsize: 23504
Current children cumulated CPU time (s) 819.64
Current children cumulated vsize (Kb) 25628

[startup+830.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5760 0 0 0 82924 41 0 0 25 0 1 0 1796976275 24068096 5661 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5876 5661 145 145 0 5731 0
[pid=11350] vsize: 23504
Current children cumulated CPU time (s) 829.65
Current children cumulated vsize (Kb) 25628

[startup+840.071 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5773 0 0 0 83924 41 0 0 25 0 1 0 1796976275 24133632 5674 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5892 5674 145 145 0 5747 0
[pid=11350] vsize: 23568
Current children cumulated CPU time (s) 839.65
Current children cumulated vsize (Kb) 25692

[startup+850.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5793 0 0 0 84924 41 0 0 25 0 1 0 1796976275 24231936 5694 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5916 5694 145 145 0 5771 0
[pid=11350] vsize: 23664
Current children cumulated CPU time (s) 849.65
Current children cumulated vsize (Kb) 25788

[startup+860.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5824 0 0 0 85923 42 0 0 25 0 1 0 1796976275 24395776 5725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5956 5725 145 145 0 5811 0
[pid=11350] vsize: 23824
Current children cumulated CPU time (s) 859.65
Current children cumulated vsize (Kb) 25948

[startup+870.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5842 0 0 0 86923 42 0 0 25 0 1 0 1796976275 24461312 5743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5972 5743 145 145 0 5827 0
[pid=11350] vsize: 23888
Current children cumulated CPU time (s) 869.65
Current children cumulated vsize (Kb) 26012

[startup+880.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5856 0 0 0 87923 42 0 0 25 0 1 0 1796976275 24526848 5757 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 5988 5757 145 145 0 5843 0
[pid=11350] vsize: 23952
Current children cumulated CPU time (s) 879.65
Current children cumulated vsize (Kb) 26076

[startup+890.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 5906 0 0 0 88923 42 0 0 25 0 1 0 1796976275 24768512 5807 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6047 5807 145 145 0 5902 0
[pid=11350] vsize: 24188
Current children cumulated CPU time (s) 889.65
Current children cumulated vsize (Kb) 26312

[startup+900.076 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6240 0 0 0 89916 44 0 0 25 0 1 0 1796976275 26161152 6141 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6387 6141 145 145 0 6242 0
[pid=11350] vsize: 25548
Current children cumulated CPU time (s) 899.6
Current children cumulated vsize (Kb) 27672

[startup+910.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6325 0 0 0 90915 45 0 0 25 0 1 0 1796976275 26505216 6226 4294967295 134512640 135094434 3221224432 3221223104 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6226 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 909.6
Current children cumulated vsize (Kb) 28008

[startup+920.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6325 0 0 0 91915 45 0 0 25 0 1 0 1796976275 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6226 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 919.6
Current children cumulated vsize (Kb) 28008

[startup+930.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6325 0 0 0 92915 45 0 0 25 0 1 0 1796976275 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6226 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 929.6
Current children cumulated vsize (Kb) 28008

[startup+940.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6325 0 0 0 93916 45 0 0 25 0 1 0 1796976275 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6226 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 939.61
Current children cumulated vsize (Kb) 28008

[startup+950.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6325 0 0 0 94916 45 0 0 25 0 1 0 1796976275 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6226 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 949.61
Current children cumulated vsize (Kb) 28008

[startup+960.081 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6326 0 0 0 95916 45 0 0 25 0 1 0 1796976275 26505216 6227 4294967295 134512640 135094434 3221224432 3221223024 134557269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6227 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 959.61
Current children cumulated vsize (Kb) 28008

[startup+970.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6326 0 0 0 96916 45 0 0 25 0 1 0 1796976275 26505216 6227 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6227 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 969.61
Current children cumulated vsize (Kb) 28008

[startup+980.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6326 0 0 0 97917 45 0 0 25 0 1 0 1796976275 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6227 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 979.62
Current children cumulated vsize (Kb) 28008

[startup+990.083 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6326 0 0 0 98916 45 0 0 25 0 1 0 1796976275 26505216 6227 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6227 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 989.61
Current children cumulated vsize (Kb) 28008

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6326 0 0 0 99916 45 0 0 25 0 1 0 1796976275 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6471 6227 145 145 0 6326 0
[pid=11350] vsize: 25884
Current children cumulated CPU time (s) 999.61
Current children cumulated vsize (Kb) 28008

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6332 0 0 0 100917 45 0 0 25 0 1 0 1796976275 26537984 6233 4294967295 134512640 135094434 3221224432 3221223104 134555252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6479 6233 145 145 0 6334 0
[pid=11350] vsize: 25916
Current children cumulated CPU time (s) 1009.62
Current children cumulated vsize (Kb) 28040

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6338 0 0 0 101917 45 0 0 25 0 1 0 1796976275 26570752 6239 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6487 6239 145 145 0 6342 0
[pid=11350] vsize: 25948
Current children cumulated CPU time (s) 1019.62
Current children cumulated vsize (Kb) 28072

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6344 0 0 0 102917 45 0 0 25 0 1 0 1796976275 26603520 6245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6495 6245 145 145 0 6350 0
[pid=11350] vsize: 25980
Current children cumulated CPU time (s) 1029.62
Current children cumulated vsize (Kb) 28104

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6345 0 0 0 103917 45 0 0 25 0 1 0 1796976275 26603520 6246 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6495 6246 145 145 0 6350 0
[pid=11350] vsize: 25980
Current children cumulated CPU time (s) 1039.62
Current children cumulated vsize (Kb) 28104

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6345 0 0 0 104917 46 0 0 25 0 1 0 1796976275 26603520 6246 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6495 6246 145 145 0 6350 0
[pid=11350] vsize: 25980
Current children cumulated CPU time (s) 1049.63
Current children cumulated vsize (Kb) 28104

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6345 0 0 0 105917 46 0 0 25 0 1 0 1796976275 26603520 6246 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6495 6246 145 145 0 6350 0
[pid=11350] vsize: 25980
Current children cumulated CPU time (s) 1059.63
Current children cumulated vsize (Kb) 28104

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6352 0 0 0 106918 46 0 0 25 0 1 0 1796976275 26636288 6253 4294967295 134512640 135094434 3221224432 3221223056 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6503 6253 145 145 0 6358 0
[pid=11350] vsize: 26012
Current children cumulated CPU time (s) 1069.64
Current children cumulated vsize (Kb) 28136

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6359 0 0 0 107918 46 0 0 25 0 1 0 1796976275 26669056 6260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6511 6260 145 145 0 6366 0
[pid=11350] vsize: 26044
Current children cumulated CPU time (s) 1079.64
Current children cumulated vsize (Kb) 28168

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6359 0 0 0 108918 46 0 0 25 0 1 0 1796976275 26669056 6260 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6511 6260 145 145 0 6366 0
[pid=11350] vsize: 26044
Current children cumulated CPU time (s) 1089.64
Current children cumulated vsize (Kb) 28168

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6382 0 0 0 109918 46 0 0 25 0 1 0 1796976275 26796032 6283 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6542 6283 145 145 0 6397 0
[pid=11350] vsize: 26168
Current children cumulated CPU time (s) 1099.64
Current children cumulated vsize (Kb) 28292

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6390 0 0 0 110918 46 0 0 25 0 1 0 1796976275 26828800 6291 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6550 6291 145 145 0 6405 0
[pid=11350] vsize: 26200
Current children cumulated CPU time (s) 1109.64
Current children cumulated vsize (Kb) 28324

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6393 0 0 0 111918 46 0 0 25 0 1 0 1796976275 26828800 6294 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6550 6294 145 145 0 6405 0
[pid=11350] vsize: 26200
Current children cumulated CPU time (s) 1119.64
Current children cumulated vsize (Kb) 28324

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6393 0 0 0 112919 46 0 0 25 0 1 0 1796976275 26828800 6294 4294967295 134512640 135094434 3221224432 3221223104 134556334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6550 6294 145 145 0 6405 0
[pid=11350] vsize: 26200
Current children cumulated CPU time (s) 1129.65
Current children cumulated vsize (Kb) 28324

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6412 0 0 0 113919 46 0 0 25 0 1 0 1796976275 26927104 6313 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6574 6313 145 145 0 6429 0
[pid=11350] vsize: 26296
Current children cumulated CPU time (s) 1139.65
Current children cumulated vsize (Kb) 28420

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6428 0 0 0 114919 46 0 0 25 0 1 0 1796976275 27025408 6329 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6598 6329 145 145 0 6453 0
[pid=11350] vsize: 26392
Current children cumulated CPU time (s) 1149.65
Current children cumulated vsize (Kb) 28516

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6449 0 0 0 115919 46 0 0 25 0 1 0 1796976275 27123712 6350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6622 6350 145 145 0 6477 0
[pid=11350] vsize: 26488
Current children cumulated CPU time (s) 1159.65
Current children cumulated vsize (Kb) 28612

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6449 0 0 0 116919 46 0 0 25 0 1 0 1796976275 27123712 6350 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6622 6350 145 145 0 6477 0
[pid=11350] vsize: 26488
Current children cumulated CPU time (s) 1169.65
Current children cumulated vsize (Kb) 28612

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6451 0 0 0 117920 46 0 0 25 0 1 0 1796976275 27123712 6352 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6622 6352 145 145 0 6477 0
[pid=11350] vsize: 26488
Current children cumulated CPU time (s) 1179.66
Current children cumulated vsize (Kb) 28612

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6459 0 0 0 118920 46 0 0 25 0 1 0 1796976275 27156480 6360 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6630 6360 145 145 0 6485 0
[pid=11350] vsize: 26520
Current children cumulated CPU time (s) 1189.66
Current children cumulated vsize (Kb) 28644

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6473 0 0 0 119920 46 0 0 25 0 1 0 1796976275 27222016 6374 4294967295 134512640 135094434 3221224432 3221222896 134780899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6646 6374 145 145 0 6501 0
[pid=11350] vsize: 26584
Current children cumulated CPU time (s) 1199.66
Current children cumulated vsize (Kb) 28708

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6490 0 0 0 120920 46 0 0 25 0 1 0 1796976275 27320320 6391 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6670 6391 145 145 0 6525 0
[pid=11350] vsize: 26680
Current children cumulated CPU time (s) 1209.66
Current children cumulated vsize (Kb) 28804



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 11350
Raw data (/proc/11346/stat): 11346 (minisat+_script) S 11345 11346 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796976270 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11346/statm): 531 226 485 147 0 384 0
[pid=11346] vsize: 2124
Raw data (/proc/11350/stat): 11350 (minisat+_64-bit) R 11346 11346 8263 0 -1 0 6490 0 0 0 120920 46 0 0 25 0 1 0 1796976275 27320320 6391 4294967295 134512640 135094434 3221224432 3221223096 134556595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11350/statm): 6670 6391 145 145 0 6525 0
[pid=11350] vsize: 26680
Current children cumulated CPU time (s) 1209.66
Current children cumulated vsize (Kb) 28804

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.69
CPU user time (s): 1209.21
CPU system time (s): 0.480926
CPU usage (%): 99.9642
Max. virtual memory (cumulated for all children) (Kb): 28804

Verifier Data

ERROR: no interpretation found !