Some explanations

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

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM4f5f6e30a602f3968daa9ca41c7da043
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1984
Optimality of the best value was proved NO
Number of terms in the objective function 133
Biggest coefficient in the objective function 128
Number of bits for the biggest coefficient in the objective function 8
Sum of the numbers in the objective function 9334
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 1024
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 9334
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.14
Number of variables133
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 constraint81

Trace number 6302

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        903792 kB
Buffers:         17956 kB
Cached:          85264 kB
SwapCached:        888 kB
Active:          22036 kB
Inactive:        83812 kB
HighTotal:      131008 kB
HighFree:        42308 kB
LowTotal:       903652 kB
LowFree:        861484 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            19220 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:41:06 (client local time) WITH STATUS 10 IN 1209.3 SECONDS
stats: 3460 7 1209.3 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:    7
c ---[  71]---> BDD-cost:    7
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    7
c ---[  63]---> BDD-cost:    7
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  868     Base: 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  898     Base: 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1011     Base: 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1043     Base: 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  488     Base: 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 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
c ---[   0]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25058    60127 |    8352       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 7865
c ---[   0]---> Sorter-cost: 2067     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   29745    71113 |    9915       2       22    11.0 |  0.000 % |
c ==============================================================================
c Found solution: 4982
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        57 |   29959    71656 |    9986      57      225     3.9 |  0.000 % |
c ==============================================================================
c Found solution: 4278
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       104 |   30029    71844 |   10009     104      412     4.0 |  0.000 % |
c ==============================================================================
c Found solution: 3709
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       122 |   30077    71967 |   10025     122      476     3.9 |  0.000 % |
c ==============================================================================
c Found solution: 3587
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       129 |   30088    71998 |   10029     129      559     4.3 |  0.000 % |
c ==============================================================================
c Found solution: 2685
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       213 |   30158    72168 |   10052     213     1235     5.8 |  0.000 % |
c ==============================================================================
c Found solution: 2654
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       235 |   30170    72207 |   10056     235     1355     5.8 |  0.000 % |
c ==============================================================================
c Found solution: 2646
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30177    72225 |   10059     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2645
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30184    72243 |   10061     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2642
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30194    72272 |   10064     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2641
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30203    72294 |   10067     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2581
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30207    72303 |   10069     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2578
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30211    72312 |   10070     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2577
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30215    72321 |   10071     244     1386     5.7 |  0.000 % |
c ==============================================================================
c Found solution: 2575
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       257 |   30221    72335 |   10073     257     1482     5.8 |  0.000 % |
c ==============================================================================
c Found solution: 2562
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       283 |   30228    72351 |   10076     283     1645     5.8 |  0.000 % |
c |       383 |   30228    72351 |   11083     383     2370     6.2 |  0.519 % |
c |       533 |   30222    72339 |   12191     532     3734     7.0 |  0.535 % |
c ==============================================================================
c Found solution: 2433
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       539 |   30243    72391 |   10081     538     3828     7.1 |  0.535 % |
c ==============================================================================
c Found solution: 2432
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       568 |   30255    72425 |   10085     567     4202     7.4 |  0.535 % |
c ==============================================================================
c Found solution: 2304
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       599 |   30265    72449 |   10088     598     4520     7.6 |  0.535 % |
c |       701 |   30265    72449 |   11096     700     5583     8.0 |  0.551 % |
c |       853 |   30265    72449 |   12206     852     8308     9.8 |  0.551 % |
c |      1079 |   30265    72449 |   13427    1078    11040    10.2 |  0.551 % |
c |      1416 |   30265    72449 |   14769    1415    16310    11.5 |  0.551 % |
c ==============================================================================
c Found solution: 2303
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1905 |   30271    72462 |   10090    1904    21674    11.4 |  0.551 % |
c |      2009 |   30269    72458 |   11099    2005    22744    11.3 |  0.562 % |
c |      2160 |   30269    72458 |   12208    2156    25543    11.8 |  0.562 % |
c |      2385 |   30259    72437 |   13429    2358    28130    11.9 |  0.594 % |
c |      2724 |   30258    72434 |   14772    2672    35247    13.2 |  0.599 % |
c ==============================================================================
c Found solution: 2302
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2936 |   30263    72445 |   10087    2884    40313    14.0 |  0.599 % |
c |      3038 |   30263    72445 |   11095    2986    41318    13.8 |  0.605 % |
c |      3188 |   30263    72445 |   12205    3136    43360    13.8 |  0.605 % |
c |      3414 |   30263    72445 |   13425    3362    47053    14.0 |  0.605 % |
c ==============================================================================
c Found solution: 2280
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3647 |   30287    72507 |   10095    3595    50008    13.9 |  0.605 % |
c |      3747 |   30287    72507 |   11104    3695    52982    14.3 |  0.615 % |
c |      3897 |   30287    72507 |   12214    3845    55042    14.3 |  0.615 % |
c ==============================================================================
c Found solution: 2278
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4089 |   30295    72532 |   10098    4037    60000    14.9 |  0.615 % |
c |      4189 |   30293    72528 |   11107    4136    61270    14.8 |  0.626 % |
c |      4340 |   30293    72528 |   12218    4287    62565    14.6 |  0.626 % |
c |      4565 |   30293    72528 |   13440    4512    68337    15.1 |  0.626 % |
c |      4905 |   30293    72528 |   14784    4852    84491    17.4 |  0.626 % |
c |      5411 |   30293    72528 |   16262    5358    96213    18.0 |  0.626 % |
c |      6170 |   30287    72514 |   17889    6098   112050    18.4 |  0.647 % |
c ==============================================================================
c Found solution: 2228
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6491 |   30294    72533 |   10098    6419   118900    18.5 |  0.647 % |
c |      6591 |   30294    72533 |   11107    6519   121991    18.7 |  0.652 % |
c |      6742 |   30294    72533 |   12218    6670   123908    18.6 |  0.652 % |
c |      6967 |   30294    72533 |   13440    6895   128894    18.7 |  0.652 % |
c |      7304 |   30294    72533 |   14784    7232   135222    18.7 |  0.652 % |
c |      7810 |   30294    72533 |   16262    7738   154229    19.9 |  0.652 % |
c ==============================================================================
c Found solution: 2163
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7969 |   30301    72554 |   10100    7897   156108    19.8 |  0.652 % |
c |      8069 |   30301    72554 |   11110    7997   158680    19.8 |  0.658 % |
c |      8219 |   30301    72554 |   12221    8147   164256    20.2 |  0.658 % |
c |      8444 |   30301    72554 |   13443    8372   168166    20.1 |  0.658 % |
c ==============================================================================
c Found solution: 2049
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8508 |   30308    72569 |   10102    8436   171099    20.3 |  0.658 % |
c |      8608 |   30308    72569 |   11112    8536   173093    20.3 |  0.663 % |
c |      8760 |   30308    72569 |   12223    8688   176166    20.3 |  0.663 % |
c |      8985 |   30308    72569 |   13445    8913   183116    20.5 |  0.663 % |
c |      9322 |   30308    72569 |   14790    9250   209552    22.7 |  0.663 % |
c ==============================================================================
c Found solution: 2048
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9770 |   30304    72561 |   10101    9696   232110    23.9 |  0.663 % |
c |      9871 |   30304    72561 |   11111    9797   233194    23.8 |  0.690 % |
c |     10021 |   30304    72561 |   12222    9947   238904    24.0 |  0.690 % |
c |     10246 |   30304    72561 |   13444   10172   243667    24.0 |  0.690 % |
c |     10584 |   30304    72561 |   14788   10510   257383    24.5 |  0.690 % |
c |     11090 |   30304    72561 |   16267   11016   272958    24.8 |  0.690 % |
c |     11849 |   30304    72561 |   17894   11775   305277    25.9 |  0.690 % |
c |     12988 |   30304    72561 |   19683   12914   325888    25.2 |  0.690 % |
c |     14697 |   30304    72561 |   21652   14623   466104    31.9 |  0.690 % |
c |     17260 |   30289    72526 |   23817   17110   529488    30.9 |  0.717 % |
c ==============================================================================
c Found solution: 2042
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20917 |   30278    72502 |   10092   20754   676782    32.6 |  0.717 % |
c |     21017 |   30278    72502 |   11101    5289   123412    23.3 |  0.781 % |
c |     21167 |   30278    72502 |   12211    5439   126170    23.2 |  0.781 % |
c |     21393 |   30278    72502 |   13432    5665   129534    22.9 |  0.781 % |
c |     21730 |   30278    72502 |   14775    6002   155817    26.0 |  0.781 % |
c |     22236 |   30278    72502 |   16253    6508   178176    27.4 |  0.781 % |
c |     22995 |   30278    72502 |   17878    7267   199606    27.5 |  0.781 % |
c |     24137 |   30276    72498 |   19666    8408   238458    28.4 |  0.787 % |
c |     25845 |   30276    72498 |   21633   10116   276591    27.3 |  0.787 % |
c |     28408 |   30276    72498 |   23796   12679   426829    33.7 |  0.787 % |
c |     32252 |   30276    72498 |   26176   16523   540088    32.7 |  0.787 % |
c ==============================================================================
c Found solution: 2040
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37912 |   30282    72511 |   10094   22183   733704    33.1 |  0.787 % |
c |     38015 |   30282    72511 |   11103    5650   122697    21.7 |  0.792 % |
c |     38165 |   30282    72511 |   12213    5800   128333    22.1 |  0.792 % |
c |     38390 |   30282    72511 |   13435    6025   138366    23.0 |  0.792 % |
c |     38727 |   30282    72511 |   14778    6362   150039    23.6 |  0.792 % |
c |     39234 |   30282    72511 |   16256    6869   168341    24.5 |  0.792 % |
c |     39995 |   30282    72511 |   17882    7630   190345    24.9 |  0.792 % |
c |     41137 |   30282    72511 |   19670    8772   221960    25.3 |  0.792 % |
c |     42846 |   30282    72511 |   21637   10481   293277    28.0 |  0.792 % |
c |     45409 |   30282    72511 |   23801   13044   470017    36.0 |  0.792 % |
c |     49257 |   30282    72511 |   26181   16892   662441    39.2 |  0.792 % |
c ==============================================================================
c Found solution: 2038
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50921 |   30293    72537 |   10097   18556   729401    39.3 |  0.792 % |
c |     51021 |   30293    72537 |   11106    9378   293455    31.3 |  0.813 % |
c |     51171 |   30293    72537 |   12217    9528   298447    31.3 |  0.813 % |
c |     51396 |   30293    72537 |   13439    9753   303506    31.1 |  0.813 % |
c |     51733 |   30293    72537 |   14783   10090   316145    31.3 |  0.813 % |
c |     52240 |   30293    72537 |   16261   10597   338448    31.9 |  0.813 % |
c |     52999 |   30293    72537 |   17887   11356   372821    32.8 |  0.813 % |
c |     54138 |   30293    72537 |   19676   12495   422072    33.8 |  0.813 % |
c |     55846 |   30293    72537 |   21643   14203   509563    35.9 |  0.813 % |
c |     58408 |   30293    72537 |   23808   16765   655374    39.1 |  0.813 % |
c |     62254 |   30293    72537 |   26189   20611   938462    45.5 |  0.813 % |
c |     68021 |   30293    72537 |   28807   26378  1255036    47.6 |  0.813 % |
c |     76670 |   30293    72537 |   31688   35027  2091568    59.7 |  0.813 % |
c |     89644 |   30293    72537 |   34857   29230  2035256    69.6 |  0.813 % |
c |    109106 |   30293    72537 |   38343   24662  1710977    69.4 |  0.813 % |
c |    138298 |   30289    72528 |   42177   31620  2254632    71.3 |  0.819 % |
c |    182089 |   30289    72528 |   46395   42844  4397296   102.6 |  0.819 % |
c ==============================================================================
c Found solution: 2037
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    208814 |   30294    72543 |   10098   40026  3122766    78.0 |  0.819 % |
c |    208914 |   30294    72543 |   11107    9107   453328    49.8 |  0.824 % |
c |    209066 |   30294    72543 |   12218    9259   460063    49.7 |  0.824 % |
c |    209291 |   30294    72543 |   13440    9484   473442    49.9 |  0.824 % |
c |    209628 |   30294    72543 |   14784    9821   497096    50.6 |  0.824 % |
c |    210134 |   30294    72543 |   16262   10327   513875    49.8 |  0.824 % |
c |    210893 |   30294    72543 |   17889   11086   558188    50.4 |  0.824 % |
c |    212033 |   30294    72543 |   19678   12226   646452    52.9 |  0.824 % |
c |    213742 |   30294    72543 |   21645   13935   758196    54.4 |  0.824 % |
c |    216305 |   30294    72543 |   23810   16498   885107    53.6 |  0.824 % |
c ==============================================================================
c Found solution: 2036
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217979 |   30298    72553 |   10099   18172   958657    52.8 |  0.824 % |
c |    218079 |   30298    72553 |   11108    9186   260984    28.4 |  0.829 % |
c |    218231 |   30298    72553 |   12219    9338   264238    28.3 |  0.829 % |
c |    218460 |   30298    72553 |   13441    9567   270453    28.3 |  0.829 % |
c |    218797 |   30298    72553 |   14785    9904   281067    28.4 |  0.829 % |
c |    219305 |   30298    72553 |   16264   10412   301155    28.9 |  0.829 % |
c |    220065 |   30298    72553 |   17890   11172   328923    29.4 |  0.829 % |
c |    221206 |   30298    72553 |   19680   12313   374119    30.4 |  0.829 % |
c |    222915 |   30298    72553 |   21648   14022   413782    29.5 |  0.829 % |
c ==============================================================================
c Found solution: 2035
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225286 |   30301    72560 |   10100   16393   497229    30.3 |  0.829 % |
c |    225386 |   30301    72560 |   11110    8297   146061    17.6 |  0.834 % |
c |    225538 |   30301    72560 |   12221    8449   150054    17.8 |  0.834 % |
c |    225763 |   30301    72560 |   13443    8674   154553    17.8 |  0.834 % |
c |    226100 |   30301    72560 |   14787    9011   161769    18.0 |  0.834 % |
c |    226606 |   30301    72560 |   16266    9517   181575    19.1 |  0.834 % |
c |    227366 |   30301    72560 |   17892   10277   216146    21.0 |  0.834 % |
c |    228506 |   30301    72560 |   19682   11417   261748    22.9 |  0.834 % |
c |    230214 |   30301    72560 |   21650   13125   312840    23.8 |  0.834 % |
c ==============================================================================
c Found solution: 2034
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    232171 |   30305    72571 |   10101   15082   399414    26.5 |  0.834 % |
c |    232271 |   30305    72571 |   11111    7641   150076    19.6 |  0.840 % |
c |    232421 |   30298    72556 |   12222    7754   152557    19.7 |  0.861 % |
c |    232646 |   30298    72556 |   13444    7979   171379    21.5 |  0.861 % |
c |    232985 |   30298    72556 |   14788    8318   184740    22.2 |  0.861 % |
c |    233492 |   30298    72556 |   16267    8825   211213    23.9 |  0.861 % |
c |    234251 |   30298    72556 |   17894    9584   244037    25.5 |  0.861 % |
c |    235390 |   30298    72556 |   19683   10723   305332    28.5 |  0.861 % |
c |    237099 |   30298    72556 |   21652   12432   363109    29.2 |  0.861 % |
c |    239661 |   30298    72556 |   23817   14994   486752    32.5 |  0.861 % |
c |    243505 |   30298    72556 |   26199   18838   856949    45.5 |  0.861 % |
c ==============================================================================
c Found solution: 2018
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    246171 |   30304    72571 |   10101   21504   948392    44.1 |  0.861 % |
c |    246272 |   30304    72571 |   11111    5477    65194    11.9 |  0.866 % |
c |    246423 |   30304    72571 |   12222    5628    67034    11.9 |  0.866 % |
c |    246648 |   30304    72571 |   13444    5853    76394    13.1 |  0.866 % |
c |    246985 |   30304    72571 |   14788    6190    92176    14.9 |  0.866 % |
c |    247491 |   30304    72571 |   16267    6696   128503    19.2 |  0.866 % |
c |    248250 |   30304    72571 |   17894    7455   161534    21.7 |  0.866 % |
c |    249389 |   30304    72571 |   19683    8594   239195    27.8 |  0.866 % |
c |    251097 |   30304    72571 |   21652   10302   363537    35.3 |  0.866 % |
c |    253660 |   30304    72571 |   23817   12865   469870    36.5 |  0.866 % |
c |    257506 |   30304    72571 |   26199   16711   628632    37.6 |  0.866 % |
c |    263273 |   30304    72571 |   28819   22478  1114326    49.6 |  0.866 % |
c |    271922 |   30304    72571 |   31701   31127  1854890    59.6 |  0.866 % |
c ==============================================================================
c Found solution: 2017
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    272492 |   30310    72586 |   10103   31697  1879788    59.3 |  0.866 % |
c |    272593 |   30310    72586 |   11113    8026   239606    29.9 |  0.871 % |
c |    272743 |   30310    72586 |   12224    8176   244624    29.9 |  0.872 % |
c |    272968 |   30310    72586 |   13447    8401   248454    29.6 |  0.871 % |
c |    273305 |   30310    72586 |   14791    8738   257058    29.4 |  0.871 % |
c |    273811 |   30114    72175 |   16270    9201   282448    30.7 |  1.366 % |
c |    274571 |   30114    72175 |   17898    9961   344514    34.6 |  1.366 % |
c |    275710 |   30114    72175 |   19687   11100   419701    37.8 |  1.366 % |
c |    277419 |   30114    72175 |   21656   12809   518184    40.5 |  1.366 % |
c |    279987 |   30114    72175 |   23822   15377   725371    47.2 |  1.366 % |
c |    283832 |   30114    72175 |   26204   19222  1130563    58.8 |  1.366 % |
c |    289601 |   30114    72175 |   28825   24991  1796894    71.9 |  1.366 % |
c |    298250 |   30114    72175 |   31707   33640  2795713    83.1 |  1.366 % |
c ==============================================================================
c Found solution: 2016
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    306549 |   30112    72174 |   10037   25118  1840003    73.3 |  1.366 % |
c |    306650 |   30112    72174 |   11040    6381    90787    14.2 |  1.393 % |
c |    306800 |   30112    72174 |   12144    6531    94048    14.4 |  1.393 % |
c |    307026 |   30112    72174 |   13359    6757   102663    15.2 |  1.393 % |
c |    307363 |   30112    72174 |   14695    7094   120332    17.0 |  1.393 % |
c |    307869 |   30112    72174 |   16164    7600   143661    18.9 |  1.393 % |
c |    308630 |   30112    72174 |   17781    8361   165407    19.8 |  1.393 % |
c |    309769 |   30091    72125 |   19559    9486   225158    23.7 |  1.431 % |
c |    311478 |   30091    72125 |   21515   11195   273080    24.4 |  1.431 % |
c |    314040 |   30091    72125 |   23666   13757   442865    32.2 |  1.431 % |
c |    317884 |   30091    72125 |   26033   17601   650760    37.0 |  1.431 % |
c |    323650 |   30080    72102 |   28636   23363   995344    42.6 |  1.452 % |
c |    332299 |   30058    72055 |   31500   15252   514538    33.7 |  1.500 % |
c |    345274 |   30058    72055 |   34650   28227  1015690    36.0 |  1.501 % |
c ==============================================================================
c Found solution: 1987
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    348188 |   30065    72071 |   10021   31141  1135656    36.5 |  1.501 % |
c |    348288 |   30065    72071 |   11023    7886   130211    16.5 |  1.506 % |
c |    348440 |   30065    72071 |   12125    8038   133603    16.6 |  1.506 % |
c |    348665 |   30065    72071 |   13337    8263   138357    16.7 |  1.506 % |
c |    349002 |   30065    72071 |   14671    8600   165696    19.3 |  1.506 % |
c |    349508 |   30060    72060 |   16138    9091   192789    21.2 |  1.522 % |
c |    350267 |   30060    72060 |   17752    9850   229398    23.3 |  1.522 % |
c |    351406 |   30060    72060 |   19528   10989   320079    29.1 |  1.522 % |
c |    353114 |   30060    72060 |   21480   12697   397146    31.3 |  1.522 % |
c ==============================================================================
c Found solution: 1986
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    354243 |   30066    72074 |   10022   13826   467725    33.8 |  1.522 % |
c |    354343 |   30066    72074 |   11024    7013   154795    22.1 |  1.527 % |
c |    354493 |   30066    72074 |   12126    7163   158225    22.1 |  1.527 % |
c |    354720 |   30066    72074 |   13339    7390   167735    22.7 |  1.527 % |
c |    355057 |   30066    72074 |   14673    7727   174615    22.6 |  1.527 % |
c |    355563 |   30066    72074 |   16140    8233   189784    23.1 |  1.527 % |
c |    356322 |   30066    72074 |   17754    8992   221782    24.7 |  1.527 % |
c |    357461 |   30066    72074 |   19530   10131   287813    28.4 |  1.527 % |
c |    359169 |   30063    72067 |   21483   11804   379485    32.1 |  1.537 % |
c |    361731 |   30063    72067 |   23631   14366   515415    35.9 |  1.538 % |
c |    365576 |   30063    72067 |   25994   18211   857635    47.1 |  1.538 % |
c |    371342 |   30063    72067 |   28593   23977  1254320    52.3 |  1.538 % |
c ==============================================================================
c Found solution: 1985
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    379796 |   30069    72081 |   10023   32431  1921379    59.2 |  1.538 % |
c |    379896 |   30069    72081 |   11025    8208   230839    28.1 |  1.543 % |
c |    380046 |   30052    72046 |   12127    8349   238475    28.6 |  1.591 % |
c |    380271 |   30052    72046 |   13340    8574   242818    28.3 |  1.591 % |
c |    380608 |   30052    72046 |   14674    8911   253941    28.5 |  1.591 % |
c |    381114 |   30052    72046 |   16142    9417   272863    29.0 |  1.591 % |
c |    381873 |   30052    72046 |   17756   10176   294633    29.0 |  1.591 % |
c |    383013 |   30052    72046 |   19531   11316   425644    37.6 |  1.591 % |
c |    384721 |   30052    72046 |   21485   13024   514701    39.5 |  1.591 % |
c |    387284 |   30039    72019 |   23633   15576   811143    52.1 |  1.629 % |
c |    391130 |   30039    72019 |   25997   19422   993229    51.1 |  1.629 % |
c |    396897 |   30039    72019 |   28596   25189  1197276    47.5 |  1.629 % |
c |    405546 |   30039    72019 |   31456   33838  2349966    69.4 |  1.629 % |
c ==============================================================================
c Found solution: 1984
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    412452 |   30045    72033 |   10015   23825  1563799    65.6 |  1.629 % |
c |    412553 |   30045    72033 |   11016    6058    63936    10.6 |  1.634 % |
c |    412706 |   30045    72033 |   12118    6211    66641    10.7 |  1.634 % |
c |    412931 |   30045    72033 |   13329    6436    73707    11.5 |  1.634 % |
c |    413268 |   30045    72033 |   14662    6772    82297    12.2 |  1.650 % |
c |    413774 |   30040    72022 |   16129    7277    90265    12.4 |  1.650 % |
c |    414535 |   30040    72022 |   17742    8038   122557    15.2 |  1.650 % |
c |    415674 |   30040    72022 |   19516    9177   145477    15.9 |  1.650 % |
c |    417383 |   30040    72022 |   21468   10886   341590    31.4 |  1.650 % |
c |    419946 |   30040    72022 |   23614   13449   485434    36.1 |  1.650 % |
c |    423792 |   30040    72022 |   25976   17295   651050    37.6 |  1.650 % |
c |    429558 |   30040    72022 |   28573   23061   852779    37.0 |  1.650 % |
c |    438208 |   30016    71967 |   31431   31704  1553912    49.0 |  1.687 % |
c |    451183 |   30002    71936 |   34574   28660  2011024    70.2 |  1.730 % |
c ==============================================================================
c Found solution: 1963
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    465057 |   30009    71953 |   10003   24428  1513836    62.0 |  1.730 % |
c |    465157 |   30006    71946 |   11003    6206   165676    26.7 |  1.746 % |
c |    465307 |   30006    71946 |   12103    6356   171394    27.0 |  1.746 % |
c |    465536 |   29882    71673 |   13313    6550   174477    26.6 |  2.095 % |
c |    465874 |   29877    71661 |   14645    6674   179880    27.0 |  2.111 % |
c |    466380 |   29877    71661 |   16109    7180   197269    27.5 |  2.111 % |
c |    467142 |   29877    71661 |   17720    7942   239540    30.2 |  2.111 % |
c |    468282 |   29877    71661 |   19493    9082   291813    32.1 |  2.111 % |
c |    469990 |   29877    71661 |   21442   10790   344114    31.9 |  2.111 % |
c |    472553 |   29877    71661 |   23586   13353   432431    32.4 |  2.111 % |
c |    476397 |   29877    71661 |   25945   17197   576325    33.5 |  2.111 % |
c |    482163 |   29877    71661 |   28539   22963  1062955    46.3 |  2.111 % |
c |    490812 |   29873    71653 |   31393   31610  1482964    46.9 |  2.122 % |
c |    503787 |   29873    71653 |   34533   22465  1213509    54.0 |  2.122 % |
c |    523249 |   29873    71653 |   37986   21048  1041990    49.5 |  2.122 % |
c |    552441 |   29865    71635 |   41785   23381  2648690   113.3 |  2.149 % |
c |    596230 |   29865    71635 |   45963   36314  3603614    99.2 |  2.149 % |
c ==============================================================================
c Found solution: 1962
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    660239 |   29872    71652 |    9957   34216  1695417    49.6 |  2.149 % |
c |    660339 |   29872    71652 |   10952    8654   132559    15.3 |  2.154 % |
c |    660489 |   29872    71652 |   12047    8804   136022    15.5 |  2.154 % |
c |    660714 |   29872    71652 |   13252    9029   151945    16.8 |  2.154 % |
c |    661051 |   29872    71652 |   14578    9366   160732    17.2 |  2.154 % |
c |    661557 |   29869    71646 |   16035    9871   193841    19.6 |  2.159 % |
c |    662317 |   29869    71646 |   17639   10631   222334    20.9 |  2.159 % |
c |    663456 |   29860    71627 |   19403   11768   255780    21.7 |  2.186 % |
c |    665164 |   29860    71627 |   21343   13476   372429    27.6 |  2.186 % |
c |    667728 |   29860    71627 |   23478   16040   668467    41.7 |  2.186 % |
c |    671575 |   29860    71627 |   25825   19887   878314    44.2 |  2.186 % |

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/28295/stat): 28295 (minisat+_script) R 28294 28295 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1856000325 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28295/statm): 174 3 169 147 0 27 0
[pid=28295] 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=28296
New process pid=28297
New process pid=28298
execve syscall for /bin/sed executable
One traced child (pid=28297) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=28298) exited with status: 0
One traced child (pid=28296) exited with status: 0
New process pid=28299
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-neos5.opb

[startup+10.0037 s]
Raw data (loadavg): 0.89 0.95 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 1993 0 0 0 978 10 0 0 25 0 1 0 1856000330 9154560 1892 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 2235 1892 145 145 0 2090 0
[pid=28299] vsize: 8940
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 11064

[startup+20.0053 s]
Raw data (loadavg): 0.90 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2394 0 0 0 1971 14 0 0 25 0 1 0 1856000330 10801152 2293 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 2637 2293 145 145 0 2492 0
[pid=28299] vsize: 10548
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 12672

[startup+30.0069 s]
Raw data (loadavg): 0.92 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2671 0 0 0 2965 18 0 0 25 0 1 0 1856000330 11972608 2570 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 2923 2570 145 145 0 2778 0
[pid=28299] vsize: 11692
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 13816

[startup+40.0075 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2671 0 0 0 3964 18 0 0 25 0 1 0 1856000330 11972608 2570 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 2923 2570 145 145 0 2778 0
[pid=28299] vsize: 11692
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 13816

[startup+50.0081 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2788 0 0 0 4962 19 0 0 25 0 1 0 1856000330 12447744 2687 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 3039 2687 145 145 0 2894 0
[pid=28299] vsize: 12156
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 14280

[startup+60.0097 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2788 0 0 0 5962 19 0 0 25 0 1 0 1856000330 12447744 2687 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 3039 2687 145 145 0 2894 0
[pid=28299] vsize: 12156
Current children cumulated CPU time (s) 59.81
Current children cumulated vsize (Kb) 14280

[startup+70.0103 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2805 0 0 0 6961 20 0 0 25 0 1 0 1856000330 12517376 2704 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 3056 2704 145 145 0 2911 0
[pid=28299] vsize: 12224
Current children cumulated CPU time (s) 69.81
Current children cumulated vsize (Kb) 14348

[startup+80.0119 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 3102 0 0 0 7956 22 0 0 25 0 1 0 1856000330 13742080 3001 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 3355 3001 145 145 0 3210 0
[pid=28299] vsize: 13420
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 15544

[startup+90.0125 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 3585 0 0 0 8946 27 0 0 25 0 1 0 1856000330 15695872 3484 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 3832 3484 145 145 0 3687 0
[pid=28299] vsize: 15328
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 17452

[startup+100.013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4234 0 0 0 9935 32 0 0 25 0 1 0 1856000330 18464768 4133 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 4508 4133 145 145 0 4363 0
[pid=28299] vsize: 18032
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 20156

[startup+110.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4304 0 0 0 10933 34 0 0 25 0 1 0 1856000330 18747392 4203 4294967295 134512640 135094434 3221224432 3221223104 134555614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 4577 4203 145 145 0 4432 0
[pid=28299] vsize: 18308
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 20432

[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4304 0 0 0 11933 34 0 0 25 0 1 0 1856000330 18747392 4203 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 4577 4203 145 145 0 4432 0
[pid=28299] vsize: 18308
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 20432

[startup+130.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4548 0 0 0 12926 37 0 0 25 0 1 0 1856000330 19750912 4447 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 4822 4447 145 145 0 4677 0
[pid=28299] vsize: 19288
Current children cumulated CPU time (s) 129.63
Current children cumulated vsize (Kb) 21412

[startup+140.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5128 0 0 0 13914 43 0 0 25 0 1 0 1856000330 22110208 5027 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5398 5027 145 145 0 5253 0
[pid=28299] vsize: 21592
Current children cumulated CPU time (s) 139.57
Current children cumulated vsize (Kb) 23716

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5478 0 0 0 14907 47 0 0 25 0 1 0 1856000330 23539712 5377 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5747 5377 145 145 0 5602 0
[pid=28299] vsize: 22988
Current children cumulated CPU time (s) 149.54
Current children cumulated vsize (Kb) 25112

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 15907 47 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0
[pid=28299] vsize: 22988
Current children cumulated CPU time (s) 159.54
Current children cumulated vsize (Kb) 25112

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 16906 48 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0
[pid=28299] vsize: 22988
Current children cumulated CPU time (s) 169.54
Current children cumulated vsize (Kb) 25112

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 17906 48 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0
[pid=28299] vsize: 22988
Current children cumulated CPU time (s) 179.54
Current children cumulated vsize (Kb) 25112

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 18906 48 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0
[pid=28299] vsize: 22988
Current children cumulated CPU time (s) 189.54
Current children cumulated vsize (Kb) 25112

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 19904 50 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0
[pid=28299] vsize: 23288
Current children cumulated CPU time (s) 199.54
Current children cumulated vsize (Kb) 25412

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 20903 50 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0
[pid=28299] vsize: 23288
Current children cumulated CPU time (s) 209.53
Current children cumulated vsize (Kb) 25412

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 21903 51 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0
[pid=28299] vsize: 23288
Current children cumulated CPU time (s) 219.54
Current children cumulated vsize (Kb) 25412

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 22902 51 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0
[pid=28299] vsize: 23288
Current children cumulated CPU time (s) 229.53
Current children cumulated vsize (Kb) 25412

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5780 0 0 0 23897 53 0 0 25 0 1 0 1856000330 24780800 5679 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 6050 5679 145 145 0 5905 0
[pid=28299] vsize: 24200
Current children cumulated CPU time (s) 239.5
Current children cumulated vsize (Kb) 26324

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6176 0 0 0 24890 56 0 0 25 0 1 0 1856000330 26386432 6075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 6442 6075 145 145 0 6297 0
[pid=28299] vsize: 25768
Current children cumulated CPU time (s) 249.46
Current children cumulated vsize (Kb) 27892

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6572 0 0 0 25884 59 0 0 25 0 1 0 1856000330 28000256 6471 4294967295 134512640 135094434 3221224432 3221223056 134562076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 6836 6471 145 145 0 6691 0
[pid=28299] vsize: 27344
Current children cumulated CPU time (s) 259.43
Current children cumulated vsize (Kb) 29468

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6884 0 0 0 26878 62 0 0 25 0 1 0 1856000330 29274112 6783 4294967295 134512640 135094434 3221224432 3221223024 134551876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7147 6783 145 145 0 7002 0
[pid=28299] vsize: 28588
Current children cumulated CPU time (s) 269.4
Current children cumulated vsize (Kb) 30712

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6884 0 0 0 27878 62 0 0 25 0 1 0 1856000330 29274112 6783 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7147 6783 145 145 0 7002 0
[pid=28299] vsize: 28588
Current children cumulated CPU time (s) 279.4
Current children cumulated vsize (Kb) 30712

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6884 0 0 0 28878 62 0 0 25 0 1 0 1856000330 29274112 6783 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7147 6783 145 145 0 7002 0
[pid=28299] vsize: 28588
Current children cumulated CPU time (s) 289.4
Current children cumulated vsize (Kb) 30712

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6889 0 0 0 29879 62 0 0 25 0 1 0 1856000330 29306880 6788 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7155 6788 145 145 0 7010 0
[pid=28299] vsize: 28620
Current children cumulated CPU time (s) 299.41
Current children cumulated vsize (Kb) 30744

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 30879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0
[pid=28299] vsize: 28620
Current children cumulated CPU time (s) 309.41
Current children cumulated vsize (Kb) 30744

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 31879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0
[pid=28299] vsize: 28620
Current children cumulated CPU time (s) 319.41
Current children cumulated vsize (Kb) 30744

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 32879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0
[pid=28299] vsize: 28620
Current children cumulated CPU time (s) 329.41
Current children cumulated vsize (Kb) 30744

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 33879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0
[pid=28299] vsize: 28620
Current children cumulated CPU time (s) 339.41
Current children cumulated vsize (Kb) 30744

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7206 0 0 0 34874 64 0 0 25 0 1 0 1856000330 30625792 7105 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7477 7105 145 145 0 7332 0
[pid=28299] vsize: 29908
Current children cumulated CPU time (s) 349.38
Current children cumulated vsize (Kb) 32032

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7562 0 0 0 35868 66 0 0 25 0 1 0 1856000330 32092160 7461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7835 7461 145 145 0 7690 0
[pid=28299] vsize: 31340
Current children cumulated CPU time (s) 359.34
Current children cumulated vsize (Kb) 33464

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 36867 67 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0
[pid=28299] vsize: 31416
Current children cumulated CPU time (s) 369.34
Current children cumulated vsize (Kb) 33540

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 37865 67 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0
[pid=28299] vsize: 31416
Current children cumulated CPU time (s) 379.32
Current children cumulated vsize (Kb) 33540

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 38865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0
[pid=28299] vsize: 31416
Current children cumulated CPU time (s) 389.33
Current children cumulated vsize (Kb) 33540

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 39865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0
[pid=28299] vsize: 31416
Current children cumulated CPU time (s) 399.33
Current children cumulated vsize (Kb) 33540

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 40865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0
[pid=28299] vsize: 31416
Current children cumulated CPU time (s) 409.33
Current children cumulated vsize (Kb) 33540

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 41865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0
[pid=28299] vsize: 31416
Current children cumulated CPU time (s) 419.33
Current children cumulated vsize (Kb) 33540

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 42865 68 0 0 25 0 1 0 1856000330 32432128 7512 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7918 7512 145 145 0 7773 0
[pid=28299] vsize: 31672
Current children cumulated CPU time (s) 429.33
Current children cumulated vsize (Kb) 33796

[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 43865 68 0 0 25 0 1 0 1856000330 32432128 7512 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7918 7512 145 145 0 7773 0
[pid=28299] vsize: 31672
Current children cumulated CPU time (s) 439.33
Current children cumulated vsize (Kb) 33796

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 44866 68 0 0 25 0 1 0 1856000330 32432128 7512 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7918 7512 145 145 0 7773 0
[pid=28299] vsize: 31672
Current children cumulated CPU time (s) 449.34
Current children cumulated vsize (Kb) 33796

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 45866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 459.34
Current children cumulated vsize (Kb) 34052

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 46866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 469.34
Current children cumulated vsize (Kb) 34052

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 47866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 479.34
Current children cumulated vsize (Kb) 34052

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 48866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 489.34
Current children cumulated vsize (Kb) 34052

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 49867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 499.35
Current children cumulated vsize (Kb) 34052

[startup+510.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 50867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 509.35
Current children cumulated vsize (Kb) 34052

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 51867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 519.35
Current children cumulated vsize (Kb) 34052

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 52867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 529.35
Current children cumulated vsize (Kb) 34052

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 53868 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 539.36
Current children cumulated vsize (Kb) 34052

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 54868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 549.37
Current children cumulated vsize (Kb) 34052

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 55868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 559.37
Current children cumulated vsize (Kb) 34052

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 56868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 569.37
Current children cumulated vsize (Kb) 34052

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 57868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223024 134551704 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 579.37
Current children cumulated vsize (Kb) 34052

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 58868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 589.37
Current children cumulated vsize (Kb) 34052

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 59868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 599.37
Current children cumulated vsize (Kb) 34052

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 60868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 609.37
Current children cumulated vsize (Kb) 34052

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 61868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 619.37
Current children cumulated vsize (Kb) 34052

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 62869 70 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 629.39
Current children cumulated vsize (Kb) 34052

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 63869 70 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 639.39
Current children cumulated vsize (Kb) 34052

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 64869 70 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 649.39
Current children cumulated vsize (Kb) 34052

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 65869 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 659.39
Current children cumulated vsize (Kb) 34052

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 66869 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 669.39
Current children cumulated vsize (Kb) 34052

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 67870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 679.4
Current children cumulated vsize (Kb) 34052

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 68870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 689.4
Current children cumulated vsize (Kb) 34052

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 69870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 699.4
Current children cumulated vsize (Kb) 34052

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 70870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 709.4
Current children cumulated vsize (Kb) 34052

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 71870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 719.4
Current children cumulated vsize (Kb) 34052

[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 72870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 729.4
Current children cumulated vsize (Kb) 34052

[startup+740.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 73871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 739.41
Current children cumulated vsize (Kb) 34052

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 74871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 749.41
Current children cumulated vsize (Kb) 34052

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 75871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 759.41
Current children cumulated vsize (Kb) 34052

[startup+770.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 76871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 769.41
Current children cumulated vsize (Kb) 34052

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 77871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 779.41
Current children cumulated vsize (Kb) 34052

[startup+790.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 78872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 789.42
Current children cumulated vsize (Kb) 34052

[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 79872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 799.42
Current children cumulated vsize (Kb) 34052

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 80872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 809.42
Current children cumulated vsize (Kb) 34052

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 81872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 819.42
Current children cumulated vsize (Kb) 34052

[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 82873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 829.43
Current children cumulated vsize (Kb) 34052

[startup+840.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 83873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 839.43
Current children cumulated vsize (Kb) 34052

[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 84873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 849.43
Current children cumulated vsize (Kb) 34052

[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 85873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 859.43
Current children cumulated vsize (Kb) 34052

[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 86873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 869.43
Current children cumulated vsize (Kb) 34052

[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 87874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 879.44
Current children cumulated vsize (Kb) 34052

[startup+890.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 88874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 889.44
Current children cumulated vsize (Kb) 34052

[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 89874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 899.44
Current children cumulated vsize (Kb) 34052

[startup+910.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 90874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 909.44
Current children cumulated vsize (Kb) 34052

[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 91874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 919.44
Current children cumulated vsize (Kb) 34052

[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 92875 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 929.45
Current children cumulated vsize (Kb) 34052

[startup+940.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 93875 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 939.45
Current children cumulated vsize (Kb) 34052

[startup+950.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 94875 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0
[pid=28299] vsize: 31928
Current children cumulated CPU time (s) 949.45
Current children cumulated vsize (Kb) 34052

[startup+960.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7825 0 0 0 95873 72 0 0 25 0 1 0 1856000330 33546240 7724 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 8190 7724 145 145 0 8045 0
[pid=28299] vsize: 32760
Current children cumulated CPU time (s) 959.45
Current children cumulated vsize (Kb) 34884

[startup+970.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 8241 0 0 0 96865 76 0 0 25 0 1 0 1856000330 35250176 8140 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 8606 8140 145 145 0 8461 0
[pid=28299] vsize: 34424
Current children cumulated CPU time (s) 969.41
Current children cumulated vsize (Kb) 36548

[startup+980.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 8707 0 0 0 97857 79 0 0 25 0 1 0 1856000330 37183488 8606 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 9078 8606 145 145 0 8933 0
[pid=28299] vsize: 36312
Current children cumulated CPU time (s) 979.36
Current children cumulated vsize (Kb) 38436

[startup+990.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9159 0 0 0 98850 82 0 0 25 0 1 0 1856000330 39043072 9058 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 9532 9058 145 145 0 9387 0
[pid=28299] vsize: 38128
Current children cumulated CPU time (s) 989.32
Current children cumulated vsize (Kb) 40252

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9578 0 0 0 99843 85 0 0 25 0 1 0 1856000330 40775680 9477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 9955 9477 145 145 0 9810 0
[pid=28299] vsize: 39820
Current children cumulated CPU time (s) 999.28
Current children cumulated vsize (Kb) 41944

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9955 0 0 0 100836 88 0 0 25 0 1 0 1856000330 42319872 9854 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10332 9854 145 145 0 10187 0
[pid=28299] vsize: 41328
Current children cumulated CPU time (s) 1009.24
Current children cumulated vsize (Kb) 43452

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 101835 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1019.23
Current children cumulated vsize (Kb) 43600

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 102836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1029.24
Current children cumulated vsize (Kb) 43600

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 103836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1039.24
Current children cumulated vsize (Kb) 43600

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 104836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1049.24
Current children cumulated vsize (Kb) 43600

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 105836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1059.24
Current children cumulated vsize (Kb) 43600

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 106836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1069.24
Current children cumulated vsize (Kb) 43600

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 107837 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1079.25
Current children cumulated vsize (Kb) 43600

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 108837 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221222048 134562841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1089.25
Current children cumulated vsize (Kb) 43600

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 109837 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1099.25
Current children cumulated vsize (Kb) 43600

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 110837 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1109.25
Current children cumulated vsize (Kb) 43600

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 111838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1119.26
Current children cumulated vsize (Kb) 43600

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 112838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1129.26
Current children cumulated vsize (Kb) 43600

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 113838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1139.26
Current children cumulated vsize (Kb) 43600

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 114838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1149.26
Current children cumulated vsize (Kb) 43600

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 115838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1159.26
Current children cumulated vsize (Kb) 43600

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 116839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1169.27
Current children cumulated vsize (Kb) 43600

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 117839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1179.27
Current children cumulated vsize (Kb) 43600

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 118839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1189.27
Current children cumulated vsize (Kb) 43600

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 119839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1199.27
Current children cumulated vsize (Kb) 43600

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 120839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1209.27
Current children cumulated vsize (Kb) 43600



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28299
Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28295/statm): 531 226 485 147 0 384 0
[pid=28295] vsize: 2124
Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 120839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0
[pid=28299] vsize: 41476
Current children cumulated CPU time (s) 1209.27
Current children cumulated vsize (Kb) 43600

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.3
CPU user time (s): 1208.39
CPU system time (s): 0.909861
CPU usage (%): 99.9336
Max. virtual memory (cumulated for all children) (Kb): 43600

Verifier Data

ERROR: no interpretation found !