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-markshare2.opb
MD5SUMb54bb080800e2327586cd478559c04ff
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 5632
Optimality of the best value was proved NO
Number of terms in the objective function 140
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 7340025
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 524288
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 7340025
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.36
Number of variables200
Total number of constraints67
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints7
Minimum length of a constraint1
Maximum length of a constraint80

Trace number 6213

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        862720 kB
Buffers:         31412 kB
Cached:         110740 kB
SwapCached:        784 kB
Active:          44984 kB
Inactive:        99784 kB
HighTotal:      131008 kB
HighFree:        28140 kB
LowTotal:       903652 kB
LowFree:        834580 kB
SwapTotal:     2097892 kB
SwapFree:      2096640 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            21408 kB
Committed_AS:    64288 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:45:48 (client local time) WITH STATUS 10 IN 1209.77 SECONDS
stats: 3367 7 1209.77 10

Solver Data

c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 431615   bits: 20/19
c ---[  10]---> Adder-cost: 380   maxlim: 461183   bits: 20/19
c ---[   8]---> Adder-cost: 350   maxlim: 445183   bits: 20/19
c ---[   6]---> Adder-cost: 340   maxlim: 477951   bits: 20/19
c ---[   4]---> Adder-cost: 390   maxlim: 451839   bits: 20/19
c ---[   2]---> Adder-cost: 358   maxlim: 468735   bits: 20/19
c ---[   0]---> Adder-cost: 374   maxlim: 444543   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17222    61228 |    6314     100      905     9.1 |  9.969 % |
c |       253 |   17214    61202 |    6945     252     2033     8.1 | 10.003 % |
c |       478 |   17206    61176 |    7639     476     4722     9.9 | 10.038 % |
c ==============================================================================
c Found solution: 866304
c ---[   0]---> Sorter-cost: 1068     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       536 |   19853    67360 |    6617     534     5740    10.7 | 10.038 % |
c ==============================================================================
c Found solution: 828672
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       632 |   19863    67400 |    6621     629    13956    22.2 | 10.038 % |
c |       733 |   19863    67400 |    7283     730    20234    27.7 |  7.644 % |
c |       884 |   19855    67374 |    8011     879    45616    51.9 |  7.696 % |
c |      1110 |   19847    67348 |    8812    1105    70591    63.9 |  7.696 % |
c |      1447 |   19839    67322 |    9693    1441    95879    66.5 |  7.723 % |
c ==============================================================================
c Found solution: 702720
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1945 |   19842    67325 |    6614    1938   159401    82.3 |  7.723 % |
c |      2046 |   19842    67325 |    7275    2039   167910    82.3 |  7.761 % |
c |      2197 |   19842    67325 |    8002    2190   179220    81.8 |  7.761 % |
c |      2423 |   19842    67325 |    8803    2416   196028    81.1 |  7.761 % |
c |      2761 |   19842    67325 |    9683    2754   236792    86.0 |  7.761 % |
c |      3268 |   19842    67325 |   10651    3261   287766    88.2 |  7.761 % |
c ==============================================================================
c Found solution: 676352
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3715 |   19858    67370 |    6619    3708   318920    86.0 |  7.761 % |
c |      3815 |   19858    67370 |    7280    3808   328892    86.4 |  7.766 % |
c |      3965 |   19858    67370 |    8008    3958   346566    87.6 |  7.766 % |
c |      4190 |   19858    67370 |    8809    4183   366380    87.6 |  7.766 % |
c |      4528 |   19852    67357 |    9690    4520   400494    88.6 |  7.819 % |
c |      5034 |   19844    67331 |   10659    5025   444892    88.5 |  7.845 % |
c |      5794 |   19836    67305 |   11725    5784   509124    88.0 |  7.871 % |
c |      6934 |   19828    67279 |   12898    6923   580155    83.8 |  7.897 % |
c ==============================================================================
c Found solution: 674304
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7359 |   19838    67302 |    6612    7348   621804    84.6 |  7.897 % |
c |      7463 |   19838    67302 |    7273    3778   243653    64.5 |  7.913 % |
c |      7614 |   19838    67302 |    8000    3929   255506    65.0 |  7.913 % |
c ==============================================================================
c Found solution: 654336
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7790 |   19849    67335 |    6616    4105   268736    65.5 |  7.913 % |
c ==============================================================================
c Found solution: 645120
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7856 |   19857    67359 |    6619    4171   271081    65.0 |  7.913 % |
c |      7958 |   19857    67359 |    7280    4273   278513    65.2 |  7.938 % |
c ==============================================================================
c Found solution: 465408
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8075 |   19869    67387 |    6623    4390   284865    64.9 |  7.938 % |
c |      8175 |   19869    67387 |    7285    4490   290752    64.8 |  7.949 % |
c |      8326 |   19869    67387 |    8013    4641   302249    65.1 |  7.949 % |
c |      8551 |   19869    67387 |    8815    4866   312895    64.3 |  7.949 % |
c |      8888 |   19869    67387 |    9696    5203   337269    64.8 |  7.949 % |
c |      9394 |   19869    67387 |   10666    5709   372234    65.2 |  7.949 % |
c |     10153 |   19869    67387 |   11733    6468   427615    66.1 |  7.949 % |
c |     11294 |   19869    67387 |   12906    7609   506572    66.6 |  7.949 % |
c |     13003 |   19863    67369 |   14196    9317   680687    73.1 |  7.975 % |
c |     15565 |   19838    67290 |   15616   11876   979173    82.4 |  8.079 % |
c |     19410 |   19838    67290 |   17178   15721  1427200    90.8 |  8.079 % |
c ==============================================================================
c Found solution: 426240
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24555 |   19802    67164 |    6600   11781   991951    84.2 |  8.079 % |
c |     24656 |   19802    67164 |    7260    5992   340445    56.8 |  8.251 % |
c |     24806 |   19802    67164 |    7986    6142   346020    56.3 |  8.251 % |
c |     25031 |   19802    67164 |    8784    6367   351779    55.3 |  8.251 % |
c |     25370 |   19802    67164 |    9663    6706   376621    56.2 |  8.251 % |
c |     25878 |   19802    67164 |   10629    7214   412120    57.1 |  8.251 % |
c |     26639 |   19802    67164 |   11692    7975   454198    57.0 |  8.251 % |
c |     27779 |   19802    67164 |   12861    9115   506655    55.6 |  8.251 % |
c |     29487 |   19802    67164 |   14147   10823   597522    55.2 |  8.251 % |
c |     32049 |   19802    67164 |   15562   13385   746703    55.8 |  8.251 % |
c |     35893 |   19802    67164 |   17118    9134   445739    48.8 |  8.251 % |
c |     41660 |   19802    67164 |   18830   14901   900002    60.4 |  8.251 % |
c |     50309 |   19802    67164 |   20713   13630   900207    66.0 |  8.251 % |
c |     63285 |   19802    67164 |   22784   15643   876282    56.0 |  8.251 % |
c |     82746 |   19802    67164 |   25063   23100  1569191    67.9 |  8.251 % |
c ==============================================================================
c Found solution: 420352
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110809 |   19810    67183 |    6603   24998  2030699    81.2 |  8.251 % |
c |    110909 |   19810    67183 |    7263    6350   368699    58.1 |  8.269 % |
c |    111061 |   19810    67183 |    7989    6502   374493    57.6 |  8.269 % |
c |    111288 |   19810    67183 |    8788    6729   385690    57.3 |  8.269 % |
c |    111626 |   19810    67183 |    9667    7067   413477    58.5 |  8.269 % |
c |    112132 |   19810    67183 |   10634    7573   438726    57.9 |  8.269 % |
c |    112891 |   19810    67183 |   11697    8332   475591    57.1 |  8.269 % |
c |    114031 |   19810    67183 |   12867    9472   602990    63.7 |  8.269 % |
c |    115740 |   19810    67183 |   14154   11181   705503    63.1 |  8.269 % |
c ==============================================================================
c Found solution: 411392
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118101 |   19822    67210 |    6607   13542   911670    67.3 |  8.269 % |
c |    118201 |   19822    67210 |    7267    6871   405686    59.0 |  8.282 % |
c |    118351 |   19822    67210 |    7994    7021   414241    59.0 |  8.282 % |
c |    118576 |   19822    67210 |    8793    7246   434055    59.9 |  8.282 % |
c |    118913 |   19822    67210 |    9673    7583   456334    60.2 |  8.282 % |
c |    119419 |   19822    67210 |   10640    8089   483898    59.8 |  8.282 % |
c |    120178 |   19822    67210 |   11704    8848   528469    59.7 |  8.282 % |
c |    121317 |   19822    67210 |   12875    9987   592730    59.4 |  8.282 % |
c |    123025 |   19822    67210 |   14162   11695   721731    61.7 |  8.282 % |
c |    125587 |   19822    67210 |   15578   14257   897308    62.9 |  8.282 % |
c |    129431 |   19822    67210 |   17136    9873   539594    54.7 |  8.282 % |
c |    135198 |   19814    67184 |   18850   15639  1121030    71.7 |  8.308 % |
c |    143849 |   19814    67184 |   20735   14328   969560    67.7 |  8.308 % |
c ==============================================================================
c Found solution: 404480
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    151309 |   19816    67186 |    6605   11073   646615    58.4 |  8.308 % |
c |    151411 |   19816    67186 |    7265    5639   309058    54.8 |  8.374 % |
c |    151561 |   19816    67186 |    7992    5789   311658    53.8 |  8.374 % |
c |    151786 |   19816    67186 |    8791    6014   337987    56.2 |  8.374 % |
c |    152124 |   19816    67186 |    9670    6352   350939    55.2 |  8.374 % |
c ==============================================================================
c Found solution: 363264
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152583 |   19829    67218 |    6609    6811   361631    53.1 |  8.374 % |
c |    152685 |   19829    67218 |    7269    6913   366844    53.1 |  8.385 % |
c |    152836 |   19829    67218 |    7996    7064   390436    55.3 |  8.385 % |
c |    153061 |   19829    67218 |    8796    7289   402314    55.2 |  8.385 % |
c |    153398 |   19829    67218 |    9676    7626   416355    54.6 |  8.385 % |
c |    153907 |   19829    67218 |   10643    8135   436418    53.6 |  8.385 % |
c |    154667 |   19829    67218 |   11708    8895   517597    58.2 |  8.385 % |
c |    155807 |   19829    67218 |   12879   10035   580468    57.8 |  8.385 % |
c |    157517 |   19829    67218 |   14166   11745   642591    54.7 |  8.385 % |
c |    160079 |   19829    67218 |   15583   14307   764160    53.4 |  8.385 % |
c ==============================================================================
c Found solution: 343936
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162554 |   19860    67292 |    6620    8590   324198    37.7 |  8.385 % |
c |    162655 |   19860    67292 |    7282    4396   151608    34.5 |  8.372 % |
c |    162807 |   19860    67292 |    8010    4548   161742    35.6 |  8.372 % |
c |    163033 |   19860    67292 |    8811    4774   168934    35.4 |  8.372 % |
c |    163371 |   19860    67292 |    9692    5112   176581    34.5 |  8.372 % |
c |    163877 |   19860    67292 |   10661    5618   253166    45.1 |  8.372 % |
c |    164636 |   19860    67292 |   11727    6377   301500    47.3 |  8.372 % |
c |    165778 |   19860    67292 |   12900    7519   356921    47.5 |  8.372 % |
c |    167486 |   19860    67292 |   14190    9227   445248    48.3 |  8.372 % |
c |    170048 |   19860    67292 |   15609   11789   602596    51.1 |  8.372 % |
c |    173892 |   19860    67292 |   17170   15633   831926    53.2 |  8.372 % |
c |    179659 |   19860    67292 |   18887   12423   597867    48.1 |  8.372 % |
c |    188308 |   19848    67265 |   20776   11130   791462    71.1 |  8.449 % |
c ==============================================================================
c Found solution: 260352
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188746 |   19854    67281 |    6618   11568   801463    69.3 |  8.449 % |
c |    188847 |   19854    67281 |    7279    5885   256847    43.6 |  8.465 % |
c |    188997 |   19854    67281 |    8007    6035   266435    44.1 |  8.465 % |
c |    189223 |   19854    67281 |    8808    6261   281425    44.9 |  8.465 % |
c |    189561 |   19854    67281 |    9689    6599   298712    45.3 |  8.465 % |
c |    190067 |   19854    67281 |   10658    7105   319291    44.9 |  8.465 % |
c |    190827 |   19854    67281 |   11724    7865   359467    45.7 |  8.465 % |
c |    191968 |   19854    67281 |   12896    9006   410789    45.6 |  8.465 % |
c |    193677 |   19854    67281 |   14186   10715   531399    49.6 |  8.465 % |
c |    196241 |   19854    67281 |   15604   13279   685851    51.6 |  8.465 % |
c |    200085 |   19854    67281 |   17165    8898   488070    54.9 |  8.465 % |
c |    205852 |   19854    67281 |   18881   14665   711080    48.5 |  8.465 % |
c ==============================================================================
c Found solution: 80128
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206193 |   19806    67113 |    6602   14727   700340    47.6 |  8.465 % |
c |    206293 |   19806    67113 |    7262    3782   103785    27.4 |  8.666 % |
c |    206444 |   19806    67113 |    7988    3933   104553    26.6 |  8.666 % |
c |    206669 |   19806    67113 |    8787    4158   107432    25.8 |  8.666 % |
c |    207006 |   19806    67113 |    9665    4495   116514    25.9 |  8.666 % |
c |    207513 |   19806    67113 |   10632    5002   128589    25.7 |  8.666 % |
c ==============================================================================
c Found solution: 64896
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207893 |   19615    66613 |    6538    5362   135046    25.2 |  8.666 % |
c |    207995 |   19615    66613 |    7191    5464   137131    25.1 | 10.089 % |
c |    208146 |   19615    66613 |    7910    5615   139840    24.9 | 10.089 % |
c |    208371 |   19615    66613 |    8702    5840   147321    25.2 | 10.089 % |
c |    208708 |   19615    66613 |    9572    6177   155749    25.2 | 10.089 % |
c |    209215 |   19615    66613 |   10529    6684   179508    26.9 | 10.089 % |
c |    209976 |   19615    66613 |   11582    7445   201615    27.1 | 10.089 % |
c |    211115 |   19615    66613 |   12740    8584   243072    28.3 | 10.089 % |
c |    212823 |   19615    66613 |   14014   10292   303964    29.5 | 10.089 % |
c |    215385 |   19615    66613 |   15416   12854   404034    31.4 | 10.089 % |
c |    219229 |   19615    66613 |   16957    8598   318726    37.1 | 10.089 % |
c ==============================================================================
c Found solution: 63616
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    222041 |   19622    66634 |    6540   11410   477534    41.9 | 10.089 % |
c |    222143 |   19622    66634 |    7194    5807   236093    40.7 | 10.102 % |
c |    222293 |   19622    66634 |    7913    5957   236962    39.8 | 10.102 % |
c |    222518 |   19622    66634 |    8704    6182   240201    38.9 | 10.102 % |
c |    222855 |   19622    66634 |    9575    6519   253550    38.9 | 10.102 % |
c |    223361 |   19622    66634 |   10532    7025   263589    37.5 | 10.102 % |
c |    224121 |   19622    66634 |   11586    7785   284201    36.5 | 10.102 % |
c |    225260 |   19622    66634 |   12744    8924   354542    39.7 | 10.102 % |
c |    226971 |   19622    66634 |   14019   10635   414350    39.0 | 10.102 % |
c |    229533 |   19622    66634 |   15420   13197   533639    40.4 | 10.102 % |
c |    233377 |   19607    66589 |   16963    8676   346338    39.9 | 10.179 % |
c |    239144 |   19607    66589 |   18659   14443   554456    38.4 | 10.179 % |
c |    247793 |   19530    66415 |   20525   13278   517714    39.0 | 10.816 % |
c |    260769 |   19429    66185 |   22577   15427   982742    63.7 | 11.633 % |
c |    280230 |   19319    65931 |   24835   23197  1024138    44.1 | 12.628 % |
c |    309423 |   19319    65931 |   27319   25948  1521579    58.6 | 12.628 % |
c ==============================================================================
c Found solution: 59008
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    327090 |   19320    65935 |    6440   27848  1354853    48.7 | 12.628 % |
c |    327191 |   19320    65935 |    7084    6666   249277    37.4 | 12.732 % |
c |    327341 |   19320    65935 |    7792    6816   250694    36.8 | 12.732 % |
c |    327566 |   19320    65935 |    8571    7041   259558    36.9 | 12.732 % |
c |    327904 |   19320    65935 |    9428    7379   266686    36.1 | 12.732 % |
c |    328410 |   19320    65935 |   10371    7885   277400    35.2 | 12.732 % |
c |    329171 |   19320    65935 |   11408    8646   299566    34.6 | 12.732 % |
c |    330310 |   19320    65935 |   12549    9785   331642    33.9 | 12.732 % |
c |    332018 |   19320    65935 |   13804   11493   456254    39.7 | 12.732 % |
c |    334582 |   19320    65935 |   15185   14057   533507    38.0 | 12.732 % |
c |    338428 |   19320    65935 |   16703    9687   452672    46.7 | 12.732 % |
c |    344195 |   19320    65935 |   18374   15454   704774    45.6 | 12.732 % |
c |    352844 |   19306    65902 |   20211   14334   779072    54.4 | 12.911 % |
c |    365818 |   19288    65862 |   22232   16842   680144    40.4 | 13.038 % |
c |    385280 |   19288    65862 |   24455   13318   512736    38.5 | 13.038 % |
c |    414473 |   19288    65862 |   26901   17159   819651    47.8 | 13.038 % |
c |    458262 |   19259    65797 |   29591   16835   605068    35.9 | 13.242 % |
c |    523948 |   19241    65756 |   32550   15348   637855    41.6 | 13.369 % |
c |    622474 |   19241    65756 |   35805   17341   946468    54.6 | 13.369 % |

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/3775/stat): 3775 (minisat+_script) R 3774 3775 5245 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855628591 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3775/statm): 174 3 169 147 0 27 0
[pid=3775] 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=3776
New process pid=3777
New process pid=3778
One traced child (pid=3777) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=3778) exited with status: 0
One traced child (pid=3776) exited with status: 0
New process pid=3779
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-markshare2.opb

[startup+10.0048 s]
Raw data (loadavg): 0.93 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 1117 0 0 0 981 6 0 0 25 0 1 0 1855628596 4976640 1104 4294967295 134512640 135094434 3221224432 3221223024 134557263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 1215 1104 145 145 0 1070 0
[pid=3779] vsize: 4860
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 6984

[startup+20.0066 s]
Raw data (loadavg): 0.94 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 1293 0 0 0 1977 8 0 0 25 0 1 0 1855628596 5685248 1280 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 1388 1280 145 145 0 1243 0
[pid=3779] vsize: 5552
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 7676

[startup+30.0075 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 1590 0 0 0 2972 9 0 0 25 0 1 0 1855628596 6918144 1577 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 1689 1577 145 145 0 1544 0
[pid=3779] vsize: 6756
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 8880

[startup+40.0084 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 1951 0 0 0 3964 13 0 0 25 0 1 0 1855628596 8384512 1938 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2047 1938 145 145 0 1902 0
[pid=3779] vsize: 8188
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 10312

[startup+50.0102 s]
Raw data (loadavg): 0.96 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2280 0 0 0 4956 17 0 0 25 0 1 0 1855628596 9728000 2267 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2375 2267 145 145 0 2230 0
[pid=3779] vsize: 9500
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 11624

[startup+60.0111 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2481 0 0 0 5952 18 0 0 25 0 1 0 1855628596 10608640 2468 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2590 2468 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 12484

[startup+70.012 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2481 0 0 0 6952 19 0 0 25 0 1 0 1855628596 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2590 2468 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 12484

[startup+80.0128 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2481 0 0 0 7951 19 0 0 25 0 1 0 1855628596 10608640 2468 4294967295 134512640 135094434 3221224432 3221223104 134556424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2590 2468 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 12484

[startup+90.0137 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2481 0 0 0 8951 20 0 0 25 0 1 0 1855628596 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2590 2468 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 89.72
Current children cumulated vsize (Kb) 12484

[startup+100.015 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2483 0 0 0 9950 20 0 0 25 0 1 0 1855628596 10608640 2470 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2590 2470 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 99.71
Current children cumulated vsize (Kb) 12484

[startup+110.015 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2483 0 0 0 10950 21 0 0 25 0 1 0 1855628596 10608640 2470 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 2590 2470 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 109.72
Current children cumulated vsize (Kb) 12484

[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2485 0 0 0 11950 21 0 0 25 0 1 0 1855628596 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2590 2472 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 119.72
Current children cumulated vsize (Kb) 12484

[startup+130.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2485 0 0 0 12950 21 0 0 25 0 1 0 1855628596 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2590 2472 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 129.72
Current children cumulated vsize (Kb) 12484

[startup+140.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2485 0 0 0 13950 21 0 0 25 0 1 0 1855628596 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2590 2472 145 145 0 2445 0
[pid=3779] vsize: 10360
Current children cumulated CPU time (s) 139.72
Current children cumulated vsize (Kb) 12484

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2552 0 0 0 14949 21 0 0 25 0 1 0 1855628596 10874880 2539 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2655 2539 145 145 0 2510 0
[pid=3779] vsize: 10620
Current children cumulated CPU time (s) 149.71
Current children cumulated vsize (Kb) 12744

[startup+160.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2556 0 0 0 15949 21 0 0 25 0 1 0 1855628596 10891264 2543 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2659 2543 145 145 0 2514 0
[pid=3779] vsize: 10636
Current children cumulated CPU time (s) 159.71
Current children cumulated vsize (Kb) 12760

[startup+170.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2560 0 0 0 16950 21 0 0 25 0 1 0 1855628596 10907648 2547 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2663 2547 145 145 0 2518 0
[pid=3779] vsize: 10652
Current children cumulated CPU time (s) 169.72
Current children cumulated vsize (Kb) 12776

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2888 0 0 0 17944 23 0 0 25 0 1 0 1855628596 12242944 2875 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 2989 2875 145 145 0 2844 0
[pid=3779] vsize: 11956
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 14080

[startup+190.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2908 0 0 0 18944 23 0 0 25 0 1 0 1855628596 12324864 2895 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3009 2895 145 145 0 2864 0
[pid=3779] vsize: 12036
Current children cumulated CPU time (s) 189.68
Current children cumulated vsize (Kb) 14160

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2908 0 0 0 19944 24 0 0 25 0 1 0 1855628596 12324864 2895 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3009 2895 145 145 0 2864 0
[pid=3779] vsize: 12036
Current children cumulated CPU time (s) 199.69
Current children cumulated vsize (Kb) 14160

[startup+210.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 2941 0 0 0 20943 24 0 0 25 0 1 0 1855628596 12460032 2928 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3042 2928 145 145 0 2897 0
[pid=3779] vsize: 12168
Current children cumulated CPU time (s) 209.68
Current children cumulated vsize (Kb) 14292

[startup+220.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3125 0 0 0 21939 26 0 0 25 0 1 0 1855628596 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3226 3112 145 145 0 3081 0
[pid=3779] vsize: 12904
Current children cumulated CPU time (s) 219.66
Current children cumulated vsize (Kb) 15028

[startup+230.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3125 0 0 0 22939 26 0 0 25 0 1 0 1855628596 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3226 3112 145 145 0 3081 0
[pid=3779] vsize: 12904
Current children cumulated CPU time (s) 229.66
Current children cumulated vsize (Kb) 15028

[startup+240.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3125 0 0 0 23939 26 0 0 25 0 1 0 1855628596 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3226 3112 145 145 0 3081 0
[pid=3779] vsize: 12904
Current children cumulated CPU time (s) 239.66
Current children cumulated vsize (Kb) 15028

[startup+250.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 24938 26 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 249.65
Current children cumulated vsize (Kb) 15240

[startup+260.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 25938 26 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 259.65
Current children cumulated vsize (Kb) 15240

[startup+270.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 26938 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 269.66
Current children cumulated vsize (Kb) 15240

[startup+280.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 27938 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223104 134556487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 279.66
Current children cumulated vsize (Kb) 15240

[startup+290.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 28938 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 289.66
Current children cumulated vsize (Kb) 15240

[startup+300.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 29938 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 299.66
Current children cumulated vsize (Kb) 15240

[startup+310.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 30939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 309.67
Current children cumulated vsize (Kb) 15240

[startup+320.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 31939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 319.67
Current children cumulated vsize (Kb) 15240

[startup+330.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 32939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 329.67
Current children cumulated vsize (Kb) 15240

[startup+340.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 33939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 339.67
Current children cumulated vsize (Kb) 15240

[startup+350.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 34939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 349.67
Current children cumulated vsize (Kb) 15240

[startup+360.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 35939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 359.67
Current children cumulated vsize (Kb) 15240

[startup+370.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 36939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 369.67
Current children cumulated vsize (Kb) 15240

[startup+380.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 37939 27 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 379.67
Current children cumulated vsize (Kb) 15240

[startup+390.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 38938 29 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 389.68
Current children cumulated vsize (Kb) 15240

[startup+400.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 39937 30 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 399.68
Current children cumulated vsize (Kb) 15240

[startup+410.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 40937 30 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 409.68
Current children cumulated vsize (Kb) 15240

[startup+420.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 41937 30 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 419.68
Current children cumulated vsize (Kb) 15240

[startup+430.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 42937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 429.69
Current children cumulated vsize (Kb) 15240

[startup+440.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 43937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 439.69
Current children cumulated vsize (Kb) 15240

[startup+450.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 44937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 449.69
Current children cumulated vsize (Kb) 15240

[startup+460.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 45937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 459.69
Current children cumulated vsize (Kb) 15240

[startup+470.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 46937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 469.69
Current children cumulated vsize (Kb) 15240

[startup+480.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 47937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 479.69
Current children cumulated vsize (Kb) 15240

[startup+490.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 48937 31 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 489.69
Current children cumulated vsize (Kb) 15240

[startup+500.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 49937 32 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 499.7
Current children cumulated vsize (Kb) 15240

[startup+510.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 50938 32 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 509.71
Current children cumulated vsize (Kb) 15240

[startup+520.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 51938 32 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 519.71
Current children cumulated vsize (Kb) 15240

[startup+530.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 52938 32 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 529.71
Current children cumulated vsize (Kb) 15240

[startup+540.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3178 0 0 0 53938 32 0 0 25 0 1 0 1855628596 13430784 3165 4294967295 134512640 135094434 3221224432 3221223104 134555795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3165 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 539.71
Current children cumulated vsize (Kb) 15240

[startup+550.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 54938 32 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 549.71
Current children cumulated vsize (Kb) 15240

[startup+560.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 55938 32 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 559.71
Current children cumulated vsize (Kb) 15240

[startup+570.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 56938 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 569.72
Current children cumulated vsize (Kb) 15240

[startup+580.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 57938 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223044 134563024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 579.72
Current children cumulated vsize (Kb) 15240

[startup+590.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 58939 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 589.73
Current children cumulated vsize (Kb) 15240

[startup+600.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 59939 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 599.73
Current children cumulated vsize (Kb) 15240

[startup+610.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 60939 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 609.73
Current children cumulated vsize (Kb) 15240

[startup+620.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 61939 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 619.73
Current children cumulated vsize (Kb) 15240

[startup+630.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 62939 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 629.73
Current children cumulated vsize (Kb) 15240

[startup+640.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 63939 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 639.73
Current children cumulated vsize (Kb) 15240

[startup+650.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 64940 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 649.74
Current children cumulated vsize (Kb) 15240

[startup+660.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 65940 33 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 659.74
Current children cumulated vsize (Kb) 15240

[startup+670.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 66940 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 669.75
Current children cumulated vsize (Kb) 15240

[startup+680.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 67940 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 679.75
Current children cumulated vsize (Kb) 15240

[startup+690.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 68940 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 689.75
Current children cumulated vsize (Kb) 15240

[startup+700.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 69940 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 699.75
Current children cumulated vsize (Kb) 15240

[startup+710.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 70941 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 709.76
Current children cumulated vsize (Kb) 15240

[startup+720.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 71941 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 719.76
Current children cumulated vsize (Kb) 15240

[startup+730.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 72941 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 729.76
Current children cumulated vsize (Kb) 15240

[startup+740.063 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 73941 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 739.76
Current children cumulated vsize (Kb) 15240

[startup+750.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3180 0 0 0 74941 34 0 0 25 0 1 0 1855628596 13430784 3167 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3167 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 749.76
Current children cumulated vsize (Kb) 15240

[startup+760.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3182 0 0 0 75941 34 0 0 25 0 1 0 1855628596 13430784 3169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3169 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 759.76
Current children cumulated vsize (Kb) 15240

[startup+770.065 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3183 0 0 0 76942 34 0 0 25 0 1 0 1855628596 13430784 3170 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3170 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 769.77
Current children cumulated vsize (Kb) 15240

[startup+780.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3183 0 0 0 77942 34 0 0 25 0 1 0 1855628596 13430784 3170 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3279 3170 145 145 0 3134 0
[pid=3779] vsize: 13116
Current children cumulated CPU time (s) 779.77
Current children cumulated vsize (Kb) 15240

[startup+790.067 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3302 0 0 0 78940 35 0 0 25 0 1 0 1855628596 13918208 3289 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3398 3289 145 145 0 3253 0
[pid=3779] vsize: 13592
Current children cumulated CPU time (s) 789.76
Current children cumulated vsize (Kb) 15716

[startup+800.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3485 0 0 0 79937 37 0 0 25 0 1 0 1855628596 14667776 3472 4294967295 134512640 135094434 3221224432 3221223104 134556210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3581 3472 145 145 0 3436 0
[pid=3779] vsize: 14324
Current children cumulated CPU time (s) 799.75
Current children cumulated vsize (Kb) 16448

[startup+810.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3488 0 0 0 80937 37 0 0 25 0 1 0 1855628596 14684160 3475 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3585 3475 145 145 0 3440 0
[pid=3779] vsize: 14340
Current children cumulated CPU time (s) 809.75
Current children cumulated vsize (Kb) 16464

[startup+820.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3505 0 0 0 81937 37 0 0 25 0 1 0 1855628596 14766080 3492 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3605 3492 145 145 0 3460 0
[pid=3779] vsize: 14420
Current children cumulated CPU time (s) 819.75
Current children cumulated vsize (Kb) 16544

[startup+830.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3507 0 0 0 82937 37 0 0 25 0 1 0 1855628596 14766080 3494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3605 3494 145 145 0 3460 0
[pid=3779] vsize: 14420
Current children cumulated CPU time (s) 829.75
Current children cumulated vsize (Kb) 16544

[startup+840.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3508 0 0 0 83938 37 0 0 25 0 1 0 1855628596 14766080 3495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3605 3495 145 145 0 3460 0
[pid=3779] vsize: 14420
Current children cumulated CPU time (s) 839.76
Current children cumulated vsize (Kb) 16544

[startup+850.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3509 0 0 0 84938 37 0 0 25 0 1 0 1855628596 14766080 3496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3605 3496 145 145 0 3460 0
[pid=3779] vsize: 14420
Current children cumulated CPU time (s) 849.76
Current children cumulated vsize (Kb) 16544

[startup+860.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3509 0 0 0 85938 37 0 0 25 0 1 0 1855628596 14766080 3496 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 3605 3496 145 145 0 3460 0
[pid=3779] vsize: 14420
Current children cumulated CPU time (s) 859.76
Current children cumulated vsize (Kb) 16544

[startup+870.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3509 0 0 0 86937 38 0 0 25 0 1 0 1855628596 14766080 3496 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3605 3496 145 145 0 3460 0
[pid=3779] vsize: 14420
Current children cumulated CPU time (s) 869.76
Current children cumulated vsize (Kb) 16544

[startup+880.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3547 0 0 0 87937 38 0 0 25 0 1 0 1855628596 15044608 3534 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3673 3534 145 145 0 3528 0
[pid=3779] vsize: 14692
Current children cumulated CPU time (s) 879.76
Current children cumulated vsize (Kb) 16816

[startup+890.076 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3560 0 0 0 88937 38 0 0 25 0 1 0 1855628596 15126528 3547 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3693 3547 145 145 0 3548 0
[pid=3779] vsize: 14772
Current children cumulated CPU time (s) 889.76
Current children cumulated vsize (Kb) 16896

[startup+900.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3566 0 0 0 89937 38 0 0 25 0 1 0 1855628596 15142912 3553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3697 3553 145 145 0 3552 0
[pid=3779] vsize: 14788
Current children cumulated CPU time (s) 899.76
Current children cumulated vsize (Kb) 16912

[startup+910.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3643 0 0 0 90936 39 0 0 25 0 1 0 1855628596 15474688 3630 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 3778 3630 145 145 0 3633 0
[pid=3779] vsize: 15112
Current children cumulated CPU time (s) 909.76
Current children cumulated vsize (Kb) 17236

[startup+920.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3892 0 0 0 91933 40 0 0 25 0 1 0 1855628596 16490496 3879 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4026 3879 145 145 0 3881 0
[pid=3779] vsize: 16104
Current children cumulated CPU time (s) 919.74
Current children cumulated vsize (Kb) 18228

[startup+930.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3892 0 0 0 92933 40 0 0 25 0 1 0 1855628596 16490496 3879 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4026 3879 145 145 0 3881 0
[pid=3779] vsize: 16104
Current children cumulated CPU time (s) 929.74
Current children cumulated vsize (Kb) 18228

[startup+940.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3915 0 0 0 93933 40 0 0 25 0 1 0 1855628596 16621568 3902 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4058 3902 145 145 0 3913 0
[pid=3779] vsize: 16232
Current children cumulated CPU time (s) 939.74
Current children cumulated vsize (Kb) 18356

[startup+950.081 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3922 0 0 0 94934 40 0 0 25 0 1 0 1855628596 16654336 3909 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4066 3909 145 145 0 3921 0
[pid=3779] vsize: 16264
Current children cumulated CPU time (s) 949.75
Current children cumulated vsize (Kb) 18388

[startup+960.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 3988 0 0 0 95932 41 0 0 25 0 1 0 1855628596 16916480 3975 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4130 3975 145 145 0 3985 0
[pid=3779] vsize: 16520
Current children cumulated CPU time (s) 959.74
Current children cumulated vsize (Kb) 18644

[startup+970.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4016 0 0 0 96932 42 0 0 25 0 1 0 1855628596 17039360 4003 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4160 4003 145 145 0 4015 0
[pid=3779] vsize: 16640
Current children cumulated CPU time (s) 969.75
Current children cumulated vsize (Kb) 18764

[startup+980.083 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4016 0 0 0 97932 42 0 0 25 0 1 0 1855628596 17039360 4003 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4160 4003 145 145 0 4015 0
[pid=3779] vsize: 16640
Current children cumulated CPU time (s) 979.75
Current children cumulated vsize (Kb) 18764

[startup+990.084 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4035 0 0 0 98930 43 0 0 25 0 1 0 1855628596 17137664 4022 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4184 4022 145 145 0 4039 0
[pid=3779] vsize: 16736
Current children cumulated CPU time (s) 989.74
Current children cumulated vsize (Kb) 18860

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4061 0 0 0 99929 44 0 0 25 0 1 0 1855628596 17235968 4048 4294967295 134512640 135094434 3221224432 3221222096 134562841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4208 4048 145 145 0 4063 0
[pid=3779] vsize: 16832
Current children cumulated CPU time (s) 999.74
Current children cumulated vsize (Kb) 18956

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4061 0 0 0 100929 45 0 0 25 0 1 0 1855628596 17235968 4048 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4208 4048 145 145 0 4063 0
[pid=3779] vsize: 16832
Current children cumulated CPU time (s) 1009.75
Current children cumulated vsize (Kb) 18956

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4064 0 0 0 101929 45 0 0 25 0 1 0 1855628596 17252352 4051 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4212 4051 145 145 0 4067 0
[pid=3779] vsize: 16848
Current children cumulated CPU time (s) 1019.75
Current children cumulated vsize (Kb) 18972

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4072 0 0 0 102929 45 0 0 25 0 1 0 1855628596 17285120 4059 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4220 4059 145 145 0 4075 0
[pid=3779] vsize: 16880
Current children cumulated CPU time (s) 1029.75
Current children cumulated vsize (Kb) 19004

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4152 0 0 0 103928 46 0 0 25 0 1 0 1855628596 17616896 4139 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4301 4139 145 145 0 4156 0
[pid=3779] vsize: 17204
Current children cumulated CPU time (s) 1039.75
Current children cumulated vsize (Kb) 19328

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4152 0 0 0 104927 47 0 0 25 0 1 0 1855628596 17616896 4139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3779/statm): 4301 4139 145 145 0 4156 0
[pid=3779] vsize: 17204
Current children cumulated CPU time (s) 1049.75
Current children cumulated vsize (Kb) 19328

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4152 0 0 0 105927 47 0 0 25 0 1 0 1855628596 17616896 4139 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4301 4139 145 145 0 4156 0
[pid=3779] vsize: 17204
Current children cumulated CPU time (s) 1059.75
Current children cumulated vsize (Kb) 19328

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4155 0 0 0 106927 47 0 0 25 0 1 0 1855628596 17633280 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4305 4142 145 145 0 4160 0
[pid=3779] vsize: 17220
Current children cumulated CPU time (s) 1069.75
Current children cumulated vsize (Kb) 19344

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4284 0 0 0 107924 48 0 0 25 0 1 0 1855628596 18145280 4271 4294967295 134512640 135094434 3221224432 3221223104 134555590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4430 4271 145 145 0 4285 0
[pid=3779] vsize: 17720
Current children cumulated CPU time (s) 1079.73
Current children cumulated vsize (Kb) 19844

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4295 0 0 0 108925 48 0 0 25 0 1 0 1855628596 18190336 4282 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4441 4282 145 145 0 4296 0
[pid=3779] vsize: 17764
Current children cumulated CPU time (s) 1089.74
Current children cumulated vsize (Kb) 19888

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4295 0 0 0 109924 48 0 0 25 0 1 0 1855628596 18190336 4282 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4441 4282 145 145 0 4296 0
[pid=3779] vsize: 17764
Current children cumulated CPU time (s) 1099.73
Current children cumulated vsize (Kb) 19888

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4298 0 0 0 110924 48 0 0 25 0 1 0 1855628596 18202624 4285 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4444 4285 145 145 0 4299 0
[pid=3779] vsize: 17776
Current children cumulated CPU time (s) 1109.73
Current children cumulated vsize (Kb) 19900

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4301 0 0 0 111925 48 0 0 25 0 1 0 1855628596 18219008 4288 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4448 4288 145 145 0 4303 0
[pid=3779] vsize: 17792
Current children cumulated CPU time (s) 1119.74
Current children cumulated vsize (Kb) 19916

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4301 0 0 0 112924 49 0 0 25 0 1 0 1855628596 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4448 4288 145 145 0 4303 0
[pid=3779] vsize: 17792
Current children cumulated CPU time (s) 1129.74
Current children cumulated vsize (Kb) 19916

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4301 0 0 0 113925 49 0 0 25 0 1 0 1855628596 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4448 4288 145 145 0 4303 0
[pid=3779] vsize: 17792
Current children cumulated CPU time (s) 1139.75
Current children cumulated vsize (Kb) 19916

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4301 0 0 0 114925 49 0 0 25 0 1 0 1855628596 18219008 4288 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4448 4288 145 145 0 4303 0
[pid=3779] vsize: 17792
Current children cumulated CPU time (s) 1149.75
Current children cumulated vsize (Kb) 19916

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4319 0 0 0 115925 49 0 0 25 0 1 0 1855628596 18317312 4306 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4472 4306 145 145 0 4327 0
[pid=3779] vsize: 17888
Current children cumulated CPU time (s) 1159.75
Current children cumulated vsize (Kb) 20012

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4321 0 0 0 116925 49 0 0 25 0 1 0 1855628596 18317312 4308 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4472 4308 145 145 0 4327 0
[pid=3779] vsize: 17888
Current children cumulated CPU time (s) 1169.75
Current children cumulated vsize (Kb) 20012

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4321 0 0 0 117925 49 0 0 25 0 1 0 1855628596 18317312 4308 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4472 4308 145 145 0 4327 0
[pid=3779] vsize: 17888
Current children cumulated CPU time (s) 1179.75
Current children cumulated vsize (Kb) 20012

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4335 0 0 0 118925 49 0 0 25 0 1 0 1855628596 18382848 4322 4294967295 134512640 135094434 3221224432 3221223104 134556394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4488 4322 145 145 0 4343 0
[pid=3779] vsize: 17952
Current children cumulated CPU time (s) 1189.75
Current children cumulated vsize (Kb) 20076

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4348 0 0 0 119926 49 0 0 25 0 1 0 1855628596 18448384 4335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4504 4335 145 145 0 4359 0
[pid=3779] vsize: 18016
Current children cumulated CPU time (s) 1199.76
Current children cumulated vsize (Kb) 20140

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4350 0 0 0 120925 50 0 0 25 0 1 0 1855628596 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4504 4337 145 145 0 4359 0
[pid=3779] vsize: 18016
Current children cumulated CPU time (s) 1209.76
Current children cumulated vsize (Kb) 20140



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3779
Raw data (/proc/3775/stat): 3775 (minisat+_script) S 3774 3775 5245 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855628591 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3775/statm): 531 226 485 147 0 384 0
[pid=3775] vsize: 2124
Raw data (/proc/3779/stat): 3779 (minisat+_64-bit) R 3775 3775 5245 0 -1 0 4350 0 0 0 120926 50 0 0 25 0 1 0 1855628596 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3779/statm): 4504 4337 145 145 0 4359 0
[pid=3779] vsize: 18016
Current children cumulated CPU time (s) 1209.77
Current children cumulated vsize (Kb) 20140

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.77
CPU user time (s): 1209.26
CPU system time (s): 0.511922
CPU usage (%): 99.9716
Max. virtual memory (cumulated for all children) (Kb): 20140

Verifier Data

ERROR: no interpretation found !