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/frb53-24-opb/normalized-frb53-24-1.opb
MD5SUM20fc65112f36a5d10cc9eaa82c0beb63
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -39
Optimality of the best value was proved NO
Number of terms in the objective function 1272
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 1272
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 1272
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 benchmark1207.03
Number of variables1272
Total number of constraints94227
Number of constraints which are clauses94227
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 2307

Launcher Data

LAUNCH ON wulflinc9 THE 2005-09-18 18:51:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2710 boxname=wulflinc9 idbench=366 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  20fc65112f36a5d10cc9eaa82c0beb63  /oldhome/oroussel/tmp/wulflinc9/normalized-frb53-24-1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-frb53-24-1.opb
IDLAUNCH: 2710
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        923516 kB
Buffers:         30512 kB
Cached:          54056 kB
SwapCached:       1044 kB
Active:          49728 kB
Inactive:        37564 kB
HighTotal:      131008 kB
HighFree:        73332 kB
LowTotal:       903652 kB
LowFree:        850184 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            18028 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:11:51 (client local time) WITH STATUS 10 IN 1207.61 SECONDS
stats: 2710 7 1207.61 10

Solver Data

c Parsing PB file...
c Converting 94227 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 |   94227   188454 |   31409       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:70300     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  169273   364509 |   56424       0        0     nan |  0.000 % |
c |       100 |  168899   363733 |   62066      65      591     9.1 |  0.407 % |
c |       250 |  168502   362906 |   68273     198     1311     6.6 |  0.828 % |
c |       475 |  167076   359832 |   75100     351     2932     8.4 |  2.494 % |
c |       812 |  165133   355593 |   82610     631     5067     8.0 |  4.688 % |
c |      1319 |  162313   349369 |   90871     972     8957     9.2 |  8.080 % |
c |      2078 |  157982   339700 |   99958    1468    15263    10.4 | 13.235 % |
c ==============================================================================
c Found solution: -39
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2296 |  157388   338635 |   52462    1645    17452    10.6 | 13.235 % |
c |      2397 |  157059   337878 |   57708    1732    17985    10.4 | 14.608 % |
c |      2548 |  155840   335129 |   63479    1821    18984    10.4 | 16.160 % |
c |      2773 |  154165   331306 |   69826    1966    20681    10.5 | 18.177 % |
c |      3110 |  151458   325155 |   76809    2174    23582    10.8 | 21.604 % |
c |      3616 |  147626   316455 |   84490    2526    28129    11.1 | 26.258 % |
c |      4375 |  143472   307009 |   92939    3028    34893    11.5 | 31.480 % |
c |      5514 |  137035   292201 |  102233    3700    43332    11.7 | 39.456 % |
c |      7223 |  129643   274879 |  112456    4787    55808    11.7 | 48.879 % |
c |      9785 |  121178   254842 |  123702    6238    75388    12.1 | 60.010 % |
c |     13629 |  111810   232544 |  136072    8363   107856    12.9 | 72.370 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13714 |  111791   232457 |   37263    8438   110430    13.1 | 72.370 % |
c |     13815 |  111736   232336 |   40989    8517   111608    13.1 | 72.463 % |
c |     13965 |  111449   231624 |   45088    8613   112090    13.0 | 72.865 % |
c |     14191 |  110875   230219 |   49597    8726   114161    13.1 | 73.663 % |
c |     14528 |  110330   228918 |   54556    8862   116391    13.1 | 74.395 % |
c |     15034 |  109915   227905 |   60012    9207   123608    13.4 | 74.966 % |
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 |     15297 |  109425   226747 |   36475    9363   132070    14.1 | 74.966 % |
c |     15397 |  108928   225548 |   40122    9368   131994    14.1 | 76.327 % |
c |     15547 |  108861   225391 |   44134    9505   134463    14.1 | 76.414 % |
c |     15772 |  108187   223757 |   48548    9615   136618    14.2 | 77.343 % |
c |     16110 |  108184   223750 |   53403    9952   143364    14.4 | 77.347 % |
c |     16616 |  107846   222930 |   58743   10285   150811    14.7 | 77.809 % |
c |     17375 |  107492   222096 |   64617   10880   162733    15.0 | 78.273 % |
c |     18516 |  106409   219476 |   71079   11485   183931    16.0 | 79.751 % |
c |     20224 |  105563   217441 |   78187   12695   231153    18.2 | 80.890 % |
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 |     22454 |  104461   214676 |   34820   14284   295984    20.7 | 80.890 % |
c |     22554 |  104247   214159 |   38302   14343   296650    20.7 | 82.669 % |
c |     22704 |  104230   214116 |   42132   14478   302277    20.9 | 82.695 % |
c |     22929 |  104077   213747 |   46345   14609   305744    20.9 | 82.903 % |
c |     23266 |  103810   213088 |   50979   14674   310610    21.2 | 83.278 % |
c |     23772 |  103661   212727 |   56077   15056   324943    21.6 | 83.483 % |
c |     24531 |  103661   212727 |   61685   15815   342397    21.7 | 83.483 % |
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 |     24866 |  103578   212555 |   34526   15940   354982    22.3 | 83.483 % |
c |     24966 |  103452   212229 |   37978   15957   356178    22.3 | 83.832 % |
c |     25116 |  103157   211504 |   41776   15858   355829    22.4 | 84.245 % |
c |     25342 |  103098   211357 |   45954   15982   361200    22.6 | 84.328 % |
c |     25679 |  103060   211263 |   50549   16275   374557    23.0 | 84.383 % |
c |     26186 |  103044   211225 |   55604   16717   403210    24.1 | 84.404 % |
c |     26946 |  102964   211037 |   61164   17402   448444    25.8 | 84.509 % |
c |     28085 |  102796   210627 |   67281   18302   513844    28.1 | 84.741 % |
c |     29794 |  102287   209397 |   74009   19277   595883    30.9 | 85.430 % |
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 |     30805 |  102185   209122 |   34061   19877   649107    32.7 | 85.430 % |
c |     30905 |  102181   209112 |   37467   19960   650513    32.6 | 85.578 % |
c |     31055 |  102181   209112 |   41213   20110   656361    32.6 | 85.578 % |
c |     31280 |  102181   209112 |   45335   20335   662267    32.6 | 85.578 % |
c |     31617 |  102139   209012 |   49868   20565   689479    33.5 | 85.635 % |
c |     32123 |  102135   209002 |   54855   21042   708226    33.7 | 85.640 % |
c |     32883 |  102044   208779 |   60341   21692   763522    35.2 | 85.765 % |
c |     34023 |  101908   208436 |   66375   22590   857752    38.0 | 85.961 % |
c |     35731 |  101761   208078 |   73012   24035   977376    40.7 | 86.166 % |
c |     38294 |  101248   206822 |   80314   25704  1211706    47.1 | 86.880 % |
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 |     40062 |  101189   206683 |   33729   27299  1370590    50.2 | 86.880 % |
c |     40164 |  101153   206593 |   37101   27290  1368576    50.1 | 87.022 % |
c |     40314 |  101153   206593 |   40812   27440  1373157    50.0 | 87.022 % |
c |     40539 |  101153   206593 |   44893   27665  1390604    50.3 | 87.022 % |
c |     40877 |  101147   206579 |   49382   27982  1417890    50.7 | 87.029 % |
c |     41383 |  101089   206432 |   54320   28284  1476102    52.2 | 87.111 % |
c |     42142 |  101046   206333 |   59752   28842  1548069    53.7 | 87.164 % |
c |     43281 |  101030   206295 |   65728   29940  1653263    55.2 | 87.185 % |
c ==============================================================================
c Found solution: -46
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43660 |  101019   206233 |   33673   30108  1656622    55.0 | 87.185 % |
c |     43762 |  100999   206179 |   37040   30194  1661991    55.0 | 87.234 % |
c |     43912 |  100999   206179 |   40744   30344  1674049    55.2 | 87.234 % |
c |     44138 |  100999   206179 |   44818   30570  1677140    54.9 | 87.234 % |
c |     44476 |  100999   206179 |   49300   30908  1697757    54.9 | 87.234 % |
c |     44983 |  100999   206179 |   54230   31415  1748048    55.6 | 87.234 % |
c |     45742 |  100961   206093 |   59653   32036  1808118    56.4 | 87.281 % |
c |     46881 |  100961   206093 |   65619   33175  1962362    59.2 | 87.281 % |
c |     48589 |  100961   206093 |   72181   34883  2133447    61.2 | 87.281 % |
c |     51151 |  100916   205984 |   79399   37289  2446159    65.6 | 87.343 % |
c |     54995 |  100889   205925 |   87339   40682  2985421    73.4 | 87.374 % |
c |     60761 |  100889   205925 |   96072   46448  3854427    83.0 | 87.374 % |
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 |     65334 |  100853   205854 |   33617   50820  4571720    90.0 | 87.374 % |
c |     65434 |  100853   205854 |   36978   50920  4575895    89.9 | 87.450 % |
c |     65584 |  100853   205854 |   40676   51070  4590180    89.9 | 87.450 % |
c |     65809 |  100853   205854 |   44744   51295  4602588    89.7 | 87.450 % |
c |     66148 |  100853   205854 |   49218   51634  4624017    89.6 | 87.450 % |
c |     66654 |  100853   205854 |   54140   52140  4670967    89.6 | 87.450 % |
c |     67414 |  100814   205757 |   59554   52773  4715984    89.4 | 87.506 % |
c |     68553 |  100814   205757 |   65510   53912  4839522    89.8 | 87.506 % |
c |     70261 |  100814   205757 |   72061   55620  5031215    90.5 | 87.506 % |
c |     72824 |  100814   205757 |   79267   58183  5325863    91.5 | 87.506 % |
c |     76668 |  100814   205757 |   87193   62027  5737838    92.5 | 87.506 % |
c |     82434 |  100720   205535 |   95913   67266  6413842    95.4 | 87.630 % |
c |     91084 |  100718   205529 |  105504   75912  7268264    95.7 | 87.634 % |
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 |     94590 |  100693   205448 |   33564   79088  7509816    95.0 | 87.634 % |
c |     94690 |  100693   205448 |   36920   19014  1203514    63.3 | 87.669 % |
c |     94840 |  100693   205448 |   40612   19164  1215224    63.4 | 87.669 % |
c |     95066 |  100610   205251 |   44673   19386  1226784    63.3 | 87.776 % |
c |     95404 |  100605   205238 |   49141   19716  1247119    63.3 | 87.784 % |
c |     95910 |  100605   205238 |   54055   20222  1293892    64.0 | 87.784 % |
c |     96671 |  100605   205238 |   59460   20983  1362659    64.9 | 87.784 % |
c |     97810 |  100602   205231 |   65406   22119  1452373    65.7 | 87.788 % |
c |     99519 |  100602   205231 |   71947   23828  1570680    65.9 | 87.788 % |
c |    102082 |  100602   205231 |   79142   26391  1796590    68.1 | 87.788 % |
c |    105926 |  100524   205033 |   87056   30221  2254790    74.6 | 87.904 % |
c |    111693 |  100513   205008 |   95762   35977  2865103    79.6 | 87.917 % |
c |    120342 |  100496   204969 |  105338   44621  3803842    85.2 | 87.939 % |
c |    133316 |  100496   204969 |  115872   57595  5193648    90.2 | 87.939 % |
c |    152777 |  100477   204922 |  127459   77043  7291374    94.6 | 87.966 % |
c |    181969 |  100467   204900 |  140205  106227 10898164   102.6 | 87.978 % |
c |    225758 |  100436   204820 |  154225  149983 15472459   103.2 | 88.024 % |
c |    291443 |  100430   204806 |  169648   36460  2449536    67.2 | 88.032 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 -C6

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/8492/stat): 8492 (minisat+_script) R 8491 8492 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785328358 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8492/statm): 174 3 169 147 0 27 0
[pid=8492] 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=8493
New process pid=8494
New process pid=8495
execve syscall for /bin/sed executable
One traced child (pid=8494) 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=8495) exited with status: 0
One traced child (pid=8493) exited with status: 0
New process pid=8496
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-frb53-24-1.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5916 0 0 0 953 25 0 0 25 0 1 0 1785328363 25022464 5903 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6109 5903 145 145 0 5964 0
[pid=8496] vsize: 24436
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 26560

[startup+20.0044 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5916 0 0 0 1953 25 0 0 25 0 1 0 1785328363 25022464 5903 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6109 5903 145 145 0 5964 0
[pid=8496] vsize: 24436
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 26560

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 2952 26 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 27124

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 3952 26 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223120 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 39.79
Current children cumulated vsize (Kb) 27124

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 4951 27 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 27124

[startup+60.0085 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 5951 27 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 27124

[startup+70.0092 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 6950 27 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 69.78
Current children cumulated vsize (Kb) 27124

[startup+80.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5998 0 0 0 7950 27 0 0 25 0 1 0 1785328363 25600000 5985 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5985 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 27124

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5998 0 0 0 8950 28 0 0 25 0 1 0 1785328363 25600000 5985 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6250 5985 145 145 0 6105 0
[pid=8496] vsize: 25000
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 27124

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6005 0 0 0 9950 28 0 0 25 0 1 0 1785328363 25624576 5992 4294967295 134512640 135094434 3221224448 3221221536 134519219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6256 5992 145 145 0 6111 0
[pid=8496] vsize: 25024
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 27148

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6023 0 0 0 10949 28 0 0 25 0 1 0 1785328363 25702400 6010 4294967295 134512640 135094434 3221224448 3221223152 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6275 6010 145 145 0 6130 0
[pid=8496] vsize: 25100
Current children cumulated CPU time (s) 109.78
Current children cumulated vsize (Kb) 27224

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6202 0 0 0 11946 30 0 0 25 0 1 0 1785328363 26226688 6139 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6403 6139 145 145 0 6258 0
[pid=8496] vsize: 25612
Current children cumulated CPU time (s) 119.77
Current children cumulated vsize (Kb) 27736

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6524 0 0 0 12942 32 0 0 25 0 1 0 1785328363 27389952 6410 4294967295 134512640 135094434 3221224448 3221223108 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 6687 6410 145 145 0 6542 0
[pid=8496] vsize: 26748
Current children cumulated CPU time (s) 129.75
Current children cumulated vsize (Kb) 28872

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6989 0 0 0 13934 35 0 0 25 0 1 0 1785328363 29069312 6824 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 7097 6824 145 145 0 6952 0
[pid=8496] vsize: 28388
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 30512

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 7481 0 0 0 14925 39 0 0 25 0 1 0 1785328363 31068160 7316 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 7585 7316 145 145 0 7440 0
[pid=8496] vsize: 30340
Current children cumulated CPU time (s) 149.65
Current children cumulated vsize (Kb) 32464

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 7995 0 0 0 15917 43 0 0 25 0 1 0 1785328363 32743424 7729 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 7994 7729 145 145 0 7849 0
[pid=8496] vsize: 31976
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 34100

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 8521 0 0 0 16909 46 0 0 25 0 1 0 1785328363 35012608 8255 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 8548 8255 145 145 0 8403 0
[pid=8496] vsize: 34192
Current children cumulated CPU time (s) 169.56
Current children cumulated vsize (Kb) 36316

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 9032 0 0 0 17899 49 0 0 25 0 1 0 1785328363 37089280 8766 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 9055 8766 145 145 0 8910 0
[pid=8496] vsize: 36220
Current children cumulated CPU time (s) 179.49
Current children cumulated vsize (Kb) 38344

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 9613 0 0 0 18891 53 0 0 25 0 1 0 1785328363 39452672 9347 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 9632 9347 145 145 0 9487 0
[pid=8496] vsize: 38528
Current children cumulated CPU time (s) 189.45
Current children cumulated vsize (Kb) 40652

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 10215 0 0 0 19879 59 0 0 25 0 1 0 1785328363 41906176 9949 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 10231 9949 145 145 0 10086 0
[pid=8496] vsize: 40924
Current children cumulated CPU time (s) 199.39
Current children cumulated vsize (Kb) 43048

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 10750 0 0 0 20868 64 0 0 25 0 1 0 1785328363 44085248 10484 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 10763 10484 145 145 0 10618 0
[pid=8496] vsize: 43052
Current children cumulated CPU time (s) 209.33
Current children cumulated vsize (Kb) 45176

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 11206 0 0 0 21860 68 0 0 25 0 1 0 1785328363 45731840 10889 4294967295 134512640 135094434 3221224448 3221222976 134780519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 11165 10889 145 145 0 11020 0
[pid=8496] vsize: 44660
Current children cumulated CPU time (s) 219.29
Current children cumulated vsize (Kb) 46784

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 11586 0 0 0 22851 72 0 0 25 0 1 0 1785328363 47276032 11269 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 11542 11269 145 145 0 11397 0
[pid=8496] vsize: 46168
Current children cumulated CPU time (s) 229.24
Current children cumulated vsize (Kb) 48292

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 11965 0 0 0 23844 74 0 0 25 0 1 0 1785328363 48816128 11648 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 11918 11648 145 145 0 11773 0
[pid=8496] vsize: 47672
Current children cumulated CPU time (s) 239.19
Current children cumulated vsize (Kb) 49796

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 12328 0 0 0 24836 77 0 0 25 0 1 0 1785328363 50290688 12011 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 12278 12011 145 145 0 12133 0
[pid=8496] vsize: 49112
Current children cumulated CPU time (s) 249.14
Current children cumulated vsize (Kb) 51236

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 12727 0 0 0 25828 80 0 0 25 0 1 0 1785328363 51912704 12410 4294967295 134512640 135094434 3221224448 3221223056 134781733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 12674 12410 145 145 0 12529 0
[pid=8496] vsize: 50696
Current children cumulated CPU time (s) 259.09
Current children cumulated vsize (Kb) 52820

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13064 0 0 0 26822 83 0 0 25 0 1 0 1785328363 53542912 12747 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 13072 12747 145 145 0 12927 0
[pid=8496] vsize: 52288
Current children cumulated CPU time (s) 269.06
Current children cumulated vsize (Kb) 54412

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13362 0 0 0 27817 85 0 0 25 0 1 0 1785328363 54755328 13045 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 13368 13045 145 145 0 13223 0
[pid=8496] vsize: 53472
Current children cumulated CPU time (s) 279.03
Current children cumulated vsize (Kb) 55596

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13676 0 0 0 28810 88 0 0 25 0 1 0 1785328363 56029184 13359 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 13679 13359 145 145 0 13534 0
[pid=8496] vsize: 54716
Current children cumulated CPU time (s) 288.99
Current children cumulated vsize (Kb) 56840

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13978 0 0 0 29804 90 0 0 25 0 1 0 1785328363 57253888 13661 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 13978 13661 145 145 0 13833 0
[pid=8496] vsize: 55912
Current children cumulated CPU time (s) 298.95
Current children cumulated vsize (Kb) 58036

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 30799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134556552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 308.92
Current children cumulated vsize (Kb) 59220

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 31799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 318.92
Current children cumulated vsize (Kb) 59220

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 32799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 328.92
Current children cumulated vsize (Kb) 59220

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 33799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 338.92
Current children cumulated vsize (Kb) 59220

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 34800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 348.93
Current children cumulated vsize (Kb) 59220

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 35800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 358.93
Current children cumulated vsize (Kb) 59220

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 36800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134556091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 368.93
Current children cumulated vsize (Kb) 59220

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 37800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 378.93
Current children cumulated vsize (Kb) 59220

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 38800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 388.93
Current children cumulated vsize (Kb) 59220

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 39800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 398.93
Current children cumulated vsize (Kb) 59220

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 40801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 408.94
Current children cumulated vsize (Kb) 59220

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 41801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 418.94
Current children cumulated vsize (Kb) 59220

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 42801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 428.94
Current children cumulated vsize (Kb) 59220

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 43801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 438.94
Current children cumulated vsize (Kb) 59220

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 44801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0
[pid=8496] vsize: 57096
Current children cumulated CPU time (s) 448.94
Current children cumulated vsize (Kb) 59220

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14432 0 0 0 45800 93 0 0 25 0 1 0 1785328363 58892288 14064 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14378 14064 145 145 0 14233 0
[pid=8496] vsize: 57512
Current children cumulated CPU time (s) 458.94
Current children cumulated vsize (Kb) 59636

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14827 0 0 0 46792 96 0 0 25 0 1 0 1785328363 60502016 14459 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 14771 14459 145 145 0 14626 0
[pid=8496] vsize: 59084
Current children cumulated CPU time (s) 468.89
Current children cumulated vsize (Kb) 61208

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 15236 0 0 0 47785 99 0 0 25 0 1 0 1785328363 62164992 14868 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 15177 14868 145 145 0 15032 0
[pid=8496] vsize: 60708
Current children cumulated CPU time (s) 478.85
Current children cumulated vsize (Kb) 62832

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 15591 0 0 0 48779 101 0 0 25 0 1 0 1785328363 63623168 15223 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 15533 15223 145 145 0 15388 0
[pid=8496] vsize: 62132
Current children cumulated CPU time (s) 488.81
Current children cumulated vsize (Kb) 64256

[startup+500.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 15972 0 0 0 49772 104 0 0 25 0 1 0 1785328363 65171456 15604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 15911 15604 145 145 0 15766 0
[pid=8496] vsize: 63644
Current children cumulated CPU time (s) 498.77
Current children cumulated vsize (Kb) 65768

[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 16349 0 0 0 50764 107 0 0 25 0 1 0 1785328363 66703360 15981 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 16285 15981 145 145 0 16140 0
[pid=8496] vsize: 65140
Current children cumulated CPU time (s) 508.72
Current children cumulated vsize (Kb) 67264

[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 16711 0 0 0 51758 111 0 0 25 0 1 0 1785328363 68177920 16343 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 16645 16343 145 145 0 16500 0
[pid=8496] vsize: 66580
Current children cumulated CPU time (s) 518.7
Current children cumulated vsize (Kb) 68704

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17054 0 0 0 52752 113 0 0 25 0 1 0 1785328363 69574656 16686 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 16986 16686 145 145 0 16841 0
[pid=8496] vsize: 67944
Current children cumulated CPU time (s) 528.66
Current children cumulated vsize (Kb) 70068

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17378 0 0 0 53746 116 0 0 25 0 1 0 1785328363 70893568 17010 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 17308 17010 145 145 0 17163 0
[pid=8496] vsize: 69232
Current children cumulated CPU time (s) 538.63
Current children cumulated vsize (Kb) 71356

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17663 0 0 0 54741 119 0 0 25 0 1 0 1785328363 72052736 17295 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 17591 17295 145 145 0 17446 0
[pid=8496] vsize: 70364
Current children cumulated CPU time (s) 548.61
Current children cumulated vsize (Kb) 72488

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17979 0 0 0 55736 121 0 0 25 0 1 0 1785328363 73334784 17611 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 17904 17611 145 145 0 17759 0
[pid=8496] vsize: 71616
Current children cumulated CPU time (s) 558.58
Current children cumulated vsize (Kb) 73740

[startup+570.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18216 0 0 0 56732 122 0 0 25 0 1 0 1785328363 74301440 17848 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 18140 17848 145 145 0 17995 0
[pid=8496] vsize: 72560
Current children cumulated CPU time (s) 568.55
Current children cumulated vsize (Kb) 74684

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18456 0 0 0 57727 125 0 0 25 0 1 0 1785328363 75276288 18088 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 18378 18088 145 145 0 18233 0
[pid=8496] vsize: 73512
Current children cumulated CPU time (s) 578.53
Current children cumulated vsize (Kb) 75636

[startup+590.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18718 0 0 0 58723 126 0 0 25 0 1 0 1785328363 76341248 18350 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 18638 18350 145 145 0 18493 0
[pid=8496] vsize: 74552
Current children cumulated CPU time (s) 588.5
Current children cumulated vsize (Kb) 76676

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18980 0 0 0 59719 128 0 0 25 0 1 0 1785328363 77402112 18612 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 18897 18612 145 145 0 18752 0
[pid=8496] vsize: 75588
Current children cumulated CPU time (s) 598.48
Current children cumulated vsize (Kb) 77712

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 19274 0 0 0 60714 129 0 0 25 0 1 0 1785328363 78602240 18906 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 19190 18906 145 145 0 19045 0
[pid=8496] vsize: 76760
Current children cumulated CPU time (s) 608.44
Current children cumulated vsize (Kb) 78884

[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 19533 0 0 0 61710 131 0 0 25 0 1 0 1785328363 79650816 19165 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 19446 19165 145 145 0 19301 0
[pid=8496] vsize: 77784
Current children cumulated CPU time (s) 618.42
Current children cumulated vsize (Kb) 79908

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 19793 0 0 0 62706 133 0 0 25 0 1 0 1785328363 80711680 19425 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 19705 19425 145 145 0 19560 0
[pid=8496] vsize: 78820
Current children cumulated CPU time (s) 628.4
Current children cumulated vsize (Kb) 80944

[startup+640.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20031 0 0 0 63701 135 0 0 25 0 1 0 1785328363 81678336 19663 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 19941 19663 145 145 0 19796 0
[pid=8496] vsize: 79764
Current children cumulated CPU time (s) 638.37
Current children cumulated vsize (Kb) 81888

[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20301 0 0 0 64696 137 0 0 25 0 1 0 1785328363 82776064 19933 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 20209 19933 145 145 0 20064 0
[pid=8496] vsize: 80836
Current children cumulated CPU time (s) 648.34
Current children cumulated vsize (Kb) 82960

[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20570 0 0 0 65691 139 0 0 25 0 1 0 1785328363 83869696 20202 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 20476 20202 145 145 0 20331 0
[pid=8496] vsize: 81904
Current children cumulated CPU time (s) 658.31
Current children cumulated vsize (Kb) 84028

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20834 0 0 0 66685 142 0 0 25 0 1 0 1785328363 85471232 20466 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 20867 20466 145 145 0 20722 0
[pid=8496] vsize: 83468
Current children cumulated CPU time (s) 668.28
Current children cumulated vsize (Kb) 85592

[startup+680.052 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21114 0 0 0 67680 144 0 0 25 0 1 0 1785328363 86605824 20746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 21144 20746 145 145 0 20999 0
[pid=8496] vsize: 84576
Current children cumulated CPU time (s) 678.25
Current children cumulated vsize (Kb) 86700

[startup+690.053 s]
Raw data (loadavg): 1.06 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21368 0 0 0 68676 146 0 0 25 0 1 0 1785328363 87638016 21000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 21396 21000 145 145 0 21251 0
[pid=8496] vsize: 85584
Current children cumulated CPU time (s) 688.23
Current children cumulated vsize (Kb) 87708

[startup+700.053 s]
Raw data (loadavg): 1.05 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21613 0 0 0 69672 147 0 0 25 0 1 0 1785328363 88629248 21245 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 21638 21245 145 145 0 21493 0
[pid=8496] vsize: 86552
Current children cumulated CPU time (s) 698.2
Current children cumulated vsize (Kb) 88676

[startup+710.054 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21883 0 0 0 70667 149 0 0 25 0 1 0 1785328363 89722880 21515 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 21905 21515 145 145 0 21760 0
[pid=8496] vsize: 87620
Current children cumulated CPU time (s) 708.17
Current children cumulated vsize (Kb) 89744

[startup+720.055 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22152 0 0 0 71662 151 0 0 25 0 1 0 1785328363 90816512 21784 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 22172 21784 145 145 0 22027 0
[pid=8496] vsize: 88688
Current children cumulated CPU time (s) 718.14
Current children cumulated vsize (Kb) 90812

[startup+730.056 s]
Raw data (loadavg): 1.03 0.99 0.92 3/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22427 0 0 0 72658 153 0 0 25 0 1 0 1785328363 91934720 22059 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 22445 22059 145 145 0 22300 0
[pid=8496] vsize: 89780
Current children cumulated CPU time (s) 728.12
Current children cumulated vsize (Kb) 91904

[startup+740.057 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22646 0 0 0 73653 154 0 0 25 0 1 0 1785328363 92823552 22278 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 22662 22278 145 145 0 22517 0
[pid=8496] vsize: 90648
Current children cumulated CPU time (s) 738.08
Current children cumulated vsize (Kb) 92772

[startup+750.058 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22883 0 0 0 74648 156 0 0 25 0 1 0 1785328363 93790208 22515 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 22898 22515 145 145 0 22753 0
[pid=8496] vsize: 91592
Current children cumulated CPU time (s) 748.05
Current children cumulated vsize (Kb) 93716

[startup+760.058 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23118 0 0 0 75644 158 0 0 25 0 1 0 1785328363 94744576 22750 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 23131 22750 145 145 0 22986 0
[pid=8496] vsize: 92524
Current children cumulated CPU time (s) 758.03
Current children cumulated vsize (Kb) 94648

[startup+770.059 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23356 0 0 0 76641 159 0 0 25 0 1 0 1785328363 95707136 22988 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 23366 22988 145 145 0 23221 0
[pid=8496] vsize: 93464
Current children cumulated CPU time (s) 768.01
Current children cumulated vsize (Kb) 95588

[startup+780.061 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23562 0 0 0 77637 161 0 0 25 0 1 0 1785328363 96542720 23194 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 23570 23194 145 145 0 23425 0
[pid=8496] vsize: 94280
Current children cumulated CPU time (s) 777.99
Current children cumulated vsize (Kb) 96404

[startup+790.062 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23760 0 0 0 78633 162 0 0 25 0 1 0 1785328363 97345536 23392 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 23766 23392 145 145 0 23621 0
[pid=8496] vsize: 95064
Current children cumulated CPU time (s) 787.96
Current children cumulated vsize (Kb) 97188

[startup+800.061 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24000 0 0 0 79629 164 0 0 25 0 1 0 1785328363 98320384 23632 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 24004 23632 145 145 0 23859 0
[pid=8496] vsize: 96016
Current children cumulated CPU time (s) 797.94
Current children cumulated vsize (Kb) 98140

[startup+810.062 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24242 0 0 0 80625 166 0 0 25 0 1 0 1785328363 99303424 23874 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 24244 23874 145 145 0 24099 0
[pid=8496] vsize: 96976
Current children cumulated CPU time (s) 807.92
Current children cumulated vsize (Kb) 99100

[startup+820.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24445 0 0 0 81621 168 0 0 25 0 1 0 1785328363 100126720 24077 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 24445 24077 145 145 0 24300 0
[pid=8496] vsize: 97780
Current children cumulated CPU time (s) 817.9
Current children cumulated vsize (Kb) 99904

[startup+830.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24624 0 0 0 82619 169 0 0 25 0 1 0 1785328363 100851712 24256 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 24622 24256 145 145 0 24477 0
[pid=8496] vsize: 98488
Current children cumulated CPU time (s) 827.89
Current children cumulated vsize (Kb) 100612

[startup+840.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24807 0 0 0 83614 171 0 0 25 0 1 0 1785328363 101593088 24439 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 24803 24439 145 145 0 24658 0
[pid=8496] vsize: 99212
Current children cumulated CPU time (s) 837.86
Current children cumulated vsize (Kb) 101336

[startup+850.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24974 0 0 0 84610 173 0 0 25 0 1 0 1785328363 102273024 24606 4294967295 134512640 135094434 3221224448 3221223040 134557143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 24969 24606 145 145 0 24824 0
[pid=8496] vsize: 99876
Current children cumulated CPU time (s) 847.84
Current children cumulated vsize (Kb) 102000

[startup+860.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25142 0 0 0 85607 174 0 0 25 0 1 0 1785328363 102952960 24774 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 25135 24774 145 145 0 24990 0
[pid=8496] vsize: 100540
Current children cumulated CPU time (s) 857.82
Current children cumulated vsize (Kb) 102664

[startup+870.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25335 0 0 0 86604 175 0 0 25 0 1 0 1785328363 103739392 24967 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 25327 24967 145 145 0 25182 0
[pid=8496] vsize: 101308
Current children cumulated CPU time (s) 867.8
Current children cumulated vsize (Kb) 103432

[startup+880.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25525 0 0 0 87601 177 0 0 25 0 1 0 1785328363 104505344 25157 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 25514 25157 145 145 0 25369 0
[pid=8496] vsize: 102056
Current children cumulated CPU time (s) 877.79
Current children cumulated vsize (Kb) 104180

[startup+890.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25704 0 0 0 88598 178 0 0 25 0 1 0 1785328363 105234432 25336 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 25692 25336 145 145 0 25547 0
[pid=8496] vsize: 102768
Current children cumulated CPU time (s) 887.77
Current children cumulated vsize (Kb) 104892

[startup+900.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25892 0 0 0 89595 179 0 0 25 0 1 0 1785328363 106016768 25524 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 25883 25524 145 145 0 25738 0
[pid=8496] vsize: 103532
Current children cumulated CPU time (s) 897.75
Current children cumulated vsize (Kb) 105656

[startup+910.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26078 0 0 0 90592 181 0 0 25 0 1 0 1785328363 106770432 25710 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 26067 25710 145 145 0 25922 0
[pid=8496] vsize: 104268
Current children cumulated CPU time (s) 907.74
Current children cumulated vsize (Kb) 106392

[startup+920.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26264 0 0 0 91588 182 0 0 25 0 1 0 1785328363 107520000 25896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 26250 25896 145 145 0 26105 0
[pid=8496] vsize: 105000
Current children cumulated CPU time (s) 917.71
Current children cumulated vsize (Kb) 107124

[startup+930.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26436 0 0 0 92585 184 0 0 25 0 1 0 1785328363 108224512 26068 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 26422 26068 145 145 0 26277 0
[pid=8496] vsize: 105688
Current children cumulated CPU time (s) 927.7
Current children cumulated vsize (Kb) 107812

[startup+940.074 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26615 0 0 0 93582 185 0 0 25 0 1 0 1785328363 108949504 26247 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 26599 26247 145 145 0 26454 0
[pid=8496] vsize: 106396
Current children cumulated CPU time (s) 937.68
Current children cumulated vsize (Kb) 108520

[startup+950.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26777 0 0 0 94580 186 0 0 25 0 1 0 1785328363 109600768 26409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 26758 26409 145 145 0 26613 0
[pid=8496] vsize: 107032
Current children cumulated CPU time (s) 947.67
Current children cumulated vsize (Kb) 109156

[startup+960.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26948 0 0 0 95576 188 0 0 25 0 1 0 1785328363 110346240 26580 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 26940 26580 145 145 0 26795 0
[pid=8496] vsize: 107760
Current children cumulated CPU time (s) 957.65
Current children cumulated vsize (Kb) 109884

[startup+970.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27097 0 0 0 96575 189 0 0 25 0 1 0 1785328363 110956544 26729 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27089 26729 145 145 0 26944 0
[pid=8496] vsize: 108356
Current children cumulated CPU time (s) 967.65
Current children cumulated vsize (Kb) 110480

[startup+980.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27223 0 0 0 97572 189 0 0 25 0 1 0 1785328363 111472640 26855 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27215 26855 145 145 0 27070 0
[pid=8496] vsize: 108860
Current children cumulated CPU time (s) 977.62
Current children cumulated vsize (Kb) 110984

[startup+990.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27362 0 0 0 98569 191 0 0 25 0 1 0 1785328363 112033792 26994 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27352 26994 145 145 0 27207 0
[pid=8496] vsize: 109408
Current children cumulated CPU time (s) 987.61
Current children cumulated vsize (Kb) 111532

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27506 0 0 0 99567 192 0 0 25 0 1 0 1785328363 112656384 27138 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27504 27138 145 145 0 27359 0
[pid=8496] vsize: 110016
Current children cumulated CPU time (s) 997.6
Current children cumulated vsize (Kb) 112140

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27646 0 0 0 100565 194 0 0 25 0 1 0 1785328363 113217536 27278 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27641 27278 145 145 0 27496 0
[pid=8496] vsize: 110564
Current children cumulated CPU time (s) 1007.6
Current children cumulated vsize (Kb) 112688

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27789 0 0 0 101562 195 0 0 25 0 1 0 1785328363 113799168 27421 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27783 27421 145 145 0 27638 0
[pid=8496] vsize: 111132
Current children cumulated CPU time (s) 1017.58
Current children cumulated vsize (Kb) 113256

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.92 3/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27927 0 0 0 102559 196 0 0 25 0 1 0 1785328363 114356224 27559 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 27919 27559 145 145 0 27774 0
[pid=8496] vsize: 111676
Current children cumulated CPU time (s) 1027.56
Current children cumulated vsize (Kb) 113800

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28058 0 0 0 103557 197 0 0 25 0 1 0 1785328363 114884608 27690 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28048 27690 145 145 0 27903 0
[pid=8496] vsize: 112192
Current children cumulated CPU time (s) 1037.55
Current children cumulated vsize (Kb) 114316

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28191 0 0 0 104555 198 0 0 25 0 1 0 1785328363 115421184 27823 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28179 27823 145 145 0 28034 0
[pid=8496] vsize: 112716
Current children cumulated CPU time (s) 1047.54
Current children cumulated vsize (Kb) 114840

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 105555 198 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1057.54
Current children cumulated vsize (Kb) 114928

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 106555 198 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1067.54
Current children cumulated vsize (Kb) 114928

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 107555 198 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1077.54
Current children cumulated vsize (Kb) 114928

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 108554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221222912 134780543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1087.54
Current children cumulated vsize (Kb) 114928

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 109553 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1097.53
Current children cumulated vsize (Kb) 114928

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 110553 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1107.53
Current children cumulated vsize (Kb) 114928

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 111553 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1117.53
Current children cumulated vsize (Kb) 114928

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 112554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1127.54
Current children cumulated vsize (Kb) 114928

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 113554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1137.54
Current children cumulated vsize (Kb) 114928

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 114554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1147.54
Current children cumulated vsize (Kb) 114928

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 115554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1157.54
Current children cumulated vsize (Kb) 114928

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 116554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1167.54
Current children cumulated vsize (Kb) 114928

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 117555 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1177.55
Current children cumulated vsize (Kb) 114928

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 118555 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1187.55
Current children cumulated vsize (Kb) 114928

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 119555 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1197.55
Current children cumulated vsize (Kb) 114928

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 120556 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1207.56
Current children cumulated vsize (Kb) 114928



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 8496
Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8492/statm): 531 226 485 147 0 384 0
[pid=8492] vsize: 2124
Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 120556 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0
[pid=8496] vsize: 112804
Current children cumulated CPU time (s) 1207.56
Current children cumulated vsize (Kb) 114928

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1207.61
CPU user time (s): 1205.56
CPU system time (s): 2.04869
CPU usage (%): 99.7901
Max. virtual memory (cumulated for all children) (Kb): 114928

Verifier Data

ERROR: no interpretation found !