Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-bell5.opb
MD5SUMfa1c29f360870381638d135cd26eadfd
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 181644428760406
Optimality of the best value was proved NO
Number of terms in the objective function 948
Biggest coefficient in the objective function 6291456000000000
Number of bits for the biggest coefficient in the objective function 53
Sum of the numbers in the objective function 104362034158211275
Number of bits of the sum of numbers in the objective function 57
Biggest number in a constraint 6291456000000000
Number of bits of the biggest number in a constraint 53
Biggest sum of numbers in a constraint 104362034158211275
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 benchmark1228.67
Number of variables1244
Total number of constraints149
Number of constraints which are clauses15
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints104
Minimum length of a constraint1
Maximum length of a constraint95

Trace number 6077

Launcher Data

LAUNCH ON wulflinc3 THE 2005-09-20 03:08:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3231 boxname=wulflinc3 idbench=887 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa1c29f360870381638d135cd26eadfd  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-bell5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-bell5.opb
IDLAUNCH: 3231
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        919448 kB
Buffers:         10528 kB
Cached:          78204 kB
SwapCached:        824 kB
Active:          22584 kB
Inactive:        68744 kB
HighTotal:      131008 kB
HighFree:        48888 kB
LowTotal:       903652 kB
LowFree:        870560 kB
SwapTotal:     2097136 kB
SwapFree:      2095740 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            18028 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:28:11 (client local time) WITH STATUS 10 IN 1209.7 SECONDS
stats: 3231 7 1209.7 10

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 108] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 114 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssss...............sssssssss
c ---[ 108]---> BDD-cost:    6
c ---[ 107]---> BDD-cost:    6
c ---[ 106]---> BDD-cost:    6
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    6
c ---[ 103]---> BDD-cost:    6
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]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> Sorter-cost: 1174     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> BDD-cost:  167
c ---[  69]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> BDD-cost:  167
c ---[  66]---> Sorter-cost: 1174     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost: 1081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost: 1174     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost: 1174     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> BDD-cost:  264
c ---[  61]---> Sorter-cost: 1081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> BDD-cost:   58
c ---[  59]---> BDD-cost:  264
c ---[  58]---> BDD-cost:   88
c ---[  57]---> BDD-cost:   73
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:   73
c ---[  54]---> BDD-cost:   73
c ---[  53]---> BDD-cost:   73
c ---[  52]---> BDD-cost:   73
c ---[  51]---> BDD-cost:   88
c ---[  50]---> BDD-cost:   88
c ---[  49]---> BDD-cost:   88
c ---[  48]---> BDD-cost:   88
c ---[  47]---> BDD-cost:   88
c ---[  46]---> BDD-cost:   88
c ---[  45]---> BDD-cost:   88
c ---[  44]---> Sorter-cost:  756     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  414     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  448     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  448     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:    9
c ---[  36]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  448     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> BDD-cost:   62
c ---[  29]---> BDD-cost:   69
c ---[  24]---> Sorter-cost: 2457     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[  23]---> Sorter-cost: 2457     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5
c ---[  20]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[  19]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[  18]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[  17]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[  16]---> BDD-cost:    5
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[  11]---> BDD-cost:    5
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    5
c ---[   8]---> BDD-cost:   61
c ---[   7]---> BDD-cost:   36
c ---[   6]---> BDD-cost:   41
c ---[   5]---> Sorter-cost: 2455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[   4]---> Sorter-cost: 2455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[   3]---> Sorter-cost: 2455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[   2]---> Sorter-cost: 2455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[   1]---> Sorter-cost: 2455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[   0]---> Sorter-cost: 2455     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  118368   278248 |   39456       0        0     nan |  0.000 % |
c |       100 |  118364   278240 |   43401      99      537     5.4 |  0.480 % |
c |       250 |  118334   278176 |   47741     247     2256     9.1 |  0.503 % |
c |       475 |  118334   278176 |   52515     472     3459     7.3 |  0.503 % |
c |       812 |  118332   278172 |   57767     807     7417     9.2 |  0.505 % |
c |      1318 |  118280   278058 |   63544    1307    10640     8.1 |  0.540 % |
c |      2077 |  118137   277744 |   69898    2060    22806    11.1 |  0.636 % |
c ==============================================================================
c Found solution: 454275098577591
c ---[   0]---> 
c *** TERMINATED ***
s SATISFIABLE
v -d1_bit0 -d2_bit0 d3_bit0 -d4_bit0 -d5_bit0 -d6_bit0 -d7_bit0 -d9_bit0 -d10_bit0 -d11_bit0 -d12_bit0 -d13_bit0 -d14_bit0 d16_bit0 h1_bit0 -h1_bit1 -h1_bit2 h1_bit3 -h1_bit4 -h1_bit5 -h1_bit6 -h1_bit7 -h1_bit8 -h1_bit9 -h1_bit10 -h1_bit11 -h1_bit12 -h1_bit13 h2_bit0 h2_bit1 h2_bit2 -h2_bit3 -h2_bit4 -h2_bit5 -h2_bit6 -h2_bit7 -h2_bit8 -h2_bit9 -h2_bit10 -h2_bit11 -h2_bit12 -h2_bit13 -h3_bit0 h3_bit1 h3_bit2 -h3_bit3 -h3_bit4 -h3_bit5 -h3_bit6 -h3_bit7 -h3_bit8 -h3_bit9 -h3_bit10 -h3_bit11 -h3_bit12 -h3_bit13 h4_bit0 h4_bit1 -h4_bit2 -h4_bit3 -h4_bit4 -h4_bit5 -h4_bit6 -h4_bit7 -h4_bit8 -h4_bit9 -h4_bit10 -h4_bit11 -h4_bit12 -h4_bit13 h5_bit0 -h5_bit1 h5_bit2 h5_bit3 -h5_bit4 -h5_bit5 -h5_bit6 -h5_bit7 -h5_bit8 -h5_bit9 -h5_bit10 -h5_bit11 -h5_bit12 -h5_bit13 -h6_bit0 -h6_bit1 -h6_bit2 -h6_bit3 -h6_bit4 -h6_bit5 -h6_bit6 -h6_bit7 -h6_bit8 -h6_bit9 -h6_bit10 -h6_bit11 -h6_bit12 -h6_bit13 -h7_bit0 -h7_bit1 -h7_bit2 h7_bit3 -h7_bit4 -h7_bit5 -h7_bit6 -h7_bit7 -h7_bit8 -h7_bit9 -h7_bit10 -h7_bit11 -h7_bit12 -h7_bit13 -h9_bit0 -h9_bit1 -h9_bit2 -h9_bit3 -h9_bit4 -h9_bit5 -h9_bit6 -h9_bit7 -h9_bit8 -h9_bit9 -h9_bit10 -h9_bit11 -h9_bit12 -h9_bit13 -h10_bit0 -h10_bit1 -h10_bit2 -h10_bit3 -h10_bit4 -h10_bit5 -h10_bit6 -h10_bit7 -h10_bit8 -h10_bit9 -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 -h14_bit0 h14_bit1 -h14_bit2 h14_bit3 -h14_bit4 -h14_bit5 -h14_bit6 -h14_bit7 -h14_bit8 -h14_bit9 h16_bit0 -h16_bit1 -h16_bit2 -h16_bit3 -h16_bit4 -h16_bit5 -h16_bit6 -h16_bit7 -h16_bit8 -h16_bit9 -g1_bit0 g1_bit1 -g1_bit2 g1_bit3 g1_bit4 g1_bit5 g1_bit6 -g1_bit7 -g1_bit8 -g1_bit9 g2_bit0 g2_bit1 g2_bit2 -g2_bit3 g2_bit4 g2_bit5 g2_bit6 g2_bit7 -g2_bit8 -g2_bit9 -g3_bit0 g3_bit1 -g3_bit2 -g3_bit3 g3_bit4 g3_bit5 g3_bit6 -g3_bit7 g3_bit8 -g3_bit9 g4_bit0 g4_bit1 g4_bit2 -g4_bit3 -g4_bit4 g4_bit5 g4_bit6 -g4_bit7 g4_bit8 -g4_bit9 -g5_bit0 g5_bit1 g5_bit2 g5_bit3 g5_bit4 g5_bit5 g5_bit6 -g5_bit7 g5_bit8 -g5_bit9 -g6_bit0 g6_bit1 -g6_bit2 -g6_bit3 g6_bit4 g6_bit5 g6_bit6 -g6_bit7 -g6_bit8 g6_bit9 -g7_bit0 g7_bit1 -g7_bit2 g7_bit3 -g7_bit4 g7_bit5 g7_bit6 -g7_bit7 g7_bit8 -g7_bit9 g9_bit0 g9_bit1 g9_bit2 g9_bit3 g9_bit4 -g9_bit5 g9_bit6 g9_bit7 -g9_bit8 -g9_bit9 g10_bit0 -g10_bit1 -g10_bit2 -g10_bit3 -g10_bit4 -g10_bit5 g10_bit6 g11_bit0 g11_bit1 g11_bit2 -g11_bit3 -g11_bit4 g11_bit5 -g11_bit6 g12_bit0 g12_bit1 g12_bit2 g12_bit3 -g12_bit4 -g12_bit5 g12_bit6 g13_bit0 -g13_bit1 -g13_bit2 g13_bit3 g13_bit4 g13_bit5 -g13_bit6 -g14_bit0 g14_bit1 g14_bit2 -g14_bit3 g14_bit4 -g14_bit5 g14_bit6 -g16_bit0 -g16_bit1 -g16_bit2 -g16_bit3 -g16_bit4 -g16_bit5 g16_bit6 -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 -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 -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 -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 -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 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 -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 -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 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 -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 -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 -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 -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 -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 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 -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 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 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 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 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 -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 -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 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 -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 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 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 -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 -b12_bit_7 -b12_bit_6 -b12_bit_5 -b12_bit_4 -b12_bit_3 -b12_bit_2 -b12_bit_1 -b12_b

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/3661/stat): 3661 (minisat+_script) R 3660 3661 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796935910 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3661/statm): 174 3 169 147 0 27 0
[pid=3661] 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=3662
New process pid=3663
New process pid=3664
execve syscall for /bin/sed executable
One traced child (pid=3663) 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=3664) exited with status: 0
One traced child (pid=3662) exited with status: 0
New process pid=3665
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-bell5.opb
One traced child (pid=3665) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=3666
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-bell5.opb

[startup+10.0042 s]
Raw data (loadavg): 0.94 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 601 0 0 0 989 2 0 0 25 0 1 0 1796935916 2584576 510 4294967295 134512640 135167914 3221224448 3221221920 134696248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 631 510 162 162 0 469 0
[pid=3666] vsize: 2524
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 4652

[startup+20.0051 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 679 0 0 0 1988 2 0 0 25 0 1 0 1796935916 3182592 588 4294967295 134512640 135167914 3221224448 3221221728 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 777 588 162 162 0 615 0
[pid=3666] vsize: 3108
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 5236

[startup+30.0079 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 924 0 0 0 2986 4 0 0 25 0 1 0 1796935916 3727360 750 4294967295 134512640 135167914 3221224448 3221221200 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 910 750 162 162 0 748 0
[pid=3666] vsize: 3640
Current children cumulated CPU time (s) 29.92
Current children cumulated vsize (Kb) 5768

[startup+40.0087 s]
Raw data (loadavg): 0.96 0.98 0.94 1/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) T 3661 3661 31915 0 -1 0 4674 0 0 0 3954 19 0 0 25 0 1 0 1796935916 19886080 4399 4294967295 134512640 135167914 3221224448 3221045436 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3666/statm): 4855 4399 162 162 0 4693 0
[pid=3666] vsize: 19420
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 21548

[startup+50.0106 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 4939 26 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134696366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 49.67
Current children cumulated vsize (Kb) 27272

[startup+60.0114 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 5939 26 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216736 134629451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 59.67
Current children cumulated vsize (Kb) 27272

[startup+70.0123 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 6938 26 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216880 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 27272

[startup+80.0141 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 7938 26 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 27272

[startup+90.0139 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 8938 27 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 27272

[startup+100.015 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 9937 27 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 27272

[startup+110.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 10937 27 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216852 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 27272

[startup+120.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 11937 27 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216472 134847058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 27272

[startup+130.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 12936 27 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217244 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 129.65
Current children cumulated vsize (Kb) 27272

[startup+140.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 13935 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216872 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 139.65
Current children cumulated vsize (Kb) 27272

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 14936 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217008 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 149.66
Current children cumulated vsize (Kb) 27272

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 15935 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216492 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 159.65
Current children cumulated vsize (Kb) 27272

[startup+170.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 16935 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216716 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 169.65
Current children cumulated vsize (Kb) 27272

[startup+180.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 17935 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216976 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 179.65
Current children cumulated vsize (Kb) 27272

[startup+190.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 18935 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216480 134720472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 189.65
Current children cumulated vsize (Kb) 27272

[startup+200.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 19934 28 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216992 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 199.64
Current children cumulated vsize (Kb) 27272

[startup+210.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 20933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216784 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 209.64
Current children cumulated vsize (Kb) 27272

[startup+220.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 21933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216736 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 219.64
Current children cumulated vsize (Kb) 27272

[startup+230.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 22933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134844723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 229.64
Current children cumulated vsize (Kb) 27272

[startup+240.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 23933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 239.64
Current children cumulated vsize (Kb) 27272

[startup+250.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 24933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 249.64
Current children cumulated vsize (Kb) 27272

[startup+260.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 25933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217416 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 259.64
Current children cumulated vsize (Kb) 27272

[startup+270.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 26933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217076 134629209 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 269.64
Current children cumulated vsize (Kb) 27272

[startup+280.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 27933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217232 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 27272

[startup+290.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 28933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217216 134694435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 27272

[startup+300.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 29933 29 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217088 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 299.64
Current children cumulated vsize (Kb) 27272

[startup+310.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 30932 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216784 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 309.64
Current children cumulated vsize (Kb) 27272

[startup+320.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 31932 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216784 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 319.64
Current children cumulated vsize (Kb) 27272

[startup+330.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 32932 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217388 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 329.64
Current children cumulated vsize (Kb) 27272

[startup+340.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 33933 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 339.65
Current children cumulated vsize (Kb) 27272

[startup+350.035 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 34933 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216876 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 349.65
Current children cumulated vsize (Kb) 27272

[startup+360.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 35932 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217056 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 359.64
Current children cumulated vsize (Kb) 27272

[startup+370.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 36932 30 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216832 134720495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 369.64
Current children cumulated vsize (Kb) 27272

[startup+380.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 37932 31 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217392 134694413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 379.65
Current children cumulated vsize (Kb) 27272

[startup+390.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 38932 31 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217424 134629290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 389.65
Current children cumulated vsize (Kb) 27272

[startup+400.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 39932 31 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217120 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 399.65
Current children cumulated vsize (Kb) 27272

[startup+410.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 40932 31 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221218060 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 409.65
Current children cumulated vsize (Kb) 27272

[startup+420.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 41931 32 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 419.65
Current children cumulated vsize (Kb) 27272

[startup+430.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 42931 32 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216976 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 429.65
Current children cumulated vsize (Kb) 27272

[startup+440.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 43931 32 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216704 134696565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 439.65
Current children cumulated vsize (Kb) 27272

[startup+450.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 44931 32 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216576 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 449.65
Current children cumulated vsize (Kb) 27272

[startup+460.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 45931 33 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134693792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 459.66
Current children cumulated vsize (Kb) 27272

[startup+470.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 46931 33 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216928 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 469.66
Current children cumulated vsize (Kb) 27272

[startup+480.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 47931 33 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217868 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 479.66
Current children cumulated vsize (Kb) 27272

[startup+490.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 48931 33 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216784 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 489.66
Current children cumulated vsize (Kb) 27272

[startup+500.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 49931 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134696754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 499.67
Current children cumulated vsize (Kb) 27272

[startup+510.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 50931 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217004 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 509.67
Current children cumulated vsize (Kb) 27272

[startup+520.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 51931 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216660 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 519.67
Current children cumulated vsize (Kb) 27272

[startup+530.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 52931 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 529.67
Current children cumulated vsize (Kb) 27272

[startup+540.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 53931 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 539.67
Current children cumulated vsize (Kb) 27272

[startup+550.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 54930 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217392 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 549.66
Current children cumulated vsize (Kb) 27272

[startup+560.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 55930 34 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217164 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 559.66
Current children cumulated vsize (Kb) 27272

[startup+570.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 56930 35 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217708 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 569.67
Current children cumulated vsize (Kb) 27272

[startup+580.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 57930 35 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217024 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 579.67
Current children cumulated vsize (Kb) 27272

[startup+590.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 58931 35 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216976 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 589.68
Current children cumulated vsize (Kb) 27272

[startup+600.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 59930 35 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217136 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 599.67
Current children cumulated vsize (Kb) 27272

[startup+610.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 60930 36 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217740 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 609.68
Current children cumulated vsize (Kb) 27272

[startup+620.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 61929 37 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216780 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 619.68
Current children cumulated vsize (Kb) 27272

[startup+630.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 62929 37 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217148 134718176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 629.68
Current children cumulated vsize (Kb) 27272

[startup+640.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 63929 37 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217168 134696618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 639.68
Current children cumulated vsize (Kb) 27272

[startup+650.063 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 64929 37 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216652 134723206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 649.68
Current children cumulated vsize (Kb) 27272

[startup+660.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 65928 38 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217136 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 659.68
Current children cumulated vsize (Kb) 27272

[startup+670.065 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 66927 38 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217248 134629224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 669.67
Current children cumulated vsize (Kb) 27272

[startup+680.065 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 67926 38 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217056 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 679.66
Current children cumulated vsize (Kb) 27272

[startup+690.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 68925 38 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 689.65
Current children cumulated vsize (Kb) 27272

[startup+700.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 69925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217884 134722231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 699.66
Current children cumulated vsize (Kb) 27272

[startup+710.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 70925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217744 134694489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 709.66
Current children cumulated vsize (Kb) 27272

[startup+720.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 71925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 719.66
Current children cumulated vsize (Kb) 27272

[startup+730.071 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 72925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216788 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 729.66
Current children cumulated vsize (Kb) 27272

[startup+740.071 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 73925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217196 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 739.66
Current children cumulated vsize (Kb) 27272

[startup+750.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 74925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134696697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 749.66
Current children cumulated vsize (Kb) 27272

[startup+760.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 75925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217212 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 759.66
Current children cumulated vsize (Kb) 27272

[startup+770.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 76925 39 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216704 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 769.66
Current children cumulated vsize (Kb) 27272

[startup+780.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 77924 40 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221218016 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 779.66
Current children cumulated vsize (Kb) 27272

[startup+790.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 78924 40 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 789.66
Current children cumulated vsize (Kb) 27272

[startup+800.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 79923 40 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217344 134849102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 799.65
Current children cumulated vsize (Kb) 27272

[startup+810.076 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 80923 40 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217204 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 809.65
Current children cumulated vsize (Kb) 27272

[startup+820.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 81923 41 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221218032 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 819.66
Current children cumulated vsize (Kb) 27272

[startup+830.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 82923 41 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217920 134694524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 829.66
Current children cumulated vsize (Kb) 27272

[startup+840.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 83923 41 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216976 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 839.66
Current children cumulated vsize (Kb) 27272

[startup+850.081 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 84923 41 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217160 134693621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 849.66
Current children cumulated vsize (Kb) 27272

[startup+860.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 85923 41 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217244 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 859.66
Current children cumulated vsize (Kb) 27272

[startup+870.081 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 86923 41 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217392 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 869.66
Current children cumulated vsize (Kb) 27272

[startup+880.083 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 87923 42 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217744 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 879.67
Current children cumulated vsize (Kb) 27272

[startup+890.084 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 88922 42 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217248 134629290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 889.66
Current children cumulated vsize (Kb) 27272

[startup+900.085 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 89922 42 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216976 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 899.66
Current children cumulated vsize (Kb) 27272

[startup+910.086 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 90922 42 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216992 134723225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 909.66
Current children cumulated vsize (Kb) 27272

[startup+920.087 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 91922 43 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216752 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 919.67
Current children cumulated vsize (Kb) 27272

[startup+930.087 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 92922 43 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217404 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 929.67
Current children cumulated vsize (Kb) 27272

[startup+940.088 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 93922 43 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217600 134629231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 939.67
Current children cumulated vsize (Kb) 27272

[startup+950.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 94921 44 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 949.67
Current children cumulated vsize (Kb) 27272

[startup+960.091 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 95921 44 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217592 134694458 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 959.67
Current children cumulated vsize (Kb) 27272

[startup+970.092 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 96921 44 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217588 134522359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 969.67
Current children cumulated vsize (Kb) 27272

[startup+980.094 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 97921 44 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216688 134849096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 979.67
Current children cumulated vsize (Kb) 27272

[startup+990.094 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 98921 44 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217568 134694532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 989.67
Current children cumulated vsize (Kb) 27272

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 99921 44 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217744 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 999.67
Current children cumulated vsize (Kb) 27272

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 100921 45 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217072 134629275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1009.68
Current children cumulated vsize (Kb) 27272

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 101921 45 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216812 134723267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1019.68
Current children cumulated vsize (Kb) 27272

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 102921 45 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217076 134630745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1029.68
Current children cumulated vsize (Kb) 27272

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 103921 45 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217840 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1039.68
Current children cumulated vsize (Kb) 27272

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 104920 45 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217504 134844860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1049.67
Current children cumulated vsize (Kb) 27272

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 105920 46 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217504 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1059.68
Current children cumulated vsize (Kb) 27272

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 106920 46 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217744 134694504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1069.68
Current children cumulated vsize (Kb) 27272

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 107920 46 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217072 134629373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1079.68
Current children cumulated vsize (Kb) 27272

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 108920 46 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1089.68
Current children cumulated vsize (Kb) 27272

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 109920 46 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217136 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1099.68
Current children cumulated vsize (Kb) 27272

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 110920 47 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217596 134696560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1109.69
Current children cumulated vsize (Kb) 27272

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 111920 47 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221216656 134720484 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1119.69
Current children cumulated vsize (Kb) 27272

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 112920 47 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1129.69
Current children cumulated vsize (Kb) 27272

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 113920 47 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217840 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1139.69
Current children cumulated vsize (Kb) 27272

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 114920 48 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217600 134629236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1149.7
Current children cumulated vsize (Kb) 27272

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 115919 48 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217724 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1159.69
Current children cumulated vsize (Kb) 27272

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 116919 48 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217896 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1169.69
Current children cumulated vsize (Kb) 27272

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 117919 48 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217136 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1179.69
Current children cumulated vsize (Kb) 27272

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 118919 48 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134693792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1189.69
Current children cumulated vsize (Kb) 27272

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 119919 48 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217404 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1199.69
Current children cumulated vsize (Kb) 27272

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 120919 49 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217568 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1209.7
Current children cumulated vsize (Kb) 27272



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 3666
Raw data (/proc/3661/stat): 3661 (minisat+_script) S 3660 3661 31915 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1796935910 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3661/statm): 532 234 485 147 0 385 0
[pid=3661] vsize: 2128
Raw data (/proc/3666/stat): 3666 (minisat+_bignum) R 3661 3661 31915 0 -1 0 6552 0 0 0 120919 49 0 0 25 0 1 0 1796935916 25747456 5699 4294967295 134512640 135167914 3221224448 3221217520 134696653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3666/statm): 6286 5699 162 162 0 6124 0
[pid=3666] vsize: 25144
Current children cumulated CPU time (s) 1209.7
Current children cumulated vsize (Kb) 27272

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.7
CPU user time (s): 1209.2
CPU system time (s): 0.505923
CPU usage (%): 99.9643
Max. virtual memory (cumulated for all children) (Kb): 27272

Verifier Data

ERROR: no interpretation found !