Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod013.opb
MD5SUMf118194cabf88b58b64a9e7aec087bc0
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 46012422
Optimality of the best value was proved NO
Number of terms in the objective function 1488
Biggest coefficient in the objective function 375272767488
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 12937590079727
Number of bits of the sum of numbers in the objective function 44
Biggest number in a constraint 375272767488
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 12937590079727
Number of bits of the biggest sum of numbers44
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.05
Number of variables1488
Total number of constraints110
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)48
Number of constraints which are nor clauses,nor cardinality constraints62
Minimum length of a constraint1
Maximum length of a constraint240

Trace number 3874

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        879376 kB
Buffers:         35632 kB
Cached:          92224 kB
SwapCached:        732 kB
Active:          63732 kB
Inactive:        66676 kB
HighTotal:      131008 kB
HighFree:        36988 kB
LowTotal:       903652 kB
LowFree:        842388 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19100 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:37:31 (client local time) WITH STATUS 10 IN 1207.99 SECONDS
stats: 2870 7 1207.99 10

Solver Data

c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   22
c ---[  62]---> BDD-cost:   19
c ---[  61]---> BDD-cost:   20
c ---[  60]---> BDD-cost:   18
c ---[  58]---> Sorter-cost: 1897     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   22
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   20
c ---[  50]---> BDD-cost:   18
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   17
c ---[  46]---> Sorter-cost: 1897     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   16
c ---[  43]---> BDD-cost:   19
c ---[  42]---> BDD-cost:   19
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   17
c ---[  37]---> BDD-cost:   17
c ---[  36]---> BDD-cost:   16
c ---[  34]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   17
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   17
c ---[  22]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   16
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   16
c ---[  12]---> BDD-cost:   16
c ---[  10]---> Sorter-cost: 1793     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   16
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   16
c ---[   4]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost: 1219     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   52235   123460 |   17411       0        0     nan |  0.000 % |
c |       100 |   52208   123399 |   19152      99      321     3.2 |  8.091 % |
c |       250 |   52197   123375 |   21067     248      956     3.9 |  8.107 % |
c |       475 |   52169   123313 |   23174     469     2028     4.3 |  8.149 % |
c ==============================================================================
c Found solution: 83322090
c ---[   0]---> Adder-cost: 5416   maxlim: 164477957   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       684 |   89762   257873 |   29920     675     3086     4.6 |  8.149 % |
c |       787 |   89607   257520 |   32912     765     3688     4.8 |  6.836 % |
c |       937 |   89607   257520 |   36203     915     4406     4.8 |  6.836 % |
c |      1162 |   89578   257454 |   39823    1139     5432     4.8 |  6.869 % |
c |      1499 |   89445   257150 |   43805    1472    11344     7.7 |  7.032 % |
c |      2005 |   89445   257150 |   48186    1978    29991    15.2 |  7.032 % |
c ==============================================================================
c Found solution: 81983676
c ---[   0]---> Adder-cost: 0   maxlim: 165816371   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2474 |   89448   257275 |   29816    2446    37724    15.4 |  7.032 % |
c |      2574 |   89318   256978 |   32797    2541    38267    15.1 |  7.250 % |
c |      2725 |   89318   256978 |   36077    2692    43881    16.3 |  7.250 % |
c |      2950 |   89293   256923 |   39685    2915    45043    15.5 |  7.282 % |
c |      3288 |   89293   256923 |   43653    3253    49459    15.2 |  7.282 % |
c |      3794 |   89293   256923 |   48018    3759    61354    16.3 |  7.282 % |
c |      4553 |   89293   256923 |   52820    4518    84106    18.6 |  7.282 % |
c ==============================================================================
c Found solution: 74364692
c ---[   0]---> Adder-cost: 0   maxlim: 173435355   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4699 |   89303   257166 |   29767    4662    92920    19.9 |  7.282 % |
c |      4799 |   89296   257151 |   32743    4761    93439    19.6 |  7.371 % |
c |      4949 |   89267   257083 |   36018    4909    95100    19.4 |  7.404 % |
c |      5174 |   89267   257083 |   39619    5134    96754    18.8 |  7.404 % |
c |      5512 |   89251   257046 |   43581    5468   118879    21.7 |  7.424 % |
c ==============================================================================
c Found solution: 45615645
c ---[   0]---> Adder-cost: 0   maxlim: 202184402   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5630 |   89219   256711 |   29739    5578   124868    22.4 |  7.424 % |
c |      5730 |   89219   256711 |   32712    5678   125580    22.1 |  7.500 % |
c |      5880 |   89219   256711 |   35984    5828   126740    21.7 |  7.500 % |
c |      6106 |   89219   256711 |   39582    6054   128379    21.2 |  7.500 % |
c |      6443 |   89203   256659 |   43540    6388   134746    21.1 |  7.513 % |
c |      6953 |   89203   256659 |   47894    6898   191637    27.8 |  7.513 % |
c |      7712 |   89203   256659 |   52684    7657   202078    26.4 |  7.513 % |
c |      8851 |   89203   256659 |   57952    8796   330991    37.6 |  7.513 % |
c |     10559 |   89163   256569 |   63748   10501   631221    60.1 |  7.561 % |
c |     13121 |   89147   256534 |   70123   13061   758387    58.1 |  7.582 % |
c |     16965 |   89147   256534 |   77135   16905  1260176    74.5 |  7.582 % |
c |     22731 |   89057   256330 |   84848   22665  1536060    67.8 |  7.700 % |
c |     31384 |   88979   256153 |   93333   31313  2170685    69.3 |  7.797 % |
c |     44361 |   88979   256153 |  102667   44290  4075055    92.0 |  7.797 % |
c |     63823 |   88975   256144 |  112933   63751  7017820   110.1 |  7.801 % |
c |     93018 |   88929   256038 |  124227   92942  9549585   102.7 |  7.858 % |
c |    136807 |   88909   255994 |  136649   23972  2635704   109.9 |  7.882 % |
c |    202492 |   88742   255609 |  150314   89642  8670166    96.7 |  8.082 % |
c |    301018 |   88539   255148 |  165346   34282  5339795   155.8 |  8.317 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1_0x2e__bit_10 C1_0x2e__bit_9 C1_0x2e__bit_8 -C1_0x2e__bit_7 C1_0x2e__bit_6 C1_0x2e__bit_5 -C1_0x2e__bit_4 -C1_0x2e__bit_3 C1_0x2e__bit_2 -C1_0x2e__bit_1 -C1_0x2e__bit0 -C1_0x2e__bit1 C1_0x2e__bit2 C1_0x2e__bit3 C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C1_0x2e__bit13 -C1_0x2e__bit14 -C1_0x2e__bit15 -C1_0x2e__bit16 -C1_0x2e__bit17 -C1_0x2e__bit18 -C1_0x2e__bit19 -C2_0x2e__bit_10 C2_0x2e__bit_9 C2_0x2e__bit_8 C2_0x2e__bit_7 -C2_0x2e__bit_6 C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 C2_0x2e__bit_2 C2_0x2e__bit_1 C2_0x2e__bit0 C2_0x2e__bit1 C2_0x2e__bit2 -C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C2_0x2e__bit13 -C2_0x2e__bit14 -C2_0x2e__bit15 -C2_0x2e__bit16 -C2_0x2e__bit17 -C2_0x2e__bit18 -C2_0x2e__bit19 -C3_0x2e__bit_10 -C3_0x2e__bit_9 -C3_0x2e__bit_8 -C3_0x2e__bit_7 -C3_0x2e__bit_6 -C3_0x2e__bit_5 -C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 -C3_0x2e__bit0 -C3_0x2e__bit1 -C3_0x2e__bit2 -C3_0x2e__bit3 -C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C3_0x2e__bit13 -C3_0x2e__bit14 -C3_0x2e__bit15 -C3_0x2e__bit16 -C3_0x2e__bit17 -C3_0x2e__bit18 -C3_0x2e__bit19 -C4_0x2e__bit_10 -C4_0x2e__bit_9 -C4_0x2e__bit_8 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 C4_0x2e__bit_4 -C4_0x2e__bit_3 C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 -C4_0x2e__bit2 C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C4_0x2e__bit13 -C4_0x2e__bit14 -C4_0x2e__bit15 -C4_0x2e__bit16 -C4_0x2e__bit17 -C4_0x2e__bit18 -C4_0x2e__bit19 -C5_0x2e__bit_10 -C5_0x2e__bit_9 -C5_0x2e__bit_8 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 -C5_0x2e__bit_3 -C5_0x2e__bit_2 -C5_0x2e__bit_1 -C5_0x2e__bit0 -C5_0x2e__bit1 -C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C5_0x2e__bit13 -C5_0x2e__bit14 -C5_0x2e__bit15 -C5_0x2e__bit16 -C5_0x2e__bit17 -C5_0x2e__bit18 -C5_0x2e__bit19 -C6_0x2e__bit_10 -C6_0x2e__bit_9 -C6_0x2e__bit_8 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C6_0x2e__bit13 -C6_0x2e__bit14 -C6_0x2e__bit15 -C6_0x2e__bit16 -C6_0x2e__bit17 -C6_0x2e__bit18 -C6_0x2e__bit19 -C7_0x2e__bit_10 C7_0x2e__bit_9 C7_0x2e__bit_8 C7_0x2e__bit_7 -C7_0x2e__bit_6 C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 C7_0x2e__bit_2 -C7_0x2e__bit_1 -C7_0x2e__bit0 -C7_0x2e__bit1 -C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C7_0x2e__bit13 -C7_0x2e__bit14 -C7_0x2e__bit15 -C7_0x2e__bit16 -C7_0x2e__bit17 -C7_0x2e__bit18 -C7_0x2e__bit19 -C8_0x2e__bit_10 C8_0x2e__bit_9 C8_0x2e__bit_8 C8_0x2e__bit_7 -C8_0x2e__bit_6 C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 -C8_0x2e__bit13 -C8_0x2e__bit14 -C8_0x2e__bit15 -C8_0x2e__bit16 -C8_0x2e__bit17 -C8_0x2e__bit18 -C8_0x2e__bit19 C9_0x2e__bit_10 C9_0x2e__bit_9 -C9_0x2e__bit_8 C9_0x2e__bit_7 C9_0x2e__bit_6 -C9_0x2e__bit_5 -C9_0x2e__bit_4 -C9_0x2e__bit_3 C9_0x2e__bit_2 C9_0x2e__bit_1 C9_0x2e__bit0 C9_0x2e__bit1 -C9_0x2e__bit2 -C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 -C9_0x2e__bit13 -C9_0x2e__bit14 -C9_0x2e__bit15 -C9_0x2e__bit16 -C9_0x2e__bit17 -C9_0x2e__bit18 -C9_0x2e__bit19 -C10_0x2e__bit_10 C10_0x2e__bit_9 -C10_0x2e__bit_8 -C10_0x2e__bit_7 C10_0x2e__bit_6 -C10_0x2e__bit_5 C10_0x2e__bit_4 C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 C10_0x2e__bit0 C10_0x2e__bit1 C10_0x2e__bit2 -C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C10_0x2e__bit13 -C10_0x2e__bit14 -C10_0x2e__bit15 -C10_0x2e__bit16 -C10_0x2e__bit17 -C10_0x2e__bit18 -C10_0x2e__bit19 -C11_0x2e__bit_10 -C11_0x2e__bit_9 -C11_0x2e__bit_8 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 C11_0x2e__bit3 C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 -C11_0x2e__bit13 -C11_0x2e__bit14 -C11_0x2e__bit15 -C11_0x2e__bit16 -C11_0x2e__bit17 -C11_0x2e__bit18 -C11_0x2e__bit19 -C12_0x2e__bit_10 -C12_0x2e__bit_9 -C12_0x2e__bit_8 -C12_0x2e__bit_7 -C12_0x2e__bit_6 -C12_0x2e__bit_5 -C12_0x2e__bit_4 -C12_0x2e__bit_3 -C12_0x2e__bit_2 -C12_0x2e__bit_1 -C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 -C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C12_0x2e__bit13 -C12_0x2e__bit14 -C12_0x2e__bit15 -C12_0x2e__bit16 -C12_0x2e__bit17 -C12_0x2e__bit18 -C12_0x2e__bit19 -C13_0x2e__bit_10 -C13_0x2e__bit_9 -C13_0x2e__bit_8 -C13_0x2e__bit_7 -C13_0x2e__bit_6 -C13_0x2e__bit_5 -C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 -C13_0x2e__bit_1 -C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 -C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C13_0x2e__bit13 -C13_0x2e__bit14 -C13_0x2e__bit15 -C13_0x2e__bit16 -C13_0x2e__bit17 -C13_0x2e__bit18 -C13_0x2e__bit19 -C14_0x2e__bit_10 -C14_0x2e__bit_9 -C14_0x2e__bit_8 C14_0x2e__bit_7 C14_0x2e__bit_6 -C14_0x2e__bit_5 C14_0x2e__bit_4 C14_0x2e__bit_3 -C14_0x2e__bit_2 C14_0x2e__bit_1 C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C14_0x2e__bit13 -C14_0x2e__bit14 -C14_0x2e__bit15 -C14_0x2e__bit16 -C14_0x2e__bit17 -C14_0x2e__bit18 -C14_0x2e__bit19 -C15_0x2e__bit_10 -C15_0x2e__bit_9 -C15_0x2e__bit_8 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C15_0x2e__bit13 -C15_0x2e__bit14 -C15_0x2e__bit15 -C15_0x2e__bit16 -C15_0x2e__bit17 -C15_0x2e__bit18 -C15_0x2e__bit19 C16_0x2e__bit_10 C16_0x2e__bit_9 -C16_0x2e__bit_8 C16_0x2e__bit_7 C16_0x2e__bit_6 C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 -C16_0x2e__bit13 -C16_0x2e__bit14 -C16_0x2e__bit15 -C16_0x2e__bit16 -C16_0x2e__bit17 -C16_0x2e__bit18 -C16_0x2e__bit19 -C17_0x2e__bit_10 -C17_0x2e__bit_9 -C17_0x2e__bit_8 -C17_0x2e__bit_7 -C17_0x2e__bit_6 -C17_0x2e__bit_5 -C17_0x2e__bit_4 -C17_0x2e__bit_3 -C17_0x2e__bit_2 -C17_0x2e__bit_1 -C17_0x2e__bit0 -C17_0x2e__bit1 -C17_0x2e__bit2 -C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 -C17_0x2e__bit13 -C17_0x2e__bit14 -C17_0x2e__bit15 -C17_0x2e__bit16 -C17_0x2e__bit17 -C17_0x2e__bit18 -C17_0x2e__bit19 -C18_0x2e__bit_10 -C18_0x2e__bit_9 -C18_0x2e__bit_8 -C18_0x2e__bit_7 -C18_0x2e__bit_6 -C18_0x2e__bit_5 -C18_0x2e__bit_4 -C18_0x2e__bit_3 -C18_0x2e__bit_2 -C18_0x2e__bit_1 C18_0x2e__bit0 C18_0x2e__bit1 C18_0x2e__bit2 C18_0x2e__bit3 -C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 -C18_0x2e__bit13 -C18_0x2e__bit14 -C18_0x2e__bit15 -C18_0x2e__bit16 -C18_0x2e__bit17 -C18_0x2e__bit18 -C18_0x2e__bit19 -C19_0x2e__bit_10 -C19_0x2e__bit_9 -C19_0x2e__bit_8 -C19_0x2e__bit_7 -C19_0x2e__bit_6 -C19_0x2e__bit_5 -C19_0x2e__bit_4 -C19_0x2e__bit_3 -C19_0x2e__bit_2 -C19_0x2e__bit_1 -C19_0x2e__bit0 -C19_0x2e__bit1 -C19_0x2e__bit2 -C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C19_0x2e__bit13 -C19_0x2e__bit14 -C19_0x2e__bit15 -C19_0x2e__bit16 -C19_0x2e__bit17 -C19_0x2e__bit18 -C19_0x2e__bit19 -C20_0x2e__bit_10 -C20_0x2e__bit_9 -C20_0x2e__bit_8 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C20_0x2e__bit13 -C20_0x2e__bit14 -C20_0x2e__bit15 -C20_0x2e__bit16 -C20_0x2e__bit17 -C20_0x2e__bit18 -C20_0x2e__bit19 -C21_0x2e__bit_10 -C21_0x2e__bit_9 -C21_0x2e__bit_8 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 C21_0x2e__bit0 C21_0x2e__bit1 C21_0x2e__bit2 C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C21_0x2e__bit13 -C21_0x2e__bit14 -C21_0x2e__bit15 -C21_0x2e__bit16 -C21_0x2e__bit17 -C21_0x2e__bit18 -C21_0x2e__bit19 -C22_0x2e__bit_10 -C22_0x2e__bit_9 -C22_0x2e__bit_8 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C22_0x2e__bit13 -C22_0x2e__bit14 -C22_0x2e__bit15 -C22_0x2e__bit16 -C22_0x2e__bit17 -C22_0x2e__bit18 -C22_0x2e__bit19 -C23_0x2e__bit_10 -C23_0x2e__bit_9 -C23_0x2e__bit_8 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C23_0x2e__bit13 -C23_0x2e__bit14 -C23_0x2e__bit15 -C23_0x2e__bit16 -C23_0x2e__bit17 -C23_0x2e__bit18 -C23_0x2e__bit19 -C24_0x2e__bit_10 -C24_0x2e__bit_9 -C24_0x2e__bit_8 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C24_0x2e__bit13 -C24_0x2e__bit14 -C24_0x2e__bit15 -C24_0x2e__bit16 -C24_0x2e__bit17 -C24_0x2e__bit18 -C24_0x2e__bit19 -C25_0x2e__bit_10 -C25_0x2e__bit_9 -C25_0x2e__bit_8 -C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C25_0x2e__bit13 -C25_0x2e__bit14 -C25_0x2e__bit15 -C25_0x2e__bit16 -C25_0x2e__bit17 -C25_0x2e__bit18 -C25_0x2e__bit19 -C26_0x2e__bit_10 -C26_0x2e__bit_9 -C26_0x2e__bit_8 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C26_0x2e__bit13 -C26_0x2e__bit14 -C26_0x2e__bit15 -C26_0x2e__bit16 -C26_0x2e__bit17 -C26_0x2e__bit18 -C26_0x2e__bit19 -C27_0x2e__bit_10 -C27_0x2e__bit_9 -C27_0x2e__bit_8 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 -C27_0x2e__bit13 -C27_0x2e__bit14 -C27_0x2e__bit15 -C27_0x2e__bit16 -C27_0x2e__bit17 -C27_0x2e__bit18 -C27_0x2e__bit19 -C28_0x2e__bit_10 -C28_0x2e__bit_9 -C28_0x2e__bit_8 -C28_0x2e__bit_7 -C28_0x2e__bit_6 -C28_0x2e__bit_5 C28_0x2e__bit_4 C28_0x2e__bit_3 -C28_0x2e__bit_2 C28_0x2e__bit_1 C28_0x2e__bit0 C28_0x2e__bit1 -C28_0x2e__bit2 C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C28_0x2e__bit13 -C28_0x2e__bit14 -C28_0x2e__bit15 -C28_0x2e__bit16 -C28_0x2e__bit17 -C28_0x2e__bit18 -C28_0x2e__bit19 -C29_0x2e__bit_10 -C29_0x2e__bit_9 -C29_0x2e__bit_8 -C29_0x2e__bit_7 -C29_0x2e__bit_6 -C29_0x2e__bit_5 -C29_0x2e__bit_4 -C29_0x2e__bit_3 -C29_0x2e__bit_2 -C29_0x2e__bit_1 -C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C29_0x2e__bit13 -C29_0x2e__bit14 -C29_0x2e__bit15 -C29_0x2e__bit16 -C29_0x2e__bit17 -C29_0x2e__bit18 -C29_0x2e__bit19 -C30_0x2e__bit_10 C30_0x2e__bit_9 -C30_0x2e__bit_8 C30_0x2e__bit_7 C30_0x2e__bit_6 C30_0x2e__bit_5 C30_0x2e__bit_4 C30_0x2e__bit_3 C30_0x2e__bit_2 C30_0x2e__bit_1 C30_0x2e__bit0 C30_0x2e__bit1 C30_0x2e__bit2 -C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C30_0x2e__bit13 -C30_0x2e__bit14 -C30_0x2e__bit15 -C30_0x2e__bit16 -C30_0x2e__bit17 -C30_0x2e__bit18 -C30_0x2e__bit19 -C31_0x2e__bit_10 -C31_0x2e__bit_9 -C31_0x2e__bit_8 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 -C31_0x2e__bit1 -C31_0x2e__bit2 -C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C31_0x2e__bit13 -C31_0x2e__bit14 -C31_0x2e__bit15 -C31_0x2e__bit16 -C31_0x2e__bit17 -C31_0x2e__bit18 -C31_0x2e__bit19 -C32_0x2e__bit_10 C32_0x2e__bit_9 C32_0x2e__bit_8 -C32_0x2e__bit_7 -C32_0x2e__bit_6 -C32_0x2e__bit_5 C32_0x2e__bit_4 -C32_0x2e__bit_3 C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 -C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C32_0x2e__bit13 -C32_0x2e__bit14 -C32_0x2e__bit15 -C32_0x2e__bit16 -C32_0x2e__bit17 -C32_0x2e__bit18 -C32_0x2e__bit19 -C33_0x2e__bit_10 -C33_0x2e__bit_9 -C33_0x2e__bit_8 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 -C33_0x2e__bit_4 -C33_0x2e__bit_3 -C33_0x2e__bit_2 -C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C33_0x2e__bit13 -C33_0x2e__bit14 -C33_0x2e__bit15 -C33_0x2e__bit16 -C33_0x2e__bit17 -C33_0x2e__bit18 -C33_0x2e__bit19 -C34_0x2e__bit_10 -C34_0x2e__bit_9 -C34_0x2e__bit_8 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 -C34_0x2e__bit_1 -C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C34_0x2e__bit13 -C34_0x2e__bit14 -C34_0x2e__bit15 -C34_0x2e__bit16 -C34_0x2e__bit17 -C34_0x2e__bit18 -C34_0x2e__bit19 -C35_0x2e__bit_10 -C35_0x2e__bit_9 -C35_0x2e__bit_8 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 -C35_0x2e__bit13 -C35_0x2e__bit14 -C35_0x2e__bit15 -C35_0x2e__bit16 -C35_0x2e__bit17 -C35_0x2e__bit18 -C35_0x2e__bit19 -C36_0x2e__bit_10 -C36_0x2e__bit_9 -C36_0x2e__bit_8 -C36_0x2e__bit_7 -C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 -C36_0x2e__bit_1 -C36_0x2e__bit0 -C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C36_0x2e__bit13 -C36_0x2e__bit14 -C36_0x2e__bit15 -C36_0x2e__bit16 -C36_0x2e__bit17 -C36_0x2e__bit18 -C36_0x2e__bit19 -C37_0x2e__bit_10 -C37_0x2e__bit_9 -C37_0x2e__bit_8 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 -C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 -C37_0x2e__bit0 -C37_0x2e__bit1 -C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C37_0x2e__bit13 -C37_0x2e__bit14 -C37_0x2e__bit15 -C37_0x2e__bit16 -C37_0x2e__bit17 -C37_0x2e__bit18 -C37_0x2e__bit19 -C38_0x2e__bit_10 C38_0x2e__bit_9 C38_0x2e__bit_8 C38_0x2e__bit_7 -C38_0x2e__bit_6 C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 C38_0x2e__bit_2 -C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38_0x2e__bit10 -C38_0x2e__bit11 -C38_0x2e__bit12 -C38_0x2e__bit13 -C38_0x2e__bit14 -C38_0x2e__bit15 -C38_0x2e__bit16 -C38_0x2e__bit17 -C38_0x2e__bit18 -C38_0x2e__bit19 -C39_0x2e__bit_10 C39_0x2e__bit_9 -C39_0x2e__bit_8 -C39_0x2e__bit_7 C39_0x2e__bit_6 -C39_0x2e__bit_5 C39_0x2e__bit_4 C39_0x2e__bit_3 -C39_0x2e__bit_2 C39_0x2e__bit_1 C39_0x2e__bit0 -C39_0x2e__bit1 -C39_0x2e__bit2 C39_0x2e__bit3 -C39_0x2e__bit4 -C39_0x2e__bit5 -C39_0x2e__bit6 -C39_0x2e__bit7 -C39_0x2e__bit8 -C39_0x2e__bit9 -C39_0x2e__bit10 -C39_0x2e__bit11 -C39_0x2e__bit12 -C39_0x2e__bit13 -C39_0x2e__bit14 -C39_0x2e__bit15 -C39_0x2e__bit16 -C39_0x2e__bit17 -C39_0x2e__bit18 -C39_0x2e__bit19 -C40_0x2e__bit_10 -C40_0x2e__bit_9 -C40_0x2e__bit_8 -C40_0x2e__bit_7 -C40_0x2e__bit_6 -C40_0x2e__bit_5 -C40_0x2e__bit_4 -C40_0x2e__bit_3 -C40_0x2e__bit_2 -C40_0x2e__bit_1 -C40_0x2e__bit0 -C40_0x2e__bit1 -C40_0x2e__bit2 -C40_0x2e__bit3 -C40_0x2e__bit4 -C40_0x2e__bit5 -C40_0x2e__bit6 -C40_0x2e__bit7 -C40_0x2e__bit8 -C40_0x2e__bit9 -C40_0x2e__bit10 -C40_0x2e__bit11 -C40_0x2e__bit12 -C40_0x2e__bit13 -C40_0x2e__bit14 -C40_0x2e__bit15 -C40_0x2e__bit16 -C40_0x2e__bit17 -C40_0x2e__bit18 -C40_0x2e__bit19 C41_0x2e__bit_10 C41_0x2e__bit_9 C41_0x2e__bit_8 C41_0x2e__bit_7 -C41_0x2e__bit_6 C41_0x2e__bit_5 -C41_0x2e__bit_4 C41_0x2e__bit_3 C41_0x2e__bit_2 C41_0x2e__bit_1 -C41_0x2e__bit0 C41_0x2e__bit1 -C41_0x2e__bit2 -C41_0x2e__bit3 -C41_0x2e__bit4 -C41_0x2e__bit5 -C41_0x2e__bit6 -C41_0x2e__bit7 -C41_0x2e__bit8 -C41_0x2e__bit9 -C41_0x2e__bit10 -C41_0x2e__bit11 -C41_0x2e__bit12 -C41_0x2e__bit13 -C41_0x2e__bit14 -C41_0x2e__bit15 -C41_0x2e__bit16 -C41_0x2e__bit17 -C41_0x2e__bit18 -C41_0x2e__bit19 -C42_0x2e__bit_10 -C42_0x2e__bit_9 -C42_0x2e__bit_8 -C42_0x2e__bit_7 -C42_0x2e__bit_6 -C42_0x2e__bit_5 -C42_0x2e__bit_4 -C42_0x2e__bit_3 -C42_0x2e__bit_2 -C42_0x2e__bit_1 -C42_0x2e__bit0 -C42_0x2e__bit1 -C42_0x2e__bit2 -C42_0x2e__bit3 -C42_0x2e__bit4 -C42_0x2e__bit5 -C42_0x2e__bi

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/24302/stat): 24302 (minisat+_script) R 24301 24302 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1788359053 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24302/statm): 174 3 169 147 0 27 0
[pid=24302] 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=24303
New process pid=24304
New process pid=24305
execve syscall for /bin/sed executable
One traced child (pid=24304) 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=24305) exited with status: 0
One traced child (pid=24303) exited with status: 0
New process pid=24306
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod013.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5009 0 0 0 964 17 0 0 25 0 1 0 1788359058 19259392 4289 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 4702 4289 145 145 0 4557 0
[pid=24306] vsize: 18808
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 20932

[startup+20.0045 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5193 0 0 0 1961 18 0 0 25 0 1 0 1788359058 19726336 4393 4294967295 134512640 135094434 3221224432 3221222432 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 4816 4393 145 145 0 4671 0
[pid=24306] vsize: 19264
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 21388

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5419 0 0 0 2958 19 0 0 25 0 1 0 1788359058 20111360 4506 4294967295 134512640 135094434 3221224432 3221221984 134599924 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 4910 4506 145 145 0 4765 0
[pid=24306] vsize: 19640
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 21764

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5551 0 0 0 3956 21 0 0 25 0 1 0 1788359058 20295680 4557 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 4955 4557 145 145 0 4810 0
[pid=24306] vsize: 19820
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 21944

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5851 0 0 0 4951 23 0 0 25 0 1 0 1788359058 21544960 4857 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 5260 4857 145 145 0 5115 0
[pid=24306] vsize: 21040
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 23164

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) T 24302 24302 9854 0 -1 0 6424 0 0 0 5941 27 0 0 25 0 1 0 1788359058 23883776 5430 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24306/statm): 5831 5430 145 145 0 5686 0
[pid=24306] vsize: 23324
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 25448

[startup+70.0095 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 6814 0 0 0 6934 31 0 0 25 0 1 0 1788359058 25526272 5820 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 6232 5820 145 145 0 6087 0
[pid=24306] vsize: 24928
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 27052

[startup+80.0113 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 7183 0 0 0 7927 33 0 0 25 0 1 0 1788359058 27017216 6189 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 6596 6189 145 145 0 6451 0
[pid=24306] vsize: 26384
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 28508

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 7541 0 0 0 8921 36 0 0 25 0 1 0 1788359058 28467200 6547 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 6950 6547 145 145 0 6805 0
[pid=24306] vsize: 27800
Current children cumulated CPU time (s) 89.58
Current children cumulated vsize (Kb) 29924

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 8032 0 0 0 9912 39 0 0 25 0 1 0 1788359058 30580736 7038 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 7466 7038 145 145 0 7321 0
[pid=24306] vsize: 29864
Current children cumulated CPU time (s) 99.52
Current children cumulated vsize (Kb) 31988

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 8632 0 0 0 10904 43 0 0 25 0 1 0 1788359058 33021952 7638 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 8062 7638 145 145 0 7917 0
[pid=24306] vsize: 32248
Current children cumulated CPU time (s) 109.48
Current children cumulated vsize (Kb) 34372

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 9359 0 0 0 11893 48 0 0 25 0 1 0 1788359058 35983360 8365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 8785 8365 145 145 0 8640 0
[pid=24306] vsize: 35140
Current children cumulated CPU time (s) 119.42
Current children cumulated vsize (Kb) 37264

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 9847 0 0 0 12885 52 0 0 25 0 1 0 1788359058 37965824 8853 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 9269 8853 145 145 0 9124 0
[pid=24306] vsize: 37076
Current children cumulated CPU time (s) 129.38
Current children cumulated vsize (Kb) 39200

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 9991 0 0 0 13882 53 0 0 25 0 1 0 1788359058 38547456 8997 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 9411 8997 145 145 0 9266 0
[pid=24306] vsize: 37644
Current children cumulated CPU time (s) 139.36
Current children cumulated vsize (Kb) 39768

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 10296 0 0 0 14876 56 0 0 25 0 1 0 1788359058 39784448 9302 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 9713 9302 145 145 0 9568 0
[pid=24306] vsize: 38852
Current children cumulated CPU time (s) 149.33
Current children cumulated vsize (Kb) 40976

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 11195 0 0 0 15863 61 0 0 25 0 1 0 1788359058 43446272 10201 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 10607 10201 145 145 0 10462 0
[pid=24306] vsize: 42428
Current children cumulated CPU time (s) 159.25
Current children cumulated vsize (Kb) 44552

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 12140 0 0 0 16849 68 0 0 25 0 1 0 1788359058 47296512 11146 4294967295 134512640 135094434 3221224432 3221223024 134557306 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 11547 11146 145 145 0 11402 0
[pid=24306] vsize: 46188
Current children cumulated CPU time (s) 169.18
Current children cumulated vsize (Kb) 48312

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) T 24302 24302 9854 0 -1 0 12964 0 0 0 17836 73 0 0 25 0 1 0 1788359058 50655232 11970 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24306/statm): 12367 11970 145 145 0 12222 0
[pid=24306] vsize: 49468
Current children cumulated CPU time (s) 179.1
Current children cumulated vsize (Kb) 51592

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 13396 0 0 0 18828 77 0 0 25 0 1 0 1788359058 52666368 12402 4294967295 134512640 135094434 3221224432 3221223080 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 12858 12402 145 145 0 12713 0
[pid=24306] vsize: 51432
Current children cumulated CPU time (s) 189.06
Current children cumulated vsize (Kb) 53556

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 13663 0 0 0 19823 79 0 0 25 0 1 0 1788359058 53747712 12669 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 13122 12669 145 145 0 12977 0
[pid=24306] vsize: 52488
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 54612

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14016 0 0 0 20817 82 0 0 25 0 1 0 1788359058 55185408 13022 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 13473 13022 145 145 0 13328 0
[pid=24306] vsize: 53892
Current children cumulated CPU time (s) 209
Current children cumulated vsize (Kb) 56016

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14331 0 0 0 21811 85 0 0 25 0 1 0 1788359058 56467456 13337 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 13786 13337 145 145 0 13641 0
[pid=24306] vsize: 55144
Current children cumulated CPU time (s) 218.97
Current children cumulated vsize (Kb) 57268

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14621 0 0 0 22805 87 0 0 25 0 1 0 1788359058 57643008 13627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 14073 13627 145 145 0 13928 0
[pid=24306] vsize: 56292
Current children cumulated CPU time (s) 228.93
Current children cumulated vsize (Kb) 58416

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14961 0 0 0 23800 89 0 0 25 0 1 0 1788359058 59023360 13967 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 14410 13967 145 145 0 14265 0
[pid=24306] vsize: 57640
Current children cumulated CPU time (s) 238.9
Current children cumulated vsize (Kb) 59764

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15237 0 0 0 24796 91 0 0 25 0 1 0 1788359058 60137472 14243 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 14682 14243 145 145 0 14537 0
[pid=24306] vsize: 58728
Current children cumulated CPU time (s) 248.88
Current children cumulated vsize (Kb) 60852

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15602 0 0 0 25791 93 0 0 25 0 1 0 1788359058 61616128 14608 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 15043 14608 145 145 0 14898 0
[pid=24306] vsize: 60172
Current children cumulated CPU time (s) 258.85
Current children cumulated vsize (Kb) 62296

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15781 0 0 0 26788 94 0 0 25 0 1 0 1788359058 62341120 14787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 15220 14787 145 145 0 15075 0
[pid=24306] vsize: 60880
Current children cumulated CPU time (s) 268.83
Current children cumulated vsize (Kb) 63004

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15896 0 0 0 27785 95 0 0 25 0 1 0 1788359058 62812160 14902 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 15335 14902 145 145 0 15190 0
[pid=24306] vsize: 61340
Current children cumulated CPU time (s) 278.81
Current children cumulated vsize (Kb) 63464

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16011 0 0 0 28784 97 0 0 25 0 1 0 1788359058 63275008 15017 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 15448 15017 145 145 0 15303 0
[pid=24306] vsize: 61792
Current children cumulated CPU time (s) 288.82
Current children cumulated vsize (Kb) 63916

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16160 0 0 0 29781 98 0 0 25 0 1 0 1788359058 63877120 15166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 15595 15166 145 145 0 15450 0
[pid=24306] vsize: 62380
Current children cumulated CPU time (s) 298.8
Current children cumulated vsize (Kb) 64504

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16351 0 0 0 30777 99 0 0 25 0 1 0 1788359058 64651264 15357 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 15784 15357 145 145 0 15639 0
[pid=24306] vsize: 63136
Current children cumulated CPU time (s) 308.77
Current children cumulated vsize (Kb) 65260

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16578 0 0 0 31773 101 0 0 25 0 1 0 1788359058 65576960 15584 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 16010 15584 145 145 0 15865 0
[pid=24306] vsize: 64040
Current children cumulated CPU time (s) 318.75
Current children cumulated vsize (Kb) 66164

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16978 0 0 0 32766 104 0 0 25 0 1 0 1788359058 67198976 15984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 16406 15984 145 145 0 16261 0
[pid=24306] vsize: 65624
Current children cumulated CPU time (s) 328.71
Current children cumulated vsize (Kb) 67748

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 17337 0 0 0 33759 107 0 0 25 0 1 0 1788359058 68661248 16343 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 16763 16343 145 145 0 16618 0
[pid=24306] vsize: 67052
Current children cumulated CPU time (s) 338.67
Current children cumulated vsize (Kb) 69176

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 17677 0 0 0 34753 109 0 0 25 0 1 0 1788359058 70041600 16683 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 17100 16683 145 145 0 16955 0
[pid=24306] vsize: 68400
Current children cumulated CPU time (s) 348.63
Current children cumulated vsize (Kb) 70524

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 17976 0 0 0 35748 111 0 0 25 0 1 0 1788359058 71258112 16982 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 17397 16982 145 145 0 17252 0
[pid=24306] vsize: 69588
Current children cumulated CPU time (s) 358.6
Current children cumulated vsize (Kb) 71712

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 18282 0 0 0 36743 114 0 0 25 0 1 0 1788359058 72503296 17288 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 17701 17288 145 145 0 17556 0
[pid=24306] vsize: 70804
Current children cumulated CPU time (s) 368.58
Current children cumulated vsize (Kb) 72928

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 18592 0 0 0 37738 116 0 0 25 0 1 0 1788359058 73768960 17598 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 18010 17598 145 145 0 17865 0
[pid=24306] vsize: 72040
Current children cumulated CPU time (s) 378.55
Current children cumulated vsize (Kb) 74164

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 18905 0 0 0 38733 118 0 0 25 0 1 0 1788359058 75042816 17911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 18321 17911 145 145 0 18176 0
[pid=24306] vsize: 73284
Current children cumulated CPU time (s) 388.52
Current children cumulated vsize (Kb) 75408

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 19229 0 0 0 39727 121 0 0 25 0 1 0 1788359058 76369920 18235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 18645 18235 145 145 0 18500 0
[pid=24306] vsize: 74580
Current children cumulated CPU time (s) 398.49
Current children cumulated vsize (Kb) 76704

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 19539 0 0 0 40720 123 0 0 25 0 1 0 1788359058 77635584 18545 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 18954 18545 145 145 0 18809 0
[pid=24306] vsize: 75816
Current children cumulated CPU time (s) 408.44
Current children cumulated vsize (Kb) 77940

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 19875 0 0 0 41715 126 0 0 25 0 1 0 1788359058 79003648 18881 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 19288 18881 145 145 0 19143 0
[pid=24306] vsize: 77152
Current children cumulated CPU time (s) 418.42
Current children cumulated vsize (Kb) 79276

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20110 0 0 0 42711 127 0 0 25 0 1 0 1788359058 79958016 19116 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 19521 19116 145 145 0 19376 0
[pid=24306] vsize: 78084
Current children cumulated CPU time (s) 428.39
Current children cumulated vsize (Kb) 80208

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20377 0 0 0 43705 129 0 0 25 0 1 0 1788359058 81043456 19383 4294967295 134512640 135094434 3221224432 3221223024 134551692 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 19786 19383 145 145 0 19641 0
[pid=24306] vsize: 79144
Current children cumulated CPU time (s) 438.35
Current children cumulated vsize (Kb) 81268

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 44700 131 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221222912 134781309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 448.32
Current children cumulated vsize (Kb) 82996

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 45700 131 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 458.32
Current children cumulated vsize (Kb) 82996

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 46699 131 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 468.31
Current children cumulated vsize (Kb) 82996

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 47698 132 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223104 134555260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 478.31
Current children cumulated vsize (Kb) 82996

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 48698 132 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 488.31
Current children cumulated vsize (Kb) 82996

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 49698 133 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 498.32
Current children cumulated vsize (Kb) 82996

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 50697 133 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 508.31
Current children cumulated vsize (Kb) 82996

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 51697 134 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 518.32
Current children cumulated vsize (Kb) 82996

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 52696 134 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 528.31
Current children cumulated vsize (Kb) 82996

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 53696 134 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 538.31
Current children cumulated vsize (Kb) 82996

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 54696 135 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 548.32
Current children cumulated vsize (Kb) 82996

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 55695 135 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 558.31
Current children cumulated vsize (Kb) 82996

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 56695 136 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 568.32
Current children cumulated vsize (Kb) 82996

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 57694 136 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 578.31
Current children cumulated vsize (Kb) 82996

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 58694 136 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 588.31
Current children cumulated vsize (Kb) 82996

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 59692 138 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 598.31
Current children cumulated vsize (Kb) 82996

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 60691 139 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 608.31
Current children cumulated vsize (Kb) 82996

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 61691 140 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 618.32
Current children cumulated vsize (Kb) 82996

[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 62690 140 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 628.31
Current children cumulated vsize (Kb) 82996

[startup+640.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 63689 141 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 638.31
Current children cumulated vsize (Kb) 82996

[startup+650.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 64689 141 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 648.31
Current children cumulated vsize (Kb) 82996

[startup+660.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 65688 142 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 658.31
Current children cumulated vsize (Kb) 82996

[startup+670.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 66688 142 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 668.31
Current children cumulated vsize (Kb) 82996

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 67687 143 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 678.31
Current children cumulated vsize (Kb) 82996

[startup+690.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 68687 144 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 688.32
Current children cumulated vsize (Kb) 82996

[startup+700.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 69687 144 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223016 134552439 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 698.32
Current children cumulated vsize (Kb) 82996

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 70686 144 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 708.31
Current children cumulated vsize (Kb) 82996

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 71686 145 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 718.32
Current children cumulated vsize (Kb) 82996

[startup+730.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 72685 145 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 728.31
Current children cumulated vsize (Kb) 82996

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 73685 146 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 738.32
Current children cumulated vsize (Kb) 82996

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 74685 146 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 748.32
Current children cumulated vsize (Kb) 82996

[startup+760.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 75684 146 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 758.31
Current children cumulated vsize (Kb) 82996

[startup+770.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 76684 147 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 768.32
Current children cumulated vsize (Kb) 82996

[startup+780.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 77684 147 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 778.32
Current children cumulated vsize (Kb) 82996

[startup+790.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 78683 148 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 788.32
Current children cumulated vsize (Kb) 82996

[startup+800.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 79683 148 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 798.32
Current children cumulated vsize (Kb) 82996

[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 80683 148 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 808.32
Current children cumulated vsize (Kb) 82996

[startup+820.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 81682 149 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 818.32
Current children cumulated vsize (Kb) 82996

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20684 0 0 0 82681 150 0 0 25 0 1 0 1788359058 82812928 19690 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19690 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 828.32
Current children cumulated vsize (Kb) 82996

[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20684 0 0 0 83681 151 0 0 25 0 1 0 1788359058 82812928 19690 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19690 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 838.33
Current children cumulated vsize (Kb) 82996

[startup+850.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20686 0 0 0 84680 151 0 0 25 0 1 0 1788359058 82812928 19692 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19692 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 848.32
Current children cumulated vsize (Kb) 82996

[startup+860.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20688 0 0 0 85680 151 0 0 25 0 1 0 1788359058 82812928 19694 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19694 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 858.32
Current children cumulated vsize (Kb) 82996

[startup+870.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20690 0 0 0 86680 152 0 0 25 0 1 0 1788359058 82812928 19696 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19696 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 868.33
Current children cumulated vsize (Kb) 82996

[startup+880.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20692 0 0 0 87679 152 0 0 25 0 1 0 1788359058 82812928 19698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19698 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 878.32
Current children cumulated vsize (Kb) 82996

[startup+890.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20695 0 0 0 88679 153 0 0 25 0 1 0 1788359058 82812928 19701 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20218 19701 145 145 0 20073 0
[pid=24306] vsize: 80872
Current children cumulated CPU time (s) 888.33
Current children cumulated vsize (Kb) 82996

[startup+900.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20870 0 0 0 89676 154 0 0 25 0 1 0 1788359058 83521536 19876 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 20391 19876 145 145 0 20246 0
[pid=24306] vsize: 81564
Current children cumulated CPU time (s) 898.31
Current children cumulated vsize (Kb) 83688

[startup+910.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 21758 0 0 0 90663 160 0 0 25 0 1 0 1788359058 87146496 20764 4294967295 134512640 135094434 3221224432 3221223024 134557055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 21276 20764 145 145 0 21131 0
[pid=24306] vsize: 85104
Current children cumulated CPU time (s) 908.24
Current children cumulated vsize (Kb) 87228

[startup+920.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 22101 0 0 0 91659 162 0 0 25 0 1 0 1788359058 88543232 21107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 21617 21107 145 145 0 21472 0
[pid=24306] vsize: 86468
Current children cumulated CPU time (s) 918.22
Current children cumulated vsize (Kb) 88592

[startup+930.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 22222 0 0 0 92656 163 0 0 25 0 1 0 1788359058 89030656 21228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 21736 21228 145 145 0 21591 0
[pid=24306] vsize: 86944
Current children cumulated CPU time (s) 928.2
Current children cumulated vsize (Kb) 89068

[startup+940.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 22696 0 0 0 93649 167 0 0 25 0 1 0 1788359058 90959872 21702 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 22207 21702 145 145 0 22062 0
[pid=24306] vsize: 88828
Current children cumulated CPU time (s) 938.17
Current children cumulated vsize (Kb) 90952

[startup+950.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 23616 0 0 0 94632 173 0 0 25 0 1 0 1788359058 94707712 22622 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 23122 22622 145 145 0 22977 0
[pid=24306] vsize: 92488
Current children cumulated CPU time (s) 948.06
Current children cumulated vsize (Kb) 94612

[startup+960.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 24443 0 0 0 95618 180 0 0 25 0 1 0 1788359058 98070528 23449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 23943 23449 145 145 0 23798 0
[pid=24306] vsize: 95772
Current children cumulated CPU time (s) 957.99
Current children cumulated vsize (Kb) 97896

[startup+970.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25236 0 0 0 96603 186 0 0 25 0 1 0 1788359058 101298176 24242 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24306/statm): 24731 24242 145 145 0 24586 0
[pid=24306] vsize: 98924
Current children cumulated CPU time (s) 967.9
Current children cumulated vsize (Kb) 101048

[startup+980.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 97600 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 977.88
Current children cumulated vsize (Kb) 101744

[startup+990.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 98601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 987.89
Current children cumulated vsize (Kb) 101744

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 99601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 997.89
Current children cumulated vsize (Kb) 101744

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 100601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1007.89
Current children cumulated vsize (Kb) 101744

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 101601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1017.89
Current children cumulated vsize (Kb) 101744

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 102601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1027.89
Current children cumulated vsize (Kb) 101744

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 103601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1037.89
Current children cumulated vsize (Kb) 101744

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 104601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1047.89
Current children cumulated vsize (Kb) 101744

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 105602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1057.9
Current children cumulated vsize (Kb) 101744

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 106602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1067.9
Current children cumulated vsize (Kb) 101744

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 107602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1077.9
Current children cumulated vsize (Kb) 101744

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 108602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1087.9
Current children cumulated vsize (Kb) 101744

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 109603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1097.91
Current children cumulated vsize (Kb) 101744

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 110603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1107.91
Current children cumulated vsize (Kb) 101744

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 111603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1117.91
Current children cumulated vsize (Kb) 101744

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 112603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1127.91
Current children cumulated vsize (Kb) 101744

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 113604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1137.92
Current children cumulated vsize (Kb) 101744

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 114604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1147.92
Current children cumulated vsize (Kb) 101744

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 115604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1157.92
Current children cumulated vsize (Kb) 101744

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 116604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1167.92
Current children cumulated vsize (Kb) 101744

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 117605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1177.93
Current children cumulated vsize (Kb) 101744

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 118605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1187.93
Current children cumulated vsize (Kb) 101744

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 119605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1197.93
Current children cumulated vsize (Kb) 101744

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 120605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1207.93
Current children cumulated vsize (Kb) 101744



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 24306
Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24302/statm): 531 226 485 147 0 384 0
[pid=24302] vsize: 2124
Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 120606 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223056 134557658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0
[pid=24306] vsize: 99620
Current children cumulated CPU time (s) 1207.94
Current children cumulated vsize (Kb) 101744

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.99
CPU user time (s): 1206.06
CPU system time (s): 1.92471
CPU usage (%): 99.8187
Max. virtual memory (cumulated for all children) (Kb): 101744

Verifier Data

ERROR: no interpretation found !