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/frb50-23-opb/normalized-frb50-23-1.opb
MD5SUMed1ca962177baf0f135b785abad8adea
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 1150
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 1150
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 1150
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 benchmark1195.06
Number of variables1150
Total number of constraints80072
Number of constraints which are clauses80072
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 2301

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        908976 kB
Buffers:         36008 kB
Cached:          57204 kB
SwapCached:        764 kB
Active:          68672 kB
Inactive:        27204 kB
HighTotal:      131008 kB
HighFree:        71204 kB
LowTotal:       903652 kB
LowFree:        837772 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            24252 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:08:36 (client local time) WITH STATUS 10 IN 1207.63 SECONDS
stats: 2705 7 1207.63 10

Solver Data

c Parsing PB file...
c Converting 80072 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 |   80072   160144 |   26690       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  147988   319466 |   49329       0        0     nan |  0.000 % |
c |       100 |  147362   318162 |   54261      77      551     7.2 |  0.736 % |
c |       250 |  146841   317054 |   59688     209     2448    11.7 |  1.369 % |
c |       475 |  145811   314812 |   65656     398     4382    11.0 |  2.680 % |
c |       812 |  144010   310871 |   72222     677     8303    12.3 |  4.995 % |
c |      1318 |  141157   304558 |   79444    1060    12573    11.9 |  8.737 % |
c |      2077 |  136776   294746 |   87389    1627    19630    12.1 | 14.610 % |
c |      3216 |  131215   282210 |   96128    2497    29631    11.9 | 22.142 % |
c |      4924 |  123727   265107 |  105741    3779    49504    13.1 | 32.476 % |
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 |      6427 |  116683   248991 |   38894    4766    61496    12.9 | 32.476 % |
c |      6527 |  116204   247870 |   42783    4831    62291    12.9 | 43.100 % |
c |      6677 |  115663   246594 |   47061    4934    63665    12.9 | 43.849 % |
c |      6902 |  114831   244655 |   51767    5110    65775    12.9 | 44.973 % |
c |      7239 |  113564   241690 |   56944    5351    69474    13.0 | 46.827 % |
c |      7746 |  111539   236942 |   62639    5688    74185    13.0 | 49.645 % |
c |      8505 |  108258   229196 |   68903    6014    79861    13.3 | 54.380 % |
c |      9645 |  106402   224792 |   75793    6813    92319    13.6 | 57.095 % |
c |     11355 |  103049   216804 |   83372    7947   113001    14.2 | 62.021 % |
c |     13917 |   98383   205681 |   91710    9480   147925    15.6 | 68.784 % |
c |     17761 |   94811   197102 |  100881   12081   211420    17.5 | 74.113 % |
c |     23527 |   91940   190193 |  110969   16325   396509    24.3 | 78.405 % |
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 |     26517 |   91505   189103 |   30501   18993   511336    26.9 | 78.405 % |
c |     26617 |   91453   188977 |   33551   19046   513223    26.9 | 79.155 % |
c |     26767 |   91403   188856 |   36906   19147   514654    26.9 | 79.230 % |
c |     26993 |   91347   188722 |   40596   19332   517806    26.8 | 79.308 % |
c |     27330 |   91347   188722 |   44656   19669   531077    27.0 | 79.308 % |
c |     27836 |   91347   188722 |   49122   20175   549790    27.3 | 79.308 % |
c |     28595 |   91336   188697 |   54034   20920   586573    28.0 | 79.323 % |
c |     29734 |   91040   187971 |   59437   21902   671987    30.7 | 79.772 % |
c |     31442 |   91021   187926 |   65381   23576   759400    32.2 | 79.800 % |
c |     34004 |   90924   187692 |   71919   26012   920916    35.4 | 79.947 % |
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 |     37368 |   90426   186513 |   30142   28875  1073664    37.2 | 79.947 % |
c |     37468 |   90272   186133 |   33156   28788  1071210    37.2 | 80.912 % |
c |     37618 |   90272   186133 |   36471   28938  1078094    37.3 | 80.912 % |
c |     37845 |   90055   185604 |   40119   28990  1084507    37.4 | 81.229 % |
c |     38182 |   89765   184919 |   44130   29091  1093267    37.6 | 81.654 % |
c |     38690 |   89677   184699 |   48543   29419  1114490    37.9 | 81.794 % |
c |     39449 |   89637   184597 |   53398   30143  1175417    39.0 | 81.859 % |
c |     40590 |   89554   184394 |   58738   31209  1251534    40.1 | 81.988 % |
c |     42298 |   89419   184073 |   64612   32883  1358367    41.3 | 82.189 % |
c |     44861 |   89408   184048 |   71073   35430  1659938    46.9 | 82.204 % |
c |     48706 |   89194   183528 |   78180   38940  1937517    49.8 | 82.527 % |
c |     54473 |   89111   183331 |   85998   44007  2548488    57.9 | 82.650 % |
c |     63122 |   88944   182914 |   94598   52476  3364323    64.1 | 82.920 % |
c |     76097 |   88814   182580 |  104058   65300  4943713    75.7 | 83.140 % |
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 |     77862 |   88826   182643 |   29608   67005  5167051    77.1 | 83.140 % |
c |     77964 |   88784   182545 |   32568   67090  5171321    77.1 | 83.214 % |
c |     78114 |   88784   182545 |   35825   67240  5180522    77.0 | 83.214 % |
c |     78339 |   88743   182450 |   39408   67391  5196716    77.1 | 83.270 % |
c |     78678 |   88708   182365 |   43349   67686  5220332    77.1 | 83.324 % |
c |     79184 |   88704   182355 |   47683   68174  5263297    77.2 | 83.330 % |
c |     79943 |   88664   182255 |   52452   68714  5301058    77.1 | 83.395 % |
c |     81082 |   88585   182068 |   57697   69580  5394262    77.5 | 83.511 % |
c |     82790 |   88519   181910 |   63467   71223  5554743    78.0 | 83.610 % |
c |     85352 |   88517   181906 |   69814   73749  5848295    79.3 | 83.612 % |
c |     89198 |   88366   181535 |   76795   77183  6388766    82.8 | 83.847 % |
c |     94964 |   88258   181285 |   84475   82844  7485378    90.4 | 83.993 % |
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 |     98263 |   88158   181016 |   29386   85817  7763842    90.5 | 83.993 % |
c |     98364 |   88158   181016 |   32324   22455  2013545    89.7 | 84.158 % |
c |     98514 |   88158   181016 |   35557   22605  2027056    89.7 | 84.158 % |
c |     98740 |   88158   181016 |   39112   22831  2038443    89.3 | 84.158 % |
c |     99077 |   88158   181016 |   43024   23168  2078602    89.7 | 84.158 % |
c |     99583 |   88158   181016 |   47326   23674  2126008    89.8 | 84.158 % |
c |    100342 |   88158   181016 |   52059   24433  2186274    89.5 | 84.158 % |
c |    101484 |   88150   180996 |   57265   25550  2295749    89.9 | 84.170 % |
c |    103195 |   88096   180868 |   62991   27218  2436552    89.5 | 84.250 % |
c |    105757 |   88096   180868 |   69290   29780  2702781    90.8 | 84.250 % |
c |    109601 |   88046   180746 |   76219   33602  3048134    90.7 | 84.328 % |
c |    115367 |   88046   180746 |   83841   39368  3668323    93.2 | 84.328 % |
c |    124016 |   88046   180746 |   92225   48017  4913028   102.3 | 84.328 % |
c |    136990 |   87949   180511 |  101448   60968  6988775   114.6 | 84.476 % |
c |    156451 |   87902   180392 |  111593   80363  9395711   116.9 | 84.553 % |
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 |    166657 |   87834   180240 |   29278   90507 10717436   118.4 | 84.553 % |
c |    166757 |   87834   180240 |   32205   23788  1691897    71.1 | 84.668 % |
c |    166907 |   87789   180133 |   35426   23933  1702187    71.1 | 84.735 % |
c |    167132 |   87789   180133 |   38969   24158  1720163    71.2 | 84.735 % |
c |    167470 |   87789   180133 |   42865   24496  1758488    71.8 | 84.735 % |
c |    167976 |   87628   179729 |   47152   24984  1795588    71.9 | 84.980 % |
c |    168736 |   87561   179560 |   51867   25707  1847965    71.9 | 85.083 % |
c |    169875 |   87561   179560 |   57054   26846  1997820    74.4 | 85.083 % |
c |    171583 |   87555   179546 |   62759   28551  2143274    75.1 | 85.092 % |
c |    174145 |   87543   179518 |   69035   31109  2357991    75.8 | 85.109 % |
c |    177989 |   87543   179518 |   75939   34953  2874390    82.2 | 85.109 % |
c |    183757 |   87535   179500 |   83533   40698  3596006    88.4 | 85.120 % |
c |    192406 |   87535   179500 |   91886   49347  4807829    97.4 | 85.120 % |
c |    205380 |   87464   179337 |  101075   62280  6436341   103.3 | 85.217 % |
c |    224841 |   87464   179337 |  111183   81741  9073077   111.0 | 85.217 % |
c |    254033 |   87464   179337 |  122301  110933 13542456   122.1 | 85.217 % |
c |    297822 |   87384   179141 |  134531  154625 20442372   132.2 | 85.339 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 C1036 -C1035 C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 C901 -C900 -C899 -C898 -C897 -C896 C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496

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/9676/stat): 9676 (minisat+_script) R 9675 9676 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843520848 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9676/statm): 174 3 169 147 0 27 0
[pid=9676] 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=9677
New process pid=9678
New process pid=9679
execve syscall for /bin/sed executable
One traced child (pid=9678) 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=9679) exited with status: 0
One traced child (pid=9677) exited with status: 0
New process pid=9680
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-frb50-23-1.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5064 0 0 0 959 22 0 0 25 0 1 0 1843520853 21643264 5051 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5284 5051 145 145 0 5139 0
[pid=9680] vsize: 21136
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 23260

[startup+20.0059 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5064 0 0 0 1959 22 0 0 25 0 1 0 1843520853 21643264 5051 4294967295 134512640 135094434 3221224448 3221223152 134558999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5284 5051 145 145 0 5139 0
[pid=9680] vsize: 21136
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 23260

[startup+30.0077 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5064 0 0 0 2959 23 0 0 25 0 1 0 1843520853 21643264 5051 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5284 5051 145 145 0 5139 0
[pid=9680] vsize: 21136
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 23260

[startup+40.0085 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5064 0 0 0 3958 23 0 0 25 0 1 0 1843520853 21643264 5051 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5284 5051 145 145 0 5139 0
[pid=9680] vsize: 21136
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 23260

[startup+50.0093 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5064 0 0 0 4958 23 0 0 25 0 1 0 1843520853 21643264 5051 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5284 5051 145 145 0 5139 0
[pid=9680] vsize: 21136
Current children cumulated CPU time (s) 49.82
Current children cumulated vsize (Kb) 23260

[startup+60.0111 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5344 0 0 0 5957 24 0 0 25 0 1 0 1843520853 23666688 5331 4294967295 134512640 135094434 3221224448 3221223152 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5778 5331 145 145 0 5633 0
[pid=9680] vsize: 23112
Current children cumulated CPU time (s) 59.82
Current children cumulated vsize (Kb) 25236

[startup+70.012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5344 0 0 0 6956 25 0 0 25 0 1 0 1843520853 23666688 5331 4294967295 134512640 135094434 3221224448 3221223152 134558999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5778 5331 145 145 0 5633 0
[pid=9680] vsize: 23112
Current children cumulated CPU time (s) 69.82
Current children cumulated vsize (Kb) 25236

[startup+80.0138 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5345 0 0 0 7955 25 0 0 25 0 1 0 1843520853 23666688 5332 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5778 5332 145 145 0 5633 0
[pid=9680] vsize: 23112
Current children cumulated CPU time (s) 79.81
Current children cumulated vsize (Kb) 25236

[startup+90.0146 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5345 0 0 0 8955 26 0 0 25 0 1 0 1843520853 23666688 5332 4294967295 134512640 135094434 3221224448 3221223108 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5778 5332 145 145 0 5633 0
[pid=9680] vsize: 23112
Current children cumulated CPU time (s) 89.82
Current children cumulated vsize (Kb) 25236

[startup+100.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5451 0 0 0 9954 27 0 0 25 0 1 0 1843520853 24100864 5438 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 5884 5438 145 145 0 5739 0
[pid=9680] vsize: 23536
Current children cumulated CPU time (s) 99.82
Current children cumulated vsize (Kb) 25660

[startup+110.017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 5776 0 0 0 10950 28 0 0 25 0 1 0 1843520853 25284608 5716 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 6173 5716 145 145 0 6028 0
[pid=9680] vsize: 24692
Current children cumulated CPU time (s) 109.79
Current children cumulated vsize (Kb) 26816

[startup+120.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 6249 0 0 0 11941 33 0 0 25 0 1 0 1843520853 27197440 6189 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 6640 6189 145 145 0 6495 0
[pid=9680] vsize: 26560
Current children cumulated CPU time (s) 119.75
Current children cumulated vsize (Kb) 28684

[startup+130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 6542 0 0 0 12937 35 0 0 25 0 1 0 1843520853 28188672 6435 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 6882 6435 145 145 0 6737 0
[pid=9680] vsize: 27528
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 29652

[startup+140.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 7068 0 0 0 13928 39 0 0 25 0 1 0 1843520853 30461952 6961 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 7437 6961 145 145 0 7292 0
[pid=9680] vsize: 29748
Current children cumulated CPU time (s) 139.68
Current children cumulated vsize (Kb) 31872

[startup+150.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 7469 0 0 0 14920 42 0 0 25 0 1 0 1843520853 32088064 7362 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 7834 7362 145 145 0 7689 0
[pid=9680] vsize: 31336
Current children cumulated CPU time (s) 149.63
Current children cumulated vsize (Kb) 33460

[startup+160.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 8019 0 0 0 15908 48 0 0 25 0 1 0 1843520853 34324480 7912 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 8380 7912 145 145 0 8235 0
[pid=9680] vsize: 33520
Current children cumulated CPU time (s) 159.57
Current children cumulated vsize (Kb) 35644

[startup+170.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 8425 0 0 0 16900 51 0 0 25 0 1 0 1843520853 35966976 8318 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 8781 8318 145 145 0 8636 0
[pid=9680] vsize: 35124
Current children cumulated CPU time (s) 169.52
Current children cumulated vsize (Kb) 37248

[startup+180.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 8902 0 0 0 17890 54 0 0 25 0 1 0 1843520853 37900288 8795 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 9253 8795 145 145 0 9108 0
[pid=9680] vsize: 37012
Current children cumulated CPU time (s) 179.45
Current children cumulated vsize (Kb) 39136

[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 9327 0 0 0 18882 59 0 0 25 0 1 0 1843520853 39628800 9220 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 9675 9220 145 145 0 9530 0
[pid=9680] vsize: 38700
Current children cumulated CPU time (s) 189.42
Current children cumulated vsize (Kb) 40824

[startup+200.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 9760 0 0 0 19874 61 0 0 25 0 1 0 1843520853 41390080 9653 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 10105 9653 145 145 0 9960 0
[pid=9680] vsize: 40420
Current children cumulated CPU time (s) 199.36
Current children cumulated vsize (Kb) 42544

[startup+210.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 10275 0 0 0 20866 65 0 0 25 0 1 0 1843520853 43487232 10168 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 10617 10168 145 145 0 10472 0
[pid=9680] vsize: 42468
Current children cumulated CPU time (s) 209.32
Current children cumulated vsize (Kb) 44592

[startup+220.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 10659 0 0 0 21857 68 0 0 25 0 1 0 1843520853 45047808 10552 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 10998 10552 145 145 0 10853 0
[pid=9680] vsize: 43992
Current children cumulated CPU time (s) 219.26
Current children cumulated vsize (Kb) 46116

[startup+230.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 11022 0 0 0 22851 71 0 0 25 0 1 0 1843520853 46596096 10869 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 11376 10869 145 145 0 11231 0
[pid=9680] vsize: 45504
Current children cumulated CPU time (s) 229.23
Current children cumulated vsize (Kb) 47628

[startup+240.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 11228 0 0 0 23847 72 0 0 25 0 1 0 1843520853 47431680 11075 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 11580 11075 145 145 0 11435 0
[pid=9680] vsize: 46320
Current children cumulated CPU time (s) 239.2
Current children cumulated vsize (Kb) 48444

[startup+250.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 11590 0 0 0 24840 75 0 0 25 0 1 0 1843520853 48902144 11437 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 11939 11437 145 145 0 11794 0
[pid=9680] vsize: 47756
Current children cumulated CPU time (s) 249.16
Current children cumulated vsize (Kb) 49880

[startup+260.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 11882 0 0 0 25834 78 0 0 25 0 1 0 1843520853 50089984 11729 4294967295 134512640 135094434 3221224448 3221223104 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 12229 11729 145 145 0 12084 0
[pid=9680] vsize: 48916
Current children cumulated CPU time (s) 259.13
Current children cumulated vsize (Kb) 51040

[startup+270.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 12312 0 0 0 26826 82 0 0 25 0 1 0 1843520853 51843072 12159 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 12657 12159 145 145 0 12512 0
[pid=9680] vsize: 50628
Current children cumulated CPU time (s) 269.09
Current children cumulated vsize (Kb) 52752

[startup+280.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 12779 0 0 0 27819 85 0 0 25 0 1 0 1843520853 53743616 12626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 13121 12626 145 145 0 12976 0
[pid=9680] vsize: 52484
Current children cumulated CPU time (s) 279.05
Current children cumulated vsize (Kb) 54608

[startup+290.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13306 0 0 0 28810 90 0 0 25 0 1 0 1843520853 55894016 13153 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 13646 13153 145 145 0 13501 0
[pid=9680] vsize: 54584
Current children cumulated CPU time (s) 289.01
Current children cumulated vsize (Kb) 56708

[startup+300.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13625 0 0 0 29805 92 0 0 25 0 1 0 1843520853 57192448 13472 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 13963 13472 145 145 0 13818 0
[pid=9680] vsize: 55852
Current children cumulated CPU time (s) 298.98
Current children cumulated vsize (Kb) 57976

[startup+310.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 30801 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 308.96
Current children cumulated vsize (Kb) 58492

[startup+320.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 31801 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 318.96
Current children cumulated vsize (Kb) 58492

[startup+330.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 32802 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 328.97
Current children cumulated vsize (Kb) 58492

[startup+340.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 33802 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 338.97
Current children cumulated vsize (Kb) 58492

[startup+350.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 34802 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 348.97
Current children cumulated vsize (Kb) 58492

[startup+360.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 35802 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 358.97
Current children cumulated vsize (Kb) 58492

[startup+370.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 36802 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 368.97
Current children cumulated vsize (Kb) 58492

[startup+380.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 37802 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 378.97
Current children cumulated vsize (Kb) 58492

[startup+390.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 38803 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 388.98
Current children cumulated vsize (Kb) 58492

[startup+400.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 39803 94 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 398.98
Current children cumulated vsize (Kb) 58492

[startup+410.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 40803 95 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 408.99
Current children cumulated vsize (Kb) 58492

[startup+420.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13801 0 0 0 41803 95 0 0 25 0 1 0 1843520853 57720832 13602 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14092 13602 145 145 0 13947 0
[pid=9680] vsize: 56368
Current children cumulated CPU time (s) 418.99
Current children cumulated vsize (Kb) 58492

[startup+430.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 13925 0 0 0 42801 95 0 0 25 0 1 0 1843520853 58228736 13726 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14216 13726 145 145 0 14071 0
[pid=9680] vsize: 56864
Current children cumulated CPU time (s) 428.97
Current children cumulated vsize (Kb) 58988

[startup+440.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 14335 0 0 0 43793 99 0 0 25 0 1 0 1843520853 59908096 14136 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14626 14136 145 145 0 14481 0
[pid=9680] vsize: 58504
Current children cumulated CPU time (s) 438.93
Current children cumulated vsize (Kb) 60628

[startup+450.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 14667 0 0 0 44787 101 0 0 25 0 1 0 1843520853 61267968 14468 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 14958 14468 145 145 0 14813 0
[pid=9680] vsize: 59832
Current children cumulated CPU time (s) 448.89
Current children cumulated vsize (Kb) 61956

[startup+460.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 14966 0 0 0 45782 103 0 0 25 0 1 0 1843520853 62492672 14767 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 15257 14767 145 145 0 15112 0
[pid=9680] vsize: 61028
Current children cumulated CPU time (s) 458.86
Current children cumulated vsize (Kb) 63152

[startup+470.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 15250 0 0 0 46777 105 0 0 25 0 1 0 1843520853 63655936 15051 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 15541 15051 145 145 0 15396 0
[pid=9680] vsize: 62164
Current children cumulated CPU time (s) 468.83
Current children cumulated vsize (Kb) 64288

[startup+480.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 15536 0 0 0 47772 107 0 0 25 0 1 0 1843520853 64831488 15337 4294967295 134512640 135094434 3221224448 3221222992 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 15828 15337 145 145 0 15683 0
[pid=9680] vsize: 63312
Current children cumulated CPU time (s) 478.8
Current children cumulated vsize (Kb) 65436

[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 15820 0 0 0 48765 110 0 0 25 0 1 0 1843520853 65994752 15621 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 16112 15621 145 145 0 15967 0
[pid=9680] vsize: 64448
Current children cumulated CPU time (s) 488.76
Current children cumulated vsize (Kb) 66572

[startup+500.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 16150 0 0 0 49760 112 0 0 25 0 1 0 1843520853 67346432 15951 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 16442 15951 145 145 0 16297 0
[pid=9680] vsize: 65768
Current children cumulated CPU time (s) 498.73
Current children cumulated vsize (Kb) 67892

[startup+510.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 16420 0 0 0 50756 115 0 0 25 0 1 0 1843520853 68444160 16221 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 16710 16221 145 145 0 16565 0
[pid=9680] vsize: 66840
Current children cumulated CPU time (s) 508.72
Current children cumulated vsize (Kb) 68964

[startup+520.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 16758 0 0 0 51750 118 0 0 25 0 1 0 1843520853 69820416 16559 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17046 16559 145 145 0 16901 0
[pid=9680] vsize: 68184
Current children cumulated CPU time (s) 518.69
Current children cumulated vsize (Kb) 70308

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 52746 119 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 528.66
Current children cumulated vsize (Kb) 71212

[startup+540.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 53746 119 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 538.66
Current children cumulated vsize (Kb) 71212

[startup+550.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 54746 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 548.67
Current children cumulated vsize (Kb) 71212

[startup+560.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 55746 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 558.67
Current children cumulated vsize (Kb) 71212

[startup+570.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 56747 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 568.68
Current children cumulated vsize (Kb) 71212

[startup+580.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 57747 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 578.68
Current children cumulated vsize (Kb) 71212

[startup+590.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 58747 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223040 134556876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 588.68
Current children cumulated vsize (Kb) 71212

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 59747 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223060 134563154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 598.68
Current children cumulated vsize (Kb) 71212

[startup+610.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 60747 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 608.68
Current children cumulated vsize (Kb) 71212

[startup+620.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 61748 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223040 134557357 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 618.69
Current children cumulated vsize (Kb) 71212

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 62748 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 628.69
Current children cumulated vsize (Kb) 71212

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 63748 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 638.69
Current children cumulated vsize (Kb) 71212

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 64748 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 648.69
Current children cumulated vsize (Kb) 71212

[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 65748 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 658.69
Current children cumulated vsize (Kb) 71212

[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 66748 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223120 134556254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 668.69
Current children cumulated vsize (Kb) 71212

[startup+680.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 67749 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 678.7
Current children cumulated vsize (Kb) 71212

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 68749 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 688.7
Current children cumulated vsize (Kb) 71212

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 69749 120 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 698.7
Current children cumulated vsize (Kb) 71212

[startup+710.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 70749 121 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 708.71
Current children cumulated vsize (Kb) 71212

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 71749 121 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 718.71
Current children cumulated vsize (Kb) 71212

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 72749 121 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 728.71
Current children cumulated vsize (Kb) 71212

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 73749 121 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 738.71
Current children cumulated vsize (Kb) 71212

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17031 0 0 0 74749 121 0 0 25 0 1 0 1843520853 70746112 16786 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17272 16786 145 145 0 17127 0
[pid=9680] vsize: 69088
Current children cumulated CPU time (s) 748.71
Current children cumulated vsize (Kb) 71212

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17036 0 0 0 75749 121 0 0 25 0 1 0 1843520853 70762496 16791 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17276 16791 145 145 0 17131 0
[pid=9680] vsize: 69104
Current children cumulated CPU time (s) 758.71
Current children cumulated vsize (Kb) 71228

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17395 0 0 0 76745 123 0 0 25 0 1 0 1843520853 72224768 17150 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17633 17150 145 145 0 17488 0
[pid=9680] vsize: 70532
Current children cumulated CPU time (s) 768.69
Current children cumulated vsize (Kb) 72656

[startup+780.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 17742 0 0 0 77738 126 0 0 25 0 1 0 1843520853 73641984 17497 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 17979 17497 145 145 0 17834 0
[pid=9680] vsize: 71916
Current children cumulated CPU time (s) 778.65
Current children cumulated vsize (Kb) 74040

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 18021 0 0 0 78734 128 0 0 25 0 1 0 1843520853 74776576 17776 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 18256 17776 145 145 0 18111 0
[pid=9680] vsize: 73024
Current children cumulated CPU time (s) 788.63
Current children cumulated vsize (Kb) 75148

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 18326 0 0 0 79729 130 0 0 25 0 1 0 1843520853 76017664 18081 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 18559 18081 145 145 0 18414 0
[pid=9680] vsize: 74236
Current children cumulated CPU time (s) 798.6
Current children cumulated vsize (Kb) 76360

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 18634 0 0 0 80724 132 0 0 25 0 1 0 1843520853 77271040 18389 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 18865 18389 145 145 0 18720 0
[pid=9680] vsize: 75460
Current children cumulated CPU time (s) 808.57
Current children cumulated vsize (Kb) 77584

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 18889 0 0 0 81719 134 0 0 25 0 1 0 1843520853 78307328 18644 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 19118 18644 145 145 0 18973 0
[pid=9680] vsize: 76472
Current children cumulated CPU time (s) 818.54
Current children cumulated vsize (Kb) 78596

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 19145 0 0 0 82714 136 0 0 25 0 1 0 1843520853 79360000 18900 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 19375 18900 145 145 0 19230 0
[pid=9680] vsize: 77500
Current children cumulated CPU time (s) 828.51
Current children cumulated vsize (Kb) 79624

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 19444 0 0 0 83709 138 0 0 25 0 1 0 1843520853 80580608 19199 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 19673 19199 145 145 0 19528 0
[pid=9680] vsize: 78692
Current children cumulated CPU time (s) 838.48
Current children cumulated vsize (Kb) 80816

[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 19708 0 0 0 84705 139 0 0 25 0 1 0 1843520853 81649664 19463 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 19934 19463 145 145 0 19789 0
[pid=9680] vsize: 79736
Current children cumulated CPU time (s) 848.45
Current children cumulated vsize (Kb) 81860

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 19951 0 0 0 85701 141 0 0 25 0 1 0 1843520853 82640896 19706 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 20176 19706 145 145 0 20031 0
[pid=9680] vsize: 80704
Current children cumulated CPU time (s) 858.43
Current children cumulated vsize (Kb) 82828

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 20171 0 0 0 86697 143 0 0 25 0 1 0 1843520853 83550208 19926 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 20398 19926 145 145 0 20253 0
[pid=9680] vsize: 81592
Current children cumulated CPU time (s) 868.41
Current children cumulated vsize (Kb) 83716

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 20483 0 0 0 87690 147 0 0 25 0 1 0 1843520853 84815872 20238 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 20707 20238 145 145 0 20562 0
[pid=9680] vsize: 82828
Current children cumulated CPU time (s) 878.38
Current children cumulated vsize (Kb) 84952

[startup+890.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 20806 0 0 0 88684 149 0 0 25 0 1 0 1843520853 86142976 20561 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 21031 20561 145 145 0 20886 0
[pid=9680] vsize: 84124
Current children cumulated CPU time (s) 888.34
Current children cumulated vsize (Kb) 86248

[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 21083 0 0 0 89679 152 0 0 25 0 1 0 1843520853 87269376 20838 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 21306 20838 145 145 0 21161 0
[pid=9680] vsize: 85224
Current children cumulated CPU time (s) 898.32
Current children cumulated vsize (Kb) 87348

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 21419 0 0 0 90674 154 0 0 25 0 1 0 1843520853 88637440 21174 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 21640 21174 145 145 0 21495 0
[pid=9680] vsize: 86560
Current children cumulated CPU time (s) 908.29
Current children cumulated vsize (Kb) 88684

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 21735 0 0 0 91668 156 0 0 25 0 1 0 1843520853 89927680 21490 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 21955 21490 145 145 0 21810 0
[pid=9680] vsize: 87820
Current children cumulated CPU time (s) 918.25
Current children cumulated vsize (Kb) 89944

[startup+930.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 22033 0 0 0 92663 157 0 0 25 0 1 0 1843520853 91140096 21788 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 22251 21788 145 145 0 22106 0
[pid=9680] vsize: 89004
Current children cumulated CPU time (s) 928.21
Current children cumulated vsize (Kb) 91128

[startup+940.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 22328 0 0 0 93659 159 0 0 25 0 1 0 1843520853 92344320 22083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 22545 22083 145 145 0 22400 0
[pid=9680] vsize: 90180
Current children cumulated CPU time (s) 938.19
Current children cumulated vsize (Kb) 92304

[startup+950.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 22602 0 0 0 94655 161 0 0 25 0 1 0 1843520853 93458432 22357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 22817 22357 145 145 0 22672 0
[pid=9680] vsize: 91268
Current children cumulated CPU time (s) 948.17
Current children cumulated vsize (Kb) 93392

[startup+960.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 22862 0 0 0 95650 163 0 0 25 0 1 0 1843520853 94519296 22617 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 23076 22617 145 145 0 22931 0
[pid=9680] vsize: 92304
Current children cumulated CPU time (s) 958.14
Current children cumulated vsize (Kb) 94428

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 23115 0 0 0 96646 165 0 0 25 0 1 0 1843520853 95547392 22870 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 23327 22870 145 145 0 23182 0
[pid=9680] vsize: 93308
Current children cumulated CPU time (s) 968.12
Current children cumulated vsize (Kb) 95432

[startup+980.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 23398 0 0 0 97641 168 0 0 25 0 1 0 1843520853 96706560 23153 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 23610 23153 145 145 0 23465 0
[pid=9680] vsize: 94440
Current children cumulated CPU time (s) 978.1
Current children cumulated vsize (Kb) 96564

[startup+990.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 23674 0 0 0 98637 171 0 0 25 0 1 0 1843520853 97837056 23429 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 23886 23429 145 145 0 23741 0
[pid=9680] vsize: 95544
Current children cumulated CPU time (s) 988.09
Current children cumulated vsize (Kb) 97668

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) T 9676 9676 28974 0 -1 0 23904 0 0 0 99632 172 0 0 25 0 1 0 1843520853 99299328 23659 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9680/statm): 24243 23659 145 145 0 24098 0
[pid=9680] vsize: 96972
Current children cumulated CPU time (s) 998.05
Current children cumulated vsize (Kb) 99096

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 24122 0 0 0 100629 173 0 0 25 0 1 0 1843520853 100188160 23877 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 24460 23877 145 145 0 24315 0
[pid=9680] vsize: 97840
Current children cumulated CPU time (s) 1008.03
Current children cumulated vsize (Kb) 99964

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 24365 0 0 0 101625 175 0 0 25 0 1 0 1843520853 101179392 24120 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 24702 24120 145 145 0 24557 0
[pid=9680] vsize: 98808
Current children cumulated CPU time (s) 1018.01
Current children cumulated vsize (Kb) 100932

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 24597 0 0 0 102621 176 0 0 25 0 1 0 1843520853 102125568 24352 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 24933 24352 145 145 0 24788 0
[pid=9680] vsize: 99732
Current children cumulated CPU time (s) 1027.98
Current children cumulated vsize (Kb) 101856

[startup+1040.1 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 24818 0 0 0 103617 178 0 0 25 0 1 0 1843520853 103034880 24573 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 25155 24573 145 145 0 25010 0
[pid=9680] vsize: 100620
Current children cumulated CPU time (s) 1037.96
Current children cumulated vsize (Kb) 102744

[startup+1050.1 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 25046 0 0 0 104612 180 0 0 25 0 1 0 1843520853 103972864 24801 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 25384 24801 145 145 0 25239 0
[pid=9680] vsize: 101536
Current children cumulated CPU time (s) 1047.93
Current children cumulated vsize (Kb) 103660

[startup+1060.1 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 25259 0 0 0 105610 181 0 0 25 0 1 0 1843520853 104841216 25014 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 25596 25014 145 145 0 25451 0
[pid=9680] vsize: 102384
Current children cumulated CPU time (s) 1057.92
Current children cumulated vsize (Kb) 104508

[startup+1070.1 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 25493 0 0 0 106605 183 0 0 25 0 1 0 1843520853 105803776 25248 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 25831 25248 145 145 0 25686 0
[pid=9680] vsize: 103324
Current children cumulated CPU time (s) 1067.89
Current children cumulated vsize (Kb) 105448

[startup+1080.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 25718 0 0 0 107603 184 0 0 25 0 1 0 1843520853 106733568 25473 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 26058 25473 145 145 0 25913 0
[pid=9680] vsize: 104232
Current children cumulated CPU time (s) 1077.88
Current children cumulated vsize (Kb) 106356

[startup+1090.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 26002 0 0 0 108597 187 0 0 25 0 1 0 1843520853 107896832 25757 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 26342 25757 145 145 0 26197 0
[pid=9680] vsize: 105368
Current children cumulated CPU time (s) 1087.85
Current children cumulated vsize (Kb) 107492

[startup+1100.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 26251 0 0 0 109594 189 0 0 25 0 1 0 1843520853 108916736 26006 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 26591 26006 145 145 0 26446 0
[pid=9680] vsize: 106364
Current children cumulated CPU time (s) 1097.84
Current children cumulated vsize (Kb) 108488

[startup+1110.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 26521 0 0 0 110589 191 0 0 25 0 1 0 1843520853 110018560 26276 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 26860 26276 145 145 0 26715 0
[pid=9680] vsize: 107440
Current children cumulated CPU time (s) 1107.81
Current children cumulated vsize (Kb) 109564

[startup+1120.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 26790 0 0 0 111584 194 0 0 25 0 1 0 1843520853 111108096 26545 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 27126 26545 145 145 0 26981 0
[pid=9680] vsize: 108504
Current children cumulated CPU time (s) 1117.79
Current children cumulated vsize (Kb) 110628

[startup+1130.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 26980 0 0 0 112581 195 0 0 25 0 1 0 1843520853 111878144 26735 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 27314 26735 145 145 0 27169 0
[pid=9680] vsize: 109256
Current children cumulated CPU time (s) 1127.77
Current children cumulated vsize (Kb) 111380

[startup+1140.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 27188 0 0 0 113577 197 0 0 25 0 1 0 1843520853 112721920 26943 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 27520 26943 145 145 0 27375 0
[pid=9680] vsize: 110080
Current children cumulated CPU time (s) 1137.75
Current children cumulated vsize (Kb) 112204

[startup+1150.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 27401 0 0 0 114573 198 0 0 25 0 1 0 1843520853 113582080 27156 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9680/statm): 27730 27156 145 145 0 27585 0
[pid=9680] vsize: 110920
Current children cumulated CPU time (s) 1147.72
Current children cumulated vsize (Kb) 113044

[startup+1160.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 27622 0 0 0 115569 200 0 0 25 0 1 0 1843520853 114491392 27377 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 27952 27377 145 145 0 27807 0
[pid=9680] vsize: 111808
Current children cumulated CPU time (s) 1157.7
Current children cumulated vsize (Kb) 113932

[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 27839 0 0 0 116564 202 0 0 25 0 1 0 1843520853 115376128 27594 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 28168 27594 145 145 0 28023 0
[pid=9680] vsize: 112672
Current children cumulated CPU time (s) 1167.67
Current children cumulated vsize (Kb) 114796

[startup+1180.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 28047 0 0 0 117561 204 0 0 25 0 1 0 1843520853 116224000 27802 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 28375 27802 145 145 0 28230 0
[pid=9680] vsize: 113500
Current children cumulated CPU time (s) 1177.66
Current children cumulated vsize (Kb) 115624

[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 28249 0 0 0 118557 205 0 0 25 0 1 0 1843520853 117051392 28004 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 28577 28004 145 145 0 28432 0
[pid=9680] vsize: 114308
Current children cumulated CPU time (s) 1187.63
Current children cumulated vsize (Kb) 116432

[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 28438 0 0 0 119554 206 0 0 25 0 1 0 1843520853 117821440 28193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 28765 28193 145 145 0 28620 0
[pid=9680] vsize: 115060
Current children cumulated CPU time (s) 1197.61
Current children cumulated vsize (Kb) 117184

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 28635 0 0 0 120550 207 0 0 25 0 1 0 1843520853 118620160 28390 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 28960 28390 145 145 0 28815 0
[pid=9680] vsize: 115840
Current children cumulated CPU time (s) 1207.58
Current children cumulated vsize (Kb) 117964



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9680
Raw data (/proc/9676/stat): 9676 (minisat+_script) S 9675 9676 28974 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843520848 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9676/statm): 531 226 485 147 0 384 0
[pid=9676] vsize: 2124
Raw data (/proc/9680/stat): 9680 (minisat+_64-bit) R 9676 9676 28974 0 -1 0 28635 0 0 0 120550 207 0 0 25 0 1 0 1843520853 118620160 28390 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9680/statm): 28960 28390 145 145 0 28815 0
[pid=9680] vsize: 115840
Current children cumulated CPU time (s) 1207.58
Current children cumulated vsize (Kb) 117964

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1207.63
CPU user time (s): 1205.5
CPU system time (s): 2.12968
CPU usage (%): 99.7906
Max. virtual memory (cumulated for all children) (Kb): 117964

Verifier Data

ERROR: no interpretation found !