Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb
MD5SUMe6bff154156b54af3a9a38f7579209b6
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 15872
Optimality of the best value was proved NO
Number of terms in the objective function 163
Biggest coefficient in the objective function 1024
Number of bits for the biggest coefficient in the objective function 11
Sum of the numbers in the objective function 74742
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 8192
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 74742
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.13
Number of variables163
Total number of constraints126
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)56
Number of constraints which are nor clauses,nor cardinality constraints70
Minimum length of a constraint1
Maximum length of a constraint102

Trace number 5910

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916796 kB
Buffers:         33096 kB
Cached:          54336 kB
SwapCached:        492 kB
Active:          36052 kB
Inactive:        53972 kB
HighTotal:      131008 kB
HighFree:        74424 kB
LowTotal:       903652 kB
LowFree:        842372 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22064 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:09:40 (client local time) WITH STATUS 10 IN 1209.51 SECONDS
stats: 3089 7 1209.51 10

Solver Data

c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1471     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost: 1060     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1241     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1058     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1195     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost: 1020     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1259     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  130     Base:
c ---[   1]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  301     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 |         0 |   28562    68458 |    9520       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 62463
c ---[   0]---> Sorter-cost: 2662     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 |         3 |   34861    83214 |   11620       3       28     9.3 |  0.000 % |
c |       103 |   34861    83214 |   12782     103      670     6.5 |  0.366 % |
c |       253 |   34861    83214 |   14060     253     2273     9.0 |  0.366 % |
c |       479 |   34861    83214 |   15466     479     4345     9.1 |  0.366 % |
c ==============================================================================
c Found solution: 28022
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 |       581 |   35195    84026 |   11731     581     4989     8.6 |  0.366 % |
c ==============================================================================
c Found solution: 27718
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 |       614 |   35214    84093 |   11738     614     5230     8.5 |  0.366 % |
c ==============================================================================
c Found solution: 25668
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 |       679 |   35257    84224 |   11752     679     5833     8.6 |  0.366 % |
c ==============================================================================
c Found solution: 24642
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 |       748 |   35275    84271 |   11758     748     6397     8.6 |  0.366 % |
c ==============================================================================
c Found solution: 21602
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 |       754 |   35316    84375 |   11772     754     6433     8.5 |  0.366 % |
c ==============================================================================
c Found solution: 21588
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 |       811 |   35330    84412 |   11776     811     6969     8.6 |  0.366 % |
c |       911 |   35330    84412 |   12953     911     7622     8.4 |  0.408 % |
c |      1062 |   35330    84412 |   14248    1062     9064     8.5 |  0.408 % |
c ==============================================================================
c Found solution: 21586
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 |      1282 |   35340    84435 |   11780    1282    12314     9.6 |  0.408 % |
c ==============================================================================
c Found solution: 19478
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 |      1331 |   35365    84497 |   11788    1331    12873     9.7 |  0.408 % |
c |      1431 |   35365    84497 |   12966    1431    13984     9.8 |  0.417 % |
c |      1581 |   35365    84497 |   14263    1581    15343     9.7 |  0.417 % |
c |      1807 |   35365    84497 |   15689    1807    18631    10.3 |  0.417 % |
c |      2145 |   35365    84497 |   17258    2145    22255    10.4 |  0.417 % |
c |      2651 |   35365    84497 |   18984    2651    30097    11.4 |  0.417 % |
c ==============================================================================
c Found solution: 19442
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 |      3201 |   35373    84523 |   11791    3201    38247    11.9 |  0.417 % |
c |      3302 |   35373    84523 |   12970    3302    42625    12.9 |  0.422 % |
c |      3453 |   35373    84523 |   14267    3453    44963    13.0 |  0.422 % |
c ==============================================================================
c Found solution: 18497
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 |      3593 |   35380    84540 |   11793    3588    46216    12.9 |  0.422 % |
c |      3693 |   35380    84540 |   12972    3688    47161    12.8 |  0.441 % |
c |      3843 |   35376    84532 |   14269    3837    49398    12.9 |  0.450 % |
c |      4069 |   35376    84532 |   15696    4063    54615    13.4 |  0.450 % |
c |      4406 |   35376    84532 |   17266    4400    62454    14.2 |  0.450 % |
c |      4913 |   35376    84532 |   18992    4907    72842    14.8 |  0.450 % |
c ==============================================================================
c Found solution: 18496
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 |      5193 |   35369    84515 |   11789    5127    76175    14.9 |  0.450 % |
c |      5293 |   35369    84515 |   12967    5227    76920    14.7 |  0.492 % |
c |      5444 |   35369    84515 |   14264    5378    77796    14.5 |  0.492 % |
c |      5669 |   35369    84515 |   15691    5603    81751    14.6 |  0.492 % |
c |      6006 |   35369    84515 |   17260    5940    86807    14.6 |  0.492 % |
c ==============================================================================
c Found solution: 18479
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 |      6132 |   35377    84534 |   11792    6066    88960    14.7 |  0.492 % |
c |      6232 |   35377    84534 |   12971    6166    89891    14.6 |  0.497 % |
c |      6384 |   35376    84531 |   14268    6229    93681    15.0 |  0.501 % |
c |      6610 |   35376    84531 |   15695    6455    98851    15.3 |  0.501 % |
c |      6947 |   35376    84531 |   17264    6792   102991    15.2 |  0.501 % |
c ==============================================================================
c Found solution: 18478
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 |      7182 |   35386    84554 |   11795    7018   106716    15.2 |  0.501 % |
c |      7282 |   35386    84554 |   12974    7118   108642    15.3 |  0.510 % |
c |      7432 |   35386    84554 |   14271    7268   110081    15.1 |  0.510 % |
c |      7657 |   35386    84554 |   15699    7493   114199    15.2 |  0.510 % |
c ==============================================================================
c Found solution: 18454
c ---[   0]---> Sorter-cost:    2     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 |      7900 |   35383    84547 |   11794    7723   118775    15.4 |  0.510 % |
c |      8000 |   35383    84547 |   12973    7823   120762    15.4 |  0.548 % |
c |      8152 |   35383    84547 |   14270    7975   123675    15.5 |  0.548 % |
c ==============================================================================
c Found solution: 18444
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 |      8212 |   35395    84574 |   11798    8035   124725    15.5 |  0.548 % |
c ==============================================================================
c Found solution: 18442
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 |      8258 |   35406    84598 |   11802    8081   125191    15.5 |  0.548 % |
c ==============================================================================
c Found solution: 17417
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 |      8323 |   35430    84655 |   11810    8146   126409    15.5 |  0.548 % |
c ==============================================================================
c Found solution: 17416
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 |      8388 |   35442    84684 |   11814    8211   127824    15.6 |  0.548 % |
c |      8488 |   35442    84684 |   12995    8311   129724    15.6 |  0.585 % |
c |      8638 |   35425    84647 |   14294    8441   132371    15.7 |  0.631 % |
c ==============================================================================
c Found solution: 17415
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 |      8796 |   35433    84664 |   11811    8599   137170    16.0 |  0.631 % |
c ==============================================================================
c Found solution: 17414
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 |      8869 |   35440    84679 |   11813    8672   138705    16.0 |  0.631 % |
c |      8969 |   35440    84679 |   12994    8772   140927    16.1 |  0.640 % |
c |      9120 |   35440    84679 |   14293    8923   143280    16.1 |  0.641 % |
c |      9345 |   35440    84679 |   15723    9148   147150    16.1 |  0.640 % |
c ==============================================================================
c Found solution: 17413
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 |      9542 |   35450    84702 |   11816    9345   154406    16.5 |  0.640 % |
c |      9642 |   35450    84702 |   12997    9445   155445    16.5 |  0.645 % |
c |      9792 |   35444    84688 |   14297    9593   159836    16.7 |  0.664 % |
c ==============================================================================
c Found solution: 17412
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 |      9841 |   35451    84703 |   11817    9642   160546    16.7 |  0.664 % |
c ==============================================================================
c Found solution: 17411
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 |      9865 |   35461    84725 |   11820    9666   161146    16.7 |  0.664 % |
c |      9966 |   35461    84725 |   13002    9767   162491    16.6 |  0.673 % |
c |     10116 |   35460    84722 |   14302    9885   167135    16.9 |  0.678 % |
c ==============================================================================
c Found solution: 17410
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 |     10276 |   35467    84737 |   11822   10045   170200    16.9 |  0.678 % |
c |     10377 |   35467    84737 |   13004   10146   171182    16.9 |  0.682 % |
c ==============================================================================
c Found solution: 17409
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 |     10491 |   35474    84752 |   11824   10260   174333    17.0 |  0.682 % |
c ==============================================================================
c Found solution: 17408
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 |     10528 |   35479    84763 |   11826   10294   175434    17.0 |  0.682 % |
c |     10628 |   35479    84763 |   13008   10394   177101    17.0 |  0.696 % |
c |     10778 |   35477    84759 |   14309   10543   179233    17.0 |  0.701 % |
c |     11004 |   35477    84759 |   15740   10769   185541    17.2 |  0.701 % |
c |     11341 |   35477    84759 |   17314   11106   187815    16.9 |  0.701 % |
c ==============================================================================
c Found solution: 17318
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 |     11751 |   35489    84790 |   11829   11516   199908    17.4 |  0.701 % |
c |     11851 |   35489    84790 |   13011   11616   201664    17.4 |  0.705 % |
c |     12001 |   35489    84790 |   14313   11766   202751    17.2 |  0.705 % |
c |     12226 |   35489    84790 |   15744   11991   214489    17.9 |  0.705 % |
c |     12563 |   35489    84790 |   17318   12328   242106    19.6 |  0.705 % |
c |     13069 |   35488    84787 |   19050   12814   280719    21.9 |  0.710 % |
c |     13828 |   35486    84783 |   20955   13572   292108    21.5 |  0.715 % |
c |     14967 |   35486    84783 |   23051   14711   344167    23.4 |  0.715 % |
c ==============================================================================
c Found solution: 16613
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 |     15651 |   35494    84803 |   11831   15395   378123    24.6 |  0.715 % |
c |     15751 |   35494    84803 |   13014    7798   221350    28.4 |  0.719 % |
c |     15901 |   35494    84803 |   14315    7948   225362    28.4 |  0.719 % |
c |     16127 |   35494    84803 |   15747    8174   234611    28.7 |  0.719 % |
c |     16465 |   35494    84803 |   17321    8512   248038    29.1 |  0.719 % |
c |     16974 |   35494    84803 |   19053    9021   270699    30.0 |  0.719 % |
c ==============================================================================
c Found solution: 16389
c ---[   0]---> Sorter-cost:    2     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 |     17391 |   35503    84822 |   11834    9438   296263    31.4 |  0.719 % |
c |     17491 |   35503    84822 |   13017    9538   298646    31.3 |  0.724 % |
c |     17642 |   35503    84822 |   14319    9689   303656    31.3 |  0.724 % |
c |     17868 |   35503    84822 |   15751    9915   307827    31.0 |  0.724 % |
c |     18205 |   35498    84811 |   17326   10250   338402    33.0 |  0.738 % |
c |     18711 |   35498    84811 |   19058   10756   347783    32.3 |  0.738 % |
c ==============================================================================
c Found solution: 16388
c ---[   0]---> Sorter-cost:    2     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 |     19431 |   35506    84828 |   11835   11476   378534    33.0 |  0.738 % |
c |     19531 |   35506    84828 |   13018   11576   379899    32.8 |  0.742 % |
c |     19682 |   35506    84828 |   14320   11727   382261    32.6 |  0.742 % |
c |     19907 |   35506    84828 |   15752   11952   386048    32.3 |  0.742 % |
c |     20244 |   35506    84828 |   17327   12289   391868    31.9 |  0.742 % |
c |     20752 |   35506    84828 |   19060   12797   400846    31.3 |  0.742 % |
c |     21513 |   35506    84828 |   20966   13558   420260    31.0 |  0.742 % |
c ==============================================================================
c Found solution: 16386
c ---[   0]---> Sorter-cost:    2     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 |     22643 |   35514    84845 |   11838   14688   444209    30.2 |  0.742 % |
c |     22743 |   35514    84845 |   13021    7444   148246    19.9 |  0.747 % |
c |     22896 |   35514    84845 |   14323    7597   155471    20.5 |  0.747 % |
c |     23122 |   35514    84845 |   15756    7823   159906    20.4 |  0.747 % |
c |     23459 |   35514    84845 |   17332    8160   166784    20.4 |  0.747 % |
c |     23966 |   35511    84838 |   19065    8324   173446    20.8 |  0.756 % |
c |     24725 |   35511    84838 |   20971    9083   213515    23.5 |  0.756 % |
c ==============================================================================
c Found solution: 16385
c ---[   0]---> Sorter-cost:    2     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 |     24919 |   35519    84855 |   11839    9277   222451    24.0 |  0.756 % |
c |     25019 |   35519    84855 |   13022    9377   223734    23.9 |  0.761 % |
c |     25172 |   35519    84855 |   14325    9530   225560    23.7 |  0.761 % |
c |     25397 |   35519    84855 |   15757    9755   234476    24.0 |  0.761 % |
c |     25734 |   35519    84855 |   17333   10092   245223    24.3 |  0.761 % |
c |     26240 |   35519    84855 |   19066   10598   262188    24.7 |  0.761 % |
c |     26999 |   35519    84855 |   20973   11357   293708    25.9 |  0.761 % |
c ==============================================================================
c Found solution: 16384
c ---[   0]---> Sorter-cost:    2     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 |     27112 |   35527    84872 |   11842   11470   299692    26.1 |  0.761 % |
c |     27213 |   35527    84872 |   13026   11571   301172    26.0 |  0.765 % |
c |     27363 |   35527    84872 |   14328   11721   302788    25.8 |  0.765 % |
c |     27588 |   35527    84872 |   15761   11946   306328    25.6 |  0.765 % |
c |     27926 |   35527    84872 |   17337   12284   318191    25.9 |  0.765 % |
c |     28432 |   35527    84872 |   19071   12790   330313    25.8 |  0.765 % |
c |     29196 |   35512    84841 |   20978   13525   342328    25.3 |  0.803 % |
c |     30336 |   35512    84841 |   23076   14665   389391    26.6 |  0.803 % |
c |     32044 |   35508    84833 |   25384   16370   459588    28.1 |  0.812 % |
c |     34607 |   35508    84833 |   27922   18933   657462    34.7 |  0.812 % |
c |     38451 |   35508    84833 |   30715   22777   797266    35.0 |  0.812 % |
c ==============================================================================
c Found solution: 16379
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 |     38650 |   35518    84854 |   11839   22976   807513    35.1 |  0.812 % |
c |     38750 |   35518    84854 |   13022   11588   426450    36.8 |  0.817 % |
c |     38902 |   35518    84854 |   14325   11740   431937    36.8 |  0.817 % |
c |     39127 |   35518    84854 |   15757   11965   438219    36.6 |  0.817 % |
c |     39464 |   35518    84854 |   17333   12302   449818    36.6 |  0.817 % |
c |     39970 |   35518    84854 |   19066   12808   460415    35.9 |  0.817 % |
c |     40729 |   35518    84854 |   20973   13567   490726    36.2 |  0.816 % |
c |     41868 |   35513    84843 |   23070   14659   550778    37.6 |  0.831 % |
c |     43576 |   35513    84843 |   25377   16367   607793    37.1 |  0.831 % |
c |     46138 |   35513    84843 |   27915   18929   729632    38.5 |  0.830 % |
c |     49983 |   35513    84843 |   30707   22774  1076270    47.3 |  0.831 % |
c ==============================================================================
c Found solution: 16378
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 |     50585 |   35522    84862 |   11840   23376  1104731    47.3 |  0.831 % |
c |     50685 |   35522    84862 |   13024   11788   537643    45.6 |  0.835 % |
c |     50838 |   35522    84862 |   14326   11941   539044    45.1 |  0.835 % |
c |     51063 |   35519    84854 |   15759   12041   545252    45.3 |  0.844 % |
c |     51401 |   35519    84854 |   17334   12379   552992    44.7 |  0.844 % |
c |     51908 |   35519    84854 |   19068   12886   610287    47.4 |  0.844 % |
c |     52667 |   35519    84854 |   20975   13645   624728    45.8 |  0.844 % |
c |     53806 |   35519    84854 |   23072   14784   682766    46.2 |  0.844 % |
c |     55514 |   35519    84854 |   25380   16492   728301    44.2 |  0.844 % |
c |     58078 |   35519    84854 |   27918   19056   817063    42.9 |  0.844 % |
c |     61922 |   35519    84854 |   30709   22900   929759    40.6 |  0.844 % |
c |     67689 |   35519    84854 |   33780   28667  1131507    39.5 |  0.844 % |
c ==============================================================================
c Found solution: 16377
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 |     74135 |   35528    84873 |   11842   35113  1446648    41.2 |  0.844 % |
c |     74235 |   35528    84873 |   13026    8879   166722    18.8 |  0.849 % |
c |     74388 |   35497    84808 |   14328    9019   169524    18.8 |  0.928 % |
c |     74613 |   35497    84808 |   15761    9244   177704    19.2 |  0.928 % |
c |     74950 |   35497    84808 |   17337    9581   190723    19.9 |  0.928 % |
c |     75456 |   35489    84790 |   19071   10086   209656    20.8 |  0.952 % |
c |     76215 |   35483    84778 |   20978   10843   227527    21.0 |  0.966 % |
c |     77354 |   35483    84778 |   23076   11982   267451    22.3 |  0.966 % |
c |     79062 |   35483    84778 |   25384   13690   312826    22.9 |  0.966 % |
c |     81624 |   35483    84778 |   27922   16252   419884    25.8 |  0.966 % |
c |     85469 |   35475    84762 |   30715   20095   496432    24.7 |  0.984 % |
c |     91236 |   35475    84762 |   33786   25862   666510    25.8 |  0.984 % |
c ==============================================================================
c Found solution: 16374
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 |     93282 |   35487    84793 |   11829   27908   746410    26.7 |  0.984 % |
c |     93383 |   35487    84793 |   13011    7078   120743    17.1 |  1.002 % |
c |     93534 |   35487    84793 |   14313    7229   128111    17.7 |  1.002 % |
c |     93759 |   35487    84793 |   15744    7454   133926    18.0 |  1.002 % |
c |     94096 |   35429    84668 |   17318    7779   142656    18.3 |  1.114 % |
c |     94602 |   35369    84547 |   19050    8275   156852    19.0 |  1.250 % |
c |     95361 |   35369    84547 |   20955    9034   172585    19.1 |  1.250 % |
c ==============================================================================
c Found solution: 16373
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 |     95608 |   35374    84566 |   11791    9281   182561    19.7 |  1.250 % |
c |     95709 |   35374    84566 |   12970    9382   184357    19.7 |  1.254 % |
c |     95859 |   35374    84566 |   14267    9532   188152    19.7 |  1.254 % |
c |     96084 |   35374    84566 |   15693    9757   192412    19.7 |  1.254 % |
c |     96421 |   35374    84566 |   17263   10094   203836    20.2 |  1.254 % |
c |     96927 |   35374    84566 |   18989   10600   223940    21.1 |  1.254 % |
c |     97686 |   35374    84566 |   20888   11359   243431    21.4 |  1.254 % |
c |     98827 |   35372    84562 |   22977   12499   297644    23.8 |  1.259 % |
c |    100535 |   35372    84562 |   25275   14207   342049    24.1 |  1.259 % |
c |    103097 |   35364    84546 |   27802   16768   433604    25.9 |  1.277 % |
c |    106942 |   35355    84527 |   30582   20609   492584    23.9 |  1.301 % |
c |    112709 |   35355    84527 |   33641   26376   599837    22.7 |  1.301 % |
c |    121359 |   35355    84527 |   37005   35026  1304901    37.3 |  1.301 % |
c ==============================================================================
c Found solution: 16372
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 |    129822 |   35359    84541 |   11786   20555   887351    43.2 |  1.301 % |
c |    129926 |   35359    84541 |   12964   10382   267450    25.8 |  1.305 % |
c |    130077 |   35359    84541 |   14261   10533   270492    25.7 |  1.305 % |
c |    130302 |   35359    84541 |   15687   10758   274374    25.5 |  1.305 % |
c |    130642 |   35359    84541 |   17255   11098   293613    26.5 |  1.305 % |
c |    131148 |   35359    84541 |   18981   11604   300344    25.9 |  1.305 % |
c |    131909 |   35359    84541 |   20879   12365   306743    24.8 |  1.305 % |
c |    133049 |   35359    84541 |   22967   13505   408446    30.2 |  1.305 % |
c |    134757 |   35307    84428 |   25264   15201   454665    29.9 |  1.426 % |
c |    137319 |   35307    84428 |   27790   17763   504562    28.4 |  1.426 % |
c |    141164 |   35307    84428 |   30569   21608   754993    34.9 |  1.426 % |
c ==============================================================================
c Found solution: 16370
c ---[   0]---> Sorter-cost:    2     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 |    142890 |   35300    84415 |   11766   23333   801569    34.4 |  1.426 % |
c |    142990 |   35300    84415 |   12942   11767   344585    29.3 |  1.454 % |
c |    143141 |   35300    84415 |   14236   11918   352269    29.6 |  1.454 % |
c ==============================================================================
c Found solution: 16368
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 |    143317 |   35304    84430 |   11768   12094   357237    29.5 |  1.454 % |
c |    143417 |   35304    84430 |   12944    6147    70829    11.5 |  1.459 % |
c |    143568 |   35304    84430 |   14239    6298    74871    11.9 |  1.459 % |
c |    143793 |   35304    84430 |   15663    6523    79668    12.2 |  1.459 % |
c |    144130 |   35304    84430 |   17229    6860   103779    15.1 |  1.459 % |
c |    144636 |   35292    84406 |   18952    7365   110974    15.1 |  1.486 % |
c |    145395 |   35292    84406 |   20847    8124   137915    17.0 |  1.486 % |
c |    146535 |   35286    84394 |   22932    9263   200019    21.6 |  1.501 % |
c |    148247 |   35276    84374 |   25225   10969   235738    21.5 |  1.524 % |
c |    150809 |   35276    84374 |   27748   13531   375590    27.8 |  1.524 % |
c |    154653 |   35276    84374 |   30523   17375   481786    27.7 |  1.524 % |
c ==============================================================================
c Found solution: 16182
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 |    159767 |   35284    84394 |   11761   22489   583554    25.9 |  1.524 % |
c |    159867 |   35284    84394 |   12937   11345   162153    14.3 |  1.528 % |
c |    160017 |   35284    84394 |   14230   11495   165778    14.4 |  1.528 % |
c |    160243 |   35284    84394 |   15653   11721   178167    15.2 |  1.528 % |
c |    160580 |   35272    84370 |   17219   12055   190971    15.8 |  1.556 % |
c |    161086 |   35272    84370 |   18941   12561   231677    18.4 |  1.556 % |
c |    161845 |   35272    84370 |   20835   13320   265684    19.9 |  1.556 % |
c |    162984 |   35272    84370 |   22918   14459   311641    21.6 |  1.556 % |
c |    164694 |   35272    84370 |   25210   16169   371354    23.0 |  1.556 % |
c |    167256 |   35272    84370 |   27731   18731   526320    28.1 |  1.556 % |
c |    171101 |   35272    84370 |   30505   22576   926819    41.1 |  1.556 % |
c |    176869 |   35272    84370 |   33555   28344  1571366    55.4 |  1.556 % |
c ==============================================================================
c Found solution: 16180
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 |    183256 |   35280    84390 |   11760   34731  1824941    52.5 |  1.556 % |
c |    183356 |   35280    84390 |   12936    8388   172686    20.6 |  1.560 % |
c |    183506 |   35280    84390 |   14229    8538   175539    20.6 |  1.560 % |
c |    183732 |   35260    84348 |   15652    8750   183779    21.0 |  1.612 % |
c |    184070 |   35180    84165 |   17217    9069   191837    21.2 |  1.789 % |
c |    184576 |   35152    84101 |   18939    9564   204206    21.4 |  1.873 % |
c |    185335 |   35152    84101 |   20833   10323   232728    22.5 |  1.872 % |
c |    186474 |   35152    84101 |   22916   11462   261772    22.8 |  1.872 % |
c |    188186 |   35152    84101 |   25208   13174   420648    31.9 |  1.872 % |
c |    190748 |   35152    84101 |   27729   15736   534414    34.0 |  1.872 % |
c |    194592 |   35134    84063 |   30502   19576   767684    39.2 |  1.919 % |
c |    200358 |   35134    84063 |   33552   25342  1158847    45.7 |  1.919 % |
c |    209008 |   35134    84063 |   36907   33992  1672385    49.2 |  1.919 % |
c |    221982 |   35134    84063 |   40598   19295  1086840    56.3 |  1.919 % |
c ==============================================================================
c Found solution: 16179
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 |    236727 |   35134    84068 |   11711   34039  2223941    65.3 |  1.919 % |
c |    236827 |   35134    84068 |   12882    8610   153797    17.9 |  1.942 % |
c |    236979 |   35131    84061 |   14170    8761   157277    18.0 |  1.951 % |
c |    237205 |   35121    84039 |   15587    8982   161179    17.9 |  1.979 % |
c |    237542 |   35111    84019 |   17146    9316   171848    18.4 |  2.002 % |
c |    238049 |   35111    84019 |   18860    9823   191365    19.5 |  2.002 % |
c |    238810 |   35086    83963 |   20746   10554   213205    20.2 |  2.058 % |
c |    239951 |   35078    83945 |   22821   11693   258260    22.1 |  2.081 % |
c |    241659 |   35074    83935 |   25103   13398   349645    26.1 |  2.095 % |
c |    244221 |   35074    83935 |   27613   15960   451885    28.3 |  2.096 % |
c |    248065 |   35074    83935 |   30375   19804   720708    36.4 |  2.095 % |
c |    253831 |   35064    83915 |   33412   25569  1046013    40.9 |  2.119 % |
c ==============================================================================
c Found solution: 16178
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 |    259485 |   35054    83899 |   11684   31220  1408668    45.1 |  2.119 % |
c |    259586 |   35054    83899 |   12852    7906   171546    21.7 |  2.165 % |
c |    259736 |   35054    83899 |   14137    8056   174230    21.6 |  2.165 % |
c |    259961 |   35054    83899 |   15551    8281   179052    21.6 |  2.165 % |
c |    260298 |   35054    83899 |   17106    8618   195671    22.7 |  2.165 % |
c |    260804 |   35054    83899 |   18817    9124   211111    23.1 |  2.165 % |
c |    261563 |   35054    83899 |   20698    9883   258658    26.2 |  2.165 % |
c |    262703 |   35054    83899 |   22768   11023   291377    26.4 |  2.165 % |
c |    264411 |   35054    83899 |   25045   12731   370236    29.1 |  2.165 % |
c ==============================================================================
c Found solution: 16118
c ---[   0]---> Sorter-cost:    4     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 |    265329 |   35061    83916 |   11687   13649   406288    29.8 |  2.165 % |
c |    265433 |   35053    83900 |   12855    6927    81243    11.7 |  2.188 % |
c |    265585 |   35053    83900 |   14141    7079    89507    12.6 |  2.188 % |
c |    265810 |   35043    83880 |   15555    7303    96354    13.2 |  2.211 % |
c |    266147 |   35043    83880 |   17110    7640   108378    14.2 |  2.211 % |
c |    266655 |   35043    83880 |   18822    8148   131177    16.1 |  2.211 % |
c |    267414 |   35043    83880 |   20704    8907   152900    17.2 |  2.211 % |
c |    268554 |   35043    83880 |   22774   10047   177411    17.7 |  2.211 % |
c ==============================================================================
c Found solution: 16117
c ---[   0]---> Sorter-cost:    4     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 |    269483 |   35050    83900 |   11683   10976   226410    20.6 |  2.211 % |
c |    269586 |   35050    83900 |   12851   11079   228675    20.6 |  2.215 % |
c |    269738 |   35050    83900 |   14136   11231   232623    20.7 |  2.215 % |
c |    269965 |   35044    83886 |   15550   11456   238346    20.8 |  2.234 % |
c |    270302 |   34737    83233 |   17105   11746   250620    21.3 |  2.918 % |
c |    270808 |   34734    83226 |   18815   12250   276586    22.6 |  2.927 % |
c |    271567 |   34727    83211 |   20697   13003   304016    23.4 |  2.946 % |
c |    272707 |   34727    83211 |   22766   14143   365781    25.9 |  2.946 % |
c |    274416 |   34727    83211 |   25043   15852   462932    29.2 |  2.946 % |
c |    276978 |   34727    83211 |   27547   18414   660017    35.8 |  2.946 % |
c |    280822 |   34727    83211 |   30302   22258   765041    34.4 |  2.946 % |
c |    286589 |   34727    83211 |   33332   28025  1213832    43.3 |  2.946 % |
c |    295238 |   34705    83167 |   36666   36668  2215407    60.4 |  2.987 % |
c |    308212 |   34699    83154 |   40332   28832  2249748    78.0 |  2.997 % |
c ==============================================================================
c Found solution: 16116
c ---[   0]---> Sorter-cost:    4     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 |    314712 |   34697    83153 |   11565   35330  2567057    72.7 |  2.997 % |
c |    314813 |   34697    83153 |   12721    8934   165532    18.5 |  3.024 % |
c |    314964 |   34697    83153 |   13993    9085   168231    18.5 |  3.024 % |
c |    315189 |   34697    83153 |   15393    9310   173303    18.6 |  3.024 % |
c |    315526 |   34697    83153 |   16932    9647   184718    19.1 |  3.024 % |
c |    316032 |   34697    83153 |   18625   10153   208876    20.6 |  3.024 % |
c |    316791 |   34697    83153 |   20488   10912   236818    21.7 |  3.024 % |
c |    317933 |   34697    83153 |   22536   12054   295954    24.6 |  3.024 % |
c |    319641 |   34685    83125 |   24790   13755   377282    27.4 |  3.061 % |
c |    322205 |   34685    83125 |   27269   16319   557138    34.1 |  3.061 % |
c |    326049 |   34685    83125 |   29996   20163   818384    40.6 |  3.061 % |
c ==============================================================================
c Found solution: 15990
c ---[   0]---> Sorter-cost:    4     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 |    327390 |   34685    83125 |   11561   21501   864903    40.2 |  3.061 % |
c |    327491 |   34685    83125 |   12717   10852   303674    28.0 |  3.084 % |
c |    327641 |   34685    83125 |   13988   11002   307758    28.0 |  3.084 % |
c |    327870 |   34675    83103 |   15387   11228   312746    27.9 |  3.112 % |
c |    328207 |   34675    83103 |   16926   11565   339526    29.4 |  3.112 % |
c |    328715 |   34675    83103 |   18619   12073   360651    29.9 |  3.112 % |
c |    329474 |   34675    83103 |   20481   12832   405674    31.6 |  3.112 % |
c |    330614 |   34675    83103 |   22529   13972   455546    32.6 |  3.112 % |
c |    332324 |   34675    83103 |   24782   15682   537323    34.3 |  3.112 % |
c ==============================================================================
c Found solution: 15989
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 |    332519 |   34683    83124 |   11561   15877   542783    34.2 |  3.112 % |
c |    332619 |   34683    83124 |   12717    8039   121748    15.1 |  3.116 % |
c |    332771 |   34683    83124 |   13988    8191   124578    15.2 |  3.116 % |
c |    332996 |   34683    83124 |   15387    8416   132510    15.7 |  3.116 % |
c |    333334 |   34683    83124 |   16926    8754   147664    16.9 |  3.116 % |
c |    333841 |   34683    83124 |   18619    9261   178758    19.3 |  3.116 % |
c |    334601 |   34683    83124 |   20481   10021   206358    20.6 |  3.116 % |
c ==============================================================================
c Found solution: 15925
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 |    334973 |   34692    83146 |   11564   10393   216399    20.8 |  3.116 % |
c |    335075 |   34692    83146 |   12720   10495   218494    20.8 |  3.120 % |
c |    335229 |   34692    83146 |   13992   10649   223205    21.0 |  3.120 % |
c |    335456 |   34692    83146 |   15391   10876   230925    21.2 |  3.120 % |
c |    335796 |   34692    83146 |   16930   11216   247406    22.1 |  3.120 % |
c |    336305 |   34692    83146 |   18623   11725   262641    22.4 |  3.120 % |
c |    337064 |   34684    83128 |   20486   12481   291182    23.3 |  3.143 % |
c |    338203 |   34684    83128 |   22534   13620   325969    23.9 |  3.143 % |
c |    339911 |   34684    83128 |   24788   15328   391851    25.6 |  3.143 % |
c |    342473 |   34684    83128 |   27267   17890   489510    27.4 |  3.143 % |
c |    346317 |   34684    83128 |   29994   21734   748012    34.4 |  3.143 % |
c ==============================================================================
c Found solution: 15910
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 |    349192 |   34691    83144 |   11563   24609   951224    38.7 |  3.143 % |
c |    349292 |   34682    83125 |   12719    6251    61443     9.8 |  3.170 % |
c |    349442 |   34682    83125 |   13991    6401    67635    10.6 |  3.170 % |
c |    349667 |   34682    83125 |   15390    6626    75197    11.3 |  3.170 % |
c |    350007 |   34657    83071 |   16929    6960    87240    12.5 |  3.226 % |
c |    350513 |   34654    83064 |   18622    7464   111076    14.9 |  3.235 % |
c |    351272 |   34654    83064 |   20484    8223   144330    17.6 |  3.235 % |
c |    352411 |   34654    83064 |   22533    9362   200327    21.4 |  3.235 % |
c |    354120 |   34654    83064 |   24786   11071   358556    32.4 |  3.235 % |
c |    356684 |   34654    83064 |   27264   13635   595110    43.6 |  3.235 % |
c |    360528 |   34654    83064 |   29991   17479  1015840    58.1 |  3.235 % |
c |    366294 |   34654    83064 |   32990   23245  1660242    71.4 |  3.235 % |
c ==============================================================================
c Found solution: 15894
c ---[   0]---> Sorter-cost:    3     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 |    371891 |   34657    83072 |   11552   28841  2177328    75.5 |  3.235 % |
c |    371991 |   34657    83072 |   12707    7311   113680    15.5 |  3.253 % |
c |    372142 |   34645    83047 |   13977    7453   115579    15.5 |  3.281 % |
c |    372367 |   34632    83018 |   15375    7607   118767    15.6 |  3.318 % |
c |    372704 |   34632    83018 |   16913    7944   129243    16.3 |  3.318 % |
c |    373212 |   34625    83003 |   18604    8450   151345    17.9 |  3.337 % |
c |    373971 |   34625    83003 |   20465    9209   199994    21.7 |  3.337 % |
c |    375112 |   34619    82991 |   22511   10348   253789    24.5 |  3.351 % |
c |    376822 |   34619    82991 |   24762   12058   406225    33.7 |  3.351 % |
c |    379385 |   34606    82962 |   27239   14619   536781    36.7 |  3.388 % |
c ==============================================================================
c Found solution: 15893
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 |    380196 |   34608    82967 |   11536   15429   575996    37.3 |  3.388 % |
c |    380298 |   34608    82967 |   12689    7817   129723    16.6 |  3.415 % |
c |    380450 |   34608    82967 |   13958    7969   133742    16.8 |  3.415 % |
c |    380676 |   34608    82967 |   15354    8195   143216    17.5 |  3.415 % |
c |    381013 |   34605    82960 |   16889    8520   150908    17.7 |  3.424 % |
c |    381519 |   34605    82960 |   18578    9026   178653    19.8 |  3.425 % |
c |    382278 |   34605    82960 |   20436    9785   210764    21.5 |  3.424 % |
c |    383418 |   34605    82960 |   22480   10925   258868    23.7 |  3.424 % |
c |    385126 |   34605    82960 |   24728   12633   366990    29.1 |  3.424 % |
c |    387688 |   34597    82941 |   27201   14969   480408    32.1 |  3.448 % |
c |    391532 |   34576    82894 |   29921   18804   798432    42.5 |  3.508 % |
c ==============================================================================
c Found solution: 15884
c ---[   0]---> Sorter-cost:    3     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 |    392902 |   34585    82914 |   11528   20174   845624    41.9 |  3.508 % |
c |    393004 |   34585    82914 |   12680   10189   281709    27.6 |  3.512 % |
c |    393154 |   34585    82914 |   13948   10339   290203    28.1 |  3.512 % |
c |    393379 |   34585    82914 |   15343   10564   301336    28.5 |  3.512 % |
c |    393717 |   34585    82914 |   16878   10902   313278    28.7 |  3.512 % |
c |    394223 |   34585    82914 |   18565   11408   326068    28.6 |  3.512 % |
c |    394983 |   34585    82914 |   20422   12168   349476    28.7 |  3.512 % |
c ==============================================================================
c Found solution: 15878
c ---[   0]---> Sorter-cost:    3     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 |    395809 |   34593    82932 |   11531   12994   390156    30.0 |  3.512 % |
c |    395909 |   34593    82932 |   12684    6597    56989     8.6 |  3.516 % |
c |    396059 |   34593    82932 |   13952    6747    64702     9.6 |  3.516 % |
c |    396284 |   34593    82932 |   15347    6972    72081    10.3 |  3.516 % |
c |    396624 |   34593    82932 |   16882    7312    86221    11.8 |  3.516 % |
c |    397132 |   34593    82932 |   18570    7820   103764    13.3 |  3.516 % |
c |    397893 |   34593    82932 |   20427    8581   151592    17.7 |  3.516 % |
c ==============================================================================
c Found solution: 15877
c ---[   0]---> Sorter-cost:    3     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 |    398834 |   34602    82952 |   11534    9522   193264    20.3 |  3.516 % |
c |    398934 |   34602    82952 |   12687    9622   196981    20.5 |  3.520 % |
c |    399084 |   34602    82952 |   13956    9772   200190    20.5 |  3.520 % |
c |    399310 |   34602    82952 |   15351    9998   207390    20.7 |  3.520 % |
c |    399651 |   34602    82952 |   16886   10339   229744    22.2 |  3.520 % |
c |    400157 |   34602    82952 |   18575   10845   246052    22.7 |  3.520 % |
c |    400916 |   34602    82952 |   20433   11604   301779    26.0 |  3.520 % |
c |    402055 |   34602    82952 |   22476   12743   373400    29.3 |  3.520 % |
c |    403763 |   34602    82952 |   24724   14451   450964    31.2 |  3.520 % |
c |    406325 |   34602    82952 |   27196   17013   560156    32.9 |  3.520 % |
c |    410170 |   34602    82952 |   29916   20858   852653    40.9 |  3.520 % |
c ==============================================================================
c Found solution: 15876
c ---[   0]---> Sorter-cost:    3     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 |    415001 |   34610    82970 |   11536   25689  1113351    43.3 |  3.520 % |
c |    415101 |   34610    82970 |   12689    6523    68241    10.5 |  3.524 % |
c |    415253 |   34610    82970 |   13958    6675    73828    11.1 |  3.524 % |
c |    415478 |   34601    82951 |   15354    6899    79352    11.5 |  3.547 % |
c |    415815 |   34601    82951 |   16889    7236    97703    13.5 |  3.547 % |
c |    416321 |   34601    82951 |   18578    7742   118010    15.2 |  3.547 % |
c |    417080 |   34601    82951 |   20436    8501   138642    16.3 |  3.547 % |
c |    418219 |   34601    82951 |   22480    9640   210486    21.8 |  3.547 % |
c ==============================================================================
c Found solution: 15875
c ---[   0]---> Sorter-cost:    3     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 |    419175 |   34602    82954 |   11534   10595   235459    22.2 |  3.547 % |
c |    419275 |   34602    82954 |   12687   10695   238166    22.3 |  3.574 % |
c |    419426 |   34602    82954 |   13956   10846   240943    22.2 |  3.575 % |
c |    419653 |   34602    82954 |   15351   11073   247548    22.4 |  3.574 % |
c |    419991 |   34602    82954 |   16886   11411   263394    23.1 |  3.574 % |
c |    420499 |   34602    82954 |   18575   11919   280370    23.5 |  3.575 % |
c |    421259 |   34602    82954 |   20433   12679   334150    26.4 |  3.575 % |
c |    422398 |   34591    82929 |   22476   13816   381315    27.6 |  3.607 % |
c ==============================================================================
c Found solution: 15873
c ---[   0]---> Sorter-cost:    3     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 |    423043 |   34599    82947 |   11533   14461   409344    28.3 |  3.607 % |
c |    423144 |   34599    82947 |   12686    7332    71936     9.8 |  3.611 % |
c |    423294 |   34599    82947 |   13954    7482    75287    10.1 |  3.611 % |
c |    423519 |   34599    82947 |   15350    7707    82530    10.7 |  3.611 % |
c |    423856 |   34599    82947 |   16885    8044    92701    11.5 |  3.611 % |
c |    424363 |   34599    82947 |   18574    8551   111070    13.0 |  3.611 % |
c |    425122 |   34599    82947 |   20431    9310   151025    16.2 |  3.611 % |
c |    426262 |   34599    82947 |   22474   10450   185862    17.8 |  3.611 % |
c |    427971 |   34599    82947 |   24722   12159   292947    24.1 |  3.611 % |
c |    430534 |   34599    82947 |   27194   14722   365461    24.8 |  3.611 % |
c ==============================================================================
c Found solution: 15872
c ---[   0]---> Sorter-cost:    3     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 |    433938 |   34593    82937 |   11531   18125   443975    24.5 |  3.611 % |
c |    434038 |   34593    82937 |   12684    9163    83902     9.2 |  3.647 % |
c |    434188 |   34593    82937 |   13952    9313    86703     9.3 |  3.647 % |
c |    434413 |   34593    82937 |   15347    9538    93482     9.8 |  3.647 % |
c |    434751 |   34593    82937 |   16882    9876   109902    11.1 |  3.647 % |
c |    435258 |   34578    82904 |   18570   10377   130823    12.6 |  3.689 % |
c |    436017 |   34578    82904 |   20427   11136   170820    15.3 |  3.689 % |
c |    437156 |   34573    82893 |   22470   12273   248739    20.3 |  3.703 % |
c |    438864 |   34573    82893 |   24717   13981   296453    21.2 |  3.703 % |
c |    441426 |   34573    82893 |   27189   16543   421400    25.5 |  3.703 % |
c |    445271 |   34573    82893 |   29908   20388   893733    43.8 |  3.703 % |
c |    451037 |   34573    82893 |   32899   26154  1230018    47.0 |  3.703 % |
c |    459686 |   34573    82893 |   36189   34803  1806221    51.9 |  3.703 % |
c |    472660 |   34573    82893 |   39808   28152  1236074    43.9 |  3.703 % |
c |    492123 |   34573    82893 |   43788   20971   470841    22.5 |  3.703 % |
c |    521316 |   34569    82885 |   48167   22801   620855    27.2 |  3.708 % |
c |    565105 |   34569    82885 |   52984   33501  2612555    78.0 |  3.708 % |
c |    630789 |   34569    82885 |   58283   27174   924872    34.0 |  3.708 % |
c |    729315 |   34551    82846 |   64111   36423  1660579    45.6 |  3.731 % |

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

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 2177 0 0 0 976 9 0 0 25 0 1 0 1796464711 10211328 2075 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 2493 2075 145 145 0 2348 0
[pid=9444] vsize: 9972
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 12096

[startup+20.005 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 2422 0 0 0 1971 11 0 0 25 0 1 0 1796464711 11223040 2320 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 2740 2320 145 145 0 2595 0
[pid=9444] vsize: 10960
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 13084

[startup+30.0068 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 2553 0 0 0 2968 12 0 0 25 0 1 0 1796464711 11751424 2451 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 2869 2451 145 145 0 2724 0
[pid=9444] vsize: 11476
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 13600

[startup+40.0076 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 2619 0 0 0 3965 13 0 0 25 0 1 0 1796464711 12021760 2517 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 2935 2517 145 145 0 2790 0
[pid=9444] vsize: 11740
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 13864

[startup+50.0084 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 2881 0 0 0 4961 15 0 0 25 0 1 0 1796464711 13148160 2779 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 3210 2779 145 145 0 3065 0
[pid=9444] vsize: 12840
Current children cumulated CPU time (s) 49.76
Current children cumulated vsize (Kb) 14964

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3068 0 0 0 5958 16 0 0 25 0 1 0 1796464711 13897728 2966 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 3393 2966 145 145 0 3248 0
[pid=9444] vsize: 13572
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 15696

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3416 0 0 0 6953 19 0 0 25 0 1 0 1796464711 15319040 3314 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 3740 3314 145 145 0 3595 0
[pid=9444] vsize: 14960
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 17084

[startup+80.0109 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3416 0 0 0 7953 19 0 0 25 0 1 0 1796464711 15319040 3314 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 3740 3314 145 145 0 3595 0
[pid=9444] vsize: 14960
Current children cumulated CPU time (s) 79.72
Current children cumulated vsize (Kb) 17084

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3577 0 0 0 8951 20 0 0 25 0 1 0 1796464711 15953920 3475 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 3895 3475 145 145 0 3750 0
[pid=9444] vsize: 15580
Current children cumulated CPU time (s) 89.71
Current children cumulated vsize (Kb) 17704

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3888 0 0 0 9946 22 0 0 25 0 1 0 1796464711 17338368 3786 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4233 3786 145 145 0 4088 0
[pid=9444] vsize: 16932
Current children cumulated CPU time (s) 99.68
Current children cumulated vsize (Kb) 19056

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3888 0 0 0 10946 22 0 0 25 0 1 0 1796464711 17338368 3786 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4233 3786 145 145 0 4088 0
[pid=9444] vsize: 16932
Current children cumulated CPU time (s) 109.68
Current children cumulated vsize (Kb) 19056

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3888 0 0 0 11946 22 0 0 25 0 1 0 1796464711 17338368 3786 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4233 3786 145 145 0 4088 0
[pid=9444] vsize: 16932
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 19056

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3888 0 0 0 12946 22 0 0 25 0 1 0 1796464711 17338368 3786 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4233 3786 145 145 0 4088 0
[pid=9444] vsize: 16932
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 19056

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3888 0 0 0 13946 23 0 0 25 0 1 0 1796464711 17338368 3786 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4233 3786 145 145 0 4088 0
[pid=9444] vsize: 16932
Current children cumulated CPU time (s) 139.69
Current children cumulated vsize (Kb) 19056

[startup+150.016 s]
Raw data (loadavg): 1.07 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 3888 0 0 0 14946 23 0 0 25 0 1 0 1796464711 17338368 3786 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4233 3786 145 145 0 4088 0
[pid=9444] vsize: 16932
Current children cumulated CPU time (s) 149.69
Current children cumulated vsize (Kb) 19056

[startup+160.017 s]
Raw data (loadavg): 1.06 1.00 0.99 1/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) T 9440 9440 8263 0 -1 0 4156 0 0 0 15942 25 0 0 25 0 1 0 1796464711 18415616 4054 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4496 4054 145 145 0 4351 0
[pid=9444] vsize: 17984
Current children cumulated CPU time (s) 159.67
Current children cumulated vsize (Kb) 20108

[startup+170.017 s]
Raw data (loadavg): 1.05 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4237 0 0 0 16940 26 0 0 25 0 1 0 1796464711 18743296 4135 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4576 4135 145 145 0 4431 0
[pid=9444] vsize: 18304
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 20428

[startup+180.019 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4237 0 0 0 17940 26 0 0 25 0 1 0 1796464711 18743296 4135 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4576 4135 145 145 0 4431 0
[pid=9444] vsize: 18304
Current children cumulated CPU time (s) 179.66
Current children cumulated vsize (Kb) 20428

[startup+190.02 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4237 0 0 0 18940 26 0 0 25 0 1 0 1796464711 18743296 4135 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4576 4135 145 145 0 4431 0
[pid=9444] vsize: 18304
Current children cumulated CPU time (s) 189.66
Current children cumulated vsize (Kb) 20428

[startup+200.02 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4237 0 0 0 19941 26 0 0 25 0 1 0 1796464711 18743296 4135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4576 4135 145 145 0 4431 0
[pid=9444] vsize: 18304
Current children cumulated CPU time (s) 199.67
Current children cumulated vsize (Kb) 20428

[startup+210.022 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4237 0 0 0 20941 26 0 0 25 0 1 0 1796464711 18743296 4135 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4576 4135 145 145 0 4431 0
[pid=9444] vsize: 18304
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 20428

[startup+220.023 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4237 0 0 0 21941 26 0 0 25 0 1 0 1796464711 18743296 4135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4576 4135 145 145 0 4431 0
[pid=9444] vsize: 18304
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 20428

[startup+230.023 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4518 0 0 0 22936 29 0 0 25 0 1 0 1796464711 19894272 4416 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4857 4416 145 145 0 4712 0
[pid=9444] vsize: 19428
Current children cumulated CPU time (s) 229.65
Current children cumulated vsize (Kb) 21552

[startup+240.024 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4518 0 0 0 23936 29 0 0 25 0 1 0 1796464711 19894272 4416 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4857 4416 145 145 0 4712 0
[pid=9444] vsize: 19428
Current children cumulated CPU time (s) 239.65
Current children cumulated vsize (Kb) 21552

[startup+250.025 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4518 0 0 0 24936 29 0 0 25 0 1 0 1796464711 19894272 4416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4857 4416 145 145 0 4712 0
[pid=9444] vsize: 19428
Current children cumulated CPU time (s) 249.65
Current children cumulated vsize (Kb) 21552

[startup+260.026 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4518 0 0 0 25936 29 0 0 25 0 1 0 1796464711 19894272 4416 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 4857 4416 145 145 0 4712 0
[pid=9444] vsize: 19428
Current children cumulated CPU time (s) 259.65
Current children cumulated vsize (Kb) 21552

[startup+270.027 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 4781 0 0 0 26931 31 0 0 25 0 1 0 1796464711 20971520 4679 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5120 4679 145 145 0 4975 0
[pid=9444] vsize: 20480
Current children cumulated CPU time (s) 269.62
Current children cumulated vsize (Kb) 22604

[startup+280.029 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5276 0 0 0 27921 35 0 0 25 0 1 0 1796464711 22990848 5174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5613 5174 145 145 0 5468 0
[pid=9444] vsize: 22452
Current children cumulated CPU time (s) 279.56
Current children cumulated vsize (Kb) 24576

[startup+290.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 28918 36 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 289.54
Current children cumulated vsize (Kb) 25336

[startup+300.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 29919 36 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 299.55
Current children cumulated vsize (Kb) 25336

[startup+310.031 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 30919 36 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 309.55
Current children cumulated vsize (Kb) 25336

[startup+320.032 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 31919 36 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 319.55
Current children cumulated vsize (Kb) 25336

[startup+330.033 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 32919 36 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 329.55
Current children cumulated vsize (Kb) 25336

[startup+340.034 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 33919 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 339.56
Current children cumulated vsize (Kb) 25336

[startup+350.034 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 34919 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 25336

[startup+360.035 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 35919 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 25336

[startup+370.036 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 36919 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223056 134562076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 369.56
Current children cumulated vsize (Kb) 25336

[startup+380.037 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 37919 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 379.56
Current children cumulated vsize (Kb) 25336

[startup+390.038 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 38919 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223104 134556517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 389.56
Current children cumulated vsize (Kb) 25336

[startup+400.039 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 39920 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 399.57
Current children cumulated vsize (Kb) 25336

[startup+410.039 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 40920 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 409.57
Current children cumulated vsize (Kb) 25336

[startup+420.04 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5467 0 0 0 41920 37 0 0 25 0 1 0 1796464711 23769088 5365 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5803 5365 145 145 0 5658 0
[pid=9444] vsize: 23212
Current children cumulated CPU time (s) 419.57
Current children cumulated vsize (Kb) 25336

[startup+430.041 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5561 0 0 0 42918 38 0 0 25 0 1 0 1796464711 24145920 5459 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5459 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 25704

[startup+440.042 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5561 0 0 0 43918 38 0 0 25 0 1 0 1796464711 24145920 5459 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5459 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 439.56
Current children cumulated vsize (Kb) 25704

[startup+450.043 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5563 0 0 0 44918 38 0 0 25 0 1 0 1796464711 24145920 5461 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5461 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 449.56
Current children cumulated vsize (Kb) 25704

[startup+460.044 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 45918 38 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 459.56
Current children cumulated vsize (Kb) 25704

[startup+470.043 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 46918 38 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 469.56
Current children cumulated vsize (Kb) 25704

[startup+480.044 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 47919 38 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 479.57
Current children cumulated vsize (Kb) 25704

[startup+490.045 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 48919 38 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 489.57
Current children cumulated vsize (Kb) 25704

[startup+500.046 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 49919 39 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 499.58
Current children cumulated vsize (Kb) 25704

[startup+510.047 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 50919 39 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 509.58
Current children cumulated vsize (Kb) 25704

[startup+520.048 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 51919 39 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 519.58
Current children cumulated vsize (Kb) 25704

[startup+530.048 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5565 0 0 0 52918 40 0 0 25 0 1 0 1796464711 24145920 5463 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5463 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 529.58
Current children cumulated vsize (Kb) 25704

[startup+540.049 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 53918 41 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 539.59
Current children cumulated vsize (Kb) 25704

[startup+550.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 54917 41 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 549.58
Current children cumulated vsize (Kb) 25704

[startup+560.052 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 55917 41 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223104 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 559.58
Current children cumulated vsize (Kb) 25704

[startup+570.053 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 56917 42 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 569.59
Current children cumulated vsize (Kb) 25704

[startup+580.054 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 57917 42 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 579.59
Current children cumulated vsize (Kb) 25704

[startup+590.054 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 58917 42 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 589.59
Current children cumulated vsize (Kb) 25704

[startup+600.055 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 59917 42 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 599.59
Current children cumulated vsize (Kb) 25704

[startup+610.056 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 60917 43 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 609.6
Current children cumulated vsize (Kb) 25704

[startup+620.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 61917 43 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 619.6
Current children cumulated vsize (Kb) 25704

[startup+630.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 62918 43 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 629.61
Current children cumulated vsize (Kb) 25704

[startup+640.06 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 63917 43 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 639.6
Current children cumulated vsize (Kb) 25704

[startup+650.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 64918 43 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 649.61
Current children cumulated vsize (Kb) 25704

[startup+660.061 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5566 0 0 0 65918 43 0 0 25 0 1 0 1796464711 24145920 5464 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5464 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 659.61
Current children cumulated vsize (Kb) 25704

[startup+670.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5568 0 0 0 66918 43 0 0 25 0 1 0 1796464711 24145920 5466 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5466 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 669.61
Current children cumulated vsize (Kb) 25704

[startup+680.063 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5568 0 0 0 67918 43 0 0 25 0 1 0 1796464711 24145920 5466 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5466 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 679.61
Current children cumulated vsize (Kb) 25704

[startup+690.064 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5568 0 0 0 68918 43 0 0 25 0 1 0 1796464711 24145920 5466 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5466 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 689.61
Current children cumulated vsize (Kb) 25704

[startup+700.065 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5568 0 0 0 69918 43 0 0 25 0 1 0 1796464711 24145920 5466 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5466 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 699.61
Current children cumulated vsize (Kb) 25704

[startup+710.065 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5569 0 0 0 70918 44 0 0 25 0 1 0 1796464711 24145920 5467 4294967295 134512640 135094434 3221224432 3221223184 134559288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5467 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 709.62
Current children cumulated vsize (Kb) 25704

[startup+720.066 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5569 0 0 0 71919 44 0 0 25 0 1 0 1796464711 24145920 5467 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5467 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 719.63
Current children cumulated vsize (Kb) 25704

[startup+730.068 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5569 0 0 0 72919 44 0 0 25 0 1 0 1796464711 24145920 5467 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 5895 5467 145 145 0 5750 0
[pid=9444] vsize: 23580
Current children cumulated CPU time (s) 729.63
Current children cumulated vsize (Kb) 25704

[startup+740.069 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 5775 0 0 0 73915 45 0 0 25 0 1 0 1796464711 24993792 5673 4294967295 134512640 135094434 3221224432 3221223104 134555792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 6102 5673 145 145 0 5957 0
[pid=9444] vsize: 24408
Current children cumulated CPU time (s) 739.6
Current children cumulated vsize (Kb) 26532

[startup+750.069 s]
Raw data (loadavg): 1.07 1.02 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 6218 0 0 0 74908 48 0 0 25 0 1 0 1796464711 26808320 6116 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 6545 6116 145 145 0 6400 0
[pid=9444] vsize: 26180
Current children cumulated CPU time (s) 749.56
Current children cumulated vsize (Kb) 28304

[startup+760.07 s]
Raw data (loadavg): 1.06 1.02 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 6623 0 0 0 75900 52 0 0 25 0 1 0 1796464711 28467200 6521 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 6950 6521 145 145 0 6805 0
[pid=9444] vsize: 27800
Current children cumulated CPU time (s) 759.52
Current children cumulated vsize (Kb) 29924

[startup+770.07 s]
Raw data (loadavg): 1.05 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7092 0 0 0 76892 56 0 0 25 0 1 0 1796464711 30375936 6990 4294967295 134512640 135094434 3221224432 3221223024 134557331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 7416 6990 145 145 0 7271 0
[pid=9444] vsize: 29664
Current children cumulated CPU time (s) 769.48
Current children cumulated vsize (Kb) 31788

[startup+780.071 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7464 0 0 0 77886 59 0 0 25 0 1 0 1796464711 31903744 7362 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 7789 7362 145 145 0 7644 0
[pid=9444] vsize: 31156
Current children cumulated CPU time (s) 779.45
Current children cumulated vsize (Kb) 33280

[startup+790.072 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7816 0 0 0 78879 62 0 0 25 0 1 0 1796464711 33345536 7714 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8141 7714 145 145 0 7996 0
[pid=9444] vsize: 32564
Current children cumulated CPU time (s) 789.41
Current children cumulated vsize (Kb) 34688

[startup+800.073 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7816 0 0 0 79879 62 0 0 25 0 1 0 1796464711 33345536 7714 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8141 7714 145 145 0 7996 0
[pid=9444] vsize: 32564
Current children cumulated CPU time (s) 799.41
Current children cumulated vsize (Kb) 34688

[startup+810.075 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7816 0 0 0 80879 62 0 0 25 0 1 0 1796464711 33345536 7714 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8141 7714 145 145 0 7996 0
[pid=9444] vsize: 32564
Current children cumulated CPU time (s) 809.41
Current children cumulated vsize (Kb) 34688

[startup+820.076 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7816 0 0 0 81878 63 0 0 25 0 1 0 1796464711 33345536 7714 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8141 7714 145 145 0 7996 0
[pid=9444] vsize: 32564
Current children cumulated CPU time (s) 819.41
Current children cumulated vsize (Kb) 34688

[startup+830.076 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7819 0 0 0 82878 63 0 0 25 0 1 0 1796464711 33361920 7717 4294967295 134512640 135094434 3221224432 3221223096 134781717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8145 7717 145 145 0 8000 0
[pid=9444] vsize: 32580
Current children cumulated CPU time (s) 829.41
Current children cumulated vsize (Kb) 34704

[startup+840.078 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7824 0 0 0 83878 63 0 0 25 0 1 0 1796464711 33394688 7722 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8153 7722 145 145 0 8008 0
[pid=9444] vsize: 32612
Current children cumulated CPU time (s) 839.41
Current children cumulated vsize (Kb) 34736

[startup+850.079 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7827 0 0 0 84878 63 0 0 25 0 1 0 1796464711 33411072 7725 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7725 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 849.41
Current children cumulated vsize (Kb) 34752

[startup+860.08 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7827 0 0 0 85878 63 0 0 25 0 1 0 1796464711 33411072 7725 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7725 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 859.41
Current children cumulated vsize (Kb) 34752

[startup+870.081 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7827 0 0 0 86878 64 0 0 25 0 1 0 1796464711 33411072 7725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7725 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 869.42
Current children cumulated vsize (Kb) 34752

[startup+880.082 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7828 0 0 0 87879 64 0 0 25 0 1 0 1796464711 33411072 7726 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7726 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 879.43
Current children cumulated vsize (Kb) 34752

[startup+890.082 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7828 0 0 0 88879 64 0 0 25 0 1 0 1796464711 33411072 7726 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7726 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 889.43
Current children cumulated vsize (Kb) 34752

[startup+900.083 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7828 0 0 0 89879 64 0 0 25 0 1 0 1796464711 33411072 7726 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7726 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 899.43
Current children cumulated vsize (Kb) 34752

[startup+910.084 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7830 0 0 0 90879 64 0 0 25 0 1 0 1796464711 33411072 7728 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7728 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 909.43
Current children cumulated vsize (Kb) 34752

[startup+920.085 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7830 0 0 0 91880 64 0 0 25 0 1 0 1796464711 33411072 7728 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7728 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 919.44
Current children cumulated vsize (Kb) 34752

[startup+930.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7830 0 0 0 92880 64 0 0 25 0 1 0 1796464711 33411072 7728 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7728 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 929.44
Current children cumulated vsize (Kb) 34752

[startup+940.087 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7830 0 0 0 93880 64 0 0 25 0 1 0 1796464711 33411072 7728 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7728 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 939.44
Current children cumulated vsize (Kb) 34752

[startup+950.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7835 0 0 0 94880 64 0 0 25 0 1 0 1796464711 33411072 7733 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8157 7733 145 145 0 8012 0
[pid=9444] vsize: 32628
Current children cumulated CPU time (s) 949.44
Current children cumulated vsize (Kb) 34752

[startup+960.087 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 95880 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 959.44
Current children cumulated vsize (Kb) 35008

[startup+970.088 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 96880 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 969.44
Current children cumulated vsize (Kb) 35008

[startup+980.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 97881 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 979.45
Current children cumulated vsize (Kb) 35008

[startup+990.091 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 98881 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 989.45
Current children cumulated vsize (Kb) 35008

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 99881 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 999.45
Current children cumulated vsize (Kb) 35008

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 100881 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1009.45
Current children cumulated vsize (Kb) 35008

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 101881 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1019.45
Current children cumulated vsize (Kb) 35008

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 102882 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1029.46
Current children cumulated vsize (Kb) 35008

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 103882 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1039.46
Current children cumulated vsize (Kb) 35008

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 104882 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1049.46
Current children cumulated vsize (Kb) 35008

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 105882 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1059.46
Current children cumulated vsize (Kb) 35008

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 106882 64 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1069.46
Current children cumulated vsize (Kb) 35008

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 107881 65 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1079.46
Current children cumulated vsize (Kb) 35008

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 108880 65 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1089.45
Current children cumulated vsize (Kb) 35008

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 109880 65 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1099.45
Current children cumulated vsize (Kb) 35008

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7839 0 0 0 110880 65 0 0 25 0 1 0 1796464711 33673216 7737 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7737 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1109.45
Current children cumulated vsize (Kb) 35008

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7843 0 0 0 111881 65 0 0 25 0 1 0 1796464711 33673216 7741 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8221 7741 145 145 0 8076 0
[pid=9444] vsize: 32884
Current children cumulated CPU time (s) 1119.46
Current children cumulated vsize (Kb) 35008

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7851 0 0 0 112879 67 0 0 25 0 1 0 1796464711 33705984 7749 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8229 7749 145 145 0 8084 0
[pid=9444] vsize: 32916
Current children cumulated CPU time (s) 1129.46
Current children cumulated vsize (Kb) 35040

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7851 0 0 0 113879 67 0 0 25 0 1 0 1796464711 33705984 7749 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8229 7749 145 145 0 8084 0
[pid=9444] vsize: 32916
Current children cumulated CPU time (s) 1139.46
Current children cumulated vsize (Kb) 35040

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7851 0 0 0 114879 67 0 0 25 0 1 0 1796464711 33705984 7749 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8229 7749 145 145 0 8084 0
[pid=9444] vsize: 32916
Current children cumulated CPU time (s) 1149.46
Current children cumulated vsize (Kb) 35040

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 115879 67 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1159.46
Current children cumulated vsize (Kb) 35072

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 116879 68 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1169.47
Current children cumulated vsize (Kb) 35072

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 117879 68 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1179.47
Current children cumulated vsize (Kb) 35072

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 118879 68 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1189.47
Current children cumulated vsize (Kb) 35072

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 119879 68 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1199.47
Current children cumulated vsize (Kb) 35072

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 120879 68 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1209.47
Current children cumulated vsize (Kb) 35072



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 9444
Raw data (/proc/9440/stat): 9440 (minisat+_script) S 9439 9440 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1796464706 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9440/statm): 531 226 485 147 0 384 0
[pid=9440] vsize: 2124
Raw data (/proc/9444/stat): 9444 (minisat+_64-bit) R 9440 9440 8263 0 -1 0 7858 0 0 0 120880 68 0 0 25 0 1 0 1796464711 33738752 7756 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9444/statm): 8237 7756 145 145 0 8092 0
[pid=9444] vsize: 32948
Current children cumulated CPU time (s) 1209.48
Current children cumulated vsize (Kb) 35072

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.51
CPU user time (s): 1208.8
CPU system time (s): 0.703892
CPU usage (%): 99.9483
Max. virtual memory (cumulated for all children) (Kb): 35072

Verifier Data

ERROR: no interpretation found !