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/miplib2003/normalized-mps-v2-13-7-markshare2.opb
MD5SUM3b5121187baf09367bd50bdc4d869d21
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 6138

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        921316 kB
Buffers:         16344 kB
Cached:          67624 kB
SwapCached:        692 kB
Active:          24108 kB
Inactive:        62424 kB
HighTotal:      131008 kB
HighFree:        61096 kB
LowTotal:       903652 kB
LowFree:        860220 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            20996 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:03:01 (client local time) WITH STATUS 10 IN 1209.87 SECONDS
stats: 3301 7 1209.87 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/27842/stat): 27842 (minisat+_script) R 27841 27842 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855368781 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27842/statm): 174 3 169 147 0 27 0
[pid=27842] 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=27843
New process pid=27844
New process pid=27845
execve syscall for /bin/sed executable
One traced child (pid=27844) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=27845) exited with status: 0
One traced child (pid=27843) exited with status: 0
New process pid=27846
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare2.opb

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1115 0 0 0 979 6 0 0 25 0 1 0 1855368786 4968448 1102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27846/statm): 1213 1102 145 145 0 1068 0
[pid=27846] vsize: 4852
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 6976

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1293 0 0 0 1976 7 0 0 25 0 1 0 1855368786 5685248 1280 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 1388 1280 145 145 0 1243 0
[pid=27846] vsize: 5552
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 7676

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1590 0 0 0 2970 10 0 0 25 0 1 0 1855368786 6918144 1577 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 1689 1577 145 145 0 1544 0
[pid=27846] vsize: 6756
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 8880

[startup+40.0079 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 1952 0 0 0 3962 13 0 0 25 0 1 0 1855368786 8388608 1939 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2048 1939 145 145 0 1903 0
[pid=27846] vsize: 8192
Current children cumulated CPU time (s) 39.76
Current children cumulated vsize (Kb) 10316

[startup+50.0087 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2282 0 0 0 4955 16 0 0 25 0 1 0 1855368786 9736192 2269 4294967295 134512640 135094434 3221224432 3221223056 134562068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2377 2269 145 145 0 2232 0
[pid=27846] vsize: 9508
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 11632

[startup+60.0095 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 5951 18 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223220 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0
[pid=27846] vsize: 10360
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 12484

[startup+70.0104 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 6951 19 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0
[pid=27846] vsize: 10360
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 12484

[startup+80.0122 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 7950 19 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0
[pid=27846] vsize: 10360
Current children cumulated CPU time (s) 79.7
Current children cumulated vsize (Kb) 12484

[startup+90.0131 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2481 0 0 0 8950 19 0 0 25 0 1 0 1855368786 10608640 2468 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2468 145 145 0 2445 0
[pid=27846] vsize: 10360
Current children cumulated CPU time (s) 89.7
Current children cumulated vsize (Kb) 12484

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2483 0 0 0 9950 19 0 0 25 0 1 0 1855368786 10608640 2470 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2470 145 145 0 2445 0
[pid=27846] vsize: 10360
Current children cumulated CPU time (s) 99.7
Current children cumulated vsize (Kb) 12484

[startup+110.016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2483 0 0 0 10950 20 0 0 25 0 1 0 1855368786 10608640 2470 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2470 145 145 0 2445 0
[pid=27846] vsize: 10360
Current children cumulated CPU time (s) 109.71
Current children cumulated vsize (Kb) 12484

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2485 0 0 0 11951 20 0 0 25 0 1 0 1855368786 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2472 145 145 0 2445 0
[pid=27846] 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.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2485 0 0 0 12951 20 0 0 25 0 1 0 1855368786 10608640 2472 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2472 145 145 0 2445 0
[pid=27846] 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.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2485 0 0 0 13951 20 0 0 25 0 1 0 1855368786 10608640 2472 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2590 2472 145 145 0 2445 0
[pid=27846] 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.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2552 0 0 0 14950 20 0 0 25 0 1 0 1855368786 10874880 2539 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2655 2539 145 145 0 2510 0
[pid=27846] vsize: 10620
Current children cumulated CPU time (s) 149.71
Current children cumulated vsize (Kb) 12744

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2558 0 0 0 15950 20 0 0 25 0 1 0 1855368786 10899456 2545 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2661 2545 145 145 0 2516 0
[pid=27846] vsize: 10644
Current children cumulated CPU time (s) 159.71
Current children cumulated vsize (Kb) 12768

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2591 0 0 0 16949 21 0 0 25 0 1 0 1855368786 11034624 2578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 2694 2578 145 145 0 2549 0
[pid=27846] vsize: 10776
Current children cumulated CPU time (s) 169.71
Current children cumulated vsize (Kb) 12900

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2908 0 0 0 17944 23 0 0 25 0 1 0 1855368786 12324864 2895 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3009 2895 145 145 0 2864 0
[pid=27846] vsize: 12036
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 14160

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2908 0 0 0 18944 23 0 0 25 0 1 0 1855368786 12324864 2895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3009 2895 145 145 0 2864 0
[pid=27846] vsize: 12036
Current children cumulated CPU time (s) 189.68
Current children cumulated vsize (Kb) 14160

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2908 0 0 0 19944 23 0 0 25 0 1 0 1855368786 12324864 2895 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3009 2895 145 145 0 2864 0
[pid=27846] vsize: 12036
Current children cumulated CPU time (s) 199.68
Current children cumulated vsize (Kb) 14160

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 2997 0 0 0 20943 24 0 0 25 0 1 0 1855368786 12689408 2984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3098 2984 145 145 0 2953 0
[pid=27846] vsize: 12392
Current children cumulated CPU time (s) 209.68
Current children cumulated vsize (Kb) 14516

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3125 0 0 0 21940 25 0 0 25 0 1 0 1855368786 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3226 3112 145 145 0 3081 0
[pid=27846] vsize: 12904
Current children cumulated CPU time (s) 219.66
Current children cumulated vsize (Kb) 15028

[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3125 0 0 0 22940 25 0 0 25 0 1 0 1855368786 13213696 3112 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3226 3112 145 145 0 3081 0
[pid=27846] vsize: 12904
Current children cumulated CPU time (s) 229.66
Current children cumulated vsize (Kb) 15028

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3125 0 0 0 23941 25 0 0 25 0 1 0 1855368786 13213696 3112 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3226 3112 145 145 0 3081 0
[pid=27846] vsize: 12904
Current children cumulated CPU time (s) 239.67
Current children cumulated vsize (Kb) 15028

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 24940 26 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 249.67
Current children cumulated vsize (Kb) 15240

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 25939 26 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 259.66
Current children cumulated vsize (Kb) 15240

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 26939 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 269.67
Current children cumulated vsize (Kb) 15240

[startup+280.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 27940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 279.68
Current children cumulated vsize (Kb) 15240

[startup+290.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 28940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 289.68
Current children cumulated vsize (Kb) 15240

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 29940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 299.68
Current children cumulated vsize (Kb) 15240

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 30940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 309.68
Current children cumulated vsize (Kb) 15240

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 31940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 319.68
Current children cumulated vsize (Kb) 15240

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 32940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 329.68
Current children cumulated vsize (Kb) 15240

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 33940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 339.68
Current children cumulated vsize (Kb) 15240

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 34940 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 349.68
Current children cumulated vsize (Kb) 15240

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 35941 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 359.69
Current children cumulated vsize (Kb) 15240

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27846
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 36941 27 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 369.69
Current children cumulated vsize (Kb) 15240

[startup+380.04 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 37940 28 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223104 134556468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 379.69
Current children cumulated vsize (Kb) 15240

[startup+390.041 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 38940 28 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 389.69
Current children cumulated vsize (Kb) 15240

[startup+400.042 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 39940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 399.7
Current children cumulated vsize (Kb) 15240

[startup+410.042 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 40940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 409.7
Current children cumulated vsize (Kb) 15240

[startup+420.043 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 41940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 419.7
Current children cumulated vsize (Kb) 15240

[startup+430.044 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 42940 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223104 134555563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 429.7
Current children cumulated vsize (Kb) 15240

[startup+440.045 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 27897
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 43941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 439.71
Current children cumulated vsize (Kb) 15240

[startup+450.045 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 44941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 449.71
Current children cumulated vsize (Kb) 15240

[startup+460.046 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 45941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 459.71
Current children cumulated vsize (Kb) 15240

[startup+470.046 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 46941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 469.71
Current children cumulated vsize (Kb) 15240

[startup+480.047 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 47941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 479.71
Current children cumulated vsize (Kb) 15240

[startup+490.048 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 48941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 489.71
Current children cumulated vsize (Kb) 15240

[startup+500.049 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 49941 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 499.71
Current children cumulated vsize (Kb) 15240

[startup+510.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 50942 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 509.72
Current children cumulated vsize (Kb) 15240

[startup+520.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 51942 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 519.72
Current children cumulated vsize (Kb) 15240

[startup+530.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3178 0 0 0 52942 29 0 0 25 0 1 0 1855368786 13430784 3165 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3165 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 529.72
Current children cumulated vsize (Kb) 15240

[startup+540.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 53943 29 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 539.73
Current children cumulated vsize (Kb) 15240

[startup+550.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 54943 29 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 549.73
Current children cumulated vsize (Kb) 15240

[startup+560.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 55943 30 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 559.74
Current children cumulated vsize (Kb) 15240

[startup+570.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 56943 30 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 569.74
Current children cumulated vsize (Kb) 15240

[startup+580.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 57942 30 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 579.73
Current children cumulated vsize (Kb) 15240

[startup+590.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 58942 31 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 589.74
Current children cumulated vsize (Kb) 15240

[startup+600.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 59942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 599.75
Current children cumulated vsize (Kb) 15240

[startup+610.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 60942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 609.75
Current children cumulated vsize (Kb) 15240

[startup+620.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 61942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 619.75
Current children cumulated vsize (Kb) 15240

[startup+630.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 62942 32 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223104 134556246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 629.75
Current children cumulated vsize (Kb) 15240

[startup+640.062 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 63942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 639.76
Current children cumulated vsize (Kb) 15240

[startup+650.063 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 64942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 649.76
Current children cumulated vsize (Kb) 15240

[startup+660.064 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 65942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 659.76
Current children cumulated vsize (Kb) 15240

[startup+670.065 s]
Raw data (loadavg): 1.20 1.03 0.93 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 66942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 669.76
Current children cumulated vsize (Kb) 15240

[startup+680.066 s]
Raw data (loadavg): 1.17 1.03 0.93 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 67942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 679.76
Current children cumulated vsize (Kb) 15240

[startup+690.066 s]
Raw data (loadavg): 1.14 1.03 0.93 2/57 27901
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 68942 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 689.76
Current children cumulated vsize (Kb) 15240

[startup+700.067 s]
Raw data (loadavg): 1.12 1.03 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 69943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 699.77
Current children cumulated vsize (Kb) 15240

[startup+710.068 s]
Raw data (loadavg): 1.10 1.03 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 70943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 709.77
Current children cumulated vsize (Kb) 15240

[startup+720.069 s]
Raw data (loadavg): 1.09 1.03 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 71943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 719.77
Current children cumulated vsize (Kb) 15240

[startup+730.07 s]
Raw data (loadavg): 1.07 1.03 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 72943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 729.77
Current children cumulated vsize (Kb) 15240

[startup+740.071 s]
Raw data (loadavg): 1.06 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3180 0 0 0 73943 33 0 0 25 0 1 0 1855368786 13430784 3167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3167 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 739.77
Current children cumulated vsize (Kb) 15240

[startup+750.07 s]
Raw data (loadavg): 1.05 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3183 0 0 0 74943 33 0 0 25 0 1 0 1855368786 13430784 3170 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3170 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 749.77
Current children cumulated vsize (Kb) 15240

[startup+760.072 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3183 0 0 0 75944 33 0 0 25 0 1 0 1855368786 13430784 3170 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3170 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 759.78
Current children cumulated vsize (Kb) 15240

[startup+770.073 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3183 0 0 0 76944 34 0 0 25 0 1 0 1855368786 13430784 3170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3279 3170 145 145 0 3134 0
[pid=27846] vsize: 13116
Current children cumulated CPU time (s) 769.79
Current children cumulated vsize (Kb) 15240

[startup+780.074 s]
Raw data (loadavg): 1.03 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3345 0 0 0 77941 34 0 0 25 0 1 0 1855368786 14094336 3332 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3441 3332 145 145 0 3296 0
[pid=27846] vsize: 13764
Current children cumulated CPU time (s) 779.76
Current children cumulated vsize (Kb) 15888

[startup+790.075 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3485 0 0 0 78939 36 0 0 25 0 1 0 1855368786 14667776 3472 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3581 3472 145 145 0 3436 0
[pid=27846] vsize: 14324
Current children cumulated CPU time (s) 789.76
Current children cumulated vsize (Kb) 16448

[startup+800.076 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3492 0 0 0 79939 36 0 0 25 0 1 0 1855368786 14700544 3479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3589 3479 145 145 0 3444 0
[pid=27846] vsize: 14356
Current children cumulated CPU time (s) 799.76
Current children cumulated vsize (Kb) 16480

[startup+810.076 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3505 0 0 0 80939 36 0 0 25 0 1 0 1855368786 14766080 3492 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3605 3492 145 145 0 3460 0
[pid=27846] vsize: 14420
Current children cumulated CPU time (s) 809.76
Current children cumulated vsize (Kb) 16544

[startup+820.077 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3508 0 0 0 81939 36 0 0 25 0 1 0 1855368786 14766080 3495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3605 3495 145 145 0 3460 0
[pid=27846] vsize: 14420
Current children cumulated CPU time (s) 819.76
Current children cumulated vsize (Kb) 16544

[startup+830.079 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3508 0 0 0 82939 36 0 0 25 0 1 0 1855368786 14766080 3495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3605 3495 145 145 0 3460 0
[pid=27846] vsize: 14420
Current children cumulated CPU time (s) 829.76
Current children cumulated vsize (Kb) 16544

[startup+840.08 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3509 0 0 0 83940 36 0 0 25 0 1 0 1855368786 14766080 3496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3605 3496 145 145 0 3460 0
[pid=27846] vsize: 14420
Current children cumulated CPU time (s) 839.77
Current children cumulated vsize (Kb) 16544

[startup+850.081 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3509 0 0 0 84939 36 0 0 25 0 1 0 1855368786 14766080 3496 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3605 3496 145 145 0 3460 0
[pid=27846] vsize: 14420
Current children cumulated CPU time (s) 849.76
Current children cumulated vsize (Kb) 16544

[startup+860.082 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3509 0 0 0 85940 36 0 0 25 0 1 0 1855368786 14766080 3496 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3605 3496 145 145 0 3460 0
[pid=27846] vsize: 14420
Current children cumulated CPU time (s) 859.77
Current children cumulated vsize (Kb) 16544

[startup+870.083 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3557 0 0 0 86939 36 0 0 25 0 1 0 1855368786 15093760 3544 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3685 3544 145 145 0 3540 0
[pid=27846] vsize: 14740
Current children cumulated CPU time (s) 869.76
Current children cumulated vsize (Kb) 16864

[startup+880.084 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3560 0 0 0 87940 36 0 0 25 0 1 0 1855368786 15126528 3547 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3693 3547 145 145 0 3548 0
[pid=27846] vsize: 14772
Current children cumulated CPU time (s) 879.77
Current children cumulated vsize (Kb) 16896

[startup+890.086 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3567 0 0 0 88940 36 0 0 25 0 1 0 1855368786 15142912 3554 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3697 3554 145 145 0 3552 0
[pid=27846] vsize: 14788
Current children cumulated CPU time (s) 889.77
Current children cumulated vsize (Kb) 16912

[startup+900.086 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3733 0 0 0 89938 37 0 0 25 0 1 0 1855368786 15843328 3720 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 3868 3720 145 145 0 3723 0
[pid=27846] vsize: 15472
Current children cumulated CPU time (s) 899.76
Current children cumulated vsize (Kb) 17596

[startup+910.087 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3892 0 0 0 90934 39 0 0 25 0 1 0 1855368786 16490496 3879 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4026 3879 145 145 0 3881 0
[pid=27846] vsize: 16104
Current children cumulated CPU time (s) 909.74
Current children cumulated vsize (Kb) 18228

[startup+920.087 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3898 0 0 0 91935 39 0 0 25 0 1 0 1855368786 16523264 3885 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4034 3885 145 145 0 3889 0
[pid=27846] vsize: 16136
Current children cumulated CPU time (s) 919.75
Current children cumulated vsize (Kb) 18260

[startup+930.089 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3917 0 0 0 92934 39 0 0 25 0 1 0 1855368786 16621568 3904 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4058 3904 145 145 0 3913 0
[pid=27846] vsize: 16232
Current children cumulated CPU time (s) 929.74
Current children cumulated vsize (Kb) 18356

[startup+940.09 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 3924 0 0 0 93935 39 0 0 25 0 1 0 1855368786 16654336 3911 4294967295 134512640 135094434 3221224432 3221223104 134555849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4066 3911 145 145 0 3921 0
[pid=27846] vsize: 16264
Current children cumulated CPU time (s) 939.75
Current children cumulated vsize (Kb) 18388

[startup+950.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4010 0 0 0 94934 39 0 0 25 0 1 0 1855368786 17006592 3997 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4152 3997 145 145 0 4007 0
[pid=27846] vsize: 16608
Current children cumulated CPU time (s) 949.74
Current children cumulated vsize (Kb) 18732

[startup+960.092 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4016 0 0 0 95934 39 0 0 25 0 1 0 1855368786 17039360 4003 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4160 4003 145 145 0 4015 0
[pid=27846] vsize: 16640
Current children cumulated CPU time (s) 959.74
Current children cumulated vsize (Kb) 18764

[startup+970.092 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4023 0 0 0 96934 39 0 0 25 0 1 0 1855368786 17072128 4010 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4168 4010 145 145 0 4023 0
[pid=27846] vsize: 16672
Current children cumulated CPU time (s) 969.74
Current children cumulated vsize (Kb) 18796

[startup+980.093 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4036 0 0 0 97934 39 0 0 25 0 1 0 1855368786 17137664 4023 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4184 4023 145 145 0 4039 0
[pid=27846] vsize: 16736
Current children cumulated CPU time (s) 979.74
Current children cumulated vsize (Kb) 18860

[startup+990.094 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4061 0 0 0 98934 40 0 0 25 0 1 0 1855368786 17235968 4048 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4208 4048 145 145 0 4063 0
[pid=27846] vsize: 16832
Current children cumulated CPU time (s) 989.75
Current children cumulated vsize (Kb) 18956

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4061 0 0 0 99934 40 0 0 25 0 1 0 1855368786 17235968 4048 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4208 4048 145 145 0 4063 0
[pid=27846] vsize: 16832
Current children cumulated CPU time (s) 999.75
Current children cumulated vsize (Kb) 18956

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4071 0 0 0 100934 40 0 0 25 0 1 0 1855368786 17285120 4058 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4220 4058 145 145 0 4075 0
[pid=27846] vsize: 16880
Current children cumulated CPU time (s) 1009.75
Current children cumulated vsize (Kb) 19004

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4073 0 0 0 101934 40 0 0 25 0 1 0 1855368786 17285120 4060 4294967295 134512640 135094434 3221224432 3221223104 134556236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4220 4060 145 145 0 4075 0
[pid=27846] vsize: 16880
Current children cumulated CPU time (s) 1019.75
Current children cumulated vsize (Kb) 19004

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4152 0 0 0 102932 41 0 0 25 0 1 0 1855368786 17616896 4139 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27846/statm): 4301 4139 145 145 0 4156 0
[pid=27846] vsize: 17204
Current children cumulated CPU time (s) 1029.74
Current children cumulated vsize (Kb) 19328

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4152 0 0 0 103931 41 0 0 25 0 1 0 1855368786 17616896 4139 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4301 4139 145 145 0 4156 0
[pid=27846] vsize: 17204
Current children cumulated CPU time (s) 1039.73
Current children cumulated vsize (Kb) 19328

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4155 0 0 0 104932 41 0 0 25 0 1 0 1855368786 17633280 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4305 4142 145 145 0 4160 0
[pid=27846] vsize: 17220
Current children cumulated CPU time (s) 1049.74
Current children cumulated vsize (Kb) 19344

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4157 0 0 0 105932 41 0 0 25 0 1 0 1855368786 17633280 4144 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4305 4144 145 145 0 4160 0
[pid=27846] vsize: 17220
Current children cumulated CPU time (s) 1059.74
Current children cumulated vsize (Kb) 19344

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4295 0 0 0 106929 42 0 0 25 0 1 0 1855368786 18190336 4282 4294967295 134512640 135094434 3221224432 3221223104 134555787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4441 4282 145 145 0 4296 0
[pid=27846] vsize: 17764
Current children cumulated CPU time (s) 1069.72
Current children cumulated vsize (Kb) 19888

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4295 0 0 0 107929 42 0 0 25 0 1 0 1855368786 18190336 4282 4294967295 134512640 135094434 3221224432 3221223104 134554886 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4441 4282 145 145 0 4296 0
[pid=27846] vsize: 17764
Current children cumulated CPU time (s) 1079.72
Current children cumulated vsize (Kb) 19888

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4298 0 0 0 108930 42 0 0 25 0 1 0 1855368786 18202624 4285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4444 4285 145 145 0 4299 0
[pid=27846] vsize: 17776
Current children cumulated CPU time (s) 1089.73
Current children cumulated vsize (Kb) 19900

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4298 0 0 0 109930 42 0 0 25 0 1 0 1855368786 18202624 4285 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4444 4285 145 145 0 4299 0
[pid=27846] vsize: 17776
Current children cumulated CPU time (s) 1099.73
Current children cumulated vsize (Kb) 19900

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 110930 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0
[pid=27846] vsize: 17792
Current children cumulated CPU time (s) 1109.73
Current children cumulated vsize (Kb) 19916

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 111930 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0
[pid=27846] vsize: 17792
Current children cumulated CPU time (s) 1119.73
Current children cumulated vsize (Kb) 19916

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 112930 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0
[pid=27846] vsize: 17792
Current children cumulated CPU time (s) 1129.73
Current children cumulated vsize (Kb) 19916

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4301 0 0 0 113931 42 0 0 25 0 1 0 1855368786 18219008 4288 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4448 4288 145 145 0 4303 0
[pid=27846] vsize: 17792
Current children cumulated CPU time (s) 1139.74
Current children cumulated vsize (Kb) 19916

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4320 0 0 0 114931 43 0 0 25 0 1 0 1855368786 18317312 4307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4472 4307 145 145 0 4327 0
[pid=27846] vsize: 17888
Current children cumulated CPU time (s) 1149.75
Current children cumulated vsize (Kb) 20012

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4321 0 0 0 115931 43 0 0 25 0 1 0 1855368786 18317312 4308 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4472 4308 145 145 0 4327 0
[pid=27846] vsize: 17888
Current children cumulated CPU time (s) 1159.75
Current children cumulated vsize (Kb) 20012

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4327 0 0 0 116931 43 0 0 25 0 1 0 1855368786 18350080 4314 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4480 4314 145 145 0 4335 0
[pid=27846] vsize: 17920
Current children cumulated CPU time (s) 1169.75
Current children cumulated vsize (Kb) 20044

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4348 0 0 0 117930 44 0 0 25 0 1 0 1855368786 18448384 4335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4504 4335 145 145 0 4359 0
[pid=27846] vsize: 18016
Current children cumulated CPU time (s) 1179.75
Current children cumulated vsize (Kb) 20140

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 118930 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0
[pid=27846] vsize: 18016
Current children cumulated CPU time (s) 1189.76
Current children cumulated vsize (Kb) 20140

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 119939 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0
[pid=27846] vsize: 18016
Current children cumulated CPU time (s) 1199.85
Current children cumulated vsize (Kb) 20140

[startup+1210.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 120939 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0
[pid=27846] vsize: 18016
Current children cumulated CPU time (s) 1209.85
Current children cumulated vsize (Kb) 20140



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 27903
Raw data (/proc/27842/stat): 27842 (minisat+_script) S 27841 27842 28974 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855368781 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27842/statm): 531 226 485 147 0 384 0
[pid=27842] vsize: 2124
Raw data (/proc/27846/stat): 27846 (minisat+_64-bit) R 27842 27842 28974 0 -1 0 4350 0 0 0 120939 45 0 0 25 0 1 0 1855368786 18448384 4337 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27846/statm): 4504 4337 145 145 0 4359 0
[pid=27846] vsize: 18016
Current children cumulated CPU time (s) 1209.85
Current children cumulated vsize (Kb) 20140

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

Child status: 10
Real time (s): 1210.22
CPU time (s): 1209.87
CPU user time (s): 1209.4
CPU system time (s): 0.465929
CPU usage (%): 99.9706
Max. virtual memory (cumulated for all children) (Kb): 20140

Verifier Data

ERROR: no interpretation found !