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-bell3b.opb
MD5SUMefb36546b6b37df68ff339bb766886b9
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4510472947583472
Optimality of the best value was proved NO
Number of terms in the objective function 1780
Biggest coefficient in the objective function 50331648000000000
Number of bits for the biggest coefficient in the objective function 56
Sum of the numbers in the objective function 1076758128151185266
Number of bits of the sum of numbers in the objective function 60
Biggest number in a constraint 50331648000000000
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 1076758128151185266
Number of bits of the biggest sum of numbers60
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.08
Number of variables2283
Total number of constraints194
Number of constraints which are clauses22
Number of constraints which are cardinality constraints (but not clauses)39
Number of constraints which are nor clauses,nor cardinality constraints133
Minimum length of a constraint1
Maximum length of a constraint195

Trace number 4467

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-19 17:23:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2845 boxname=wulflinc5 idbench=501 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  efb36546b6b37df68ff339bb766886b9  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb
IDLAUNCH: 2845
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        901944 kB
Buffers:         35560 kB
Cached:          72800 kB
SwapCached:        780 kB
Active:          73124 kB
Inactive:        37936 kB
HighTotal:      131008 kB
HighFree:        54572 kB
LowTotal:       903652 kB
LowFree:        847372 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15980 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 17:43:39 (client local time) WITH STATUS 10 IN 1209.51 SECONDS
stats: 2845 7 1209.51 10

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 137] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 151 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssss......................ssssss
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> Sorter-cost:  974     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost: 1414     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> BDD-cost:   70
c ---[  91]---> Sorter-cost:  921     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost:  532     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> BDD-cost:   70
c ---[  85]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost:  512     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost:  532     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> Sorter-cost:  974     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  80]---> Sorter-cost: 2069     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  79]---> Sorter-cost: 2707     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  78]---> Sorter-cost: 1414     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> BDD-cost:   70
c ---[  76]---> Sorter-cost:  552     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> BDD-cost:  131
c ---[  74]---> BDD-cost:  106
c ---[  73]---> BDD-cost:  106
c ---[  72]---> BDD-cost:  106
c ---[  71]---> BDD-cost:  106
c ---[  70]---> BDD-cost:  106
c ---[  69]---> BDD-cost:  106
c ---[  68]---> BDD-cost:  131
c ---[  67]---> BDD-cost:  106
c ---[  66]---> BDD-cost:  106
c ---[  65]---> BDD-cost:  131
c ---[  64]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  131
c ---[  62]---> BDD-cost:  140
c ---[  61]---> BDD-cost:  131
c ---[  60]---> BDD-cost:  122
c ---[  59]---> BDD-cost:  219
c ---[  58]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   76
c ---[  56]---> Sorter-cost:  493     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> BDD-cost:    7
c ---[  53]---> Sorter-cost:  502     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  502     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  503     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:   61
c ---[  48]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  508     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1475     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1994     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:   74
c ---[  36]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  35]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  34]---> Sorter-cost: 2837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  33]---> Sorter-cost: 2836     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  32]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  31]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  30]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  29]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  28]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  27]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  26]---> Sorter-cost: 2837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  25]---> Sorter-cost: 2837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  24]---> Sorter-cost: 3073     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  23]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  22]---> Sorter-cost: 3361     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[  21]---> Sorter-cost: 3682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[  20]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  19]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  18]---> Sorter-cost: 3311     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[  17]---> Sorter-cost: 2970     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  16]---> Sorter-cost: 2837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  15]---> Sorter-cost: 2837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[  14]---> Sorter-cost: 3311     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[  11]---> BDD-cost:    5
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    5
c ---[   8]---> BDD-cost:    5
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   54
c ---[   4]---> BDD-cost:   78
c ---[   3]---> BDD-cost:   32
c ---[   2]---> BDD-cost:    7
c ---[   1]---> BDD-cost:    7
c ---[   0]---> BDD-cost:   70
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  247783   580424 |   82594       0        0     nan |  0.000 % |
c |       102 |  247774   580405 |   90853     101      652     6.5 |  0.656 % |
c |       252 |  247774   580405 |   99938     251     1692     6.7 |  0.656 % |
c |       477 |  246332   577134 |  109932     471     3195     6.8 |  1.152 % |
c |       814 |  246332   577134 |  120925     808     6254     7.7 |  1.152 % |
c |      1321 |  245579   575421 |  133018    1311    10114     7.7 |  1.409 % |
c |      2080 |  245512   575273 |  146320    2066    16014     7.8 |  1.430 % |
c |      3219 |  245512   575273 |  160952    3205    71289    22.2 |  1.430 % |
c |      4927 |  245325   574849 |  177047    4898    85171    17.4 |  1.492 % |
c |      7489 |  245261   574703 |  194752    7458   163056    21.9 |  1.510 % |
c |     11335 |  245261   574703 |  214227   11304   309019    27.3 |  1.510 % |
c |     17103 |  245261   574703 |  235650   17072   813712    47.7 |  1.510 % |
c ==============================================================================
c Found solution: 34068288466405961
c ---[   0]---> 
c *** TERMINATED ***
s SATISFIABLE
v -d1_bit0 -d2_bit0 d3_bit0 -d4_bit0 d5_bit0 -d6_bit0 -d7_bit0 -d9_bit0 -d10_bit0 -d12_bit0 -d13_bit0 -d15_bit0 -d16_bit0 d17_bit0 -d20_bit0 -d21_bit0 h1_bit0 -h1_bit1 -h1_bit2 -h1_bit3 -h1_bit4 -h1_bit5 -h1_bit6 -h1_bit7 -h1_bit8 -h1_bit9 -h1_bit10 -h1_bit11 -h1_bit12 -h1_bit13 h2_bit0 -h2_bit1 h2_bit2 -h2_bit3 -h2_bit4 -h2_bit5 -h2_bit6 -h2_bit7 -h2_bit8 -h2_bit9 -h2_bit10 -h2_bit11 -h2_bit12 -h2_bit13 -h3_bit0 -h3_bit1 h3_bit2 h3_bit3 -h3_bit4 -h3_bit5 -h3_bit6 -h3_bit7 -h3_bit8 -h3_bit9 -h3_bit10 -h3_bit11 -h3_bit12 -h3_bit13 h4_bit0 -h4_bit1 -h4_bit2 -h4_bit3 h4_bit4 -h4_bit5 -h4_bit6 -h4_bit7 -h4_bit8 -h4_bit9 -h4_bit10 -h4_bit11 -h4_bit12 -h4_bit13 h5_bit0 h5_bit1 -h5_bit2 h5_bit3 -h5_bit4 -h5_bit5 -h5_bit6 -h5_bit7 -h5_bit8 -h5_bit9 -h5_bit10 -h5_bit11 -h5_bit12 -h5_bit13 -h6_bit0 -h6_bit1 h6_bit2 h6_bit3 -h6_bit4 -h6_bit5 -h6_bit6 -h6_bit7 -h6_bit8 -h6_bit9 -h6_bit10 -h6_bit11 -h6_bit12 -h6_bit13 -h7_bit0 -h7_bit1 -h7_bit2 -h7_bit3 -h7_bit4 -h7_bit5 -h7_bit6 -h7_bit7 -h7_bit8 -h7_bit9 -h7_bit10 -h7_bit11 -h7_bit12 -h7_bit13 -h9_bit0 -h9_bit1 -h9_bit2 -h9_bit3 -h9_bit4 -h9_bit5 -h9_bit6 -h9_bit7 -h9_bit8 -h9_bit9 -h9_bit10 -h9_bit11 -h9_bit12 -h9_bit13 -h10_bit0 -h10_bit1 h10_bit2 -h10_bit3 h10_bit4 -h10_bit5 -h10_bit6 -h10_bit7 -h10_bit8 -h10_bit9 -h12_bit0 -h12_bit1 -h12_bit2 -h12_bit3 -h12_bit4 -h12_bit5 -h12_bit6 -h12_bit7 -h12_bit8 -h12_bit9 -h13_bit0 -h13_bit1 -h13_bit2 -h13_bit3 -h13_bit4 -h13_bit5 -h13_bit6 -h13_bit7 -h13_bit8 -h13_bit9 h15_bit0 h15_bit1 -h15_bit2 -h15_bit3 -h15_bit4 -h15_bit5 -h15_bit6 -h15_bit7 -h15_bit8 -h15_bit9 h16_bit0 -h16_bit1 -h16_bit2 h16_bit3 -h16_bit4 -h16_bit5 -h16_bit6 -h16_bit7 -h16_bit8 -h16_bit9 h17_bit0 -h17_bit1 h17_bit2 -h17_bit3 -h17_bit4 -h17_bit5 -h17_bit6 -h17_bit7 -h17_bit8 -h17_bit9 -h20_bit0 -h20_bit1 -h20_bit2 -h20_bit3 -h20_bit4 -h20_bit5 -h20_bit6 -h20_bit7 -h20_bit8 -h20_bit9 -h21_bit0 -h21_bit1 -h21_bit2 -h21_bit3 -h21_bit4 -h21_bit5 -h21_bit6 -h21_bit7 -h21_bit8 -h21_bit9 g1_bit0 -g1_bit1 g1_bit2 -g1_bit3 g1_bit4 -g1_bit5 -g1_bit6 g1_bit7 g1_bit8 g1_bit9 -g1_bit10 -g1_bit11 -g1_bit12 -g1_bit13 g2_bit0 -g2_bit1 -g2_bit2 g2_bit3 g2_bit4 -g2_bit5 g2_bit6 -g2_bit7 g2_bit8 g2_bit9 -g2_bit10 -g2_bit11 g2_bit12 -g2_bit13 -g3_bit0 g3_bit1 g3_bit2 g3_bit3 g3_bit4 -g3_bit5 g3_bit6 -g3_bit7 g3_bit8 -g3_bit9 g3_bit10 -g3_bit11 -g3_bit12 -g3_bit13 -g4_bit0 g4_bit1 -g4_bit2 g4_bit3 g4_bit4 g4_bit5 -g4_bit6 -g4_bit7 -g4_bit8 g4_bit9 g4_bit10 -g4_bit11 -g4_bit12 -g4_bit13 -g5_bit0 -g5_bit1 g5_bit2 g5_bit3 -g5_bit4 g5_bit5 -g5_bit6 g5_bit7 g5_bit8 -g5_bit9 g5_bit10 -g5_bit11 g5_bit12 -g5_bit13 g6_bit0 -g6_bit1 g6_bit2 g6_bit3 -g6_bit4 g6_bit5 g6_bit6 -g6_bit7 g6_bit8 -g6_bit9 -g6_bit10 -g6_bit11 -g6_bit12 g6_bit13 -g7_bit0 g7_bit1 g7_bit2 g7_bit3 g7_bit4 g7_bit5 g7_bit6 g7_bit7 -g7_bit8 -g7_bit9 g7_bit10 -g7_bit11 -g7_bit12 -g7_bit13 g9_bit0 g9_bit1 g9_bit2 g9_bit3 g9_bit4 -g9_bit5 g9_bit6 g9_bit7 g9_bit8 g9_bit9 -g9_bit10 g9_bit11 -g9_bit12 -g9_bit13 g10_bit0 -g10_bit1 -g10_bit2 g10_bit3 g10_bit4 g10_bit5 -g10_bit6 g10_bit7 -g10_bit8 g10_bit9 -g12_bit0 g12_bit1 g12_bit2 -g12_bit3 -g12_bit4 -g12_bit5 g12_bit6 g12_bit7 -g12_bit8 g12_bit9 -g13_bit0 g13_bit1 -g13_bit2 -g13_bit3 -g13_bit4 -g13_bit5 -g13_bit6 g13_bit7 g13_bit8 g13_bit9 g15_bit0 -g15_bit1 g15_bit2 -g15_bit3 g15_bit4 -g15_bit5 g15_bit6 g15_bit7 g15_bit8 g15_bit9 -g16_bit0 g16_bit1 g16_bit2 g16_bit3 g16_bit4 -g16_bit5 g16_bit6 g16_bit7 -g16_bit8 -g16_bit9 g17_bit0 g17_bit1 g17_bit2 -g17_bit3 g17_bit4 -g17_bit5 -g17_bit6 g17_bit7 -g17_bit8 g17_bit9 -g20_bit0 -g20_bit1 -g20_bit2 -g20_bit3 -g20_bit4 g20_bit5 g20_bit6 -g20_bit7 g20_bit8 -g20_bit9 g21_bit0 -g21_bit1 g21_bit2 -g21_bit3 -g21_bit4 -g21_bit5 g21_bit6 -g21_bit7 g21_bit8 g21_bit9 a1_bit_10 -a1_bit_9 -a1_bit_8 a1_bit_7 a1_bit_6 -a1_bit_5 a1_bit_4 a1_bit_3 a1_bit_2 a1_bit_1 -a1_bit0 a1_bit1 -a1_bit2 a1_bit3 -a1_bit4 a1_bit5 a1_bit6 -a1_bit7 -a1_bit8 -a1_bit9 -a1_bit10 -a1_bit11 -a1_bit12 -a1_bit13 -a1_bit14 -a1_bit15 -a1_bit16 -a1_bit17 -a1_bit18 -a1_bit19 a2_bit_10 -a2_bit_9 a2_bit_8 a2_bit_7 a2_bit_6 -a2_bit_5 a2_bit_4 a2_bit_3 -a2_bit_2 -a2_bit_1 a2_bit0 a2_bit1 a2_bit2 -a2_bit3 a2_bit4 a2_bit5 -a2_bit6 -a2_bit7 a2_bit8 -a2_bit9 -a2_bit10 -a2_bit11 -a2_bit12 -a2_bit13 -a2_bit14 -a2_bit15 -a2_bit16 -a2_bit17 -a2_bit18 -a2_bit19 -a3_bit_10 -a3_bit_9 a3_bit_8 -a3_bit_7 a3_bit_6 -a3_bit_5 -a3_bit_4 -a3_bit_3 -a3_bit_2 a3_bit_1 a3_bit0 -a3_bit1 -a3_bit2 -a3_bit3 a3_bit4 a3_bit5 a3_bit6 -a3_bit7 -a3_bit8 -a3_bit9 -a3_bit10 -a3_bit11 -a3_bit12 -a3_bit13 -a3_bit14 -a3_bit15 -a3_bit16 -a3_bit17 -a3_bit18 -a3_bit19 -a4_bit_10 -a4_bit_9 -a4_bit_8 -a4_bit_7 a4_bit_6 -a4_bit_5 -a4_bit_4 -a4_bit_3 -a4_bit_2 a4_bit_1 -a4_bit0 a4_bit1 a4_bit2 a4_bit3 a4_bit4 -a4_bit5 a4_bit6 a4_bit7 -a4_bit8 -a4_bit9 -a4_bit10 -a4_bit11 -a4_bit12 -a4_bit13 -a4_bit14 -a4_bit15 -a4_bit16 -a4_bit17 -a4_bit18 -a4_bit19 -a5_bit_10 a5_bit_9 -a5_bit_8 -a5_bit_7 -a5_bit_6 a5_bit_5 a5_bit_4 a5_bit_3 -a5_bit_2 -a5_bit_1 -a5_bit0 -a5_bit1 -a5_bit2 -a5_bit3 -a5_bit4 -a5_bit5 a5_bit6 a5_bit7 -a5_bit8 -a5_bit9 -a5_bit10 -a5_bit11 -a5_bit12 -a5_bit13 -a5_bit14 -a5_bit15 -a5_bit16 -a5_bit17 -a5_bit18 -a5_bit19 a6_bit_10 a6_bit_9 a6_bit_8 a6_bit_7 a6_bit_6 -a6_bit_5 a6_bit_4 a6_bit_3 a6_bit_2 -a6_bit_1 a6_bit0 a6_bit1 a6_bit2 a6_bit3 -a6_bit4 -a6_bit5 -a6_bit6 -a6_bit7 -a6_bit8 a6_bit9 a6_bit10 -a6_bit11 -a6_bit12 -a6_bit13 -a6_bit14 -a6_bit15 -a6_bit16 -a6_bit17 -a6_bit18 -a6_bit19 -a7_bit_10 -a7_bit_9 a7_bit_8 a7_bit_7 a7_bit_6 -a7_bit_5 a7_bit_4 a7_bit_3 -a7_bit_2 -a7_bit_1 a7_bit0 a7_bit1 -a7_bit2 -a7_bit3 a7_bit4 -a7_bit5 -a7_bit6 a7_bit7 a7_bit8 -a7_bit9 a7_bit10 -a7_bit11 -a7_bit12 -a7_bit13 -a7_bit14 -a7_bit15 -a7_bit16 -a7_bit17 -a7_bit18 -a7_bit19 -a8_bit_10 -a8_bit_9 -a8_bit_8 -a8_bit_7 -a8_bit_6 -a8_bit_5 a8_bit_4 -a8_bit_3 -a8_bit_2 -a8_bit_1 -a8_bit0 a8_bit1 -a8_bit2 -a8_bit3 -a8_bit4 -a8_bit5 -a8_bit6 a8_bit7 a8_bit8 a8_bit9 -a8_bit10 -a8_bit11 -a8_bit12 -a8_bit13 -a8_bit14 -a8_bit15 -a8_bit16 -a8_bit17 -a8_bit18 -a8_bit19 -a9_bit_10 -a9_bit_9 a9_bit_8 -a9_bit_7 a9_bit_6 -a9_bit_5 -a9_bit_4 -a9_bit_3 a9_bit_2 -a9_bit_1 a9_bit0 a9_bit1 a9_bit2 -a9_bit3 a9_bit4 -a9_bit5 a9_bit6 -a9_bit7 -a9_bit8 a9_bit9 -a9_bit10 -a9_bit11 -a9_bit12 -a9_bit13 -a9_bit14 -a9_bit15 -a9_bit16 -a9_bit17 -a9_bit18 -a9_bit19 a10_bit_10 -a10_bit_9 a10_bit_8 a10_bit_7 a10_bit_6 a10_bit_5 a10_bit_4 a10_bit_3 -a10_bit_2 -a10_bit_1 a10_bit0 -a10_bit1 a10_bit2 a10_bit3 a10_bit4 a10_bit5 -a10_bit6 -a10_bit7 -a10_bit8 -a10_bit9 a10_bit10 -a10_bit11 -a10_bit12 -a10_bit13 -a10_bit14 -a10_bit15 -a10_bit16 -a10_bit17 -a10_bit18 -a10_bit19 -a11_bit_10 a11_bit_9 -a11_bit_8 a11_bit_7 -a11_bit_6 a11_bit_5 -a11_bit_4 -a11_bit_3 -a11_bit_2 a11_bit_1 -a11_bit0 a11_bit1 a11_bit2 -a11_bit3 a11_bit4 -a11_bit5 a11_bit6 a11_bit7 a11_bit8 a11_bit9 -a11_bit10 -a11_bit11 -a11_bit12 -a11_bit13 -a11_bit14 -a11_bit15 -a11_bit16 -a11_bit17 -a11_bit18 -a11_bit19 -a12_bit_10 -a12_bit_9 -a12_bit_8 -a12_bit_7 -a12_bit_6 -a12_bit_5 -a12_bit_4 -a12_bit_3 a12_bit_2 a12_bit_1 a12_bit0 -a12_bit1 -a12_bit2 a12_bit3 -a12_bit4 -a12_bit5 -a12_bit6 a12_bit7 a12_bit8 -a12_bit9 -a12_bit10 -a12_bit11 -a12_bit12 -a12_bit13 -a12_bit14 -a12_bit15 -a12_bit16 -a12_bit17 -a12_bit18 -a12_bit19 -a13_bit_10 -a13_bit_9 -a13_bit_8 -a13_bit_7 -a13_bit_6 -a13_bit_5 -a13_bit_4 -a13_bit_3 -a13_bit_2 -a13_bit_1 -a13_bit0 -a13_bit1 -a13_bit2 -a13_bit3 -a13_bit4 -a13_bit5 a13_bit6 -a13_bit7 -a13_bit8 -a13_bit9 -a13_bit10 -a13_bit11 -a13_bit12 -a13_bit13 -a13_bit14 -a13_bit15 -a13_bit16 -a13_bit17 -a13_bit18 -a13_bit19 a14_bit_10 -a14_bit_9 -a14_bit_8 a14_bit_7 -a14_bit_6 -a14_bit_5 a14_bit_4 a14_bit_3 -a14_bit_2 -a14_bit_1 a14_bit0 -a14_bit1 a14_bit2 a14_bit3 -a14_bit4 -a14_bit5 -a14_bit6 -a14_bit7 -a14_bit8 -a14_bit9 -a14_bit10 a14_bit11 -a14_bit12 -a14_bit13 -a14_bit14 -a14_bit15 -a14_bit16 -a14_bit17 -a14_bit18 -a14_bit19 -a15_bit_10 -a15_bit_9 -a15_bit_8 a15_bit_7 -a15_bit_6 -a15_bit_5 -a15_bit_4 -a15_bit_3 -a15_bit_2 -a15_bit_1 -a15_bit0 -a15_bit1 -a15_bit2 a15_bit3 -a15_bit4 a15_bit5 a15_bit6 a15_bit7 a15_bit8 -a15_bit9 -a15_bit10 -a15_bit11 -a15_bit12 -a15_bit13 -a15_bit14 -a15_bit15 -a15_bit16 -a15_bit17 -a15_bit18 -a15_bit19 -a16_bit_10 a16_bit_9 -a16_bit_8 a16_bit_7 a16_bit_6 -a16_bit_5 a16_bit_4 a16_bit_3 -a16_bit_2 a16_bit_1 a16_bit0 a16_bit1 a16_bit2 a16_bit3 a16_bit4 -a16_bit5 -a16_bit6 a16_bit7 -a16_bit8 a16_bit9 -a16_bit10 -a16_bit11 -a16_bit12 -a16_bit13 -a16_bit14 -a16_bit15 -a16_bit16 -a16_bit17 -a16_bit18 -a16_bit19 a17_bit_10 -a17_bit_9 a17_bit_8 -a17_bit_7 -a17_bit_6 -a17_bit_5 a17_bit_4 -a17_bit_3 -a17_bit_2 -a17_bit_1 -a17_bit0 -a17_bit1 -a17_bit2 a17_bit3 -a17_bit4 a17_bit5 a17_bit6 a17_bit7 a17_bit8 -a17_bit9 -a17_bit10 -a17_bit11 -a17_bit12 -a17_bit13 -a17_bit14 -a17_bit15 -a17_bit16 -a17_bit17 -a17_bit18 -a17_bit19 -a18_bit_10 -a18_bit_9 -a18_bit_8 -a18_bit_7 -a18_bit_6 -a18_bit_5 -a18_bit_4 -a18_bit_3 -a18_bit_2 -a18_bit_1 -a18_bit0 -a18_bit1 -a18_bit2 a18_bit3 -a18_bit4 a18_bit5 a18_bit6 a18_bit7 a18_bit8 a18_bit9 -a18_bit10 -a18_bit11 -a18_bit12 -a18_bit13 -a18_bit14 -a18_bit15 -a18_bit16 -a18_bit17 -a18_bit18 -a18_bit19 -a19_bit_10 -a19_bit_9 a19_bit_8 -a19_bit_7 -a19_bit_6 -a19_bit_5 a19_bit_4 -a19_bit_3 -a19_bit_2 a19_bit_1 -a19_bit0 -a19_bit1 a19_bit2 -a19_bit3 a19_bit4 a19_bit5 -a19_bit6 -a19_bit7 -a19_bit8 a19_bit9 -a19_bit10 -a19_bit11 -a19_bit12 -a19_bit13 -a19_bit14 -a19_bit15 -a19_bit16 -a19_bit17 -a19_bit18 -a19_bit19 -a20_bit_10 a20_bit_9 -a20_bit_8 a20_bit_7 a20_bit_6 a20_bit_5 -a20_bit_4 a20_bit_3 a20_bit_2 a20_bit_1 -a20_bit0 -a20_bit1 a20_bit2 a20_bit3 -a20_bit4 -a20_bit5 a20_bit6 a20_bit7 -a20_bit8 -a20_bit9 -a20_bit10 -a20_bit11 -a20_bit12 -a20_bit13 -a20_bit14 -a20_bit15 -a20_bit16 -a20_bit17 -a20_bit18 -a20_bit19 -a21_bit_10 -a21_bit_9 -a21_bit_8 -a21_bit_7 -a21_bit_6 -a21_bit_5 a21_bit_4 a21_bit_3 a21_bit_2 -a21_bit_1 a21_bit0 a21_bit1 -a21_bit2 a21_bit3 a21_bit4 a21_bit5 -a21_bit6 a21_bit7 -a21_bit8 -a21_bit9 a21_bit10 -a21_bit11 -a21_bit12 -a21_bit13 -a21_bit14 -a21_bit15 -a21_bit16 -a21_bit17 -a21_bit18 -a21_bit19 -a22_bit_10 a22_bit_9 -a22_bit_8 a22_bit_7 a22_bit_6 -a22_bit_5 -a22_bit_4 a22_bit_3 a22_bit_2 a22_bit_1 a22_bit0 a22_bit1 -a22_bit2 -a22_bit3 a22_bit4 -a22_bit5 a22_bit6 a22_bit7 a22_bit8 -a22_bit9 a22_bit10 -a22_bit11 -a22_bit12 -a22_bit13 -a22_bit14 -a22_bit15 -a22_bit16 -a22_bit17 -a22_bit18 -a22_bit19 -a23_bit_10 -a23_bit_9 -a23_bit_8 a23_bit_7 -a23_bit_6 a23_bit_5 -a23_bit_4 a23_bit_3 a23_bit_2 a23_bit_1 a23_bit0 a23_bit1 -a23_bit2 -a23_bit3 -a23_bit4 -a23_bit5 -a23_bit6 -a23_bit7 a23_bit8 -a23_bit9 a23_bit10 a23_bit11 -a23_bit12 -a23_bit13 -a23_bit14 -a23_bit15 -a23_bit16 -a23_bit17 -a23_bit18 -a23_bit19 b1_bit_10 -b1_bit_9 -b1_bit_8 -b1_bit_7 b1_bit_6 -b1_bit_5 b1_bit_4 b1_bit_3 b1_bit_2 b1_bit_1 b1_bit0 b1_bit1 -b1_bit2 b1_bit3 b1_bit4 -b1_bit5 -b1_bit6 -b1_bit7 -b1_bit8 b1_bit9 -b1_bit10 -b1_bit11 -b1_bit12 b1_bit13 -b1_bit14 -b1_bit15 -b1_bit16 -b1_bit17 -b1_bit18 -b1_bit19 -b2_bit_10 -b2_bit_9 b2_bit_8 b2_bit_7 -b2_bit_6 b2_bit_5 b2_bit_4 b2_bit_3 b2_bit_2 b2_bit_1 b2_bit0 -b2_bit1 b2_bit2 b2_bit3 -b2_bit4 -b2_bit5 -b2_bit6 b2_bit7 b2_bit8 -b2_bit9 b2_bit10 b2_bit11 b2_bit12 -b2_bit13 -b2_bit14 -b2_bit15 -b2_bit16 -b2_bit17 -b2_bit18 -b2_bit19 -b3_bit_10 b3_bit_9 b3_bit_8 b3_bit_7 -b3_bit_6 b3_bit_5 b3_bit_4 b3_bit_3 b3_bit_2 -b3_bit_1 -b3_bit0 -b3_bit1 -b3_bit2 b3_bit3 b3_bit4 b3_bit5 b3_bit6 b3_bit7 -b3_bit8 b3_bit9 -b3_bit10 b3_bit11 -b3_bit12 -b3_bit13 -b3_bit14 -b3_bit15 -b3_bit16 -b3_bit17 -b3_bit18 -b3_bit19 -b4_bit_10 b4_bit_9 b4_bit_8 b4_bit_7 -b4_bit_6 b4_bit_5 b4_bit_4 b4_bit_3 b4_bit_2 -b4_bit_1 b4_bit0 b4_bit1 b4_bit2 b4_bit3 b4_bit4 b4_bit5 b4_bit6 b4_bit7 -b4_bit8 b4_bit9 -b4_bit10 b4_bit11 b4_bit12 -b4_bit13 -b4_bit14 -b4_bit15 -b4_bit16 -b4_bit17 -b4_bit18 -b4_bit19 b5_bit_10 b5_bit_9 b5_bit_8 -b5_bit_7 b5_bit_6 b5_bit_5 b5_bit_4 b5_bit_3 b5_bit_2 -b5_bit_1 b5_bit0 -b5_bit1 -b5_bit2 -b5_bit3 -b5_bit4 b5_bit5 -b5_bit6 b5_bit7 -b5_bit8 -b5_bit9 -b5_bit10 b5_bit11 b5_bit12 -b5_bit13 -b5_bit14 -b5_bit15 -b5_bit16 -b5_bit17 -b5_bit18 -b5_bit19 -b6_bit_10 b6_bit_9 -b6_bit_8 -b6_bit_7 b6_bit_6 -b6_bit_5 -b6_bit_4 -b6_bit_3 b6_bit_2 b6_bit_1 -b6_bit0 -b6_bit1 -b6_bit2 -b6_bit3 -b6_bit4 -b6_bit5 -b6_bit6 -b6_bit7 -b6_bit8 -b6_bit9 -b6_bit10 b6_bit11 b6_bit12 -b6_bit13 -b6_bit14 -b6_bit15 -b6_bit16 -b6_bit17 -b6_bit18 -b6_bit19 -b7_bit_10 b7_bit_9 -b7_bit_8 -b7_bit_7 -b7_bit_6 -b7_bit_5 b7_bit_4 -b7_bit_3 b7_bit_2 -b7_bit_1 -b7_bit0 b7_bit1 b7_bit2 b7_bit3 b7_bit4 b7_bit5 b7_bit6 b7_bit7 b7_bit8 b7_bit9 b7_bit10 -b7_bit11 b7_bit12 -b7_bit13 -b7_bit14 -b7_bit15 -b7_bit16 -b7_bit17 -b7_bit18 -b7_bit19 b8_bit_10 -b8_bit_9 -b8_bit_8 b8_bit_7 -b8_bit_6 b8_bit_5 -b8_bit_4 -b8_bit_3 -b8_bit_2 b8_bit_1 b8_bit0 -b8_bit1 -b8_bit2 b8_bit3 b8_bit4 -b8_bit5 b8_bit6 b8_bit7 -b8_bit8 -b8_bit9 -b8_bit10 b8_bit11 -b8_bit12 -b8_bit13 -b8_bit14 -b8_bit15 -b8_bit16 -b8_bit17 -b8_bit18 -b8_bit19 -b9_bit_10 -b9_bit_9 -b9_bit_8 b9_bit_7 -b9_bit_6 -b9_bit_5 b9_bit_4 b9_bit_3 b9_bit_2 -b9_bit_1 -b9_bit0 b9_bit1 b9_bit2 -b9_bit3 b9_bit4 b9_bit5 b9_bit6 b9_bit7 b9_bit8 -b9_bit9 -b9_bit10 -b9_bit11 -b9_bit12 -b9_bit13 -b9_bit14 -b9_bit15 -b9_bit16 -b9_bit17 -b9_bit18 -b9_bit19 b10_bit_10 -b10_bit_9 b10_bit_8 b10_bit_7 b10_bit_6 b10_bit_5 -b10_bit_4 -b10_bit_3 -b10_bit_2 -b10_bit_1 -b10_bit0 -b10_bit1 -b10_bit2 -b10_bit3 -b10_bit4 -b10_bit5 -b10_bit6 -b10_bit7 -b10_bit8 -b10_bit9 -b10_bit10 -b10_bit11 b10_bit12 -b10_bit13 -b10_bit14 -b10_bit15 -b10_bit16 -b10_bit17 -b10_bit18 -b10_bit19 -b11_bit_10 -b11_bit_9 -b11_bit_8 -b11_bit_7 -b11_bit_6 b11_bit_5 -b11_bit_4 b11_bit_3 b11_bit_2 b11_bit_1 b11_bit0 b11_bit1 -b11_bit2 b11_bit3 b11_bit4 b11_bit5 b11_bit6 b11_bit7 b11_bit8 -b11_bit9 b11_bit10 -b11_bit11 -b11_bit12 -b11_bit13 -b11_bit14 -b11_bit15 -b11_bit16 -b11_bit17 -b11_bit18 -b11_bit19 -b12_bit_10 b12_bit_9 -b12_bit_8 -b12_bit_7 -b12_bit_6 -b12_bit_5 -b12_bit_4 b12_bit_3 b12_bit_2 -b12_bit_1 -b12_bit0 b12_bit1 -b12_bit2 -b12_bit3 -b12_bit4 -b12_bit5 b12_bit6 b12_bit7 b12_bit8 -b12_bit9 b12_bit10 -b12_bit11 -b12_bit12 -b12_bit13 -b12_bit14 -b12_bit15 -b12_bit16 -b12_bit17 -b12_bit18 -b12_bit19 -b13_bit_10 -b13_bit_9 -b13_bit_8 -b13_bit_7 -b13_bit_6 -b13_bit_5 -b13_bit_4 -b13_bit_3 -b13_bit_2 -b13_bit_1 -b13_bit0 -b13_bit1 -b13_bit2 -b13_bit3 -b13_bit4 -b13_bit5 -b13_bit6 -b13_bit7 -b13_bit8 -b13_bit9 -b13_bit10 -b13_bit11 -b13_bit12 -b13_bit13 -b13_bit14 -b13_bit15 -b13_bit16 -b13_bit17 -b13_bit18 -b13_bit19 -b14_bit_10 b14_bit_9 -b14_bit_8 b14_bit_7 b14_bit_6 -b14_bit_5 -b14_bit_4 b14_bit_3 b14_bit_2 -b14_bit_1 -b14_bit0 -b14_bit1 b14_bit2 -b14_bit3 -b14_bit4 b14_bit5 -b14_bit6 b14_bit7 -b14_bit8 -b14_bit9 -b14_bit10 b14_bit11 -b14_bit12 -b14_bit13 -b14_bit14 -b14_bit15 -b14_bit16 -b14_bit17 -b14_bit18 -b14_bit19 -b15_bit_10 -b15_bit_9 b15_bit_8 -b15_bit_7 -b15_bit_6 b15_bit_5 -b15_bit_4 b15_bit_3 -b15_bit_2 -b15_bit_1 -b15_bit0 -b15_bit1 -b15_bit2 -b15_bit3 -b15_bit4 -b15_bit5 -b15_bit6 -b15_bit7 -b15_bit8 -b15_bit9 -b15_bit10 -b15_bit11 -b15_bit12 -b15_bit13 -b15_bit14 -b15_bit15 -b15_bit16 -b15_bit17 -b15_bit18 -b15_bit19 b16_bit_10 b16_bit_9 -b16_bit_8 -b16_bit_7 -b16_bit_6 b16_bit_5 b16_bit_4 -b16_bit_3 -b16_bit_2 b16_bit_1 b16_bit0 b16_bit1 b16_bit2 -b16_bit3 b16_bit4 b16_bit5 -b16_bit6 -b16_bit7 b16_bit8 -b16_bit9 -b16_bit10 b16_bit11 -b16_bit12 -b16_bit13 -b16_bit14 -b16_bit15 -b16_bit16 -b16_bit17 -b16_bit18 -b16_bit19 -b17_bit_10 b17_bit_9 -b17_bit_8 -b17_bit_7 -b17_bit_6 -b17_bit_5 -b17_bit_4 -b17_bit_3 -b17_bit_2 -b17_bit_1 -b17_bit0 -b17_bit1 -b17_bit2 -b17_bit3 -b17_bit4 b17_bit5 -b17_bit6 -b17_bit7 b17_bit8 b17_bit9 -b17_bit10 b17_bit11 b17_bit12 -b17_bit13 -b17_bit14 -b17_bit15 -b17_bit16 -b17_bit17 -b17_bit18 -b17_bit19 -b18_bit_10 -b18_bit_9 -b18_bit_8 -b18_bit_7 -b18_bit_6 -b18_bit_5 b18_bit_4 -b18_bit_3 -b18_bit_2 -b18_bit_1 -b18_bit0 -b18_bit1 -b18_bit2 -b18_bit3 -b18_bit4 -b18_bit5 -b18_bit6 -b18_bit7 -b18_bit8 -b18_bit9 -b18_bit10 -b18_bit11 -b18_bit12 -b18_bit13 -b18_bit14 -b18_bit15 -b18_bit16 -b18_bit17 -b18_bit18 -b18_bit19 b19_bit_10 b19_bit_9 b19_bit_8 -b19_bit_7 -b19_bit_6 b19_bit_5 -b19_bit_4 -b19_bit_3 -b19_bit_2 -b19_bit_1 -b19_bit0 -b19_bit1 -b19_bit2 -b19_bit3 -b19_bit4 b19_bit5 b19_bit6 -b19_bit7 -b19_bit8 -b19_bit9 b19_bit10 -b19_bit11 b19_bit12 -b19_bit13 -b19_bit14 -b19_bit15 -b19_bit16 -b19_bit17 -b19_bit18 -b19_bit19 -b20_bit_10 -b20_bit_9 b20_bit_8 b20_bit_7 -b20_bit_6 -b20_bit_5 b20_bit_4 -b20_bit_3 b20_bit_2 -b20_bit_1 b20_bit0 -b20_bit1 b20_bit2 b20_bit3 -b20_bit4 -b20_bit5 b20_bit6 -b20_bit7 -b20_bit8 -b20_bit9 b20_bit10 b20_bit11 -b20_bit12 -b20_bit13 -b20_bit14 -b20_bit15 -b20_bit16 -b20_bit17 -b20_bit18 -b20_bit19 -b21_bit_10 b21_bit_9 -b21_bit_8 b21_bit_7 -b21_bit_6 b21_bit_5 -b21_bit_4 -b21_bit_3 b21_bit_2 b21_bit_1 b21_bit0 b21_bit1 -b21_bit2 -b21_bit3 -b21_bit4 b21_bit5 -b21_bit6 b21_bit7 b21_bit8 -b21_bit9 -b21_bit10 -b21_bit11 -b21_bit12 -b21_bit13 -b21_bit14 -b21_bit15 -b21_bit16 -b21_bit17 -b21_bit18 -b21_bit19 b22_bit_10 b22_bit_9 b22_bit_8 b22_bit_7 -b22_bit_6 b22_bit_5 b22_bit_4 -b22_bit_3 -b22_bit_2 -b22_bit_1 -b22_bit0 -b22_bit1 b22_bit2 -b22_bit3 -b22_bit4 -b22_bit5 -b22_bit6 b22_bit7 -b22_bit8 -b22_bit9 -b22_bit10 -b22_bit11 -b22_bit12 -b22_bit13 -b22_bit14 -b22_bit15 -b22_bit16 -b22_bit17 -b22_bit18 -b22_bit19 b23_bit_10 b23_bit_9 b23_bit_8 b23_bit_7 -b23_bit_6 b23_bit_5 b23_bit_4 -b23_bit_3 -b23_bit_2 -b23_bit_1 -b23_bit0 -b23_bit1 -b23_bit2 b23_bit3 b23_bit4 -b23_bit5 -b23_bit6 -b23_bit7 -b23_bit8 -b23_bit9 b23_bit10 -b23_bit11 -b23_bit12 -b23_bit13 -b23_bit14 -b23_bit15 -b23_bit16 -b23_bit17 -b23_bit18 -b23_bit19 c1_bit0 c2_bit0 c3_bit0 c4_bit0 c5_bit0 c6_bit0 -c7_bit0 -c8_bit0 -c9_bit0 c10_bit0 -c11_bit0 -c12_bit0 -c13_bit0 -c14_bit0 c15_bit0 c16_bit0 c17_bit0 c18_bit0 -c19_bit0 -c20_bit0 -c21_bit0 -c22_bit0 c23_bit0 -f1_bit_10 -f1_bit_9 f1_bit_8 -f1_bit_7 -f1_bit_6 f1_bit_5 f1_bit_4 f1_bit_3 f1_bit_2 f1_bit_1 f1_bit0 -f1_bit1 f1_bit2 f1_bit3 -f1_bit4 -f1_bit5 f1_bit6 f1_bit7 f1_bit8 -f1_bit9 -f1_bit10 f1_bit11 -f1_bit12 -f1_bit13 -f1_bit14 -f1_bit15 -f1_bit16 -f1_bit17 -f1_bit18 -f1_bit19 -f10_bit_10 -f10_bit_9 -f10_bit_8 -f10_bit_7 -f10_bit_6 -f10_bit_5 -f10_bit_4 f10_bit_3 f10_bit_2 -f10_bit_1 f10_bit0 f10_bit1 f10_bit2 -f10_bit3 f10_bit4 f10_bit5 -f10_bit6 -f10_bit7 f10_bit8 f10_bit9 f10_bit10 f10_bit11 f10_bit12 -f10_bit13 -f10_bit14 -f10_bit15 -f10_bit16 -f10_bit17 -f10_bit18 -f10_bit19 -f12_bit_10 -f12_bit_9 -f12_bit_8 -f12_bit_7 -f12_bit_6 -f12_bit_5 -f12_bit_4 f12_bit_3 f12_bit_2 -f12_bit_1 -f12_bit0 f12_bit1 f12_bit2 f12_bit3 f12_bit4 f12_bit5 -f12_bit6 f12_bit7 f12_bit8 -f12_bit9 f12_bit10 -f12_bit11 -f12_bit12 -f12_bit13 -f12_bit14 -f12_bit15 -f12_bit16 -f12_bit17 -f12_bit18 -f12_bit19 -f13_bit_10 -f13_bit_9 -f13_bit_8 -f13_bit_7 -f13_bit_6 -f13_bit_5 -f13_bit_4 -f13_bit_3 -f13_bit_2 -f13_bit_1 -f13_bit0 -f13_bit1 -f13_bit2 -f13_bit3 -f13_bit4 -f13_bit5 -f13_bit6 -f13_bit7 -f13_bit8 -f13_bit9 -f13_bit10 -f13_bit11 -f13_bit12 -f13_bit13 -f13_bit14 -f13_bit15 -f13_bit16 -f13_bit17 -f13_bit18 -f13_bit19 f15_bit_10 -f15_bit_9 -f15_bit_8 -f15_bit_7 f15_bit_6 -f15_bit_5 f15_bit_4 f15_bit_3 f15_bit_2 f15_bit_1 f15_bit0 f15_bit1 f15_bit2 f15_bit3 -f15_bit4 -f15_bit5 -f15_bit6 -f15_bit7 f15_bit8 -f15_bit9 f15_bit10 -f15_bit11 -f15_bit12 -f15_bit13 -f15_bit14 -f15_bit15 -f15_bit16 -f15_bit17 -f15_bit18 -f15_bit19 -f16_bit_10 -f16_bit_9 f16_bit_8 -f16_bit_7 -f16_bit_6 -f16_bit_5 f16_bit_4 f16_bit_3 -f16_bit_2 -f16_bit_1 -f16_bit0 f16_bit1 -f16_bit2 f16_bit3 -f16_bit4 -f16_bit5 -f16_bit6 -f16_bit7 -f16_bit8 -f16_bit9 f16_bit10 f16_bit11 -f16_bit12 -f16_bit13 -f16_bit14 -f16_bit15 -f16_bit16 -f16_bit17 -f16_bit18 -f16_bit19 -f17_bit_10 -f17_bit_9 -f17_bit_8 -f17_bit_7 -f17_bit_6 -f17_bit_5 f17_bit_4 f17_bit_3 f17_bit_2 f17_bit_1 f17_bit0 f17_bit1 f17_bit2 f17_bit3 f17_bit4 f17_bit5 f17_bit6 f17_bit7 f17_bit8 -f17_bit9 -f17_bit10 f17_bit11 -f17_bit12 f17_bit13 -f17_bit14 -f17_bit15 -f17_bit16 -f17_bit17 -f17_bit18 -f17_bit19 -f2_bit_10 f2_bit_9 f2_bit_8 f2_bit_7 f2_bit_6 f2_bit_5 f2_bit_4 f2_bit_3 f2_bit_2 f2_bit_1 f2_bit0 -f2_bit1 f2_bit2 -f2_bit3 -f2_bit4 -f2_bit5 -f2_bit6 -f2_bit7 f2_bit8 -f2_bit9 f2_bit10 -f2_bit11 -f2_bit12 f2_bit13 -f2_bit14 -f2_bit15 -f2_bit16 -f2_bit17 -f2_bit18 -f2_bit19 -f20_bit_10 f20_bit_9 -f20_bit_8 -f20_bit_7 f20_bit_6 -f20_bit_5 -f20_bit_4 f20_bit_3 -f20_bit_2 -f20_bit_1 -f20_bit0 -f20_bit1 f20_bit2 f20_bit3 f20_bit4

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/18986/stat): 18986 (minisat+_script) R 18985 18986 824 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1793445351 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/18986/statm): 174 3 169 147 0 27 0
[pid=18986] 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=18987
New process pid=18988
New process pid=18989
execve syscall for /bin/sed executable
One traced child (pid=18988) 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=18989) exited with status: 0
One traced child (pid=18987) exited with status: 0
New process pid=18990
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb
One traced child (pid=18990) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=18991
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb

[startup+10.0042 s]
Raw data (loadavg): 0.15 0.03 0.01 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 751 0 4 0 971 4 0 0 25 0 1 0 1793445365 3190784 663 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 779 663 162 162 0 617 0
[pid=18991] vsize: 3116
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 5244

[startup+20.0059 s]
Raw data (loadavg): 0.28 0.06 0.02 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 819 0 4 0 1971 4 0 0 25 0 1 0 1793445365 3760128 731 4294967295 134512640 135167914 3221224448 3221219088 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 918 731 162 162 0 756 0
[pid=18991] vsize: 3672
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 5800

[startup+30.0066 s]
Raw data (loadavg): 0.39 0.09 0.03 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1032 0 4 0 2971 4 0 0 25 0 1 0 1793445365 4218880 861 4294967295 134512640 135167914 3221224448 3221221280 134849096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1030 861 162 162 0 868 0
[pid=18991] vsize: 4120
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 6248

[startup+40.0073 s]
Raw data (loadavg): 0.49 0.12 0.04 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1079 0 4 0 3970 5 0 0 25 0 1 0 1793445365 4341760 908 4294967295 134512640 135167914 3221224448 3221222080 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1060 908 162 162 0 898 0
[pid=18991] vsize: 4240
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 6368

[startup+50.008 s]
Raw data (loadavg): 0.56 0.15 0.05 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1148 0 4 0 4970 5 0 0 25 0 1 0 1793445365 4517888 977 4294967295 134512640 135167914 3221224448 3221220896 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1103 977 162 162 0 941 0
[pid=18991] vsize: 4412
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 6540

[startup+60.0078 s]
Raw data (loadavg): 0.63 0.18 0.06 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1196 0 4 0 5969 6 0 0 25 0 1 0 1793445365 5431296 1025 4294967295 134512640 135167914 3221224448 3221221904 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1326 1025 162 162 0 1164 0
[pid=18991] vsize: 5304
Current children cumulated CPU time (s) 59.77
Current children cumulated vsize (Kb) 7432

[startup+70.0085 s]
Raw data (loadavg): 0.69 0.21 0.07 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1260 0 4 0 6969 6 0 0 25 0 1 0 1793445365 5615616 1089 4294967295 134512640 135167914 3221224448 3221221392 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1371 1089 162 162 0 1209 0
[pid=18991] vsize: 5484
Current children cumulated CPU time (s) 69.77
Current children cumulated vsize (Kb) 7612

[startup+80.0092 s]
Raw data (loadavg): 0.73 0.23 0.08 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1300 0 4 0 7969 6 0 0 25 0 1 0 1793445365 5701632 1129 4294967295 134512640 135167914 3221224448 3221221472 134629148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1392 1129 162 162 0 1230 0
[pid=18991] vsize: 5568
Current children cumulated CPU time (s) 79.77
Current children cumulated vsize (Kb) 7696

[startup+90.0099 s]
Raw data (loadavg): 0.77 0.26 0.09 2/57 18991
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1680 0 4 0 8968 7 0 0 25 0 1 0 1793445365 6508544 1344 4294967295 134512640 135167914 3221224448 3221221280 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1589 1344 162 162 0 1427 0
[pid=18991] vsize: 6356
Current children cumulated CPU time (s) 89.77
Current children cumulated vsize (Kb) 8484

[startup+100.011 s]
Raw data (loadavg): 0.89 0.31 0.11 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1749 0 4 0 9967 7 0 0 25 0 1 0 1793445365 6684672 1413 4294967295 134512640 135167914 3221224448 3221218096 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 1632 1413 162 162 0 1470 0
[pid=18991] vsize: 6528
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 8656

[startup+110.011 s]
Raw data (loadavg): 0.91 0.33 0.12 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 7706 0 4 0 10914 36 0 0 25 0 1 0 1793445365 33697792 7326 4294967295 134512640 135167914 3221224448 3221223156 134558175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18991/statm): 8227 7326 162 162 0 8065 0
[pid=18991] vsize: 32908
Current children cumulated CPU time (s) 109.52
Current children cumulated vsize (Kb) 35036

[startup+120.013 s]
Raw data (loadavg): 0.92 0.35 0.12 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) T 18986 18986 824 0 -1 0 7911 0 4 0 11909 38 0 0 25 0 1 0 1793445365 34471936 7531 4294967295 134512640 135167914 3221224448 3221222876 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/18991/statm): 8416 7531 162 162 0 8254 0
[pid=18991] vsize: 33664
Current children cumulated CPU time (s) 119.49
Current children cumulated vsize (Kb) 35792

[startup+130.013 s]
Raw data (loadavg): 0.93 0.37 0.13 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 8086 0 4 0 12904 40 0 0 25 0 1 0 1793445365 35213312 7706 4294967295 134512640 135167914 3221224448 3221223088 134561462 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 8597 7706 162 162 0 8435 0
[pid=18991] vsize: 34388
Current children cumulated CPU time (s) 129.46
Current children cumulated vsize (Kb) 36516

[startup+140.015 s]
Raw data (loadavg): 0.94 0.39 0.14 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 8340 0 4 0 13900 42 0 0 25 0 1 0 1793445365 36237312 7960 4294967295 134512640 135167914 3221224448 3221223120 134562393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 8847 7960 162 162 0 8685 0
[pid=18991] vsize: 35388
Current children cumulated CPU time (s) 139.44
Current children cumulated vsize (Kb) 37516

[startup+150.015 s]
Raw data (loadavg): 0.95 0.41 0.15 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 8661 0 4 0 14894 44 0 0 25 0 1 0 1793445365 37609472 8281 4294967295 134512640 135167914 3221224448 3221223184 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 9182 8281 162 162 0 9020 0
[pid=18991] vsize: 36728
Current children cumulated CPU time (s) 149.4
Current children cumulated vsize (Kb) 38856

[startup+160.016 s]
Raw data (loadavg): 0.96 0.43 0.16 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 10080 0 4 0 15881 49 0 0 25 0 1 0 1793445365 42647552 9575 4294967295 134512640 135167914 3221224448 3220922608 134843118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 10412 9575 162 162 0 10250 0
[pid=18991] vsize: 41648
Current children cumulated CPU time (s) 159.32
Current children cumulated vsize (Kb) 43776

[startup+170.017 s]
Raw data (loadavg): 0.96 0.45 0.17 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 16868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215456 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 169.25
Current children cumulated vsize (Kb) 49444

[startup+180.016 s]
Raw data (loadavg): 0.97 0.47 0.18 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 17868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216348 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 179.25
Current children cumulated vsize (Kb) 49444

[startup+190.018 s]
Raw data (loadavg): 0.97 0.48 0.19 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 18868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215756 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 189.25
Current children cumulated vsize (Kb) 49444

[startup+200.019 s]
Raw data (loadavg): 0.98 0.50 0.19 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 19868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216016 134629080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 199.25
Current children cumulated vsize (Kb) 49444

[startup+210.019 s]
Raw data (loadavg): 0.98 0.52 0.20 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 20869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215824 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 209.26
Current children cumulated vsize (Kb) 49444

[startup+220.019 s]
Raw data (loadavg): 0.98 0.53 0.21 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 21869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215548 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 219.26
Current children cumulated vsize (Kb) 49444

[startup+230.02 s]
Raw data (loadavg): 0.98 0.55 0.22 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 22869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215896 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 229.26
Current children cumulated vsize (Kb) 49444

[startup+240.021 s]
Raw data (loadavg): 0.99 0.56 0.22 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 23869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216032 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 239.26
Current children cumulated vsize (Kb) 49444

[startup+250.022 s]
Raw data (loadavg): 0.99 0.58 0.23 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 24870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216096 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 249.27
Current children cumulated vsize (Kb) 49444

[startup+260.022 s]
Raw data (loadavg): 0.99 0.59 0.24 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 25870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215856 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 259.27
Current children cumulated vsize (Kb) 49444

[startup+270.023 s]
Raw data (loadavg): 0.99 0.60 0.25 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 26870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216540 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 269.27
Current children cumulated vsize (Kb) 49444

[startup+280.024 s]
Raw data (loadavg): 0.99 0.61 0.26 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 27870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215788 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 279.27
Current children cumulated vsize (Kb) 49444

[startup+290.025 s]
Raw data (loadavg): 0.99 0.63 0.26 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 28871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216208 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 289.28
Current children cumulated vsize (Kb) 49444

[startup+300.026 s]
Raw data (loadavg): 0.99 0.64 0.27 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 29871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215936 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 299.28
Current children cumulated vsize (Kb) 49444

[startup+310.026 s]
Raw data (loadavg): 0.99 0.65 0.28 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 30871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215808 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 309.28
Current children cumulated vsize (Kb) 49444

[startup+320.027 s]
Raw data (loadavg): 0.99 0.66 0.29 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 31871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216360 134694369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 319.28
Current children cumulated vsize (Kb) 49444

[startup+330.027 s]
Raw data (loadavg): 0.99 0.67 0.29 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 32872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215680 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 329.29
Current children cumulated vsize (Kb) 49444

[startup+340.028 s]
Raw data (loadavg): 0.99 0.68 0.30 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 33872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215200 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 339.29
Current children cumulated vsize (Kb) 49444

[startup+350.029 s]
Raw data (loadavg): 0.99 0.69 0.31 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 34872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217232 134849193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 349.29
Current children cumulated vsize (Kb) 49444

[startup+360.029 s]
Raw data (loadavg): 0.99 0.70 0.31 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 35872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 359.29
Current children cumulated vsize (Kb) 49444

[startup+370.03 s]
Raw data (loadavg): 0.99 0.71 0.32 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 36872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215936 134696587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 369.29
Current children cumulated vsize (Kb) 49444

[startup+380.03 s]
Raw data (loadavg): 0.99 0.72 0.33 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 37873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216536 134693801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 379.3
Current children cumulated vsize (Kb) 49444

[startup+390.031 s]
Raw data (loadavg): 0.99 0.73 0.33 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 38873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216652 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 389.3
Current children cumulated vsize (Kb) 49444

[startup+400.031 s]
Raw data (loadavg): 0.99 0.74 0.34 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 39873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216368 134629358 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 399.3
Current children cumulated vsize (Kb) 49444

[startup+410.032 s]
Raw data (loadavg): 0.99 0.74 0.35 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 40873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216284 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 409.3
Current children cumulated vsize (Kb) 49444

[startup+420.033 s]
Raw data (loadavg): 0.99 0.75 0.35 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 41874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216256 134718501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 419.31
Current children cumulated vsize (Kb) 49444

[startup+430.034 s]
Raw data (loadavg): 0.99 0.76 0.36 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 42874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216096 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 429.31
Current children cumulated vsize (Kb) 49444

[startup+440.034 s]
Raw data (loadavg): 0.99 0.77 0.37 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 43874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215932 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 439.31
Current children cumulated vsize (Kb) 49444

[startup+450.035 s]
Raw data (loadavg): 0.99 0.77 0.37 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 44874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216992 134696578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 449.31
Current children cumulated vsize (Kb) 49444

[startup+460.035 s]
Raw data (loadavg): 0.99 0.78 0.38 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 45875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216300 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 459.32
Current children cumulated vsize (Kb) 49444

[startup+470.035 s]
Raw data (loadavg): 0.99 0.79 0.39 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 46875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216172 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 469.32
Current children cumulated vsize (Kb) 49444

[startup+480.035 s]
Raw data (loadavg): 0.99 0.80 0.39 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 47875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 479.32
Current children cumulated vsize (Kb) 49444

[startup+490.036 s]
Raw data (loadavg): 0.99 0.80 0.40 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 48875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216304 134722527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 489.32
Current children cumulated vsize (Kb) 49444

[startup+500.037 s]
Raw data (loadavg): 0.99 0.81 0.40 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 49875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215988 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 499.32
Current children cumulated vsize (Kb) 49444

[startup+510.036 s]
Raw data (loadavg): 0.99 0.81 0.41 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 50876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216140 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 509.33
Current children cumulated vsize (Kb) 49444

[startup+520.037 s]
Raw data (loadavg): 0.99 0.82 0.41 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 51876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215920 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 519.33
Current children cumulated vsize (Kb) 49444

[startup+530.038 s]
Raw data (loadavg): 0.99 0.82 0.42 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 52876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216048 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 529.33
Current children cumulated vsize (Kb) 49444

[startup+540.038 s]
Raw data (loadavg): 0.99 0.83 0.43 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 53876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215920 134844668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 539.33
Current children cumulated vsize (Kb) 49444

[startup+550.039 s]
Raw data (loadavg): 0.99 0.83 0.43 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 54877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216400 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 549.34
Current children cumulated vsize (Kb) 49444

[startup+560.04 s]
Raw data (loadavg): 0.99 0.84 0.44 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 55877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217040 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 559.34
Current children cumulated vsize (Kb) 49444

[startup+570.041 s]
Raw data (loadavg): 0.99 0.84 0.44 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 56877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 569.34
Current children cumulated vsize (Kb) 49444

[startup+580.04 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 57877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216132 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 579.34
Current children cumulated vsize (Kb) 49444

[startup+590.042 s]
Raw data (loadavg): 0.99 0.85 0.46 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 58877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216400 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 589.34
Current children cumulated vsize (Kb) 49444

[startup+600.043 s]
Raw data (loadavg): 0.99 0.86 0.46 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 59878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216636 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 599.35
Current children cumulated vsize (Kb) 49444

[startup+610.044 s]
Raw data (loadavg): 0.99 0.86 0.47 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 60878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216560 134629442 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 609.35
Current children cumulated vsize (Kb) 49444

[startup+620.044 s]
Raw data (loadavg): 0.99 0.87 0.47 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 61878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217164 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 619.35
Current children cumulated vsize (Kb) 49444

[startup+630.044 s]
Raw data (loadavg): 0.99 0.87 0.47 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 62878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216640 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 629.35
Current children cumulated vsize (Kb) 49444

[startup+640.045 s]
Raw data (loadavg): 0.99 0.87 0.48 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 63879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216704 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 639.36
Current children cumulated vsize (Kb) 49444

[startup+650.045 s]
Raw data (loadavg): 0.99 0.88 0.48 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 64879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216528 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 649.36
Current children cumulated vsize (Kb) 49444

[startup+660.045 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 65879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216284 134723267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 659.36
Current children cumulated vsize (Kb) 49444

[startup+670.046 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 66879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216456 134693626 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 669.36
Current children cumulated vsize (Kb) 49444

[startup+680.047 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 67879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216424 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 679.36
Current children cumulated vsize (Kb) 49444

[startup+690.047 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 68880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216608 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 689.37
Current children cumulated vsize (Kb) 49444

[startup+700.048 s]
Raw data (loadavg): 0.99 0.89 0.51 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 69880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216576 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 699.37
Current children cumulated vsize (Kb) 49444

[startup+710.049 s]
Raw data (loadavg): 0.99 0.90 0.51 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 70880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216084 134718502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 709.37
Current children cumulated vsize (Kb) 49444

[startup+720.05 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 71880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216560 134629448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 719.37
Current children cumulated vsize (Kb) 49444

[startup+730.049 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 72881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216300 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 729.38
Current children cumulated vsize (Kb) 49444

[startup+740.05 s]
Raw data (loadavg): 0.99 0.91 0.53 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 73881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216128 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 739.38
Current children cumulated vsize (Kb) 49444

[startup+750.051 s]
Raw data (loadavg): 0.99 0.91 0.53 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 74881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215680 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 749.38
Current children cumulated vsize (Kb) 49444

[startup+760.051 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 75881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 759.38
Current children cumulated vsize (Kb) 49444

[startup+770.051 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 76881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216432 134845909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 769.38
Current children cumulated vsize (Kb) 49444

[startup+780.052 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 77882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 779.39
Current children cumulated vsize (Kb) 49444

[startup+790.053 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 78882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216880 134694364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 789.39
Current children cumulated vsize (Kb) 49444

[startup+800.053 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 79882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216540 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 799.39
Current children cumulated vsize (Kb) 49444

[startup+810.053 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 80882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216172 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 809.39
Current children cumulated vsize (Kb) 49444

[startup+820.054 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 81883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216720 134630893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 819.4
Current children cumulated vsize (Kb) 49444

[startup+830.055 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 82883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217168 134696283 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 829.4
Current children cumulated vsize (Kb) 49444

[startup+840.055 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 83883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216272 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 839.4
Current children cumulated vsize (Kb) 49444

[startup+850.056 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 84883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216448 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 849.4
Current children cumulated vsize (Kb) 49444

[startup+860.056 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 85883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216524 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 859.4
Current children cumulated vsize (Kb) 49444

[startup+870.056 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 86884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216272 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 869.41
Current children cumulated vsize (Kb) 49444

[startup+880.056 s]
Raw data (loadavg): 0.99 0.93 0.59 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 87884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216448 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 879.41
Current children cumulated vsize (Kb) 49444

[startup+890.058 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 88884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217428 134629281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 889.41
Current children cumulated vsize (Kb) 49444

[startup+900.059 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 89884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216480 134695319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 899.41
Current children cumulated vsize (Kb) 49444

[startup+910.058 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 90885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216508 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 909.42
Current children cumulated vsize (Kb) 49444

[startup+920.059 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 91885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217008 134849108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 919.42
Current children cumulated vsize (Kb) 49444

[startup+930.059 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 92885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216736 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 929.42
Current children cumulated vsize (Kb) 49444

[startup+940.059 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 93885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216880 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 939.42
Current children cumulated vsize (Kb) 49444

[startup+950.06 s]
Raw data (loadavg): 0.99 0.95 0.61 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 94885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216560 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 949.42
Current children cumulated vsize (Kb) 49444

[startup+960.061 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 95886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216448 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 959.43
Current children cumulated vsize (Kb) 49444

[startup+970.062 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 96886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216172 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 969.43
Current children cumulated vsize (Kb) 49444

[startup+980.061 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 97886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216684 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 979.43
Current children cumulated vsize (Kb) 49444

[startup+990.062 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 98886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216128 134720503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 989.43
Current children cumulated vsize (Kb) 49444

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 99887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215920 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 999.44
Current children cumulated vsize (Kb) 49444

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 100887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216864 134694386 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1009.44
Current children cumulated vsize (Kb) 49444

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 101887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216540 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1019.44
Current children cumulated vsize (Kb) 49444

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 102887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216984 134693693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1029.44
Current children cumulated vsize (Kb) 49444

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.95 0.65 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 103888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217056 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1039.45
Current children cumulated vsize (Kb) 49444

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.95 0.65 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 104888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216256 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1049.45
Current children cumulated vsize (Kb) 49444

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.96 0.65 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 105888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216352 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1059.45
Current children cumulated vsize (Kb) 49444

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 106888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216336 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1069.45
Current children cumulated vsize (Kb) 49444

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 107888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216108 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1079.45
Current children cumulated vsize (Kb) 49444

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 108889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134694528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1089.46
Current children cumulated vsize (Kb) 49444

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 109889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216284 134723267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1099.46
Current children cumulated vsize (Kb) 49444

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 110889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216256 134718501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1109.46
Current children cumulated vsize (Kb) 49444

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 111889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216688 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1119.46
Current children cumulated vsize (Kb) 49444

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 112890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216384 134629024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1129.47
Current children cumulated vsize (Kb) 49444

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.96 0.68 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 113890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216360 134693734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1139.47
Current children cumulated vsize (Kb) 49444

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.96 0.68 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 114890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216544 134629069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1149.47
Current children cumulated vsize (Kb) 49444

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.68 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 115890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134696710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1159.47
Current children cumulated vsize (Kb) 49444

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.68 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 116891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216688 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1169.48
Current children cumulated vsize (Kb) 49444

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 117891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1179.48
Current children cumulated vsize (Kb) 49444

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 118891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217088 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1189.48
Current children cumulated vsize (Kb) 49444

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 119891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216976 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1199.48
Current children cumulated vsize (Kb) 49444

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.70 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 120891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216288 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1209.48
Current children cumulated vsize (Kb) 49444



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.70 2/57 18999
Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/18986/statm): 532 234 485 147 0 385 0
[pid=18986] vsize: 2128
Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 120892 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216288 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0
[pid=18991] vsize: 47316
Current children cumulated CPU time (s) 1209.49
Current children cumulated vsize (Kb) 49444

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.51
CPU user time (s): 1208.92
CPU system time (s): 0.581911
CPU usage (%): 99.9503
Max. virtual memory (cumulated for all children) (Kb): 49444

Verifier Data

ERROR: no interpretation found !