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/miplib3/normalized-mps-v2-13-7-bell5.opb
MD5SUMde15576cff54b253255390d90c832bf8
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 benchmark1238.69
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 6181

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        838064 kB
Buffers:         38528 kB
Cached:         126488 kB
SwapCached:        768 kB
Active:          31764 kB
Inactive:       135824 kB
HighTotal:      131008 kB
HighFree:        36148 kB
LowTotal:       903652 kB
LowFree:        801916 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            23396 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:30:36 (client local time) WITH STATUS 10 IN 1200 SECONDS
stats: 3346 7 1200 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/5324/stat): 5324 (minisat+_script) R 5323 5324 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855540443 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5324/statm): 174 3 169 147 0 27 0
[pid=5324] 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=5325
New process pid=5326
New process pid=5327
One traced child (pid=5326) exited with status: 0
execve syscall for /bin/sed executable
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=5327) exited with status: 0
One traced child (pid=5325) exited with status: 0
New process pid=5328
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-bell5.opb
One traced child (pid=5328) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=5329
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-bell5.opb

[startup+10.0041 s]
Raw data (loadavg): 0.89 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 601 0 0 0 990 1 0 0 25 0 1 0 1855540450 2584576 510 4294967295 134512640 135167914 3221224448 3221222016 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 631 510 162 162 0 469 0
[pid=5329] vsize: 2524
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 4652

[startup+20.0049 s]
Raw data (loadavg): 0.90 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 679 0 0 0 1990 1 0 0 25 0 1 0 1855540450 3182592 588 4294967295 134512640 135167914 3221224448 3221222272 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 777 588 162 162 0 615 0
[pid=5329] vsize: 3108
Current children cumulated CPU time (s) 19.93
Current children cumulated vsize (Kb) 5236

[startup+30.0047 s]
Raw data (loadavg): 0.92 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 924 0 0 0 2989 2 0 0 25 0 1 0 1855540450 3727360 750 4294967295 134512640 135167914 3221224448 3221221456 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5329/statm): 910 750 162 162 0 748 0
[pid=5329] vsize: 3640
Current children cumulated CPU time (s) 29.93
Current children cumulated vsize (Kb) 5768

[startup+40.0055 s]
Raw data (loadavg): 0.93 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 4867 0 0 0 3962 16 0 0 25 0 1 0 1855540450 20676608 4592 4294967295 134512640 135167914 3221224448 3221045832 134694369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 5048 4592 162 162 0 4886 0
[pid=5329] vsize: 20192
Current children cumulated CPU time (s) 39.8
Current children cumulated vsize (Kb) 22320

[startup+50.0063 s]
Raw data (loadavg): 0.94 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 4945 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216336 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 27272

[startup+60.0071 s]
Raw data (loadavg): 0.95 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 5945 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216864 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 27272

[startup+70.0079 s]
Raw data (loadavg): 0.96 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 6945 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216624 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 69.7
Current children cumulated vsize (Kb) 27272

[startup+80.0086 s]
Raw data (loadavg): 0.96 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 7946 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216720 134630738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 27272

[startup+90.0094 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 8946 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216700 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 89.71
Current children cumulated vsize (Kb) 27272

[startup+100.01 s]
Raw data (loadavg): 1.05 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 9946 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217020 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 99.71
Current children cumulated vsize (Kb) 27272

[startup+110.012 s]
Raw data (loadavg): 1.04 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 10946 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 109.71
Current children cumulated vsize (Kb) 27272

[startup+120.013 s]
Raw data (loadavg): 1.04 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 11947 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216860 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 119.72
Current children cumulated vsize (Kb) 27272

[startup+130.014 s]
Raw data (loadavg): 1.03 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 12947 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216884 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 129.72
Current children cumulated vsize (Kb) 27272

[startup+140.014 s]
Raw data (loadavg): 1.03 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 13947 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217136 134718501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 139.72
Current children cumulated vsize (Kb) 27272

[startup+150.015 s]
Raw data (loadavg): 1.02 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 14947 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216704 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 149.72
Current children cumulated vsize (Kb) 27272

[startup+160.016 s]
Raw data (loadavg): 1.02 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 15948 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216460 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 159.73
Current children cumulated vsize (Kb) 27272

[startup+170.017 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 16948 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216752 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 169.73
Current children cumulated vsize (Kb) 27272

[startup+180.017 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 17948 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217236 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 179.73
Current children cumulated vsize (Kb) 27272

[startup+190.018 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 18948 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217064 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 189.73
Current children cumulated vsize (Kb) 27272

[startup+200.018 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 19949 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216816 134696264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 199.74
Current children cumulated vsize (Kb) 27272

[startup+210.019 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 20949 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216904 134628659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 209.74
Current children cumulated vsize (Kb) 27272

[startup+220.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 21949 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217052 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 219.74
Current children cumulated vsize (Kb) 27272

[startup+230.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 22949 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217012 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 229.74
Current children cumulated vsize (Kb) 27272

[startup+240.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 23950 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216828 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 239.75
Current children cumulated vsize (Kb) 27272

[startup+250.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 24950 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 249.75
Current children cumulated vsize (Kb) 27272

[startup+260.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 25950 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216640 134696194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 259.75
Current children cumulated vsize (Kb) 27272

[startup+270.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 26950 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 269.75
Current children cumulated vsize (Kb) 27272

[startup+280.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 27951 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 279.76
Current children cumulated vsize (Kb) 27272

[startup+290.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 28951 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216668 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 289.76
Current children cumulated vsize (Kb) 27272

[startup+300.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 29951 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217664 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 299.76
Current children cumulated vsize (Kb) 27272

[startup+310.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 30951 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217328 134696710 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 309.76
Current children cumulated vsize (Kb) 27272

[startup+320.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 31952 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216860 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 319.77
Current children cumulated vsize (Kb) 27272

[startup+330.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 32952 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217408 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 329.77
Current children cumulated vsize (Kb) 27272

[startup+340.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 33952 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217160 134693693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 339.77
Current children cumulated vsize (Kb) 27272

[startup+350.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 34952 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217016 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 349.77
Current children cumulated vsize (Kb) 27272

[startup+360.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 35953 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217184 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 359.78
Current children cumulated vsize (Kb) 27272

[startup+370.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 36953 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217264 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 369.78
Current children cumulated vsize (Kb) 27272

[startup+380.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 37953 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 379.78
Current children cumulated vsize (Kb) 27272

[startup+390.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 38953 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217232 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 389.78
Current children cumulated vsize (Kb) 27272

[startup+400.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 39954 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216784 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 399.79
Current children cumulated vsize (Kb) 27272

[startup+410.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 40954 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217424 134630835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 409.79
Current children cumulated vsize (Kb) 27272

[startup+420.036 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 41954 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217328 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 419.79
Current children cumulated vsize (Kb) 27272

[startup+430.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 42954 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217708 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 429.79
Current children cumulated vsize (Kb) 27272

[startup+440.038 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 43955 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 439.8
Current children cumulated vsize (Kb) 27272

[startup+450.039 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 44955 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216832 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 449.8
Current children cumulated vsize (Kb) 27272

[startup+460.039 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 45955 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216560 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 459.8
Current children cumulated vsize (Kb) 27272

[startup+470.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 46955 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216988 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 469.8
Current children cumulated vsize (Kb) 27272

[startup+480.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 47956 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217856 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 479.81
Current children cumulated vsize (Kb) 27272

[startup+490.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 48956 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217196 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 489.81
Current children cumulated vsize (Kb) 27272

[startup+500.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 49956 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217180 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 499.81
Current children cumulated vsize (Kb) 27272

[startup+510.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 50956 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217364 134522496 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 509.81
Current children cumulated vsize (Kb) 27272

[startup+520.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 51957 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217520 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 519.82
Current children cumulated vsize (Kb) 27272

[startup+530.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 52957 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216672 134522341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 529.82
Current children cumulated vsize (Kb) 27272

[startup+540.046 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 53957 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217132 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 539.82
Current children cumulated vsize (Kb) 27272

[startup+550.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 54957 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217072 134629259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 549.82
Current children cumulated vsize (Kb) 27272

[startup+560.047 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 55958 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217164 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 559.83
Current children cumulated vsize (Kb) 27272

[startup+570.048 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 56958 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217856 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 569.83
Current children cumulated vsize (Kb) 27272

[startup+580.049 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 57958 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217360 134720503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 579.83
Current children cumulated vsize (Kb) 27272

[startup+590.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 58958 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217216 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 589.83
Current children cumulated vsize (Kb) 27272

[startup+600.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 59959 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216832 134718199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 599.84
Current children cumulated vsize (Kb) 27272

[startup+610.052 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 60959 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 609.84
Current children cumulated vsize (Kb) 27272

[startup+620.053 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 61959 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217344 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 619.84
Current children cumulated vsize (Kb) 27272

[startup+630.054 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 62959 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217056 134694351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 629.84
Current children cumulated vsize (Kb) 27272

[startup+640.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 63960 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217372 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 639.85
Current children cumulated vsize (Kb) 27272

[startup+650.055 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 64960 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 649.85
Current children cumulated vsize (Kb) 27272

[startup+660.056 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 65960 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216976 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 659.85
Current children cumulated vsize (Kb) 27272

[startup+670.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 66960 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217760 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 669.85
Current children cumulated vsize (Kb) 27272

[startup+680.057 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 67961 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217328 134696386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 679.86
Current children cumulated vsize (Kb) 27272

[startup+690.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 68961 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217232 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 689.86
Current children cumulated vsize (Kb) 27272

[startup+700.058 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 69961 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134696316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 699.86
Current children cumulated vsize (Kb) 27272

[startup+710.059 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 70961 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216864 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 709.86
Current children cumulated vsize (Kb) 27272

[startup+720.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 71962 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217420 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 719.87
Current children cumulated vsize (Kb) 27272

[startup+730.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 72962 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217760 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 729.87
Current children cumulated vsize (Kb) 27272

[startup+740.06 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 73962 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217180 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 739.87
Current children cumulated vsize (Kb) 27272

[startup+750.061 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 74964 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217076 134629364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 749.89
Current children cumulated vsize (Kb) 27272

[startup+760.075 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 75964 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216656 134718188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 759.89
Current children cumulated vsize (Kb) 27272

[startup+770.076 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 76964 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216836 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 769.89
Current children cumulated vsize (Kb) 27272

[startup+780.077 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 77964 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134843081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 779.89
Current children cumulated vsize (Kb) 27272

[startup+790.077 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 78964 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216864 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 789.89
Current children cumulated vsize (Kb) 27272

[startup+800.077 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 79965 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 799.9
Current children cumulated vsize (Kb) 27272

[startup+810.079 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 80965 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217216 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 809.9
Current children cumulated vsize (Kb) 27272

[startup+820.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 81965 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221218008 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 819.9
Current children cumulated vsize (Kb) 27272

[startup+830.079 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 82965 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217040 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 829.9
Current children cumulated vsize (Kb) 27272

[startup+840.08 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 83966 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216636 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 839.91
Current children cumulated vsize (Kb) 27272

[startup+850.081 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 84966 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217340 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 849.91
Current children cumulated vsize (Kb) 27272

[startup+860.082 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 85966 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217596 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 859.91
Current children cumulated vsize (Kb) 27272

[startup+870.083 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 86966 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217216 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 869.91
Current children cumulated vsize (Kb) 27272

[startup+880.083 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 87967 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217184 134718203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 879.92
Current children cumulated vsize (Kb) 27272

[startup+890.084 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 88967 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216624 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 889.92
Current children cumulated vsize (Kb) 27272

[startup+900.085 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 89967 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217708 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 899.92
Current children cumulated vsize (Kb) 27272

[startup+910.087 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 90967 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217232 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 909.92
Current children cumulated vsize (Kb) 27272

[startup+920.087 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 91968 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216716 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 919.93
Current children cumulated vsize (Kb) 27272

[startup+930.088 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 92968 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217292 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 929.93
Current children cumulated vsize (Kb) 27272

[startup+940.089 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 93968 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217388 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 939.93
Current children cumulated vsize (Kb) 27272

[startup+950.09 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 94968 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216836 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 949.93
Current children cumulated vsize (Kb) 27272

[startup+960.091 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 95969 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217568 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 959.94
Current children cumulated vsize (Kb) 27272

[startup+970.091 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 96969 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217068 134696788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 969.94
Current children cumulated vsize (Kb) 27272

[startup+980.092 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 97969 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217680 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 979.94
Current children cumulated vsize (Kb) 27272

[startup+990.093 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 98969 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217872 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 989.94
Current children cumulated vsize (Kb) 27272

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 99970 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217852 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 999.95
Current children cumulated vsize (Kb) 27272

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 100970 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217376 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1009.95
Current children cumulated vsize (Kb) 27272

[startup+1020.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 101970 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217224 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1019.95
Current children cumulated vsize (Kb) 27272

[startup+1030.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 102970 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217392 134694386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1029.95
Current children cumulated vsize (Kb) 27272

[startup+1040.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 103971 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1039.96
Current children cumulated vsize (Kb) 27272

[startup+1050.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 104971 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216896 134628649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1049.96
Current children cumulated vsize (Kb) 27272

[startup+1060.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 105971 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221216800 134696342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1059.96
Current children cumulated vsize (Kb) 27272

[startup+1070.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 106971 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217076 134629209 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1069.96
Current children cumulated vsize (Kb) 27272

[startup+1080.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 107972 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217152 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1079.97
Current children cumulated vsize (Kb) 27272

[startup+1090.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 108972 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217328 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1089.97
Current children cumulated vsize (Kb) 27272

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 109972 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217380 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1099.97
Current children cumulated vsize (Kb) 27272

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 110972 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217316 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1109.97
Current children cumulated vsize (Kb) 27272

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 111973 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217312 134718501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1119.98
Current children cumulated vsize (Kb) 27272

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 112973 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217408 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1129.98
Current children cumulated vsize (Kb) 27272

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 113973 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217164 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1139.98
Current children cumulated vsize (Kb) 27272

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 114973 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217584 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1149.98
Current children cumulated vsize (Kb) 27272

[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 115974 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217884 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1159.99
Current children cumulated vsize (Kb) 27272

[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 116974 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221218220 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1169.99
Current children cumulated vsize (Kb) 27272

[startup+1180.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 117974 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217504 134696353 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1179.99
Current children cumulated vsize (Kb) 27272

[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 118974 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217344 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1189.99
Current children cumulated vsize (Kb) 27272

[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 119975 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217088 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1200
Current children cumulated vsize (Kb) 27272



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 5329
Raw data (/proc/5324/stat): 5324 (minisat+_script) S 5323 5324 19818 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1855540443 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5324/statm): 532 234 485 147 0 385 0
[pid=5324] vsize: 2128
Raw data (/proc/5329/stat): 5329 (minisat+_bignum) R 5324 5324 19818 0 -1 0 6552 0 0 0 119975 23 0 0 25 0 1 0 1855540450 25747456 5699 4294967295 134512640 135167914 3221224448 3221217216 134849099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5329/statm): 6286 5699 162 162 0 6124 0
[pid=5329] vsize: 25144
Current children cumulated CPU time (s) 1200
Current children cumulated vsize (Kb) 27272

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

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200
CPU user time (s): 1199.75
CPU system time (s): 0.244962
CPU usage (%): 99.9892
Max. virtual memory (cumulated for all children) (Kb): 27272

Verifier Data

ERROR: no interpretation found !