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

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb56-25-opb/normalized-frb56-25-1.opb
MD5SUM02058527b1ad27d5be75faa6974ffa0f
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -41
Optimality of the best value was proved NO
Number of terms in the objective function 1400
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1400
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1400
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1204.33
Number of variables1400
Total number of constraints109676
Number of constraints which are clauses109676
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 2313

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-18 18:53:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2715 boxname=wulflinc31 idbench=371 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  02058527b1ad27d5be75faa6974ffa0f  /oldhome/oroussel/tmp/wulflinc31/normalized-frb56-25-1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-frb56-25-1.opb
IDLAUNCH: 2715
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        688072 kB
Buffers:         35972 kB
Cached:         279552 kB
SwapCached:       1016 kB
Active:         108116 kB
Inactive:       210172 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        687820 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            22628 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:13:17 (client local time) WITH STATUS 10 IN 1207.11 SECONDS
stats: 2715 7 1207.11 10

Solver Data

c Parsing PB file...
c Converting 109676 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  109676   219352 |   36558       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -39
c ---[   0]---> Sorter-cost:78076     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  193374   415660 |   64458       0        0     nan |  0.000 % |
c |       100 |  192719   414299 |   70903      63     1093    17.3 |  0.622 % |
c |       250 |  192264   413332 |   77994     193     3275    17.0 |  1.071 % |
c |       476 |  191415   411505 |   85793     346     4129    11.9 |  1.930 % |
c |       813 |  188955   406147 |   94372     570     6726    11.8 |  4.475 % |
c |      1319 |  186406   400564 |  103810     962    13044    13.6 |  7.139 % |
c |      2078 |  180912   388275 |  114191    1479    18824    12.7 | 13.094 % |
c |      3217 |  175709   376585 |  125610    2357    32192    13.7 | 18.778 % |
c |      4925 |  166673   356010 |  138171    3574    49702    13.9 | 28.824 % |
c |      7487 |  157658   335240 |  151988    5415    74543    13.8 | 39.079 % |
c |     11331 |  143138   301148 |  167187    7961   113671    14.3 | 55.865 % |
c ==============================================================================
c Found solution: -43
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12525 |  140763   295746 |   46921    8929   130833    14.7 | 55.865 % |
c |     12625 |  139918   293726 |   51613    8922   130380    14.6 | 59.751 % |
c |     12775 |  139671   293133 |   56774    9032   131953    14.6 | 60.052 % |
c |     13000 |  139283   292232 |   62451    9203   135203    14.7 | 60.501 % |
c |     13337 |  138691   290861 |   68697    9414   138503    14.7 | 61.171 % |
c |     13843 |  138328   290009 |   75566    9866   147954    15.0 | 61.597 % |
c |     14602 |  137121   287145 |   83123   10409   155824    15.0 | 63.131 % |
c |     15741 |  135695   283700 |   91435   11210   169938    15.2 | 64.772 % |
c |     17449 |  133720   279037 |  100579   12512   198089    15.8 | 67.074 % |
c |     20011 |  128643   266845 |  110637   13856   224025    16.2 | 73.177 % |
c |     23856 |  125354   258987 |  121700   16543   306442    18.5 | 77.142 % |
c |     29622 |  122874   253024 |  133871   20367   492068    24.2 | 80.137 % |
c ==============================================================================
c Found solution: -44
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30967 |  122645   252423 |   40881   21516   531155    24.7 | 80.137 % |
c |     31067 |  122645   252423 |   44969   21616   531997    24.6 | 80.427 % |
c |     31217 |  122636   252402 |   49466   21757   536269    24.6 | 80.437 % |
c |     31442 |  122593   252300 |   54412   21951   542487    24.7 | 80.488 % |
c |     31779 |  122436   251912 |   59853   22120   548490    24.8 | 80.684 % |
c |     32285 |  122436   251912 |   65839   22626   572074    25.3 | 80.684 % |
c |     33044 |  122390   251788 |   72423   23361   600618    25.7 | 80.751 % |
c |     34183 |  122320   251616 |   79665   24453   657839    26.9 | 80.840 % |
c |     35892 |  122035   250934 |   87632   26003   710446    27.3 | 81.185 % |
c |     38454 |  121806   250367 |   96395   28222   984902    34.9 | 81.476 % |
c ==============================================================================
c Found solution: -45
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38938 |  121634   249984 |   40544   28578  1022037    35.8 | 81.476 % |
c |     39038 |  121617   249941 |   44598   28653  1023964    35.7 | 81.716 % |
c |     39188 |  121349   249292 |   49058   28508  1022934    35.9 | 82.043 % |
c |     39413 |  121349   249292 |   53964   28733  1031080    35.9 | 82.043 % |
c |     39750 |  121213   248952 |   59360   29014  1043187    36.0 | 82.215 % |
c |     40256 |  121088   248654 |   65296   29472  1065725    36.2 | 82.365 % |
c |     41015 |  121034   248515 |   71826   30083  1084053    36.0 | 82.437 % |
c |     42154 |  120996   248419 |   79008   31210  1134841    36.4 | 82.488 % |
c |     43862 |  120814   247954 |   86909   32806  1219139    37.2 | 82.733 % |
c |     46425 |  120660   247566 |   95600   35272  1481711    42.0 | 82.934 % |
c |     50269 |  120426   247002 |  105160   38769  1679322    43.3 | 83.221 % |
c ==============================================================================
c Found solution: -46
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55508 |  120404   246861 |   40134   43705  2184532    50.0 | 83.221 % |
c |     55608 |  120404   246861 |   44147   43805  2187268    49.9 | 83.253 % |
c |     55759 |  120401   246854 |   48562   43919  2198441    50.1 | 83.257 % |
c |     55984 |  120297   246612 |   53418   44129  2204023    49.9 | 83.377 % |
c |     56322 |  120297   246612 |   58760   44467  2221646    50.0 | 83.377 % |
c |     56828 |  120262   246523 |   64636   44943  2244896    49.9 | 83.425 % |
c |     57588 |  120262   246523 |   71099   45703  2321279    50.8 | 83.425 % |
c |     58727 |  120173   246296 |   78209   45708  2347180    51.4 | 83.542 % |
c |     60435 |  120173   246296 |   86030   47416  2483476    52.4 | 83.542 % |
c |     62998 |  119939   245717 |   94633   49359  2778436    56.3 | 83.841 % |
c ==============================================================================
c Found solution: -47
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65455 |  119986   245861 |   39995   51816  3103184    59.9 | 83.841 % |
c |     65555 |  119986   245861 |   43994   51916  3106425    59.8 | 83.823 % |
c |     65705 |  119842   245523 |   48393   51870  3106898    59.9 | 83.990 % |
c |     65931 |  119801   245428 |   53233   52001  3128578    60.2 | 84.037 % |
c |     66268 |  119776   245371 |   58556   52307  3156736    60.4 | 84.064 % |
c |     66774 |  119755   245323 |   64412   52795  3188273    60.4 | 84.086 % |
c |     67533 |  119752   245316 |   70853   53553  3227607    60.3 | 84.090 % |
c |     68672 |  119752   245316 |   77938   54692  3351972    61.3 | 84.090 % |
c |     70380 |  119623   244995 |   85732   55978  3468009    62.0 | 84.254 % |
c |     72942 |  119551   244815 |   94306   58246  3772441    64.8 | 84.346 % |
c |     76786 |  119544   244798 |  103736   62089  4097900    66.0 | 84.355 % |
c |     82552 |  119337   244296 |  114110   67497  4883125    72.3 | 84.607 % |
c ==============================================================================
c Found solution: -48
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91183 |  119326   244244 |   39775   75532  5875208    77.8 | 84.607 % |
c |     91283 |  119326   244244 |   43752   75632  5876836    77.7 | 84.623 % |
c |     91433 |  119326   244244 |   48127   75782  5886804    77.7 | 84.623 % |
c |     91658 |  119174   243872 |   52940   75571  5878542    77.8 | 84.815 % |
c |     91995 |  119169   243861 |   58234   75798  5913726    78.0 | 84.820 % |
c |     92501 |  119169   243861 |   64058   76304  5962450    78.1 | 84.820 % |
c |     93260 |  119169   243861 |   70463   77063  6047017    78.5 | 84.820 % |
c |     94399 |  119169   243861 |   77510   78202  6141731    78.5 | 84.820 % |
c |     96107 |  119164   243850 |   85261   79903  6346087    79.4 | 84.825 % |
c |     98670 |  119164   243850 |   93787   82466  6693670    81.2 | 84.825 % |
c |    102515 |  119130   243772 |  103166   86111  7282535    84.6 | 84.864 % |
c |    108281 |  119010   243470 |  113482   91427  8357465    91.4 | 85.016 % |
c |    116930 |  118952   243328 |  124830  100035  9709566    97.1 | 85.089 % |
c |    129904 |  118839   243050 |  137314  112031 11367601   101.5 | 85.232 % |
c ==============================================================================
c Found solution: -49
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142656 |  118861   243115 |   39620  124783 13424185   107.6 | 85.232 % |
c |    142756 |  118809   242989 |   43582   22640  2136428    94.4 | 85.280 % |
c |    142906 |  118809   242989 |   47940   22790  2140780    93.9 | 85.280 % |
c |    143131 |  118741   242820 |   52734   22993  2162172    94.0 | 85.368 % |
c |    143468 |  118741   242820 |   58007   23330  2174648    93.2 | 85.368 % |
c |    143974 |  118733   242802 |   63808   23832  2203863    92.5 | 85.376 % |
c |    144733 |  118722   242773 |   70189   24588  2263679    92.1 | 85.392 % |
c |    145872 |  118722   242773 |   77208   25727  2328778    90.5 | 85.392 % |
c |    147580 |  118596   242466 |   84928   27418  2490341    90.8 | 85.549 % |
c |    150144 |  118596   242466 |   93421   29982  2825667    94.2 | 85.549 % |
c |    153988 |  118581   242431 |  102764   33809  3133516    92.7 | 85.567 % |
c |    159757 |  118486   242200 |  113040   39498  3825619    96.9 | 85.685 % |
c |    168406 |  118465   242145 |  124344   48141  5116869   106.3 | 85.715 % |
c |    181380 |  118409   242007 |  136778   61109  6776970   110.9 | 85.787 % |
c |    200842 |  118409   242007 |  150456   80571  9946562   123.5 | 85.787 % |
c |    230034 |  118372   241919 |  165502  109697 15616229   142.4 | 85.830 % |
c |    273823 |  118197   241494 |  182052  153345 23390472   152.5 | 86.048 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 -C1383 C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 C827 -C826 -C825 -C824 C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 C102 -C

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/16974/stat): 16974 (minisat+_script) R 16973 16974 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843524583 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16974/statm): 174 3 169 147 0 27 0
[pid=16974] 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=16975
New process pid=16976
New process pid=16977
One traced child (pid=16976) 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=16977) exited with status: 0
One traced child (pid=16975) exited with status: 0
New process pid=16978
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-frb56-25-1.opb

[startup+10.0045 s]
Raw data (loadavg): 0.93 0.96 0.97 2/58 16978
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 945 28 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223152 134559005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 30132

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.96 0.97 2/58 16980
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 1944 29 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 30132

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.96 0.97 2/58 16980
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 2944 29 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 30132

[startup+40.0073 s]
Raw data (loadavg): 0.96 0.96 0.97 2/58 16980
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 3943 29 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 30132

[startup+50.0082 s]
Raw data (loadavg): 0.96 0.96 0.97 2/58 16980
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 4943 30 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 30132

[startup+60.0091 s]
Raw data (loadavg): 0.97 0.96 0.97 2/58 16980
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 5942 30 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223132 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 30132

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.96 0.97 2/58 16980
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 6941 31 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223120 134553437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 30132

[startup+80.011 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 16982
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 7941 31 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 79.72
Current children cumulated vsize (Kb) 30132

[startup+90.0119 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 16982
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 8941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 30132

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 16982
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 9941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223116 134553438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 30132

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.97 2/58 16982
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 10941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 30132

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16982
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 11941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 30132

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16982
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 12941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 30132

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16984
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 13941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 139.73
Current children cumulated vsize (Kb) 30132

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16984
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 14941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0
[pid=16978] vsize: 28008
Current children cumulated CPU time (s) 149.73
Current children cumulated vsize (Kb) 30132

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16984
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 7092 0 0 0 15938 34 0 0 25 0 1 0 1843524588 29339648 7004 4294967295 134512640 135094434 3221224448 3221223104 134670074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7163 7004 145 145 0 7018 0
[pid=16978] vsize: 28652
Current children cumulated CPU time (s) 159.72
Current children cumulated vsize (Kb) 30776

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16984
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 7345 0 0 0 16933 35 0 0 25 0 1 0 1843524588 30375936 7257 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7416 7257 145 145 0 7271 0
[pid=16978] vsize: 29664
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 31788

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16984
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 7801 0 0 0 17928 37 0 0 25 0 1 0 1843524588 31936512 7638 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 7797 7638 145 145 0 7652 0
[pid=16978] vsize: 31188
Current children cumulated CPU time (s) 179.65
Current children cumulated vsize (Kb) 33312

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.97 1/58 16984
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) T 16974 16974 9102 0 -1 0 8219 0 0 0 18921 39 0 0 25 0 1 0 1843524588 33767424 8056 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16978/statm): 8244 8056 145 145 0 8099 0
[pid=16978] vsize: 32976
Current children cumulated CPU time (s) 189.6
Current children cumulated vsize (Kb) 35100

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16986
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 8592 0 0 0 19914 42 0 0 25 0 1 0 1843524588 35274752 8429 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 8612 8429 145 145 0 8467 0
[pid=16978] vsize: 34448
Current children cumulated CPU time (s) 199.56
Current children cumulated vsize (Kb) 36572

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16986
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 9140 0 0 0 20905 45 0 0 25 0 1 0 1843524588 37191680 8901 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 9080 8901 145 145 0 8935 0
[pid=16978] vsize: 36320
Current children cumulated CPU time (s) 209.5
Current children cumulated vsize (Kb) 38444

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16986
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 9436 0 0 0 21899 47 0 0 25 0 1 0 1843524588 38391808 9197 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 9373 9197 145 145 0 9228 0
[pid=16978] vsize: 37492
Current children cumulated CPU time (s) 219.46
Current children cumulated vsize (Kb) 39616

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16986
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 9864 0 0 0 22892 51 0 0 25 0 1 0 1843524588 40132608 9625 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 9798 9625 145 145 0 9653 0
[pid=16978] vsize: 39192
Current children cumulated CPU time (s) 229.43
Current children cumulated vsize (Kb) 41316

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16986
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 10278 0 0 0 23886 53 0 0 25 0 1 0 1843524588 41508864 9963 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 10134 9963 145 145 0 9989 0
[pid=16978] vsize: 40536
Current children cumulated CPU time (s) 239.39
Current children cumulated vsize (Kb) 42660

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16986
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 10594 0 0 0 24881 56 0 0 25 0 1 0 1843524588 42790912 10279 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 10447 10279 145 145 0 10302 0
[pid=16978] vsize: 41788
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 43912

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16988
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 11012 0 0 0 25873 61 0 0 25 0 1 0 1843524588 44490752 10697 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 10862 10697 145 145 0 10717 0
[pid=16978] vsize: 43448
Current children cumulated CPU time (s) 259.34
Current children cumulated vsize (Kb) 45572

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16988
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 11356 0 0 0 26866 64 0 0 25 0 1 0 1843524588 45883392 11041 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 11202 11041 145 145 0 11057 0
[pid=16978] vsize: 44808
Current children cumulated CPU time (s) 269.3
Current children cumulated vsize (Kb) 46932

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16988
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 11802 0 0 0 27858 67 0 0 25 0 1 0 1843524588 47960064 11487 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 11709 11487 145 145 0 11564 0
[pid=16978] vsize: 46836
Current children cumulated CPU time (s) 279.25
Current children cumulated vsize (Kb) 48960

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16988
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 12189 0 0 0 28849 71 0 0 25 0 1 0 1843524588 49537024 11874 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 12094 11874 145 145 0 11949 0
[pid=16978] vsize: 48376
Current children cumulated CPU time (s) 289.2
Current children cumulated vsize (Kb) 50500

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16988
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 12614 0 0 0 29841 74 0 0 25 0 1 0 1843524588 51265536 12299 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 12516 12299 145 145 0 12371 0
[pid=16978] vsize: 50064
Current children cumulated CPU time (s) 299.15
Current children cumulated vsize (Kb) 52188

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16988
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 13069 0 0 0 30833 78 0 0 25 0 1 0 1843524588 53112832 12754 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 12967 12754 145 145 0 12822 0
[pid=16978] vsize: 51868
Current children cumulated CPU time (s) 309.11
Current children cumulated vsize (Kb) 53992

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16990
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 13381 0 0 0 31826 82 0 0 25 0 1 0 1843524588 54079488 12991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 13203 12991 145 145 0 13058 0
[pid=16978] vsize: 52812
Current children cumulated CPU time (s) 319.08
Current children cumulated vsize (Kb) 54936

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16990
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 13698 0 0 0 32821 83 0 0 25 0 1 0 1843524588 55365632 13308 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 13517 13308 145 145 0 13372 0
[pid=16978] vsize: 54068
Current children cumulated CPU time (s) 329.04
Current children cumulated vsize (Kb) 56192

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16990
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 14120 0 0 0 33813 88 0 0 25 0 1 0 1843524588 57081856 13730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 13936 13730 145 145 0 13791 0
[pid=16978] vsize: 55744
Current children cumulated CPU time (s) 339.01
Current children cumulated vsize (Kb) 57868

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16990
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 14519 0 0 0 34806 90 0 0 25 0 1 0 1843524588 58707968 14129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 14333 14129 145 145 0 14188 0
[pid=16978] vsize: 57332
Current children cumulated CPU time (s) 348.96
Current children cumulated vsize (Kb) 59456

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16990
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 14919 0 0 0 35800 93 0 0 25 0 1 0 1843524588 60338176 14529 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 14731 14529 145 145 0 14586 0
[pid=16978] vsize: 58924
Current children cumulated CPU time (s) 358.93
Current children cumulated vsize (Kb) 61048

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16990
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 15396 0 0 0 36792 96 0 0 25 0 1 0 1843524588 62279680 15006 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 15205 15006 145 145 0 15060 0
[pid=16978] vsize: 60820
Current children cumulated CPU time (s) 368.88
Current children cumulated vsize (Kb) 62944

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16992
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 15912 0 0 0 37783 100 0 0 25 0 1 0 1843524588 64385024 15522 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 15719 15522 145 145 0 15574 0
[pid=16978] vsize: 62876
Current children cumulated CPU time (s) 378.83
Current children cumulated vsize (Kb) 65000

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16992
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 16250 0 0 0 38778 103 0 0 25 0 1 0 1843524588 65761280 15860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 16055 15860 145 145 0 15910 0
[pid=16978] vsize: 64220
Current children cumulated CPU time (s) 388.81
Current children cumulated vsize (Kb) 66344

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16992
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 16603 0 0 0 39772 105 0 0 25 0 1 0 1843524588 67198976 16213 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 16406 16213 145 145 0 16261 0
[pid=16978] vsize: 65624
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 67748

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16992
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 16980 0 0 0 40766 107 0 0 25 0 1 0 1843524588 68730880 16590 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 16780 16590 145 145 0 16635 0
[pid=16978] vsize: 67120
Current children cumulated CPU time (s) 408.73
Current children cumulated vsize (Kb) 69244

[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16992
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 17381 0 0 0 41758 110 0 0 25 0 1 0 1843524588 70365184 16991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 17179 16991 145 145 0 17034 0
[pid=16978] vsize: 68716
Current children cumulated CPU time (s) 418.68
Current children cumulated vsize (Kb) 70840

[startup+430.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16992
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 17839 0 0 0 42751 113 0 0 25 0 1 0 1843524588 72232960 17449 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 17635 17449 145 145 0 17490 0
[pid=16978] vsize: 70540
Current children cumulated CPU time (s) 428.64
Current children cumulated vsize (Kb) 72664

[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16994
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18162 0 0 0 43745 115 0 0 25 0 1 0 1843524588 73547776 17772 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 17956 17772 145 145 0 17811 0
[pid=16978] vsize: 71824
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 73948

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16994
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18386 0 0 0 44741 118 0 0 25 0 1 0 1843524588 74457088 17996 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 18178 17996 145 145 0 18033 0
[pid=16978] vsize: 72712
Current children cumulated CPU time (s) 448.59
Current children cumulated vsize (Kb) 74836

[startup+460.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16994
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18689 0 0 0 45737 119 0 0 25 0 1 0 1843524588 75694080 18299 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 18480 18299 145 145 0 18335 0
[pid=16978] vsize: 73920
Current children cumulated CPU time (s) 458.56
Current children cumulated vsize (Kb) 76044

[startup+470.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16994
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18965 0 0 0 46732 121 0 0 25 0 1 0 1843524588 76812288 18575 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 18753 18575 145 145 0 18608 0
[pid=16978] vsize: 75012
Current children cumulated CPU time (s) 468.53
Current children cumulated vsize (Kb) 77136

[startup+480.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16994
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 19288 0 0 0 47726 124 0 0 25 0 1 0 1843524588 78127104 18898 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 19074 18898 145 145 0 18929 0
[pid=16978] vsize: 76296
Current children cumulated CPU time (s) 478.5
Current children cumulated vsize (Kb) 78420

[startup+490.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16994
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 19598 0 0 0 48721 125 0 0 25 0 1 0 1843524588 79392768 19208 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 19383 19208 145 145 0 19238 0
[pid=16978] vsize: 77532
Current children cumulated CPU time (s) 488.46
Current children cumulated vsize (Kb) 79656

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16996
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 19987 0 0 0 49714 129 0 0 25 0 1 0 1843524588 80977920 19597 4294967295 134512640 135094434 3221224448 3221223088 134538541 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 19770 19597 145 145 0 19625 0
[pid=16978] vsize: 79080
Current children cumulated CPU time (s) 498.43
Current children cumulated vsize (Kb) 81204

[startup+510.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16996
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 20346 0 0 0 50707 131 0 0 25 0 1 0 1843524588 82440192 19956 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 20127 19956 145 145 0 19982 0
[pid=16978] vsize: 80508
Current children cumulated CPU time (s) 508.38
Current children cumulated vsize (Kb) 82632

[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16996
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 20645 0 0 0 51701 134 0 0 25 0 1 0 1843524588 83656704 20255 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 20424 20255 145 145 0 20279 0
[pid=16978] vsize: 81696
Current children cumulated CPU time (s) 518.35
Current children cumulated vsize (Kb) 83820

[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16996
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 20945 0 0 0 52695 136 0 0 25 0 1 0 1843524588 84881408 20555 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 20723 20555 145 145 0 20578 0
[pid=16978] vsize: 82892
Current children cumulated CPU time (s) 528.31
Current children cumulated vsize (Kb) 85016

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16996
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21204 0 0 0 53691 138 0 0 25 0 1 0 1843524588 85934080 20814 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 20980 20814 145 145 0 20835 0
[pid=16978] vsize: 83920
Current children cumulated CPU time (s) 538.29
Current children cumulated vsize (Kb) 86044

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16996
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 54689 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 548.28
Current children cumulated vsize (Kb) 86416

[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16998
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 55689 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 558.28
Current children cumulated vsize (Kb) 86416

[startup+570.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16998
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 56690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 568.29
Current children cumulated vsize (Kb) 86416

[startup+580.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16998
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 57690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 578.29
Current children cumulated vsize (Kb) 86416

[startup+590.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16998
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 58690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 588.29
Current children cumulated vsize (Kb) 86416

[startup+600.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16998
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 59690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 598.29
Current children cumulated vsize (Kb) 86416

[startup+610.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 16998
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 60690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 608.29
Current children cumulated vsize (Kb) 86416

[startup+620.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17000
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 61691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 618.3
Current children cumulated vsize (Kb) 86416

[startup+630.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17000
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 62691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 628.3
Current children cumulated vsize (Kb) 86416

[startup+640.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17000
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 63691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223040 134557435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 638.3
Current children cumulated vsize (Kb) 86416

[startup+650.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17000
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 64691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 648.3
Current children cumulated vsize (Kb) 86416

[startup+660.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17000
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 65691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 658.3
Current children cumulated vsize (Kb) 86416

[startup+670.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17000
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 66692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 668.31
Current children cumulated vsize (Kb) 86416

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17002
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 67692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 678.31
Current children cumulated vsize (Kb) 86416

[startup+690.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17002
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 68692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 688.31
Current children cumulated vsize (Kb) 86416

[startup+700.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17002
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 69692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 698.31
Current children cumulated vsize (Kb) 86416

[startup+710.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17002
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 70693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 708.32
Current children cumulated vsize (Kb) 86416

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17002
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 71693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 718.32
Current children cumulated vsize (Kb) 86416

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17002
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 72693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 728.32
Current children cumulated vsize (Kb) 86416

[startup+740.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17004
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 73693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 738.32
Current children cumulated vsize (Kb) 86416

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17004
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 74693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 748.32
Current children cumulated vsize (Kb) 86416

[startup+760.073 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17004
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 75694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 758.33
Current children cumulated vsize (Kb) 86416

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17004
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 76694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 768.33
Current children cumulated vsize (Kb) 86416

[startup+780.075 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17004
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 77694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 778.33
Current children cumulated vsize (Kb) 86416

[startup+790.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17004
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 78694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 788.33
Current children cumulated vsize (Kb) 86416

[startup+800.077 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17006
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 79694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0
[pid=16978] vsize: 84292
Current children cumulated CPU time (s) 798.33
Current children cumulated vsize (Kb) 86416

[startup+810.078 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17006
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21472 0 0 0 80693 140 0 0 25 0 1 0 1843524588 86724608 21007 4294967295 134512640 135094434 3221224448 3221223120 134555931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21173 21007 145 145 0 21028 0
[pid=16978] vsize: 84692
Current children cumulated CPU time (s) 808.33
Current children cumulated vsize (Kb) 86816

[startup+820.079 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17006
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21883 0 0 0 81685 144 0 0 25 0 1 0 1843524588 88408064 21418 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21584 21418 145 145 0 21439 0
[pid=16978] vsize: 86336
Current children cumulated CPU time (s) 818.29
Current children cumulated vsize (Kb) 88460

[startup+830.079 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17006
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 22256 0 0 0 82679 146 0 0 25 0 1 0 1843524588 89935872 21791 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 21957 21791 145 145 0 21812 0
[pid=16978] vsize: 87828
Current children cumulated CPU time (s) 828.25
Current children cumulated vsize (Kb) 89952

[startup+840.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17006
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 22627 0 0 0 83672 149 0 0 25 0 1 0 1843524588 91455488 22162 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 22328 22162 145 145 0 22183 0
[pid=16978] vsize: 89312
Current children cumulated CPU time (s) 838.21
Current children cumulated vsize (Kb) 91436

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17006
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 23015 0 0 0 84665 152 0 0 25 0 1 0 1843524588 93044736 22550 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 22716 22550 145 145 0 22571 0
[pid=16978] vsize: 90864
Current children cumulated CPU time (s) 848.17
Current children cumulated vsize (Kb) 92988

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17008
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 23399 0 0 0 85659 154 0 0 25 0 1 0 1843524588 94617600 22934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 23100 22934 145 145 0 22955 0
[pid=16978] vsize: 92400
Current children cumulated CPU time (s) 858.13
Current children cumulated vsize (Kb) 94524

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17008
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 23818 0 0 0 86652 157 0 0 25 0 1 0 1843524588 96337920 23353 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16978/statm): 23520 23353 145 145 0 23375 0
[pid=16978] vsize: 94080
Current children cumulated CPU time (s) 868.09
Current children cumulated vsize (Kb) 96204

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17008
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 24078 0 0 0 87646 159 0 0 25 0 1 0 1843524588 97411072 23613 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 23782 23613 145 145 0 23637 0
[pid=16978] vsize: 95128
Current children cumulated CPU time (s) 878.05
Current children cumulated vsize (Kb) 97252

[startup+890.085 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17008
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 24348 0 0 0 88642 161 0 0 25 0 1 0 1843524588 98516992 23883 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 24052 23883 145 145 0 23907 0
[pid=16978] vsize: 96208
Current children cumulated CPU time (s) 888.03
Current children cumulated vsize (Kb) 98332

[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17008
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 24712 0 0 0 89636 164 0 0 25 0 1 0 1843524588 100007936 24247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 24416 24247 145 145 0 24271 0
[pid=16978] vsize: 97664
Current children cumulated CPU time (s) 898
Current children cumulated vsize (Kb) 99788

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17008
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 25067 0 0 0 90629 167 0 0 25 0 1 0 1843524588 101462016 24602 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 24771 24602 145 145 0 24626 0
[pid=16978] vsize: 99084
Current children cumulated CPU time (s) 907.96
Current children cumulated vsize (Kb) 101208

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17010
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 25484 0 0 0 91621 170 0 0 25 0 1 0 1843524588 103170048 25019 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 25188 25019 145 145 0 25043 0
[pid=16978] vsize: 100752
Current children cumulated CPU time (s) 917.91
Current children cumulated vsize (Kb) 102876

[startup+930.088 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17010
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 25925 0 0 0 92613 173 0 0 25 0 1 0 1843524588 104976384 25460 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 25629 25460 145 145 0 25484 0
[pid=16978] vsize: 102516
Current children cumulated CPU time (s) 927.86
Current children cumulated vsize (Kb) 104640

[startup+940.089 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17010
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 26314 0 0 0 93606 176 0 0 25 0 1 0 1843524588 106569728 25849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 26018 25849 145 145 0 25873 0
[pid=16978] vsize: 104072
Current children cumulated CPU time (s) 937.82
Current children cumulated vsize (Kb) 106196

[startup+950.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17010
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 26691 0 0 0 94601 178 0 0 25 0 1 0 1843524588 108113920 26226 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 26395 26226 145 145 0 26250 0
[pid=16978] vsize: 105580
Current children cumulated CPU time (s) 947.79
Current children cumulated vsize (Kb) 107704

[startup+960.092 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17010
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 27124 0 0 0 95593 181 0 0 25 0 1 0 1843524588 109879296 26659 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 26826 26659 145 145 0 26681 0
[pid=16978] vsize: 107304
Current children cumulated CPU time (s) 957.74
Current children cumulated vsize (Kb) 109428

[startup+970.093 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17010
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 27464 0 0 0 96587 184 0 0 25 0 1 0 1843524588 111267840 26999 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 27165 26999 145 145 0 27020 0
[pid=16978] vsize: 108660
Current children cumulated CPU time (s) 967.71
Current children cumulated vsize (Kb) 110784

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17012
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 27778 0 0 0 97582 186 0 0 25 0 1 0 1843524588 112549888 27313 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 27478 27313 145 145 0 27333 0
[pid=16978] vsize: 109912
Current children cumulated CPU time (s) 977.68
Current children cumulated vsize (Kb) 112036

[startup+990.094 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17012
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28027 0 0 0 98577 188 0 0 25 0 1 0 1843524588 113569792 27562 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 27727 27562 145 145 0 27582 0
[pid=16978] vsize: 110908
Current children cumulated CPU time (s) 987.65
Current children cumulated vsize (Kb) 113032

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17012
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28365 0 0 0 99571 189 0 0 25 0 1 0 1843524588 115474432 27900 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 28192 27900 145 145 0 28047 0
[pid=16978] vsize: 112768
Current children cumulated CPU time (s) 997.6
Current children cumulated vsize (Kb) 114892

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17012
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28636 0 0 0 100567 191 0 0 25 0 1 0 1843524588 116580352 28171 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 28462 28171 145 145 0 28317 0
[pid=16978] vsize: 113848
Current children cumulated CPU time (s) 1007.58
Current children cumulated vsize (Kb) 115972

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17012
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28725 0 0 0 101566 192 0 0 25 0 1 0 1843524588 116948992 28260 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 28552 28260 145 145 0 28407 0
[pid=16978] vsize: 114208
Current children cumulated CPU time (s) 1017.58
Current children cumulated vsize (Kb) 116332

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17012
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 29020 0 0 0 102561 194 0 0 25 0 1 0 1843524588 118153216 28555 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 28846 28555 145 145 0 28701 0
[pid=16978] vsize: 115384
Current children cumulated CPU time (s) 1027.55
Current children cumulated vsize (Kb) 117508

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17014
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 29358 0 0 0 103556 196 0 0 25 0 1 0 1843524588 119529472 28893 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 29182 28893 145 145 0 29037 0
[pid=16978] vsize: 116728
Current children cumulated CPU time (s) 1037.52
Current children cumulated vsize (Kb) 118852

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17014
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 29759 0 0 0 104550 199 0 0 25 0 1 0 1843524588 121167872 29294 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 29582 29294 145 145 0 29437 0
[pid=16978] vsize: 118328
Current children cumulated CPU time (s) 1047.49
Current children cumulated vsize (Kb) 120452

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17014
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30081 0 0 0 105545 201 0 0 25 0 1 0 1843524588 122478592 29616 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 29902 29616 145 145 0 29757 0
[pid=16978] vsize: 119608
Current children cumulated CPU time (s) 1057.46
Current children cumulated vsize (Kb) 121732

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17014
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30353 0 0 0 106539 203 0 0 25 0 1 0 1843524588 123588608 29888 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 30173 29888 145 145 0 30028 0
[pid=16978] vsize: 120692
Current children cumulated CPU time (s) 1067.42
Current children cumulated vsize (Kb) 122816

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17014
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30563 0 0 0 107535 205 0 0 25 0 1 0 1843524588 124448768 30098 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 30383 30098 145 145 0 30238 0
[pid=16978] vsize: 121532
Current children cumulated CPU time (s) 1077.4
Current children cumulated vsize (Kb) 123656

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17014
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30791 0 0 0 108531 207 0 0 25 0 1 0 1843524588 125378560 30326 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 30610 30326 145 145 0 30465 0
[pid=16978] vsize: 122440
Current children cumulated CPU time (s) 1087.38
Current children cumulated vsize (Kb) 124564

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17016
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31076 0 0 0 109525 210 0 0 25 0 1 0 1843524588 126537728 30611 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 30893 30611 145 145 0 30748 0
[pid=16978] vsize: 123572
Current children cumulated CPU time (s) 1097.35
Current children cumulated vsize (Kb) 125696

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17016
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31310 0 0 0 110520 212 0 0 25 0 1 0 1843524588 127500288 30845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 31128 30845 145 145 0 30983 0
[pid=16978] vsize: 124512
Current children cumulated CPU time (s) 1107.32
Current children cumulated vsize (Kb) 126636

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17016
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31543 0 0 0 111516 213 0 0 25 0 1 0 1843524588 128442368 31078 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 31358 31078 145 145 0 31213 0
[pid=16978] vsize: 125432
Current children cumulated CPU time (s) 1117.29
Current children cumulated vsize (Kb) 127556

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17016
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31873 0 0 0 112510 217 0 0 25 0 1 0 1843524588 129789952 31408 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 31687 31408 145 145 0 31542 0
[pid=16978] vsize: 126748
Current children cumulated CPU time (s) 1127.27
Current children cumulated vsize (Kb) 128872

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17016
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32100 0 0 0 113505 218 0 0 25 0 1 0 1843524588 130711552 31635 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 31912 31635 145 145 0 31767 0
[pid=16978] vsize: 127648
Current children cumulated CPU time (s) 1137.23
Current children cumulated vsize (Kb) 129772

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17016
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32316 0 0 0 114501 220 0 0 25 0 1 0 1843524588 131596288 31851 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 32128 31851 145 145 0 31983 0
[pid=16978] vsize: 128512
Current children cumulated CPU time (s) 1147.21
Current children cumulated vsize (Kb) 130636

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32605 0 0 0 115496 222 0 0 25 0 1 0 1843524588 132780032 32140 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 32417 32140 145 145 0 32272 0
[pid=16978] vsize: 129668
Current children cumulated CPU time (s) 1157.18
Current children cumulated vsize (Kb) 131792

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32842 0 0 0 116491 224 0 0 25 0 1 0 1843524588 133734400 32377 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 32650 32377 145 145 0 32505 0
[pid=16978] vsize: 130600
Current children cumulated CPU time (s) 1167.15
Current children cumulated vsize (Kb) 132724

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33092 0 0 0 117485 226 0 0 25 0 1 0 1843524588 134754304 32627 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 32899 32627 145 145 0 32754 0
[pid=16978] vsize: 131596
Current children cumulated CPU time (s) 1177.11
Current children cumulated vsize (Kb) 133720

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33345 0 0 0 118481 228 0 0 25 0 1 0 1843524588 135790592 32880 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 33152 32880 145 145 0 33007 0
[pid=16978] vsize: 132608
Current children cumulated CPU time (s) 1187.09
Current children cumulated vsize (Kb) 134732

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33594 0 0 0 119476 229 0 0 25 0 1 0 1843524588 136806400 33129 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 33400 33129 145 145 0 33255 0
[pid=16978] vsize: 133600
Current children cumulated CPU time (s) 1197.05
Current children cumulated vsize (Kb) 135724

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33805 0 0 0 120473 231 0 0 25 0 1 0 1843524588 137670656 33340 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 33611 33340 145 145 0 33466 0
[pid=16978] vsize: 134444
Current children cumulated CPU time (s) 1207.04
Current children cumulated vsize (Kb) 136568



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 17018
Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16974/statm): 531 226 485 147 0 384 0
[pid=16974] vsize: 2124
Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33805 0 0 0 120473 231 0 0 25 0 1 0 1843524588 137670656 33340 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16978/statm): 33611 33340 145 145 0 33466 0
[pid=16978] vsize: 134444
Current children cumulated CPU time (s) 1207.04
Current children cumulated vsize (Kb) 136568

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

Child status: 10
Real time (s): 1210.19
CPU time (s): 1207.11
CPU user time (s): 1204.73
CPU system time (s): 2.37964
CPU usage (%): 99.746
Max. virtual memory (cumulated for all children) (Kb): 136568

Verifier Data

ERROR: no interpretation found !