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-2.opb
MD5SUM550a32227cb0042826e9d8b0433b2655
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -42
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 benchmark1203.08
Number of variables1400
Total number of constraints109401
Number of constraints which are clauses109401
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 2314

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-18 18:53:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2716 boxname=wulflinc2 idbench=372 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  550a32227cb0042826e9d8b0433b2655  /oldhome/oroussel/tmp/wulflinc2/normalized-frb56-25-2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-frb56-25-2.opb
IDLAUNCH: 2716
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        920360 kB
Buffers:         33076 kB
Cached:          57004 kB
SwapCached:       1040 kB
Active:          57704 kB
Inactive:        35076 kB
HighTotal:      131008 kB
HighFree:        70532 kB
LowTotal:       903652 kB
LowFree:        849828 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            15812 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:13:18 (client local time) WITH STATUS 10 IN 1206.72 SECONDS
stats: 2716 7 1206.72 10

Solver Data

c Parsing PB file...
c Converting 109401 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 |  109401   218802 |   36467       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:78076     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  193094   415099 |   64364       0        0     nan |  0.000 % |
c |       100 |  192550   413981 |   70800      81      590     7.3 |  0.516 % |
c |       250 |  191694   412157 |   77880     191     2087    10.9 |  1.412 % |
c |       476 |  190523   409618 |   85668     373     4634    12.4 |  2.568 % |
c |       814 |  188009   404076 |   94235     603     7316    12.1 |  5.226 % |
c |      1320 |  185071   397592 |  103658    1000    11541    11.5 |  8.340 % |
c |      2079 |  180361   387088 |  114024    1525    18000    11.8 | 13.428 % |
c |      3218 |  174052   372857 |  125427    2298    26933    11.7 | 20.384 % |
c |      4926 |  167171   357178 |  137969    3480    42305    12.2 | 28.065 % |
c |      7488 |  157158   334221 |  151766    5331    61838    11.6 | 39.255 % |
c |     11332 |  144436   304457 |  166943    8039    94187    11.7 | 53.917 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16748 |  134807   281657 |   44935   11523   152767    13.3 | 53.917 % |
c |     16848 |  134472   280875 |   49428   11599   153817    13.3 | 65.787 % |
c |     16998 |  134230   280308 |   54371   11738   156796    13.4 | 66.068 % |
c |     17223 |  133770   279211 |   59808   11876   159392    13.4 | 66.599 % |
c |     17560 |  133293   278066 |   65789   12117   163106    13.5 | 67.168 % |
c |     18067 |  132451   276026 |   72368   12355   166879    13.5 | 68.197 % |
c |     18826 |  132034   275016 |   79605   12963   188616    14.6 | 68.700 % |
c |     19965 |  130866   272248 |   87565   13720   203418    14.8 | 70.076 % |
c |     21673 |  129525   269009 |   96322   15069   249486    16.6 | 71.703 % |
c |     24236 |  126370   261437 |  105954   16906   301322    17.8 | 75.533 % |
c ==============================================================================
c Found solution: -42
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27120 |  124797   257602 |   41599   19327   366556    19.0 | 75.533 % |
c |     27221 |  124609   257169 |   45758   19390   367451    19.0 | 77.656 % |
c |     27372 |  124609   257169 |   50334   19541   373598    19.1 | 77.656 % |
c |     27597 |  124480   256852 |   55368   19696   382342    19.4 | 77.819 % |
c |     27934 |  124352   256539 |   60905   19950   393222    19.7 | 77.981 % |
c |     28442 |  124246   256284 |   66995   20427   408671    20.0 | 78.109 % |
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 |     28536 |  124314   256509 |   41438   20521   411801    20.1 | 78.109 % |
c |     28636 |  124278   256419 |   45581   20615   413150    20.0 | 78.122 % |
c |     28787 |  124212   256258 |   50139   20594   416116    20.2 | 78.206 % |
c |     29012 |  124155   256115 |   55153   20774   422744    20.3 | 78.281 % |
c |     29349 |  123998   255722 |   60669   21061   432926    20.6 | 78.481 % |
c |     29855 |  123924   255541 |   66736   21542   455907    21.2 | 78.574 % |
c |     30614 |  123477   254457 |   73409   22107   479117    21.7 | 79.122 % |
c |     31753 |  123112   253584 |   80750   23117   523958    22.7 | 79.563 % |
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 |     32704 |  122868   252983 |   40956   23796   542190    22.8 | 79.563 % |
c |     32804 |  122868   252983 |   45051   23896   544156    22.8 | 79.858 % |
c |     32954 |  122865   252976 |   49556   24045   548175    22.8 | 79.862 % |
c |     33180 |  122748   252701 |   54512   24233   556503    23.0 | 79.998 % |
c |     33518 |  122695   252573 |   59963   24544   575429    23.4 | 80.063 % |
c |     34025 |  122496   252082 |   65960   24965   615467    24.7 | 80.303 % |
c |     34784 |  122447   251963 |   72556   25704   643849    25.0 | 80.363 % |
c |     35923 |  122348   251715 |   79811   26752   724264    27.1 | 80.490 % |
c |     37631 |  122084   251065 |   87792   28017   788957    28.2 | 80.823 % |
c |     40193 |  121936   250714 |   96572   30493  1096807    36.0 | 80.996 % |
c |     44037 |  121613   249937 |  106229   33966  1333260    39.3 | 81.387 % |
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 |     44649 |  121598   249931 |   40532   34330  1361086    39.6 | 81.387 % |
c |     44750 |  121598   249931 |   44585   34431  1363689    39.6 | 81.415 % |
c |     44901 |  121496   249687 |   49043   34550  1367121    39.6 | 81.537 % |
c |     45126 |  121026   248536 |   53948   34437  1367468    39.7 | 82.124 % |
c |     45463 |  121001   248473 |   59342   34739  1383805    39.8 | 82.157 % |
c |     45970 |  120940   248317 |   65277   35124  1405818    40.0 | 82.236 % |
c |     46730 |  120930   248293 |   71804   35808  1432323    40.0 | 82.248 % |
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 |     47417 |  120940   248346 |   40313   36448  1451377    39.8 | 82.248 % |
c |     47517 |  120934   248332 |   44344   36543  1455647    39.8 | 82.292 % |
c |     47667 |  120876   248204 |   48778   36594  1456457    39.8 | 82.353 % |
c |     47894 |  120869   248187 |   53656   36738  1463986    39.8 | 82.362 % |
c |     48231 |  120869   248187 |   59022   37075  1473745    39.8 | 82.362 % |
c |     48738 |  120659   247667 |   64924   37412  1495976    40.0 | 82.628 % |
c |     49497 |  120597   247517 |   71416   37982  1561617    41.1 | 82.703 % |
c |     50636 |  120480   247240 |   78558   38839  1642896    42.3 | 82.842 % |
c |     52344 |  120473   247225 |   86414   40501  1739485    42.9 | 82.849 % |
c |     54906 |  120255   246700 |   95055   42829  1975102    46.1 | 83.118 % |
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 |     57045 |  120216   246582 |   40072   44648  2278364    51.0 | 83.118 % |
c |     57145 |  120216   246582 |   44079   44748  2281325    51.0 | 83.168 % |
c |     57297 |  120216   246582 |   48487   44900  2288955    51.0 | 83.168 % |
c |     57523 |  120130   246364 |   53335   44971  2304412    51.2 | 83.280 % |
c |     57860 |  120109   246315 |   58669   45276  2317982    51.2 | 83.304 % |
c |     58367 |  120058   246202 |   64536   45762  2356290    51.5 | 83.358 % |
c |     59126 |  120058   246202 |   70989   46521  2419971    52.0 | 83.358 % |
c |     60265 |  120058   246202 |   78088   47660  2507609    52.6 | 83.358 % |
c |     61973 |  120001   246053 |   85897   49258  2633802    53.5 | 83.437 % |
c |     64535 |  119961   245951 |   94487   51758  2848264    55.0 | 83.491 % |
c |     68379 |  119845   245672 |  103936   55463  3195026    57.6 | 83.630 % |
c |     74146 |  119845   245672 |  114330   61230  4034130    65.9 | 83.630 % |
c |     82795 |  119662   245221 |  125763   69629  4758092    68.3 | 83.864 % |
c |     95770 |  119456   244722 |  138339   82302  6937965    84.3 | 84.119 % |
c |    115231 |  119197   244098 |  152173  101081  9562562    94.6 | 84.432 % |
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 |    128578 |  119061   243777 |   39687  114237 11744294   102.8 | 84.432 % |
c |    128679 |  119050   243750 |   43655   23872  2191084    91.8 | 84.625 % |
c |    128830 |  119050   243750 |   48021   24023  2198095    91.5 | 84.625 % |
c |    129057 |  119041   243727 |   52823   24247  2206430    91.0 | 84.638 % |
c |    129395 |  119041   243727 |   58105   24585  2234797    90.9 | 84.638 % |
c |    129901 |  119041   243727 |   63916   25091  2270090    90.5 | 84.638 % |
c |    130660 |  119041   243727 |   70307   25850  2324765    89.9 | 84.638 % |
c |    131800 |  119036   243714 |   77338   26967  2390314    88.6 | 84.645 % |
c |    133508 |  119024   243684 |   85072   28662  2521904    88.0 | 84.660 % |
c |    136070 |  118994   243606 |   93579   31211  2742209    87.9 | 84.702 % |
c |    139914 |  118994   243606 |  102937   35055  3395400    96.9 | 84.702 % |
c |    145680 |  118852   243246 |  113231   40787  4097071   100.5 | 84.885 % |
c |    154329 |  118811   243143 |  124554   49099  5460303   111.2 | 84.938 % |
c |    167303 |  118690   242854 |  137010   61891  7674838   124.0 | 85.081 % |
c |    186764 |  118443   242262 |  150711   81251 12728039   156.7 | 85.381 % |
c |    215956 |  118381   242110 |  165782  110427 18354731   166.2 | 85.459 % |
c |    259746 |  118130   241494 |  182360  153926 26304046   170.9 | 85.777 % |
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/15403/stat): 15403 (minisat+_script) R 15402 15403 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785349239 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/15403/statm): 174 3 169 147 0 27 0
[pid=15403] 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=15404
New process pid=15405
New process pid=15406
execve syscall for /bin/sed executable
One traced child (pid=15405) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15406) exited with status: 0
One traced child (pid=15404) exited with status: 0
New process pid=15407
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-frb56-25-2.opb

[startup+10.0032 s]
Raw data (loadavg): 0.87 0.94 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 30032

[startup+20.0049 s]
Raw data (loadavg): 0.89 0.94 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 1942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 30032

[startup+30.0056 s]
Raw data (loadavg): 0.91 0.94 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 2942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 30032

[startup+40.0064 s]
Raw data (loadavg): 0.92 0.94 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 3941 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 30032

[startup+50.008 s]
Raw data (loadavg): 0.93 0.94 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 4941 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 30032

[startup+60.0077 s]
Raw data (loadavg): 0.94 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 5942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 30032

[startup+70.0094 s]
Raw data (loadavg): 0.95 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 6942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 30032

[startup+80.0101 s]
Raw data (loadavg): 0.96 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 7942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 30032

[startup+90.0098 s]
Raw data (loadavg): 0.96 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 8942 31 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 30032

[startup+100.011 s]
Raw data (loadavg): 0.97 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 9941 32 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 30032

[startup+110.011 s]
Raw data (loadavg): 0.97 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 10941 32 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223120 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 30032

[startup+120.012 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 11941 32 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 30032

[startup+130.013 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 12941 32 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 30032

[startup+140.013 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 13941 32 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 139.73
Current children cumulated vsize (Kb) 30032

[startup+150.014 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 6830 0 0 0 14941 32 0 0 25 0 1 0 1785349244 28577792 6817 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 6977 6817 145 145 0 6832 0
[pid=15407] vsize: 27908
Current children cumulated CPU time (s) 149.73
Current children cumulated vsize (Kb) 30032

[startup+160.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 7065 0 0 0 15939 34 0 0 25 0 1 0 1785349244 29073408 6938 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 7098 6938 145 145 0 6953 0
[pid=15407] vsize: 28392
Current children cumulated CPU time (s) 159.73
Current children cumulated vsize (Kb) 30516

[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 7419 0 0 0 16934 35 0 0 25 0 1 0 1785349244 30216192 7217 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 7377 7217 145 145 0 7232 0
[pid=15407] vsize: 29508
Current children cumulated CPU time (s) 169.69
Current children cumulated vsize (Kb) 31632

[startup+180.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 7872 0 0 0 17928 38 0 0 25 0 1 0 1785349244 32071680 7670 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 7830 7670 145 145 0 7685 0
[pid=15407] vsize: 31320
Current children cumulated CPU time (s) 179.66
Current children cumulated vsize (Kb) 33444

[startup+190.017 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 8208 0 0 0 18923 40 0 0 25 0 1 0 1785349244 33259520 7930 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 8120 7930 145 145 0 7975 0
[pid=15407] vsize: 32480
Current children cumulated CPU time (s) 189.63
Current children cumulated vsize (Kb) 34604

[startup+200.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 8507 0 0 0 19918 42 0 0 25 0 1 0 1785349244 34160640 8154 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 8340 8154 145 145 0 8195 0
[pid=15407] vsize: 33360
Current children cumulated CPU time (s) 199.6
Current children cumulated vsize (Kb) 35484

[startup+210.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 8892 0 0 0 20911 45 0 0 25 0 1 0 1785349244 35721216 8539 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 8721 8539 145 145 0 8576 0
[pid=15407] vsize: 34884
Current children cumulated CPU time (s) 209.56
Current children cumulated vsize (Kb) 37008

[startup+220.019 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 9413 0 0 0 21903 48 0 0 25 0 1 0 1785349244 37535744 8985 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 9164 8985 145 145 0 9019 0
[pid=15407] vsize: 36656
Current children cumulated CPU time (s) 219.51
Current children cumulated vsize (Kb) 38780

[startup+230.02 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 9789 0 0 0 22897 50 0 0 25 0 1 0 1785349244 39059456 9361 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 9536 9361 145 145 0 9391 0
[pid=15407] vsize: 38144
Current children cumulated CPU time (s) 229.47
Current children cumulated vsize (Kb) 40268

[startup+240.019 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 10170 0 0 0 23890 52 0 0 25 0 1 0 1785349244 40603648 9742 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 9913 9742 145 145 0 9768 0
[pid=15407] vsize: 39652
Current children cumulated CPU time (s) 239.42
Current children cumulated vsize (Kb) 41776

[startup+250.02 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 10652 0 0 0 24880 57 0 0 25 0 1 0 1785349244 42561536 10224 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 10391 10224 145 145 0 10246 0
[pid=15407] vsize: 41564
Current children cumulated CPU time (s) 249.37
Current children cumulated vsize (Kb) 43688

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 11185 0 0 0 25871 61 0 0 25 0 1 0 1785349244 44732416 10757 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 10921 10757 145 145 0 10776 0
[pid=15407] vsize: 43684
Current children cumulated CPU time (s) 259.32
Current children cumulated vsize (Kb) 45808

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 11465 0 0 0 26867 63 0 0 25 0 1 0 1785349244 45862912 11037 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 11197 11037 145 145 0 11052 0
[pid=15407] vsize: 44788
Current children cumulated CPU time (s) 269.3
Current children cumulated vsize (Kb) 46912

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 11943 0 0 0 27859 66 0 0 25 0 1 0 1785349244 48070656 11515 4294967295 134512640 135094434 3221224448 3221223072 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 11736 11515 145 145 0 11591 0
[pid=15407] vsize: 46944
Current children cumulated CPU time (s) 279.25
Current children cumulated vsize (Kb) 49068

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 12220 0 0 0 28854 68 0 0 25 0 1 0 1785349244 49192960 11792 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 12010 11792 145 145 0 11865 0
[pid=15407] vsize: 48040
Current children cumulated CPU time (s) 289.22
Current children cumulated vsize (Kb) 50164

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 12661 0 0 0 29845 72 0 0 25 0 1 0 1785349244 50987008 12233 4294967295 134512640 135094434 3221224448 3221223120 134556538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 12448 12233 145 145 0 12303 0
[pid=15407] vsize: 49792
Current children cumulated CPU time (s) 299.17
Current children cumulated vsize (Kb) 51916

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 13208 0 0 0 30837 76 0 0 25 0 1 0 1785349244 53215232 12780 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 12992 12780 145 145 0 12847 0
[pid=15407] vsize: 51968
Current children cumulated CPU time (s) 309.13
Current children cumulated vsize (Kb) 54092

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 13773 0 0 0 31826 80 0 0 25 0 1 0 1785349244 55521280 13345 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 13555 13345 145 145 0 13410 0
[pid=15407] vsize: 54220
Current children cumulated CPU time (s) 319.06
Current children cumulated vsize (Kb) 56344

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) T 15403 15403 6872 0 -1 0 14279 0 0 0 32817 83 0 0 25 0 1 0 1785349244 57585664 13851 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15407/statm): 14059 13851 145 145 0 13914 0
[pid=15407] vsize: 56236
Current children cumulated CPU time (s) 329
Current children cumulated vsize (Kb) 58360

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 14656 0 0 0 33809 87 0 0 25 0 1 0 1785349244 59117568 14228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 14433 14228 145 145 0 14288 0
[pid=15407] vsize: 57732
Current children cumulated CPU time (s) 338.96
Current children cumulated vsize (Kb) 59856

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 15050 0 0 0 34803 90 0 0 25 0 1 0 1785349244 60719104 14622 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 14824 14622 145 145 0 14679 0
[pid=15407] vsize: 59296
Current children cumulated CPU time (s) 348.93
Current children cumulated vsize (Kb) 61420

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 15419 0 0 0 35799 91 0 0 25 0 1 0 1785349244 62222336 14991 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 15191 14991 145 145 0 15046 0
[pid=15407] vsize: 60764
Current children cumulated CPU time (s) 358.9
Current children cumulated vsize (Kb) 62888

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 15760 0 0 0 36793 93 0 0 25 0 1 0 1785349244 63610880 15332 4294967295 134512640 135094434 3221224448 3221223040 134557199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 15530 15332 145 145 0 15385 0
[pid=15407] vsize: 62120
Current children cumulated CPU time (s) 368.86
Current children cumulated vsize (Kb) 64244

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 16079 0 0 0 37786 96 0 0 25 0 1 0 1785349244 64909312 15651 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 15847 15651 145 145 0 15702 0
[pid=15407] vsize: 63388
Current children cumulated CPU time (s) 378.82
Current children cumulated vsize (Kb) 65512

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) T 15403 15403 6872 0 -1 0 16506 0 0 0 38778 99 0 0 25 0 1 0 1785349244 66650112 16078 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15407/statm): 16272 16078 145 145 0 16127 0
[pid=15407] vsize: 65088
Current children cumulated CPU time (s) 388.77
Current children cumulated vsize (Kb) 67212

[startup+400.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 16864 0 0 0 39773 102 0 0 25 0 1 0 1785349244 68108288 16436 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 16628 16436 145 145 0 16483 0
[pid=15407] vsize: 66512
Current children cumulated CPU time (s) 398.75
Current children cumulated vsize (Kb) 68636

[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 17053 0 0 0 40769 103 0 0 25 0 1 0 1785349244 68878336 16625 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 16816 16625 145 145 0 16671 0
[pid=15407] vsize: 67264
Current children cumulated CPU time (s) 408.72
Current children cumulated vsize (Kb) 69388

[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 17379 0 0 0 41764 106 0 0 25 0 1 0 1785349244 70205440 16951 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 17140 16951 145 145 0 16995 0
[pid=15407] vsize: 68560
Current children cumulated CPU time (s) 418.7
Current children cumulated vsize (Kb) 70684

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 17733 0 0 0 42758 108 0 0 25 0 1 0 1785349244 71643136 17305 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 17491 17305 145 145 0 17346 0
[pid=15407] vsize: 69964
Current children cumulated CPU time (s) 428.66
Current children cumulated vsize (Kb) 72088

[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 18011 0 0 0 43753 110 0 0 25 0 1 0 1785349244 72777728 17583 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 17768 17583 145 145 0 17623 0
[pid=15407] vsize: 71072
Current children cumulated CPU time (s) 438.63
Current children cumulated vsize (Kb) 73196

[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 18449 0 0 0 44747 111 0 0 25 0 1 0 1785349244 74559488 18021 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 18203 18021 145 145 0 18058 0
[pid=15407] vsize: 72812
Current children cumulated CPU time (s) 448.58
Current children cumulated vsize (Kb) 74936

[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 18817 0 0 0 45739 114 0 0 25 0 1 0 1785349244 76062720 18389 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 18570 18389 145 145 0 18425 0
[pid=15407] vsize: 74280
Current children cumulated CPU time (s) 458.53
Current children cumulated vsize (Kb) 76404

[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19259 0 0 0 46730 118 0 0 25 0 1 0 1785349244 77864960 18831 4294967295 134512640 135094434 3221224448 3221223120 134555609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19010 18831 145 145 0 18865 0
[pid=15407] vsize: 76040
Current children cumulated CPU time (s) 468.48
Current children cumulated vsize (Kb) 78164

[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 47725 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 478.46
Current children cumulated vsize (Kb) 79136

[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 48725 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223072 134562070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 488.46
Current children cumulated vsize (Kb) 79136

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 49725 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 498.46
Current children cumulated vsize (Kb) 79136

[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 50726 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 508.47
Current children cumulated vsize (Kb) 79136

[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 51726 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 518.47
Current children cumulated vsize (Kb) 79136

[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 52726 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223072 134557633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 528.47
Current children cumulated vsize (Kb) 79136

[startup+540.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 53726 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 538.47
Current children cumulated vsize (Kb) 79136

[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 54726 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223120 134555842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 548.47
Current children cumulated vsize (Kb) 79136

[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 55727 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 558.48
Current children cumulated vsize (Kb) 79136

[startup+570.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 56727 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 568.48
Current children cumulated vsize (Kb) 79136

[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 57727 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 578.48
Current children cumulated vsize (Kb) 79136

[startup+590.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 58727 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 588.48
Current children cumulated vsize (Kb) 79136

[startup+600.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 59727 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 598.48
Current children cumulated vsize (Kb) 79136

[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 60728 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 608.49
Current children cumulated vsize (Kb) 79136

[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 61728 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 618.49
Current children cumulated vsize (Kb) 79136

[startup+630.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 62728 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 628.49
Current children cumulated vsize (Kb) 79136

[startup+640.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19578 0 0 0 63728 121 0 0 25 0 1 0 1785349244 78860288 19075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19075 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 638.49
Current children cumulated vsize (Kb) 79136

[startup+650.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19579 0 0 0 64729 121 0 0 25 0 1 0 1785349244 78860288 19076 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19076 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 648.5
Current children cumulated vsize (Kb) 79136

[startup+660.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19579 0 0 0 65729 121 0 0 25 0 1 0 1785349244 78860288 19076 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19253 19076 145 145 0 19108 0
[pid=15407] vsize: 77012
Current children cumulated CPU time (s) 658.5
Current children cumulated vsize (Kb) 79136

[startup+670.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 19963 0 0 0 66723 123 0 0 25 0 1 0 1785349244 80433152 19460 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 19637 19460 145 145 0 19492 0
[pid=15407] vsize: 78548
Current children cumulated CPU time (s) 668.46
Current children cumulated vsize (Kb) 80672

[startup+680.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 20549 0 0 0 67712 128 0 0 25 0 1 0 1785349244 82837504 20046 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 20224 20046 145 145 0 20079 0
[pid=15407] vsize: 80896
Current children cumulated CPU time (s) 678.4
Current children cumulated vsize (Kb) 83020

[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 20928 0 0 0 68703 132 0 0 25 0 1 0 1785349244 84389888 20425 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 20603 20425 145 145 0 20458 0
[pid=15407] vsize: 82412
Current children cumulated CPU time (s) 688.35
Current children cumulated vsize (Kb) 84536

[startup+700.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 21180 0 0 0 69698 134 0 0 25 0 1 0 1785349244 85422080 20677 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 20855 20677 145 145 0 20710 0
[pid=15407] vsize: 83420
Current children cumulated CPU time (s) 698.32
Current children cumulated vsize (Kb) 85544

[startup+710.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 21599 0 0 0 70692 136 0 0 25 0 1 0 1785349244 87138304 21096 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 21274 21096 145 145 0 21129 0
[pid=15407] vsize: 85096
Current children cumulated CPU time (s) 708.28
Current children cumulated vsize (Kb) 87220

[startup+720.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 21986 0 0 0 71687 139 0 0 25 0 1 0 1785349244 88723456 21483 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 21661 21483 145 145 0 21516 0
[pid=15407] vsize: 86644
Current children cumulated CPU time (s) 718.26
Current children cumulated vsize (Kb) 88768

[startup+730.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 22314 0 0 0 72682 141 0 0 25 0 1 0 1785349244 90071040 21811 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 21990 21811 145 145 0 21845 0
[pid=15407] vsize: 87960
Current children cumulated CPU time (s) 728.23
Current children cumulated vsize (Kb) 90084

[startup+740.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 22647 0 0 0 73676 143 0 0 25 0 1 0 1785349244 91443200 22144 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 22325 22144 145 145 0 22180 0
[pid=15407] vsize: 89300
Current children cumulated CPU time (s) 738.19
Current children cumulated vsize (Kb) 91424

[startup+750.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 22897 0 0 0 74673 146 0 0 25 0 1 0 1785349244 92467200 22394 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 22575 22394 145 145 0 22430 0
[pid=15407] vsize: 90300
Current children cumulated CPU time (s) 748.19
Current children cumulated vsize (Kb) 92424

[startup+760.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 23259 0 0 0 75667 148 0 0 25 0 1 0 1785349244 93941760 22756 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 22935 22756 145 145 0 22790 0
[pid=15407] vsize: 91740
Current children cumulated CPU time (s) 758.15
Current children cumulated vsize (Kb) 93864

[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 23709 0 0 0 76658 151 0 0 25 0 1 0 1785349244 95784960 23206 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 23385 23206 145 145 0 23240 0
[pid=15407] vsize: 93540
Current children cumulated CPU time (s) 768.09
Current children cumulated vsize (Kb) 95664

[startup+780.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 24171 0 0 0 77651 155 0 0 25 0 1 0 1785349244 97677312 23668 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 23847 23668 145 145 0 23702 0
[pid=15407] vsize: 95388
Current children cumulated CPU time (s) 778.06
Current children cumulated vsize (Kb) 97512

[startup+790.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 24621 0 0 0 78644 157 0 0 25 0 1 0 1785349244 99520512 24118 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 24297 24118 145 145 0 24152 0
[pid=15407] vsize: 97188
Current children cumulated CPU time (s) 788.01
Current children cumulated vsize (Kb) 99312

[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 25068 0 0 0 79638 160 0 0 25 0 1 0 1785349244 101351424 24565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 24744 24565 145 145 0 24599 0
[pid=15407] vsize: 98976
Current children cumulated CPU time (s) 797.98
Current children cumulated vsize (Kb) 101100

[startup+810.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 25515 0 0 0 80631 162 0 0 25 0 1 0 1785349244 103186432 25012 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 25192 25012 145 145 0 25047 0
[pid=15407] vsize: 100768
Current children cumulated CPU time (s) 807.93
Current children cumulated vsize (Kb) 102892

[startup+820.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 25933 0 0 0 81623 166 0 0 25 0 1 0 1785349244 104898560 25430 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 25610 25430 145 145 0 25465 0
[pid=15407] vsize: 102440
Current children cumulated CPU time (s) 817.89
Current children cumulated vsize (Kb) 104564

[startup+830.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 26331 0 0 0 82615 169 0 0 25 0 1 0 1785349244 106528768 25828 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 26008 25828 145 145 0 25863 0
[pid=15407] vsize: 104032
Current children cumulated CPU time (s) 827.84
Current children cumulated vsize (Kb) 106156

[startup+840.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 26604 0 0 0 83610 171 0 0 25 0 1 0 1785349244 107646976 26101 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 26281 26101 145 145 0 26136 0
[pid=15407] vsize: 105124
Current children cumulated CPU time (s) 837.81
Current children cumulated vsize (Kb) 107248

[startup+850.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 26944 0 0 0 84604 173 0 0 25 0 1 0 1785349244 109039616 26441 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 26621 26441 145 145 0 26476 0
[pid=15407] vsize: 106484
Current children cumulated CPU time (s) 847.77
Current children cumulated vsize (Kb) 108608

[startup+860.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 27310 0 0 0 85597 176 0 0 25 0 1 0 1785349244 110530560 26807 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 26985 26807 145 145 0 26840 0
[pid=15407] vsize: 107940
Current children cumulated CPU time (s) 857.73
Current children cumulated vsize (Kb) 110064

[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 27556 0 0 0 86593 177 0 0 25 0 1 0 1785349244 111542272 27053 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 27232 27053 145 145 0 27087 0
[pid=15407] vsize: 108928
Current children cumulated CPU time (s) 867.7
Current children cumulated vsize (Kb) 111052

[startup+880.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 27942 0 0 0 87587 180 0 0 25 0 1 0 1785349244 113115136 27439 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 27616 27439 145 145 0 27471 0
[pid=15407] vsize: 110464
Current children cumulated CPU time (s) 877.67
Current children cumulated vsize (Kb) 112588

[startup+890.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 28151 0 0 0 88585 181 0 0 25 0 1 0 1785349244 113975296 27648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 27826 27648 145 145 0 27681 0
[pid=15407] vsize: 111304
Current children cumulated CPU time (s) 887.66
Current children cumulated vsize (Kb) 113428

[startup+900.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 28353 0 0 0 89582 181 0 0 25 0 1 0 1785349244 114798592 27850 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 28027 27850 145 145 0 27882 0
[pid=15407] vsize: 112108
Current children cumulated CPU time (s) 897.63
Current children cumulated vsize (Kb) 114232

[startup+910.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 28624 0 0 0 90577 183 0 0 25 0 1 0 1785349244 115908608 28121 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 28298 28121 145 145 0 28153 0
[pid=15407] vsize: 113192
Current children cumulated CPU time (s) 907.6
Current children cumulated vsize (Kb) 115316

[startup+920.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 28889 0 0 0 91572 185 0 0 25 0 1 0 1785349244 116981760 28386 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 28560 28386 145 145 0 28415 0
[pid=15407] vsize: 114240
Current children cumulated CPU time (s) 917.57
Current children cumulated vsize (Kb) 116364

[startup+930.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 29269 0 0 0 92566 188 0 0 25 0 1 0 1785349244 118534144 28766 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 28939 28766 145 145 0 28794 0
[pid=15407] vsize: 115756
Current children cumulated CPU time (s) 927.54
Current children cumulated vsize (Kb) 117880

[startup+940.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 29703 0 0 0 93559 190 0 0 25 0 1 0 1785349244 120299520 29200 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 29370 29200 145 145 0 29225 0
[pid=15407] vsize: 117480
Current children cumulated CPU time (s) 937.49
Current children cumulated vsize (Kb) 119604

[startup+950.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 30111 0 0 0 94552 193 0 0 25 0 1 0 1785349244 122490880 29608 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 29905 29608 145 145 0 29760 0
[pid=15407] vsize: 119620
Current children cumulated CPU time (s) 947.45
Current children cumulated vsize (Kb) 121744

[startup+960.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 30521 0 0 0 95545 196 0 0 25 0 1 0 1785349244 124166144 30018 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 30314 30018 145 145 0 30169 0
[pid=15407] vsize: 121256
Current children cumulated CPU time (s) 957.41
Current children cumulated vsize (Kb) 123380

[startup+970.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 30883 0 0 0 96539 198 0 0 25 0 1 0 1785349244 125640704 30380 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 30674 30380 145 145 0 30529 0
[pid=15407] vsize: 122696
Current children cumulated CPU time (s) 967.37
Current children cumulated vsize (Kb) 124820

[startup+980.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 31236 0 0 0 97533 201 0 0 25 0 1 0 1785349244 127082496 30733 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 31026 30733 145 145 0 30881 0
[pid=15407] vsize: 124104
Current children cumulated CPU time (s) 977.34
Current children cumulated vsize (Kb) 126228

[startup+990.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 31605 0 0 0 98527 203 0 0 25 0 1 0 1785349244 128589824 31102 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 31394 31102 145 145 0 31249 0
[pid=15407] vsize: 125576
Current children cumulated CPU time (s) 987.3
Current children cumulated vsize (Kb) 127700

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 31861 0 0 0 99521 205 0 0 25 0 1 0 1785349244 129634304 31358 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 31649 31358 145 145 0 31504 0
[pid=15407] vsize: 126596
Current children cumulated CPU time (s) 997.26
Current children cumulated vsize (Kb) 128720

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 32125 0 0 0 100516 207 0 0 25 0 1 0 1785349244 130707456 31622 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 31911 31622 145 145 0 31766 0
[pid=15407] vsize: 127644
Current children cumulated CPU time (s) 1007.23
Current children cumulated vsize (Kb) 129768

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 32414 0 0 0 101510 210 0 0 25 0 1 0 1785349244 131891200 31911 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 32200 31911 145 145 0 32055 0
[pid=15407] vsize: 128800
Current children cumulated CPU time (s) 1017.2
Current children cumulated vsize (Kb) 130924

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 32814 0 0 0 102503 213 0 0 25 0 1 0 1785349244 133521408 32311 4294967295 134512640 135094434 3221224448 3221223040 134551920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 32598 32311 145 145 0 32453 0
[pid=15407] vsize: 130392
Current children cumulated CPU time (s) 1027.16
Current children cumulated vsize (Kb) 132516

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 33222 0 0 0 103496 215 0 0 25 0 1 0 1785349244 135184384 32719 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 33004 32719 145 145 0 32859 0
[pid=15407] vsize: 132016
Current children cumulated CPU time (s) 1037.11
Current children cumulated vsize (Kb) 134140

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 33544 0 0 0 104492 216 0 0 25 0 1 0 1785349244 136499200 33041 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 33325 33041 145 145 0 33180 0
[pid=15407] vsize: 133300
Current children cumulated CPU time (s) 1047.08
Current children cumulated vsize (Kb) 135424

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 33814 0 0 0 105488 218 0 0 25 0 1 0 1785349244 137601024 33311 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 33594 33311 145 145 0 33449 0
[pid=15407] vsize: 134376
Current children cumulated CPU time (s) 1057.06
Current children cumulated vsize (Kb) 136500

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 34120 0 0 0 106483 221 0 0 25 0 1 0 1785349244 138846208 33617 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 33898 33617 145 145 0 33753 0
[pid=15407] vsize: 135592
Current children cumulated CPU time (s) 1067.04
Current children cumulated vsize (Kb) 137716

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 34414 0 0 0 107478 223 0 0 25 0 1 0 1785349244 140046336 33911 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 34191 33911 145 145 0 34046 0
[pid=15407] vsize: 136764
Current children cumulated CPU time (s) 1077.01
Current children cumulated vsize (Kb) 138888

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 34702 0 0 0 108472 225 0 0 25 0 1 0 1785349244 141213696 34199 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 34476 34199 145 145 0 34331 0
[pid=15407] vsize: 137904
Current children cumulated CPU time (s) 1086.97
Current children cumulated vsize (Kb) 140028

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 34987 0 0 0 109467 227 0 0 25 0 1 0 1785349244 142376960 34484 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 34760 34484 145 145 0 34615 0
[pid=15407] vsize: 139040
Current children cumulated CPU time (s) 1096.94
Current children cumulated vsize (Kb) 141164

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 35228 0 0 0 110464 228 0 0 25 0 1 0 1785349244 143372288 34725 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 35003 34725 145 145 0 34858 0
[pid=15407] vsize: 140012
Current children cumulated CPU time (s) 1106.92
Current children cumulated vsize (Kb) 142136

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 35492 0 0 0 111459 231 0 0 25 0 1 0 1785349244 144445440 34989 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 35265 34989 145 145 0 35120 0
[pid=15407] vsize: 141060
Current children cumulated CPU time (s) 1116.9
Current children cumulated vsize (Kb) 143184

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 35747 0 0 0 112455 232 0 0 25 0 1 0 1785349244 145489920 35244 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 35520 35244 145 145 0 35375 0
[pid=15407] vsize: 142080
Current children cumulated CPU time (s) 1126.87
Current children cumulated vsize (Kb) 144204

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 36026 0 0 0 113451 234 0 0 25 0 1 0 1785349244 146628608 35523 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 35798 35523 145 145 0 35653 0
[pid=15407] vsize: 143192
Current children cumulated CPU time (s) 1136.85
Current children cumulated vsize (Kb) 145316

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 36290 0 0 0 114447 236 0 0 25 0 1 0 1785349244 147714048 35787 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 36063 35787 145 145 0 35918 0
[pid=15407] vsize: 144252
Current children cumulated CPU time (s) 1146.83
Current children cumulated vsize (Kb) 146376

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 36586 0 0 0 115442 238 0 0 25 0 1 0 1785349244 148910080 36083 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 36355 36083 145 145 0 36210 0
[pid=15407] vsize: 145420
Current children cumulated CPU time (s) 1156.8
Current children cumulated vsize (Kb) 147544

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 36947 0 0 0 116435 241 0 0 25 0 1 0 1785349244 150384640 36444 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 36715 36444 145 145 0 36570 0
[pid=15407] vsize: 146860
Current children cumulated CPU time (s) 1166.76
Current children cumulated vsize (Kb) 148984

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 37302 0 0 0 117429 243 0 0 25 0 1 0 1785349244 151830528 36799 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15407/statm): 37068 36799 145 145 0 36923 0
[pid=15407] vsize: 148272
Current children cumulated CPU time (s) 1176.72
Current children cumulated vsize (Kb) 150396

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 37620 0 0 0 118425 245 0 0 25 0 1 0 1785349244 153141248 37117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 37388 37117 145 145 0 37243 0
[pid=15407] vsize: 149552
Current children cumulated CPU time (s) 1186.7
Current children cumulated vsize (Kb) 151676

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 37929 0 0 0 119419 248 0 0 25 0 1 0 1785349244 154394624 37426 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 37694 37426 145 145 0 37549 0
[pid=15407] vsize: 150776
Current children cumulated CPU time (s) 1196.67
Current children cumulated vsize (Kb) 152900

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 38224 0 0 0 120413 250 0 0 25 0 1 0 1785349244 155594752 37721 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 37987 37721 145 145 0 37842 0
[pid=15407] vsize: 151948
Current children cumulated CPU time (s) 1206.63
Current children cumulated vsize (Kb) 154072



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 15407
Raw data (/proc/15403/stat): 15403 (minisat+_script) S 15402 15403 6872 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785349239 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15403/statm): 531 226 485 147 0 384 0
[pid=15403] vsize: 2124
Raw data (/proc/15407/stat): 15407 (minisat+_64-bit) R 15403 15403 6872 0 -1 0 38224 0 0 0 120413 250 0 0 25 0 1 0 1785349244 155594752 37721 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15407/statm): 37987 37721 145 145 0 37842 0
[pid=15407] vsize: 151948
Current children cumulated CPU time (s) 1206.63
Current children cumulated vsize (Kb) 154072

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1206.72
CPU user time (s): 1204.14
CPU system time (s): 2.57461
CPU usage (%): 99.7151
Max. virtual memory (cumulated for all children) (Kb): 154072

Verifier Data

ERROR: no interpretation found !