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/miplib3/normalized-mps-v2-13-7-misc07.opb
MD5SUM54df16ee65da54d5975ffedee80d2bb9
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.03
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 6216

Launcher Data

LAUNCH ON wulflinc13 THE 2005-09-20 04:29:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3372 boxname=wulflinc13 idbench=1028 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  54df16ee65da54d5975ffedee80d2bb9  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 3372
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        897084 kB
Buffers:         31844 kB
Cached:          78364 kB
SwapCached:        700 kB
Active:          37612 kB
Inactive:        75224 kB
HighTotal:      131008 kB
HighFree:        48776 kB
LowTotal:       903652 kB
LowFree:        848308 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            19100 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:50:03 (client local time) WITH STATUS 10 IN 1209.64 SECONDS
stats: 3372 7 1209.64 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/22283/stat): 22283 (minisat+_script) R 22282 22283 1333 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797458771 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22283/statm): 174 3 169 147 0 27 0
[pid=22283] 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=22284
New process pid=22285
New process pid=22286
execve syscall for /bin/sed executable
One traced child (pid=22285) 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=22286) exited with status: 0
One traced child (pid=22284) exited with status: 0
New process pid=22287
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-misc07.opb

[startup+10.004 s]
Raw data (loadavg): 0.95 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 1555 0 0 0 977 8 0 0 25 0 1 0 1797458776 6418432 1456 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 1567 1456 145 145 0 1422 0
[pid=22287] vsize: 6268
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8392

[startup+20.0047 s]
Raw data (loadavg): 0.96 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 2119 0 0 0 1967 12 0 0 25 0 1 0 1797458776 8744960 2020 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 2135 2020 145 145 0 1990 0
[pid=22287] vsize: 8540
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 10664

[startup+30.0064 s]
Raw data (loadavg): 0.96 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 2245 0 0 0 2966 13 0 0 25 0 1 0 1797458776 9256960 2146 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 2260 2146 145 145 0 2115 0
[pid=22287] vsize: 9040
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 11164

[startup+40.007 s]
Raw data (loadavg): 0.97 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 2472 0 0 0 3961 15 0 0 25 0 1 0 1797458776 10178560 2373 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 2485 2373 145 145 0 2340 0
[pid=22287] vsize: 9940
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 12064

[startup+50.0077 s]
Raw data (loadavg): 0.97 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 2472 0 0 0 4960 16 0 0 25 0 1 0 1797458776 10178560 2373 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 2485 2373 145 145 0 2340 0
[pid=22287] vsize: 9940
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 12064

[startup+60.0093 s]
Raw data (loadavg): 0.98 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 2639 0 0 0 5957 17 0 0 25 0 1 0 1797458776 10858496 2540 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 2651 2540 145 145 0 2506 0
[pid=22287] vsize: 10604
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 12728

[startup+70.01 s]
Raw data (loadavg): 0.98 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 3155 0 0 0 6947 22 0 0 25 0 1 0 1797458776 13021184 3056 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 3179 3056 145 145 0 3034 0
[pid=22287] vsize: 12716
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 14840

[startup+80.0116 s]
Raw data (loadavg): 0.98 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 3585 0 0 0 7939 24 0 0 25 0 1 0 1797458776 14766080 3486 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 3605 3486 145 145 0 3460 0
[pid=22287] vsize: 14420
Current children cumulated CPU time (s) 79.65
Current children cumulated vsize (Kb) 16544

[startup+90.0123 s]
Raw data (loadavg): 0.98 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 3805 0 0 0 8934 27 0 0 25 0 1 0 1797458776 15659008 3706 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 3823 3706 145 145 0 3678 0
[pid=22287] vsize: 15292
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 17416

[startup+100.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 3805 0 0 0 9934 27 0 0 25 0 1 0 1797458776 15659008 3706 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 3823 3706 145 145 0 3678 0
[pid=22287] vsize: 15292
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 17416

[startup+110.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 3888 0 0 0 10932 29 0 0 25 0 1 0 1797458776 16007168 3789 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 3908 3789 145 145 0 3763 0
[pid=22287] vsize: 15632
Current children cumulated CPU time (s) 109.63
Current children cumulated vsize (Kb) 17756

[startup+120.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4161 0 0 0 11928 30 0 0 25 0 1 0 1797458776 17117184 4062 4294967295 134512640 135094434 3221224432 3221222544 134562841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4062 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 18840

[startup+130.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4161 0 0 0 12928 30 0 0 25 0 1 0 1797458776 17117184 4062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4062 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 18840

[startup+140.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4161 0 0 0 13929 30 0 0 25 0 1 0 1797458776 17117184 4062 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4062 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 18840

[startup+150.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4161 0 0 0 14929 30 0 0 25 0 1 0 1797458776 17117184 4062 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4062 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 18840

[startup+160.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 15929 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 18840

[startup+170.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 16929 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 169.61
Current children cumulated vsize (Kb) 18840

[startup+180.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 17930 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 18840

[startup+190.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 18930 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 18840

[startup+200.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 19930 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 18840

[startup+210.021 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 20930 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 209.62
Current children cumulated vsize (Kb) 18840

[startup+220.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 21930 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 219.62
Current children cumulated vsize (Kb) 18840

[startup+230.021 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 22931 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 229.63
Current children cumulated vsize (Kb) 18840

[startup+240.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 23931 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 239.63
Current children cumulated vsize (Kb) 18840

[startup+250.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 24931 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 18840

[startup+260.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 25931 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 18840

[startup+270.023 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4164 0 0 0 26931 30 0 0 25 0 1 0 1797458776 17117184 4065 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4179 4065 145 145 0 4034 0
[pid=22287] vsize: 16716
Current children cumulated CPU time (s) 269.63
Current children cumulated vsize (Kb) 18840

[startup+280.023 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4198 0 0 0 27931 31 0 0 25 0 1 0 1797458776 17256448 4099 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4213 4099 145 145 0 4068 0
[pid=22287] vsize: 16852
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 18976

[startup+290.023 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4202 0 0 0 28931 31 0 0 25 0 1 0 1797458776 17272832 4103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4217 4103 145 145 0 4072 0
[pid=22287] vsize: 16868
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 18992

[startup+300.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4210 0 0 0 29931 31 0 0 25 0 1 0 1797458776 17305600 4111 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4225 4111 145 145 0 4080 0
[pid=22287] vsize: 16900
Current children cumulated CPU time (s) 299.64
Current children cumulated vsize (Kb) 19024

[startup+310.025 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4669 0 0 0 30921 35 0 0 25 0 1 0 1797458776 19185664 4570 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4684 4570 145 145 0 4539 0
[pid=22287] vsize: 18736
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 20860

[startup+320.025 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4669 0 0 0 31921 35 0 0 25 0 1 0 1797458776 19185664 4570 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4684 4570 145 145 0 4539 0
[pid=22287] vsize: 18736
Current children cumulated CPU time (s) 319.58
Current children cumulated vsize (Kb) 20860

[startup+330.026 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4669 0 0 0 32922 35 0 0 25 0 1 0 1797458776 19185664 4570 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4684 4570 145 145 0 4539 0
[pid=22287] vsize: 18736
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 20860

[startup+340.027 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4684 0 0 0 33922 35 0 0 25 0 1 0 1797458776 19247104 4585 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4699 4585 145 145 0 4554 0
[pid=22287] vsize: 18796
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 20920

[startup+350.026 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4701 0 0 0 34922 35 0 0 25 0 1 0 1797458776 19329024 4602 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4719 4602 145 145 0 4574 0
[pid=22287] vsize: 18876
Current children cumulated CPU time (s) 349.59
Current children cumulated vsize (Kb) 21000

[startup+360.028 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 4759 0 0 0 35921 35 0 0 25 0 1 0 1797458776 19566592 4660 4294967295 134512640 135094434 3221224432 3221222976 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 4777 4660 145 145 0 4632 0
[pid=22287] vsize: 19108
Current children cumulated CPU time (s) 359.58
Current children cumulated vsize (Kb) 21232

[startup+370.029 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 36914 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 23004

[startup+380.028 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 37914 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221222012 134563371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 379.55
Current children cumulated vsize (Kb) 23004

[startup+390.029 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 38914 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 389.55
Current children cumulated vsize (Kb) 23004

[startup+400.03 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 39914 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 399.55
Current children cumulated vsize (Kb) 23004

[startup+410.03 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 40915 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 409.56
Current children cumulated vsize (Kb) 23004

[startup+420.031 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 41915 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223056 134562090 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 419.56
Current children cumulated vsize (Kb) 23004

[startup+430.032 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 42915 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 23004

[startup+440.032 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 43915 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 439.56
Current children cumulated vsize (Kb) 23004

[startup+450.033 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 44916 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 449.57
Current children cumulated vsize (Kb) 23004

[startup+460.034 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 45916 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 459.57
Current children cumulated vsize (Kb) 23004

[startup+470.034 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 46916 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 469.57
Current children cumulated vsize (Kb) 23004

[startup+480.035 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 47916 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 479.57
Current children cumulated vsize (Kb) 23004

[startup+490.035 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 48917 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 489.58
Current children cumulated vsize (Kb) 23004

[startup+500.036 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 49917 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 499.58
Current children cumulated vsize (Kb) 23004

[startup+510.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 50917 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 509.58
Current children cumulated vsize (Kb) 23004

[startup+520.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 51917 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223024 134556878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 519.58
Current children cumulated vsize (Kb) 23004

[startup+530.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 52917 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 529.58
Current children cumulated vsize (Kb) 23004

[startup+540.039 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 53918 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 539.59
Current children cumulated vsize (Kb) 23004

[startup+550.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 54918 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 549.59
Current children cumulated vsize (Kb) 23004

[startup+560.039 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 55918 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 559.59
Current children cumulated vsize (Kb) 23004

[startup+570.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 56918 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 569.59
Current children cumulated vsize (Kb) 23004

[startup+580.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 57918 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 579.59
Current children cumulated vsize (Kb) 23004

[startup+590.041 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 58919 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 589.6
Current children cumulated vsize (Kb) 23004

[startup+600.042 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5175 0 0 0 59919 39 0 0 25 0 1 0 1797458776 21381120 5076 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5076 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 599.6
Current children cumulated vsize (Kb) 23004

[startup+610.043 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 60919 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 609.6
Current children cumulated vsize (Kb) 23004

[startup+620.044 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 61919 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 619.6
Current children cumulated vsize (Kb) 23004

[startup+630.045 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 62920 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 629.61
Current children cumulated vsize (Kb) 23004

[startup+640.046 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 63920 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 639.61
Current children cumulated vsize (Kb) 23004

[startup+650.047 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 64920 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 649.61
Current children cumulated vsize (Kb) 23004

[startup+660.048 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 65920 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 659.61
Current children cumulated vsize (Kb) 23004

[startup+670.048 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 66921 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 669.62
Current children cumulated vsize (Kb) 23004

[startup+680.049 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 67921 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 679.62
Current children cumulated vsize (Kb) 23004

[startup+690.05 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 68921 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 689.62
Current children cumulated vsize (Kb) 23004

[startup+700.05 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5176 0 0 0 69921 39 0 0 25 0 1 0 1797458776 21381120 5077 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5220 5077 145 145 0 5075 0
[pid=22287] vsize: 20880
Current children cumulated CPU time (s) 699.62
Current children cumulated vsize (Kb) 23004

[startup+710.052 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5237 0 0 0 70921 40 0 0 25 0 1 0 1797458776 21651456 5138 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5286 5138 145 145 0 5141 0
[pid=22287] vsize: 21144
Current children cumulated CPU time (s) 709.63
Current children cumulated vsize (Kb) 23268

[startup+720.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5237 0 0 0 71921 40 0 0 25 0 1 0 1797458776 21651456 5138 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5286 5138 145 145 0 5141 0
[pid=22287] vsize: 21144
Current children cumulated CPU time (s) 719.63
Current children cumulated vsize (Kb) 23268

[startup+730.052 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5247 0 0 0 72921 40 0 0 25 0 1 0 1797458776 21716992 5148 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5302 5148 145 145 0 5157 0
[pid=22287] vsize: 21208
Current children cumulated CPU time (s) 729.63
Current children cumulated vsize (Kb) 23332

[startup+740.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5261 0 0 0 73921 40 0 0 25 0 1 0 1797458776 21782528 5162 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5318 5162 145 145 0 5173 0
[pid=22287] vsize: 21272
Current children cumulated CPU time (s) 739.63
Current children cumulated vsize (Kb) 23396

[startup+750.053 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5293 0 0 0 74921 40 0 0 25 0 1 0 1797458776 21946368 5194 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5358 5194 145 145 0 5213 0
[pid=22287] vsize: 21432
Current children cumulated CPU time (s) 749.63
Current children cumulated vsize (Kb) 23556

[startup+760.055 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5308 0 0 0 75921 40 0 0 25 0 1 0 1797458776 22011904 5209 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5374 5209 145 145 0 5229 0
[pid=22287] vsize: 21496
Current children cumulated CPU time (s) 759.63
Current children cumulated vsize (Kb) 23620

[startup+770.056 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5327 0 0 0 76922 40 0 0 25 0 1 0 1797458776 22110208 5228 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5398 5228 145 145 0 5253 0
[pid=22287] vsize: 21592
Current children cumulated CPU time (s) 769.64
Current children cumulated vsize (Kb) 23716

[startup+780.057 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5341 0 0 0 77922 40 0 0 25 0 1 0 1797458776 22208512 5242 4294967295 134512640 135094434 3221224432 3221223104 134555590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5422 5242 145 145 0 5277 0
[pid=22287] vsize: 21688
Current children cumulated CPU time (s) 779.64
Current children cumulated vsize (Kb) 23812

[startup+790.057 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5380 0 0 0 78922 40 0 0 25 0 1 0 1797458776 22405120 5281 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5470 5281 145 145 0 5325 0
[pid=22287] vsize: 21880
Current children cumulated CPU time (s) 789.64
Current children cumulated vsize (Kb) 24004

[startup+800.058 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5552 0 0 0 79920 41 0 0 25 0 1 0 1797458776 23179264 5453 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5659 5453 145 145 0 5514 0
[pid=22287] vsize: 22636
Current children cumulated CPU time (s) 799.63
Current children cumulated vsize (Kb) 24760

[startup+810.058 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5735 0 0 0 80917 42 0 0 25 0 1 0 1797458776 23961600 5636 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5850 5636 145 145 0 5705 0
[pid=22287] vsize: 23400
Current children cumulated CPU time (s) 809.61
Current children cumulated vsize (Kb) 25524

[startup+820.06 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5760 0 0 0 81917 42 0 0 25 0 1 0 1797458776 24068096 5661 4294967295 134512640 135094434 3221224432 3221223104 134555232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5876 5661 145 145 0 5731 0
[pid=22287] vsize: 23504
Current children cumulated CPU time (s) 819.61
Current children cumulated vsize (Kb) 25628

[startup+830.06 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5766 0 0 0 82917 42 0 0 25 0 1 0 1797458776 24100864 5667 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5884 5667 145 145 0 5739 0
[pid=22287] vsize: 23536
Current children cumulated CPU time (s) 829.61
Current children cumulated vsize (Kb) 25660

[startup+840.06 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5786 0 0 0 83917 42 0 0 25 0 1 0 1797458776 24199168 5687 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5908 5687 145 145 0 5763 0
[pid=22287] vsize: 23632
Current children cumulated CPU time (s) 839.61
Current children cumulated vsize (Kb) 25756

[startup+850.061 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5818 0 0 0 84916 43 0 0 25 0 1 0 1797458776 24363008 5719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 5948 5719 145 145 0 5803 0
[pid=22287] vsize: 23792
Current children cumulated CPU time (s) 849.61
Current children cumulated vsize (Kb) 25916

[startup+860.062 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5839 0 0 0 85915 43 0 0 25 0 1 0 1797458776 24461312 5740 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5972 5740 145 145 0 5827 0
[pid=22287] vsize: 23888
Current children cumulated CPU time (s) 859.6
Current children cumulated vsize (Kb) 26012

[startup+870.062 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5855 0 0 0 86915 43 0 0 25 0 1 0 1797458776 24526848 5756 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5988 5756 145 145 0 5843 0
[pid=22287] vsize: 23952
Current children cumulated CPU time (s) 869.6
Current children cumulated vsize (Kb) 26076

[startup+880.063 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 5856 0 0 0 87916 43 0 0 25 0 1 0 1797458776 24526848 5757 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 5988 5757 145 145 0 5843 0
[pid=22287] vsize: 23952
Current children cumulated CPU time (s) 879.61
Current children cumulated vsize (Kb) 26076

[startup+890.064 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6088 0 0 0 88912 45 0 0 25 0 1 0 1797458776 25538560 5989 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6235 5989 145 145 0 6090 0
[pid=22287] vsize: 24940
Current children cumulated CPU time (s) 889.59
Current children cumulated vsize (Kb) 27064

[startup+900.064 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6325 0 0 0 89907 47 0 0 25 0 1 0 1797458776 26505216 6226 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6226 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 899.56
Current children cumulated vsize (Kb) 28008

[startup+910.065 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6325 0 0 0 90907 47 0 0 25 0 1 0 1797458776 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6226 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 909.56
Current children cumulated vsize (Kb) 28008

[startup+920.066 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6325 0 0 0 91908 47 0 0 25 0 1 0 1797458776 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6226 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 919.57
Current children cumulated vsize (Kb) 28008

[startup+930.066 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6325 0 0 0 92908 47 0 0 25 0 1 0 1797458776 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6226 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 929.57
Current children cumulated vsize (Kb) 28008

[startup+940.068 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6325 0 0 0 93908 47 0 0 25 0 1 0 1797458776 26505216 6226 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6226 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 939.57
Current children cumulated vsize (Kb) 28008

[startup+950.068 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6326 0 0 0 94908 47 0 0 25 0 1 0 1797458776 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6227 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 949.57
Current children cumulated vsize (Kb) 28008

[startup+960.069 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6326 0 0 0 95909 47 0 0 25 0 1 0 1797458776 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6227 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 959.58
Current children cumulated vsize (Kb) 28008

[startup+970.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6326 0 0 0 96909 47 0 0 25 0 1 0 1797458776 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6227 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 969.58
Current children cumulated vsize (Kb) 28008

[startup+980.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6326 0 0 0 97908 47 0 0 25 0 1 0 1797458776 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22287/statm): 6471 6227 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 979.57
Current children cumulated vsize (Kb) 28008

[startup+990.071 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6326 0 0 0 98909 47 0 0 25 0 1 0 1797458776 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6227 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 989.58
Current children cumulated vsize (Kb) 28008

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6326 0 0 0 99909 47 0 0 25 0 1 0 1797458776 26505216 6227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6471 6227 145 145 0 6326 0
[pid=22287] vsize: 25884
Current children cumulated CPU time (s) 999.58
Current children cumulated vsize (Kb) 28008

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6338 0 0 0 100909 47 0 0 25 0 1 0 1797458776 26570752 6239 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6487 6239 145 145 0 6342 0
[pid=22287] vsize: 25948
Current children cumulated CPU time (s) 1009.58
Current children cumulated vsize (Kb) 28072

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6343 0 0 0 101909 47 0 0 25 0 1 0 1797458776 26603520 6244 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6495 6244 145 145 0 6350 0
[pid=22287] vsize: 25980
Current children cumulated CPU time (s) 1019.58
Current children cumulated vsize (Kb) 28104

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6345 0 0 0 102909 47 0 0 25 0 1 0 1797458776 26603520 6246 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6495 6246 145 145 0 6350 0
[pid=22287] vsize: 25980
Current children cumulated CPU time (s) 1029.58
Current children cumulated vsize (Kb) 28104

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6345 0 0 0 103910 47 0 0 25 0 1 0 1797458776 26603520 6246 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6495 6246 145 145 0 6350 0
[pid=22287] vsize: 25980
Current children cumulated CPU time (s) 1039.59
Current children cumulated vsize (Kb) 28104

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6345 0 0 0 104910 47 0 0 25 0 1 0 1797458776 26603520 6246 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6495 6246 145 145 0 6350 0
[pid=22287] vsize: 25980
Current children cumulated CPU time (s) 1049.59
Current children cumulated vsize (Kb) 28104

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6351 0 0 0 105910 47 0 0 25 0 1 0 1797458776 26636288 6252 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6503 6252 145 145 0 6358 0
[pid=22287] vsize: 26012
Current children cumulated CPU time (s) 1059.59
Current children cumulated vsize (Kb) 28136

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6359 0 0 0 106910 48 0 0 25 0 1 0 1797458776 26669056 6260 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6511 6260 145 145 0 6366 0
[pid=22287] vsize: 26044
Current children cumulated CPU time (s) 1069.6
Current children cumulated vsize (Kb) 28168

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6359 0 0 0 107911 48 0 0 25 0 1 0 1797458776 26669056 6260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6511 6260 145 145 0 6366 0
[pid=22287] vsize: 26044
Current children cumulated CPU time (s) 1079.61
Current children cumulated vsize (Kb) 28168

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6382 0 0 0 108911 48 0 0 25 0 1 0 1797458776 26796032 6283 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6542 6283 145 145 0 6397 0
[pid=22287] vsize: 26168
Current children cumulated CPU time (s) 1089.61
Current children cumulated vsize (Kb) 28292

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6384 0 0 0 109911 48 0 0 25 0 1 0 1797458776 26796032 6285 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6542 6285 145 145 0 6397 0
[pid=22287] vsize: 26168
Current children cumulated CPU time (s) 1099.61
Current children cumulated vsize (Kb) 28292

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6391 0 0 0 110911 48 0 0 25 0 1 0 1797458776 26828800 6292 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6550 6292 145 145 0 6405 0
[pid=22287] vsize: 26200
Current children cumulated CPU time (s) 1109.61
Current children cumulated vsize (Kb) 28324

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6393 0 0 0 111911 48 0 0 25 0 1 0 1797458776 26828800 6294 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6550 6294 145 145 0 6405 0
[pid=22287] vsize: 26200
Current children cumulated CPU time (s) 1119.61
Current children cumulated vsize (Kb) 28324

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6412 0 0 0 112912 48 0 0 25 0 1 0 1797458776 26927104 6313 4294967295 134512640 135094434 3221224432 3221223024 134556724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6574 6313 145 145 0 6429 0
[pid=22287] vsize: 26296
Current children cumulated CPU time (s) 1129.62
Current children cumulated vsize (Kb) 28420

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6428 0 0 0 113912 48 0 0 25 0 1 0 1797458776 27025408 6329 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6598 6329 145 145 0 6453 0
[pid=22287] vsize: 26392
Current children cumulated CPU time (s) 1139.62
Current children cumulated vsize (Kb) 28516

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6449 0 0 0 114912 48 0 0 25 0 1 0 1797458776 27123712 6350 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6622 6350 145 145 0 6477 0
[pid=22287] vsize: 26488
Current children cumulated CPU time (s) 1149.62
Current children cumulated vsize (Kb) 28612

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6449 0 0 0 115912 48 0 0 25 0 1 0 1797458776 27123712 6350 4294967295 134512640 135094434 3221224432 3221222992 134550329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6622 6350 145 145 0 6477 0
[pid=22287] vsize: 26488
Current children cumulated CPU time (s) 1159.62
Current children cumulated vsize (Kb) 28612

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6458 0 0 0 116913 48 0 0 25 0 1 0 1797458776 27156480 6359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6630 6359 145 145 0 6485 0
[pid=22287] vsize: 26520
Current children cumulated CPU time (s) 1169.63
Current children cumulated vsize (Kb) 28644

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6459 0 0 0 117913 48 0 0 25 0 1 0 1797458776 27156480 6360 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6630 6360 145 145 0 6485 0
[pid=22287] vsize: 26520
Current children cumulated CPU time (s) 1179.63
Current children cumulated vsize (Kb) 28644

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6482 0 0 0 118913 48 0 0 25 0 1 0 1797458776 27287552 6383 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6662 6383 145 145 0 6517 0
[pid=22287] vsize: 26648
Current children cumulated CPU time (s) 1189.63
Current children cumulated vsize (Kb) 28772

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6490 0 0 0 119913 48 0 0 25 0 1 0 1797458776 27320320 6391 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6670 6391 145 145 0 6525 0
[pid=22287] vsize: 26680
Current children cumulated CPU time (s) 1199.63
Current children cumulated vsize (Kb) 28804

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6492 0 0 0 120913 48 0 0 25 0 1 0 1797458776 27320320 6393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6670 6393 145 145 0 6525 0
[pid=22287] vsize: 26680
Current children cumulated CPU time (s) 1209.63
Current children cumulated vsize (Kb) 28804



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.99 0.92 2/57 22287
Raw data (/proc/22283/stat): 22283 (minisat+_script) S 22282 22283 1333 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797458771 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22283/statm): 531 226 485 147 0 384 0
[pid=22283] vsize: 2124
Raw data (/proc/22287/stat): 22287 (minisat+_64-bit) R 22283 22283 1333 0 -1 0 6492 0 0 0 120913 48 0 0 25 0 1 0 1797458776 27320320 6393 4294967295 134512640 135094434 3221224432 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22287/statm): 6670 6393 145 145 0 6525 0
[pid=22287] vsize: 26680
Current children cumulated CPU time (s) 1209.63
Current children cumulated vsize (Kb) 28804

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

Child status: 10
Real time (s): 1210.1
CPU time (s): 1209.64
CPU user time (s): 1209.14
CPU system time (s): 0.495924
CPU usage (%): 99.9614
Max. virtual memory (cumulated for all children) (Kb): 28804

Verifier Data

ERROR: no interpretation found !