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-bell4.opb
MD5SUM3cce8c056d32fd25c784b4e9cbdd2db6
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 540233279610250
Optimality of the best value was proved NO
Number of terms in the objective function 1527
Biggest coefficient in the objective function 4949278720000000
Number of bits for the biggest coefficient in the objective function 53
Sum of the numbers in the objective function 114314457147588882
Number of bits of the sum of numbers in the objective function 57
Biggest number in a constraint 4949278720000000
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 114314457147588882
Number of bits of the biggest sum of numbers57
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.07
Number of variables1996
Total number of constraints169
Number of constraints which are clauses18
Number of constraints which are cardinality constraints (but not clauses)34
Number of constraints which are nor clauses,nor cardinality constraints117
Minimum length of a constraint1
Maximum length of a constraint135

Trace number 3847

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        891056 kB
Buffers:         35220 kB
Cached:          74164 kB
SwapCached:        844 kB
Active:          48428 kB
Inactive:        63588 kB
HighTotal:      131008 kB
HighFree:        53648 kB
LowTotal:       903652 kB
LowFree:        837408 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            25848 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:25:25 (client local time) WITH STATUS 10 IN 1209.95 SECONDS
stats: 2846 7 1209.95 10

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 121] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 134 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssss..................ssss
c ---[ 128]---> BDD-cost:   13
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> 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 ---[  79]---> Sorter-cost:  513     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 ---[  78]---> Sorter-cost: 1482     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]---> Sorter-cost: 1469     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 ---[  76]---> 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 ---[  75]---> BDD-cost:   73
c ---[  74]---> 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 ---[  73]---> BDD-cost:   75
c ---[  72]---> BDD-cost:   71
c ---[  71]---> 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 ---[  70]---> Sorter-cost:  978     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 ---[  69]---> Sorter-cost:  978     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 ---[  68]---> Sorter-cost:  978     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 ---[  67]---> Sorter-cost: 1482     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 ---[  66]---> Sorter-cost: 1458     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 ---[  65]---> Sorter-cost:  952     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 ---[  64]---> 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 ---[  63]---> Sorter-cost:  557     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 ---[  62]---> BDD-cost:  131
c ---[  61]---> BDD-cost:  106
c ---[  60]---> BDD-cost:  106
c ---[  59]---> BDD-cost:  106
c ---[  58]---> BDD-cost:  106
c ---[  57]---> BDD-cost:  106
c ---[  56]---> BDD-cost:  106
c ---[  55]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  131
c ---[  53]---> BDD-cost:  131
c ---[  52]---> BDD-cost:  131
c ---[  51]---> BDD-cost:  131
c ---[  50]---> BDD-cost:  122
c ---[  49]---> BDD-cost:  131
c ---[  48]---> BDD-cost:  131
c ---[  47]---> BDD-cost:  219
c ---[  45]---> Sorter-cost:  883     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 ---[  44]---> Sorter-cost:  877     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> BDD-cost:   79
c ---[  41]---> Sorter-cost:  494     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 ---[  39]---> BDD-cost:   85
c ---[  38]---> BDD-cost:   81
c ---[  37]---> BDD-cost:   81
c ---[  36]---> 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 ---[  35]---> 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 ---[  34]---> BDD-cost:  216
c ---[  33]---> Sorter-cost:  858     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 ---[  32]---> Sorter-cost:  851     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 ---[  31]---> Sorter-cost:  497     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 ---[  30]---> BDD-cost:  216
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: 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 ---[  26]---> 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 ---[  25]---> 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 ---[  24]---> 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 ---[  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: 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 ---[  21]---> 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 ---[  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: 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 ---[  17]---> 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 ---[  16]---> 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 ---[  15]---> 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 ---[  14]---> 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 ---[  13]---> 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 ---[  12]---> 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 ---[  11]---> 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 ---[  10]---> 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 ---[   9]---> BDD-cost:    5
c ---[   8]---> BDD-cost:    5
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:   72
c ---[   2]---> BDD-cost:   55
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:   75
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  192158   451028 |   64052       0        0     nan |  0.000 % |
c |       100 |  192145   451000 |   70457      99      926     9.4 |  0.743 % |
c |       250 |  192145   451000 |   77502     249     2104     8.4 |  0.743 % |
c |       475 |  192089   450872 |   85253     471     4080     8.7 |  0.764 % |
c |       812 |  192089   450872 |   93778     808     7766     9.6 |  0.764 % |
c |      1318 |  192089   450872 |  103156    1314    12104     9.2 |  0.764 % |
c |      2078 |  192087   450868 |  113472    2073    20214     9.8 |  0.766 % |
c |      3217 |  192087   450868 |  124819    3212    30436     9.5 |  0.766 % |
c |      4926 |  192073   450838 |  137301    4919    63407    12.9 |  0.772 % |
c |      7488 |  190577   447433 |  151031    7452   154345    20.7 |  1.397 % |
c ==============================================================================
c Found solution: 4386416678763260
c ---[   0]---> 
c *** TERMINATED ***
s SATISFIABLE
v d1_bit0 -d2_bit0 -d3_bit0 d4_bit0 d5_bit0 d6_bit0 -d7_bit0 -d8_bit0 -d9_bit0 d10_bit0 -d11_bit0 d12_bit0 -d13_bit0 -d15_bit0 -d19_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 -h8_bit0 -h8_bit1 -h8_bit2 -h8_bit3 -h8_bit4 -h8_bit5 -h8_bit6 -h8_bit7 -h8_bit8 -h8_bit9 -h8_bit10 -h8_bit11 -h8_bit12 -h8_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 h11_bit0 -h11_bit1 h11_bit2 -h11_bit3 -h11_bit4 -h11_bit5 -h11_bit6 -h11_bit7 -h11_bit8 -h11_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 -h19_bit0 -h19_bit1 -h19_bit2 -h19_bit3 -h19_bit4 -h19_bit5 -h19_bit6 -h19_bit7 -h19_bit8 -h19_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 g8_bit0 -g8_bit1 g8_bit2 g8_bit3 g8_bit4 -g8_bit5 g8_bit6 g8_bit7 -g8_bit8 -g8_bit9 g8_bit10 -g8_bit11 g8_bit12 -g8_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 g11_bit0 -g11_bit1 g11_bit2 -g11_bit3 g11_bit4 g11_bit5 g11_bit6 -g11_bit7 g11_bit8 g11_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 g19_bit0 -g19_bit1 g19_bit2 g19_bit3 g19_bit4 -g19_bit5 g19_bit6 g19_bit7 g19_bit8 -g19_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 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 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 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 -f11_bit_10 -f11_bit_9 f11_bit_8 -f11_bit_7 f11_bit_6 f11_bit_5 -f11_bit_4 -f11_bit_3 -f11_bit_2 f11_bit_1 -f11_bit0 f11_bit1 f11_bit2 -f11_bit3 -f11_bit4 f11_bit5 f11_bit6 f11_bit7 f11_bit8 f11_bit9 f11_bit10 -f11_bit11 f11_bit12 -f11_bit13 -f11_bit14 -f11_bit15 -f11_bit16 -f11_bit17 -f11_bit18 -f11_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_bit

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/16370/stat): 16370 (minisat+_script) R 16369 16370 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1846483845 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16370/statm): 174 3 169 147 0 27 0
[pid=16370] 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=16371
New process pid=16372
New process pid=16373
execve syscall for /bin/sed executable
One traced child (pid=16372) 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=16373) exited with status: 0
One traced child (pid=16371) exited with status: 0
New process pid=16374
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bell4.opb
One traced child (pid=16374) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=16375
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bell4.opb

[startup+10.0044 s]
Raw data (loadavg): 0.57 0.86 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 673 0 0 0 989 2 0 0 25 0 1 0 1846483851 2830336 583 4294967295 134512640 135167914 3221224448 3221221440 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 691 583 162 162 0 529 0
[pid=16375] vsize: 2764
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 4892

[startup+20.0053 s]
Raw data (loadavg): 0.63 0.86 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 721 0 0 0 1988 3 0 0 25 0 1 0 1846483851 3346432 631 4294967295 134512640 135167914 3221224448 3221222144 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 817 631 162 162 0 655 0
[pid=16375] vsize: 3268
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 5396

[startup+30.0063 s]
Raw data (loadavg): 0.69 0.87 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 791 0 0 0 2988 3 0 0 25 0 1 0 1846483851 3530752 701 4294967295 134512640 135167914 3221224448 3221221528 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 862 701 162 162 0 700 0
[pid=16375] vsize: 3448
Current children cumulated CPU time (s) 29.92
Current children cumulated vsize (Kb) 5576

[startup+40.0142 s]
Raw data (loadavg): 0.74 0.87 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1003 0 0 0 3988 4 0 0 25 0 1 0 1846483851 3989504 830 4294967295 134512640 135167914 3221224448 3221222320 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 974 830 162 162 0 812 0
[pid=16375] vsize: 3896
Current children cumulated CPU time (s) 39.93
Current children cumulated vsize (Kb) 6024

[startup+50.0151 s]
Raw data (loadavg): 0.78 0.87 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1076 0 0 0 4987 5 0 0 25 0 1 0 1846483851 4177920 903 4294967295 134512640 135167914 3221224448 3221220848 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 1020 903 162 162 0 858 0
[pid=16375] vsize: 4080
Current children cumulated CPU time (s) 49.93
Current children cumulated vsize (Kb) 6208

[startup+60.016 s]
Raw data (loadavg): 0.81 0.88 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1126 0 0 0 5987 6 0 0 25 0 1 0 1846483851 4308992 953 4294967295 134512640 135167914 3221224448 3221221536 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 1052 953 162 162 0 890 0
[pid=16375] vsize: 4208
Current children cumulated CPU time (s) 59.94
Current children cumulated vsize (Kb) 6336

[startup+70.024 s]
Raw data (loadavg): 0.84 0.88 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1173 0 0 0 6987 6 0 0 25 0 1 0 1846483851 5218304 1000 4294967295 134512640 135167914 3221224448 3221222336 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 1274 1000 162 162 0 1112 0
[pid=16375] vsize: 5096
Current children cumulated CPU time (s) 69.94
Current children cumulated vsize (Kb) 7224

[startup+80.0249 s]
Raw data (loadavg): 0.86 0.88 0.95 1/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) T 16370 16370 31027 0 -1 0 5167 0 0 0 7956 21 0 0 23 0 1 0 1846483851 22745088 4953 4294967295 134512640 135167914 3221224448 3221213212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16375/statm): 5553 4953 162 162 0 5391 0
[pid=16375] vsize: 22212
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 24340

[startup+90.0259 s]
Raw data (loadavg): 0.88 0.89 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 6083 0 0 0 8945 28 0 0 25 0 1 0 1846483851 29450240 5869 4294967295 134512640 135167914 3221224448 3221223152 134562877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16375/statm): 7190 5869 162 162 0 7028 0
[pid=16375] vsize: 28760
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 30888

[startup+100.027 s]
Raw data (loadavg): 0.90 0.89 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 9930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221215900 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 36076

[startup+110.029 s]
Raw data (loadavg): 0.92 0.89 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 10930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216096 134696376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 36076

[startup+120.03 s]
Raw data (loadavg): 0.93 0.90 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 11930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216348 134696182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 36076

[startup+130.031 s]
Raw data (loadavg): 0.94 0.90 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 12930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216624 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 36076

[startup+140.031 s]
Raw data (loadavg): 0.95 0.90 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 13931 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 36076

[startup+150.032 s]
Raw data (loadavg): 0.95 0.91 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 14931 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216528 134694338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 149.67
Current children cumulated vsize (Kb) 36076

[startup+160.033 s]
Raw data (loadavg): 0.96 0.91 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 15931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221215932 134723236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 36076

[startup+170.034 s]
Raw data (loadavg): 0.97 0.91 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 16931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 36076

[startup+180.035 s]
Raw data (loadavg): 0.97 0.91 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 17931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216528 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 36076

[startup+190.036 s]
Raw data (loadavg): 0.98 0.92 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 18931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216160 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 189.68
Current children cumulated vsize (Kb) 36076

[startup+200.037 s]
Raw data (loadavg): 0.98 0.92 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 19931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216988 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 199.68
Current children cumulated vsize (Kb) 36076

[startup+210.038 s]
Raw data (loadavg): 0.98 0.92 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 20932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216716 134694459 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 209.69
Current children cumulated vsize (Kb) 36076

[startup+220.039 s]
Raw data (loadavg): 0.98 0.92 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 21932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216624 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 219.69
Current children cumulated vsize (Kb) 36076

[startup+230.039 s]
Raw data (loadavg): 0.99 0.92 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 22932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216336 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 229.69
Current children cumulated vsize (Kb) 36076

[startup+240.04 s]
Raw data (loadavg): 0.99 0.93 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 23932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221215932 134723246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 239.69
Current children cumulated vsize (Kb) 36076

[startup+250.041 s]
Raw data (loadavg): 0.99 0.93 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 24932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217680 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 249.69
Current children cumulated vsize (Kb) 36076

[startup+260.042 s]
Raw data (loadavg): 0.99 0.93 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 25933 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217056 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 259.7
Current children cumulated vsize (Kb) 36076

[startup+270.043 s]
Raw data (loadavg): 0.99 0.93 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 26933 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216900 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 269.7
Current children cumulated vsize (Kb) 36076

[startup+280.043 s]
Raw data (loadavg): 0.99 0.93 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 27933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217252 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 279.71
Current children cumulated vsize (Kb) 36076

[startup+290.044 s]
Raw data (loadavg): 0.99 0.93 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 28933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217056 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 289.71
Current children cumulated vsize (Kb) 36076

[startup+300.044 s]
Raw data (loadavg): 0.99 0.94 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 29933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 299.71
Current children cumulated vsize (Kb) 36076

[startup+310.045 s]
Raw data (loadavg): 0.99 0.94 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 30933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217216 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 309.71
Current children cumulated vsize (Kb) 36076

[startup+320.046 s]
Raw data (loadavg): 0.99 0.94 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 31934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216524 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 319.72
Current children cumulated vsize (Kb) 36076

[startup+330.046 s]
Raw data (loadavg): 0.99 0.94 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 32934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 329.72
Current children cumulated vsize (Kb) 36076

[startup+340.047 s]
Raw data (loadavg): 0.99 0.94 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 33934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217412 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 339.72
Current children cumulated vsize (Kb) 36076

[startup+350.048 s]
Raw data (loadavg): 0.99 0.94 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 34934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216976 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 349.72
Current children cumulated vsize (Kb) 36076

[startup+360.049 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 35934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217724 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 359.72
Current children cumulated vsize (Kb) 36076

[startup+370.05 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 36935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216812 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 369.73
Current children cumulated vsize (Kb) 36076

[startup+380.05 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 37935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217152 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 379.73
Current children cumulated vsize (Kb) 36076

[startup+390.051 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 38935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216896 134630183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 389.73
Current children cumulated vsize (Kb) 36076

[startup+400.052 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 39935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216624 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 399.73
Current children cumulated vsize (Kb) 36076

[startup+410.053 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 40935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217056 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 409.73
Current children cumulated vsize (Kb) 36076

[startup+420.054 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 41935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 419.73
Current children cumulated vsize (Kb) 36076

[startup+430.054 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 42936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217072 134629045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 429.74
Current children cumulated vsize (Kb) 36076

[startup+440.055 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 43936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216536 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 439.74
Current children cumulated vsize (Kb) 36076

[startup+450.056 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 44936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217088 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 449.74
Current children cumulated vsize (Kb) 36076

[startup+460.057 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 45936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217420 134696788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 459.74
Current children cumulated vsize (Kb) 36076

[startup+470.058 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 46936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 469.74
Current children cumulated vsize (Kb) 36076

[startup+480.058 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 47937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217180 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 479.75
Current children cumulated vsize (Kb) 36076

[startup+490.06 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 48937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 489.75
Current children cumulated vsize (Kb) 36076

[startup+500.061 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 49937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217356 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 499.75
Current children cumulated vsize (Kb) 36076

[startup+510.062 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 50937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216996 134723216 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 36076

[startup+520.063 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 51938 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217004 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 519.76
Current children cumulated vsize (Kb) 36076

[startup+530.063 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 52937 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217120 134845720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 529.76
Current children cumulated vsize (Kb) 36076

[startup+540.064 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 53938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216912 134629476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 539.77
Current children cumulated vsize (Kb) 36076

[startup+550.065 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 54938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217136 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 549.77
Current children cumulated vsize (Kb) 36076

[startup+560.066 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 55938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 559.77
Current children cumulated vsize (Kb) 36076

[startup+570.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 56938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217052 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 569.77
Current children cumulated vsize (Kb) 36076

[startup+580.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 57939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217500 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 579.78
Current children cumulated vsize (Kb) 36076

[startup+590.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 58939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 589.78
Current children cumulated vsize (Kb) 36076

[startup+600.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 59939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217388 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 599.78
Current children cumulated vsize (Kb) 36076

[startup+610.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 60939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217568 134694495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 609.78
Current children cumulated vsize (Kb) 36076

[startup+620.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 61939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217264 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 619.78
Current children cumulated vsize (Kb) 36076

[startup+630.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 62940 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217744 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 629.79
Current children cumulated vsize (Kb) 36076

[startup+640.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 63940 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216456 134693662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 639.79
Current children cumulated vsize (Kb) 36076

[startup+650.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 64939 39 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216736 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 649.79
Current children cumulated vsize (Kb) 36076

[startup+660.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 65939 40 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217224 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 659.8
Current children cumulated vsize (Kb) 36076

[startup+670.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 66939 40 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217664 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 669.8
Current children cumulated vsize (Kb) 36076

[startup+680.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 67939 40 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217204 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 679.8
Current children cumulated vsize (Kb) 36076

[startup+690.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 68939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216876 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 689.81
Current children cumulated vsize (Kb) 36076

[startup+700.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 69939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217232 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 699.81
Current children cumulated vsize (Kb) 36076

[startup+710.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 70939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217344 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 709.81
Current children cumulated vsize (Kb) 36076

[startup+720.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 71939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217052 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 719.81
Current children cumulated vsize (Kb) 36076

[startup+730.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 72939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217004 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 729.81
Current children cumulated vsize (Kb) 36076

[startup+740.083 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 73939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217380 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 739.81
Current children cumulated vsize (Kb) 36076

[startup+750.083 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 74940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221218112 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 749.82
Current children cumulated vsize (Kb) 36076

[startup+760.085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 75940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217344 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 759.82
Current children cumulated vsize (Kb) 36076

[startup+770.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 76940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217552 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 769.82
Current children cumulated vsize (Kb) 36076

[startup+780.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 77940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216716 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 779.82
Current children cumulated vsize (Kb) 36076

[startup+790.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 78940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216608 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 789.83
Current children cumulated vsize (Kb) 36076

[startup+800.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 79940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216688 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 799.83
Current children cumulated vsize (Kb) 36076

[startup+810.089 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 80940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217240 134694369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 809.83
Current children cumulated vsize (Kb) 36076

[startup+820.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 81941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216976 134844694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 819.84
Current children cumulated vsize (Kb) 36076

[startup+830.091 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 82940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217424 134629172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 829.83
Current children cumulated vsize (Kb) 36076

[startup+840.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 83941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217072 134630853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 839.84
Current children cumulated vsize (Kb) 36076

[startup+850.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 84941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217584 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 849.84
Current children cumulated vsize (Kb) 36076

[startup+860.094 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 85941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217732 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 859.84
Current children cumulated vsize (Kb) 36076

[startup+870.095 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 86942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217856 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 869.85
Current children cumulated vsize (Kb) 36076

[startup+880.096 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 87942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217060 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 879.85
Current children cumulated vsize (Kb) 36076

[startup+890.097 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 88942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 889.85
Current children cumulated vsize (Kb) 36076

[startup+900.098 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 89942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217392 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 899.85
Current children cumulated vsize (Kb) 36076

[startup+910.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 90942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217024 134522331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 909.85
Current children cumulated vsize (Kb) 36076

[startup+920.101 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 91943 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217212 134630279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 919.86
Current children cumulated vsize (Kb) 36076

[startup+930.102 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 92943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217392 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 929.87
Current children cumulated vsize (Kb) 36076

[startup+940.103 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 93943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216516 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 939.87
Current children cumulated vsize (Kb) 36076

[startup+950.104 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 94943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217068 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 949.87
Current children cumulated vsize (Kb) 36076

[startup+960.105 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 95943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217372 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 959.87
Current children cumulated vsize (Kb) 36076

[startup+970.106 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 96944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217596 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 969.88
Current children cumulated vsize (Kb) 36076

[startup+980.107 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 97944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217536 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 979.88
Current children cumulated vsize (Kb) 36076

[startup+990.107 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 98944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217152 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 989.88
Current children cumulated vsize (Kb) 36076

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 99944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221218240 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 999.88
Current children cumulated vsize (Kb) 36076

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 100944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217136 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1009.88
Current children cumulated vsize (Kb) 36076

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 101945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217240 134693744 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1019.89
Current children cumulated vsize (Kb) 36076

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 102945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217568 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1029.89
Current children cumulated vsize (Kb) 36076

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 103945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217680 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1039.89
Current children cumulated vsize (Kb) 36076

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 104945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217740 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1049.89
Current children cumulated vsize (Kb) 36076

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 105945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217312 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1059.89
Current children cumulated vsize (Kb) 36076

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 106945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217568 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1069.89
Current children cumulated vsize (Kb) 36076

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 107946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217600 134629358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1079.9
Current children cumulated vsize (Kb) 36076

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 108946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217496 134718503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1089.9
Current children cumulated vsize (Kb) 36076

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 109946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217968 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1099.9
Current children cumulated vsize (Kb) 36076

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 110946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216976 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1109.9
Current children cumulated vsize (Kb) 36076

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 111947 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217088 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1119.91
Current children cumulated vsize (Kb) 36076

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 112947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217632 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1129.92
Current children cumulated vsize (Kb) 36076

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 113947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216960 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1139.92
Current children cumulated vsize (Kb) 36076

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 114947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216816 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1149.92
Current children cumulated vsize (Kb) 36076

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 115947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216640 134696656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1159.92
Current children cumulated vsize (Kb) 36076

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 116948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216800 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1169.93
Current children cumulated vsize (Kb) 36076

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 117948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217036 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1179.93
Current children cumulated vsize (Kb) 36076

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 118948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217388 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1189.93
Current children cumulated vsize (Kb) 36076

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 119948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216928 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1199.93
Current children cumulated vsize (Kb) 36076

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 120949 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217488 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1209.94
Current children cumulated vsize (Kb) 36076



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 16375
Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16370/statm): 532 234 485 147 0 385 0
[pid=16370] vsize: 2128
Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 120949 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217440 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0
[pid=16375] vsize: 33948
Current children cumulated CPU time (s) 1209.94
Current children cumulated vsize (Kb) 36076

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.95
CPU user time (s): 1209.5
CPU system time (s): 0.45493
CPU usage (%): 99.9833
Max. virtual memory (cumulated for all children) (Kb): 36076

Verifier Data

ERROR: no interpretation found !