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/frb59-26-opb/normalized-frb59-26-4.opb
MD5SUMf6c01aa815aa7b4a79652c8bfa8bef11
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -43
Optimality of the best value was proved NO
Number of terms in the objective function 1534
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 1534
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 1534
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1203.77
Number of variables1534
Total number of constraints127011
Number of constraints which are clauses127011
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 2335

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        923872 kB
Buffers:         31796 kB
Cached:          51248 kB
SwapCached:        732 kB
Active:          47480 kB
Inactive:        38128 kB
HighTotal:      131008 kB
HighFree:        77924 kB
LowTotal:       903652 kB
LowFree:        845948 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19384 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:24:37 (client local time) WITH STATUS 10 IN 1207.2 SECONDS
stats: 2722 7 1207.2 10

Solver Data

c Parsing PB file...
c Converting 127011 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 |  127011   254022 |   42337       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -39
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  217724   466825 |   72574       0        0     nan |  0.000 % |
c |       101 |  217100   465520 |   79831      75     1891    25.2 |  0.552 % |
c |       251 |  216142   463482 |   87814     175     2869    16.4 |  1.472 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       283 |  215895   463068 |   71965     196     3081    15.7 |  1.472 % |
c |       383 |  215282   461707 |   79161     278     3977    14.3 |  2.308 % |
c |       533 |  214159   459226 |   87077     364     4788    13.2 |  3.458 % |
c |       758 |  213006   456739 |   95785     549     6483    11.8 |  4.484 % |
c |      1095 |  209782   449507 |  105363     745     9421    12.6 |  7.724 % |
c |      1601 |  206432   442115 |  115900    1112    13705    12.3 | 10.979 % |
c |      2360 |  201924   431973 |  127490    1602    20009    12.5 | 15.533 % |
c |      3500 |  195490   417458 |  140239    2379    31301    13.2 | 22.054 % |
c |      5208 |  186285   396444 |  154263    3408    43041    12.6 | 31.638 % |
c |      7770 |  173869   367796 |  169689    5209    63334    12.2 | 44.393 % |
c |     11614 |  161751   339183 |  186658    7679    87729    11.4 | 57.565 % |
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 |     13187 |  157688   329476 |   52562    8663   102201    11.8 | 57.565 % |
c |     13287 |  156933   327666 |   57818    8663   102407    11.8 | 62.822 % |
c |     13437 |  156496   326637 |   63600    8745   104289    11.9 | 63.301 % |
c |     13662 |  155926   325281 |   69960    8819   104473    11.8 | 63.932 % |
c |     13999 |  155223   323650 |   76956    9083   108132    11.9 | 64.683 % |
c |     14505 |  153620   319797 |   84651    9246   108097    11.7 | 66.481 % |
c |     15266 |  152501   317114 |   93116    9748   115430    11.8 | 67.730 % |
c |     16405 |  150344   311979 |  102428   10394   122912    11.8 | 70.057 % |
c |     18113 |  147697   305619 |  112671   11549   139462    12.1 | 72.985 % |
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 |     18694 |  147539   305334 |   49179   12008   148388    12.4 | 72.985 % |
c |     18794 |  147400   304996 |   54096   12090   148857    12.3 | 73.377 % |
c |     18945 |  146811   303591 |   59506   12125   150381    12.4 | 74.016 % |
c |     19170 |  146618   303111 |   65457   12274   152728    12.4 | 74.244 % |
c |     19507 |  145916   301459 |   72002   12424   155150    12.5 | 75.006 % |
c |     20013 |  145431   300287 |   79203   12767   162117    12.7 | 75.554 % |
c |     20772 |  144765   298681 |   87123   13375   171555    12.8 | 76.309 % |
c |     21911 |  143552   295765 |   95835   14116   185523    13.1 | 77.671 % |
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 |     23059 |  142709   293706 |   47569   14897   209048    14.0 | 77.671 % |
c |     23159 |  142510   293231 |   52325   14949   209340    14.0 | 78.860 % |
c |     23310 |  142062   292140 |   57558   14929   208787    14.0 | 79.346 % |
c |     23536 |  141876   291690 |   63314   15084   214231    14.2 | 79.559 % |
c |     23873 |  141619   291066 |   69645   15263   216726    14.2 | 79.842 % |
c |     24380 |  141451   290658 |   76610   15623   225005    14.4 | 80.026 % |
c |     25139 |  141389   290517 |   84271   16374   240561    14.7 | 80.090 % |
c |     26278 |  141010   289613 |   92698   17296   268483    15.5 | 80.505 % |
c |     27986 |  140784   289062 |  101968   18835   308966    16.4 | 80.767 % |
c |     30548 |  140209   287664 |  112165   21022   405981    19.3 | 81.421 % |
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 |     31778 |  139373   285667 |   46457   21842   443937    20.3 | 81.421 % |
c |     31878 |  139276   285430 |   51102   21902   444674    20.3 | 82.494 % |
c |     32029 |  139276   285430 |   56212   22053   447802    20.3 | 82.494 % |
c |     32254 |  139132   285074 |   61834   22160   457327    20.6 | 82.665 % |
c |     32591 |  139096   284980 |   68017   22456   466009    20.8 | 82.711 % |
c |     33097 |  139094   284976 |   74819   22954   500316    21.8 | 82.712 % |
c |     33856 |  139054   284872 |   82301   23600   526498    22.3 | 82.762 % |
c |     34995 |  138920   284556 |   90531   24549   663204    27.0 | 82.909 % |
c ==============================================================================
c Found solution: -46
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36284 |  138821   284259 |   46273   25668   883732    34.4 | 82.909 % |
c |     36385 |  138694   283953 |   50900   25669   884126    34.4 | 83.174 % |
c |     36536 |  138694   283953 |   55990   25820   891891    34.5 | 83.174 % |
c |     36762 |  138602   283731 |   61589   25934   893650    34.5 | 83.279 % |
c |     37100 |  138554   283617 |   67748   26205   902693    34.4 | 83.333 % |
c |     37606 |  138370   283163 |   74523   26546   924148    34.8 | 83.550 % |
c |     38365 |  138313   283026 |   81975   27113   948062    35.0 | 83.615 % |
c ==============================================================================
c Found solution: -48
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38791 |  138360   283160 |   46120   27022   836672    31.0 | 83.615 % |
c |     38892 |  138358   283156 |   50732   27122   837742    30.9 | 83.607 % |
c |     39043 |  138332   283094 |   55805   27268   842795    30.9 | 83.636 % |
c |     39268 |  138117   282577 |   61385   27410   845816    30.9 | 83.879 % |
c |     39605 |  138117   282577 |   67524   27747   884440    31.9 | 83.879 % |
c |     40111 |  138075   282477 |   74276   28208   904104    32.1 | 83.926 % |
c |     40870 |  137982   282266 |   81704   28889   956337    33.1 | 84.019 % |
c |     42009 |  137859   281970 |   89874   29943  1018380    34.0 | 84.157 % |
c |     43717 |  137738   281685 |   98862   31588  1206634    38.2 | 84.288 % |
c |     46279 |  137357   280740 |  108748   33696  1418373    42.1 | 84.732 % |
c |     50123 |  137309   280630 |  119623   37526  2132174    56.8 | 84.782 % |
c ==============================================================================
c Found solution: -49
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55401 |  137127   280197 |   45709   42680  2974708    69.7 | 84.782 % |
c |     55501 |  137127   280197 |   50279   42780  2976346    69.6 | 85.002 % |
c |     55651 |  136978   279835 |   55307   42557  2970739    69.8 | 85.168 % |
c |     55876 |  136978   279835 |   60838   42782  2981811    69.7 | 85.168 % |
c |     56213 |  136946   279745 |   66922   42968  2999837    69.8 | 85.208 % |
c |     56720 |  136769   279322 |   73614   42865  3011417    70.3 | 85.406 % |
c |     57479 |  136682   279123 |   80976   43566  3091567    71.0 | 85.496 % |
c |     58618 |  136682   279123 |   89073   44705  3176085    71.0 | 85.496 % |
c |     60327 |  136677   279112 |   97981   46359  3394772    73.2 | 85.501 % |
c |     62889 |  136606   278935 |  107779   48822  3952476    81.0 | 85.586 % |
c |     66734 |  136606   278935 |  118557   52667  4362427    82.8 | 85.586 % |
c ==============================================================================
c Found solution: -50
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70484 |  136545   278743 |   45515   56061  4839854    86.3 | 85.586 % |
c |     70585 |  136545   278743 |   50066   56162  4844298    86.3 | 85.659 % |
c |     70735 |  136545   278743 |   55073   56312  4853620    86.2 | 85.659 % |
c |     70965 |  136508   278657 |   60580   56513  4877293    86.3 | 85.698 % |
c |     71302 |  136496   278631 |   66638   56834  4903232    86.3 | 85.709 % |
c |     71808 |  136496   278631 |   73302   57340  4937196    86.1 | 85.709 % |
c |     72567 |  136496   278631 |   80632   58099  4981194    85.7 | 85.709 % |
c |     73706 |  136461   278546 |   88695   59205  5136627    86.8 | 85.749 % |
c |     75418 |  136461   278546 |   97565   60917  5434311    89.2 | 85.749 % |
c |     77980 |  136417   278438 |  107321   63453  5774796    91.0 | 85.799 % |
c |     81824 |  136321   278208 |  118054   67105  6309832    94.0 | 85.907 % |
c |     87590 |  136321   278208 |  129859   72871  7685311   105.5 | 85.907 % |
c |     96241 |  136217   277949 |  142845   81328  9191572   113.0 | 86.031 % |
c |    109215 |  136204   277918 |  157130   94286 11641845   123.5 | 86.046 % |
c ==============================================================================
c Found solution: -51
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125220 |  136194   277914 |   45398  110254 16471650   149.4 | 86.046 % |
c |    125320 |  136181   277883 |   49937   20057  4267558   212.8 | 86.113 % |
c |    125470 |  136169   277853 |   54931   20206  4271480   211.4 | 86.113 % |
c |    125697 |  136169   277853 |   60424   20433  4273810   209.2 | 86.113 % |
c |    126034 |  136117   277724 |   66467   20608  4287831   208.1 | 86.174 % |
c |    126540 |  135890   277186 |   73113   21097  4314903   204.5 | 86.423 % |
c |    127299 |  135890   277186 |   80425   21856  4363796   199.7 | 86.423 % |
c |    128438 |  135890   277186 |   88467   22995  4434339   192.8 | 86.423 % |
c |    130146 |  135868   277130 |   97314   24672  4540070   184.0 | 86.451 % |
c |    132709 |  135755   276862 |  107046   27219  4704140   172.8 | 86.574 % |
c |    136554 |  135751   276852 |  117750   31061  5320921   171.3 | 86.579 % |
c |    142320 |  135645   276598 |  129525   36769  5908029   160.7 | 86.698 % |
c |    150969 |  135622   276541 |  142478   45411  7122478   156.8 | 86.725 % |
c |    163943 |  135377   275953 |  156726   58104  8615626   148.3 | 86.995 % |
c |    183404 |  135186   275506 |  172398   77279 11243538   145.5 | 87.201 % |
c |    212596 |  135136   275378 |  189638  106355 16308482   153.3 | 87.262 % |
c |    256385 |  135136   275378 |  208602  150144 24609310   163.9 | 87.262 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 -C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 -C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 -C1518 -C1517 -C1516 -C1515 -C1514 C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 -C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 -C1493 -C1492 -C1491 -C1490 -C1489 -C1488 -C1487 -C1486 -C1485 -C1484 C1483 -C1482 -C1481 -C1480 C1479 -C1478 -C1477 -C1476 -C1475 -C1474 -C1473 -C1472 -C1471 -C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 -C1458 -C1457 -C1456 C1455 -C1454 -C1453 -C1452 -C1451 -C1450 -C1449 -C1448 -C1447 -C1446 -C1445 -C1444 -C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 -C1424 C1423 -C1422 -C1421 -C1420 -C1419 -C1418 -C1417 -C1416 -C1415 -C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 -C1401 -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 C860 -C859 -C858 -C857 -C856 C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258

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/16531/stat): 16531 (minisat+_script) R 16530 16531 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785401273 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16531/statm): 174 3 169 147 0 27 0
[pid=16531] 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=16532
New process pid=16533
New process pid=16534
execve syscall for /bin/sed executable
One traced child (pid=16533) 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=16534) exited with status: 0
One traced child (pid=16532) exited with status: 0
New process pid=16535
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-frb59-26-4.opb

[startup+10.0042 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 935 37 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 34112

[startup+20.005 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 1935 37 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 34112

[startup+30.0068 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 2935 37 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 34112

[startup+40.0076 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 3935 37 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 34112

[startup+50.0093 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 4934 38 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223136 134558987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 34112

[startup+60.0101 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 5934 38 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 34112

[startup+70.0109 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 6934 38 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 34112

[startup+80.0127 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 7933 39 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 34112

[startup+90.0135 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 8933 39 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 34112

[startup+100.014 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 9933 39 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 34112

[startup+110.015 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 10932 40 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 34112

[startup+120.016 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 11932 40 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223152 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 34112

[startup+130.017 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 12932 40 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223060 134563104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 34112

[startup+140.017 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 13932 40 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 139.73
Current children cumulated vsize (Kb) 34112

[startup+150.019 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 14932 40 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 149.73
Current children cumulated vsize (Kb) 34112

[startup+160.02 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 15931 41 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223132 134553526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 159.73
Current children cumulated vsize (Kb) 34112

[startup+170.021 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 16931 41 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 169.73
Current children cumulated vsize (Kb) 34112

[startup+180.022 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 17931 42 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 179.74
Current children cumulated vsize (Kb) 34112

[startup+190.022 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7889 0 0 0 18930 43 0 0 25 0 1 0 1785401278 32755712 7876 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 7997 7876 145 145 0 7852 0
[pid=16535] vsize: 31988
Current children cumulated CPU time (s) 189.74
Current children cumulated vsize (Kb) 34112

[startup+200.023 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 7992 0 0 0 19928 44 0 0 25 0 1 0 1785401278 33165312 7979 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 8097 7979 145 145 0 7952 0
[pid=16535] vsize: 32388
Current children cumulated CPU time (s) 199.73
Current children cumulated vsize (Kb) 34512

[startup+210.024 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 8287 0 0 0 20924 46 0 0 25 0 1 0 1785401278 33746944 8120 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 8239 8120 145 145 0 8094 0
[pid=16535] vsize: 32956
Current children cumulated CPU time (s) 209.71
Current children cumulated vsize (Kb) 35080

[startup+220.025 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 8669 0 0 0 21918 49 0 0 25 0 1 0 1785401278 35311616 8502 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 8621 8502 145 145 0 8476 0
[pid=16535] vsize: 34484
Current children cumulated CPU time (s) 219.68
Current children cumulated vsize (Kb) 36608

[startup+230.025 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 9395 0 0 0 22907 54 0 0 25 0 1 0 1785401278 38400000 9228 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 9375 9228 145 145 0 9230 0
[pid=16535] vsize: 37500
Current children cumulated CPU time (s) 229.62
Current children cumulated vsize (Kb) 39624

[startup+240.025 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 9973 0 0 0 23898 59 0 0 25 0 1 0 1785401278 40751104 9806 4294967295 134512640 135094434 3221224448 3221223104 134558281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 9949 9806 145 145 0 9804 0
[pid=16535] vsize: 39796
Current children cumulated CPU time (s) 239.58
Current children cumulated vsize (Kb) 41920

[startup+250.026 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 10550 0 0 0 24891 62 0 0 25 0 1 0 1785401278 42786816 10306 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 10446 10306 145 145 0 10301 0
[pid=16535] vsize: 41784
Current children cumulated CPU time (s) 249.54
Current children cumulated vsize (Kb) 43908

[startup+260.028 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 10993 0 0 0 25883 66 0 0 25 0 1 0 1785401278 44589056 10749 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 10886 10749 145 145 0 10741 0
[pid=16535] vsize: 43544
Current children cumulated CPU time (s) 259.5
Current children cumulated vsize (Kb) 45668

[startup+270.028 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 11676 0 0 0 26871 70 0 0 25 0 1 0 1785401278 47366144 11432 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 11564 11432 145 145 0 11419 0
[pid=16535] vsize: 46256
Current children cumulated CPU time (s) 269.42
Current children cumulated vsize (Kb) 48380

[startup+280.029 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 12242 0 0 0 27862 74 0 0 25 0 1 0 1785401278 49672192 11998 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 12127 11998 145 145 0 11982 0
[pid=16535] vsize: 48508
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 50632

[startup+290.03 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 12658 0 0 0 28855 77 0 0 25 0 1 0 1785401278 51052544 12338 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 12464 12338 145 145 0 12319 0
[pid=16535] vsize: 49856
Current children cumulated CPU time (s) 289.33
Current children cumulated vsize (Kb) 51980

[startup+300.031 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 13066 0 0 0 29847 81 0 0 25 0 1 0 1785401278 52711424 12746 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 12869 12746 145 145 0 12724 0
[pid=16535] vsize: 51476
Current children cumulated CPU time (s) 299.29
Current children cumulated vsize (Kb) 53600

[startup+310.032 s]
Raw data (loadavg): 1.00 0.97 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 13557 0 0 0 30840 84 0 0 25 0 1 0 1785401278 54710272 13237 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 13357 13237 145 145 0 13212 0
[pid=16535] vsize: 53428
Current children cumulated CPU time (s) 309.25
Current children cumulated vsize (Kb) 55552

[startup+320.033 s]
Raw data (loadavg): 1.08 0.99 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 13953 0 0 0 31831 88 0 0 25 0 1 0 1785401278 56582144 13633 4294967295 134512640 135094434 3221224448 3221223040 134551876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 13814 13633 145 145 0 13669 0
[pid=16535] vsize: 55256
Current children cumulated CPU time (s) 319.2
Current children cumulated vsize (Kb) 57380

[startup+330.034 s]
Raw data (loadavg): 1.07 0.99 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 14425 0 0 0 32822 93 0 0 25 0 1 0 1785401278 58503168 14105 4294967295 134512640 135094434 3221224448 3221223064 134778837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 14283 14105 145 145 0 14138 0
[pid=16535] vsize: 57132
Current children cumulated CPU time (s) 329.16
Current children cumulated vsize (Kb) 59256

[startup+340.035 s]
Raw data (loadavg): 1.06 0.99 0.99 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 15092 0 0 0 33811 98 0 0 25 0 1 0 1785401278 61227008 14772 4294967295 134512640 135094434 3221224448 3221223040 134557297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 14948 14772 145 145 0 14803 0
[pid=16535] vsize: 59792
Current children cumulated CPU time (s) 339.1
Current children cumulated vsize (Kb) 61916

[startup+350.036 s]
Raw data (loadavg): 1.13 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 15612 0 0 0 34802 101 0 0 25 0 1 0 1785401278 63348736 15292 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 15466 15292 145 145 0 15321 0
[pid=16535] vsize: 61864
Current children cumulated CPU time (s) 349.04
Current children cumulated vsize (Kb) 63988

[startup+360.037 s]
Raw data (loadavg): 1.18 1.02 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 16129 0 0 0 35792 105 0 0 25 0 1 0 1785401278 65454080 15809 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 15980 15809 145 145 0 15835 0
[pid=16535] vsize: 63920
Current children cumulated CPU time (s) 358.98
Current children cumulated vsize (Kb) 66044

[startup+370.038 s]
Raw data (loadavg): 1.15 1.02 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 16436 0 0 0 36786 107 0 0 25 0 1 0 1785401278 66707456 16116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 16286 16116 145 145 0 16141 0
[pid=16535] vsize: 65144
Current children cumulated CPU time (s) 368.94
Current children cumulated vsize (Kb) 67268

[startup+380.039 s]
Raw data (loadavg): 1.13 1.02 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 16917 0 0 0 37778 111 0 0 25 0 1 0 1785401278 68665344 16597 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 16764 16597 145 145 0 16619 0
[pid=16535] vsize: 67056
Current children cumulated CPU time (s) 378.9
Current children cumulated vsize (Kb) 69180

[startup+390.04 s]
Raw data (loadavg): 1.11 1.02 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 17317 0 0 0 38770 115 0 0 25 0 1 0 1785401278 70295552 16997 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 17162 16997 145 145 0 17017 0
[pid=16535] vsize: 68648
Current children cumulated CPU time (s) 388.86
Current children cumulated vsize (Kb) 70772

[startup+400.042 s]
Raw data (loadavg): 1.09 1.02 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 17787 0 0 0 39762 118 0 0 25 0 1 0 1785401278 72208384 17467 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 17629 17467 145 145 0 17484 0
[pid=16535] vsize: 70516
Current children cumulated CPU time (s) 398.81
Current children cumulated vsize (Kb) 72640

[startup+410.043 s]
Raw data (loadavg): 1.08 1.02 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 18202 0 0 0 40755 121 0 0 25 0 1 0 1785401278 73900032 17882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 18042 17882 145 145 0 17897 0
[pid=16535] vsize: 72168
Current children cumulated CPU time (s) 408.77
Current children cumulated vsize (Kb) 74292

[startup+420.043 s]
Raw data (loadavg): 1.06 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 18599 0 0 0 41747 125 0 0 25 0 1 0 1785401278 75517952 18279 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 18437 18279 145 145 0 18292 0
[pid=16535] vsize: 73748
Current children cumulated CPU time (s) 418.73
Current children cumulated vsize (Kb) 75872

[startup+430.044 s]
Raw data (loadavg): 1.05 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 19049 0 0 0 42739 128 0 0 25 0 1 0 1785401278 77352960 18729 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 18885 18729 145 145 0 18740 0
[pid=16535] vsize: 75540
Current children cumulated CPU time (s) 428.68
Current children cumulated vsize (Kb) 77664

[startup+440.045 s]
Raw data (loadavg): 1.05 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 19483 0 0 0 43732 131 0 0 25 0 1 0 1785401278 79122432 19163 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 19317 19163 145 145 0 19172 0
[pid=16535] vsize: 77268
Current children cumulated CPU time (s) 438.64
Current children cumulated vsize (Kb) 79392

[startup+450.046 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 19848 0 0 0 44726 134 0 0 25 0 1 0 1785401278 80609280 19528 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 19680 19528 145 145 0 19535 0
[pid=16535] vsize: 78720
Current children cumulated CPU time (s) 448.61
Current children cumulated vsize (Kb) 80844

[startup+460.047 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 20291 0 0 0 45720 136 0 0 25 0 1 0 1785401278 82415616 19971 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 20121 19971 145 145 0 19976 0
[pid=16535] vsize: 80484
Current children cumulated CPU time (s) 458.57
Current children cumulated vsize (Kb) 82608

[startup+470.047 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 20783 0 0 0 46711 140 0 0 25 0 1 0 1785401278 84422656 20463 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 20611 20463 145 145 0 20466 0
[pid=16535] vsize: 82444
Current children cumulated CPU time (s) 468.52
Current children cumulated vsize (Kb) 84568

[startup+480.048 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 21332 0 0 0 47702 144 0 0 25 0 1 0 1785401278 86667264 21012 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 21159 21012 145 145 0 21014 0
[pid=16535] vsize: 84636
Current children cumulated CPU time (s) 478.47
Current children cumulated vsize (Kb) 86760

[startup+490.049 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 21883 0 0 0 48693 147 0 0 25 0 1 0 1785401278 88915968 21563 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 21708 21563 145 145 0 21563 0
[pid=16535] vsize: 86832
Current children cumulated CPU time (s) 488.41
Current children cumulated vsize (Kb) 88956

[startup+500.051 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 22453 0 0 0 49685 151 0 0 25 0 1 0 1785401278 91246592 22133 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 22277 22133 145 145 0 22132 0
[pid=16535] vsize: 89108
Current children cumulated CPU time (s) 498.37
Current children cumulated vsize (Kb) 91232

[startup+510.051 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 22960 0 0 0 50679 153 0 0 25 0 1 0 1785401278 93315072 22640 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 22782 22640 145 145 0 22637 0
[pid=16535] vsize: 91128
Current children cumulated CPU time (s) 508.33
Current children cumulated vsize (Kb) 93252

[startup+520.052 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 23371 0 0 0 51674 156 0 0 25 0 1 0 1785401278 94994432 23051 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 23192 23051 145 145 0 23047 0
[pid=16535] vsize: 92768
Current children cumulated CPU time (s) 518.31
Current children cumulated vsize (Kb) 94892

[startup+530.053 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 23814 0 0 0 52667 159 0 0 25 0 1 0 1785401278 96804864 23494 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 23634 23494 145 145 0 23489 0
[pid=16535] vsize: 94536
Current children cumulated CPU time (s) 528.27
Current children cumulated vsize (Kb) 96660

[startup+540.054 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24309 0 0 0 53660 162 0 0 25 0 1 0 1785401278 98828288 23989 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24128 23989 145 145 0 23983 0
[pid=16535] vsize: 96512
Current children cumulated CPU time (s) 538.23
Current children cumulated vsize (Kb) 98636

[startup+550.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 54655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 548.2
Current children cumulated vsize (Kb) 99952

[startup+560.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 55655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 558.2
Current children cumulated vsize (Kb) 99952

[startup+570.056 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 56655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 568.2
Current children cumulated vsize (Kb) 99952

[startup+580.057 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 57655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 578.2
Current children cumulated vsize (Kb) 99952

[startup+590.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 58655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 588.2
Current children cumulated vsize (Kb) 99952

[startup+600.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 59655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 598.2
Current children cumulated vsize (Kb) 99952

[startup+610.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 60655 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223108 134553506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 608.2
Current children cumulated vsize (Kb) 99952

[startup+620.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 61656 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223040 134556866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 618.21
Current children cumulated vsize (Kb) 99952

[startup+630.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 62656 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 628.21
Current children cumulated vsize (Kb) 99952

[startup+640.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 63656 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 638.21
Current children cumulated vsize (Kb) 99952

[startup+650.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 64656 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 648.21
Current children cumulated vsize (Kb) 99952

[startup+660.064 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 65657 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 658.22
Current children cumulated vsize (Kb) 99952

[startup+670.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 66657 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 668.22
Current children cumulated vsize (Kb) 99952

[startup+680.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 67657 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 678.22
Current children cumulated vsize (Kb) 99952

[startup+690.068 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 68657 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 688.22
Current children cumulated vsize (Kb) 99952

[startup+700.069 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 69658 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 698.23
Current children cumulated vsize (Kb) 99952

[startup+710.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 70658 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 708.23
Current children cumulated vsize (Kb) 99952

[startup+720.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 71658 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 718.23
Current children cumulated vsize (Kb) 99952

[startup+730.071 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 72658 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 728.23
Current children cumulated vsize (Kb) 99952

[startup+740.072 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 73659 164 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 738.24
Current children cumulated vsize (Kb) 99952

[startup+750.073 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 74659 165 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221222928 134780607 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 748.25
Current children cumulated vsize (Kb) 99952

[startup+760.074 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 75659 165 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 758.25
Current children cumulated vsize (Kb) 99952

[startup+770.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 76659 165 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 768.25
Current children cumulated vsize (Kb) 99952

[startup+780.076 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 77658 166 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 778.25
Current children cumulated vsize (Kb) 99952

[startup+790.077 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 78658 166 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 788.25
Current children cumulated vsize (Kb) 99952

[startup+800.078 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 79658 167 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 798.26
Current children cumulated vsize (Kb) 99952

[startup+810.079 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 80658 167 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 808.26
Current children cumulated vsize (Kb) 99952

[startup+820.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 81658 167 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223120 134556268 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 818.26
Current children cumulated vsize (Kb) 99952

[startup+830.081 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 82658 167 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 828.26
Current children cumulated vsize (Kb) 99952

[startup+840.081 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 24711 0 0 0 83658 168 0 0 25 0 1 0 1785401278 100175872 24316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24457 24316 145 145 0 24312 0
[pid=16535] vsize: 97828
Current children cumulated CPU time (s) 838.27
Current children cumulated vsize (Kb) 99952

[startup+850.083 s]
Raw data (loadavg): 1.00 1.00 1.00 1/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) T 16531 16531 9854 0 -1 0 24928 0 0 0 84655 169 0 0 25 0 1 0 1785401278 101068800 24533 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16535/statm): 24675 24533 145 145 0 24530 0
[pid=16535] vsize: 98700
Current children cumulated CPU time (s) 848.25
Current children cumulated vsize (Kb) 100824

[startup+860.084 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 25240 0 0 0 85647 172 0 0 25 0 1 0 1785401278 102346752 24845 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 24987 24845 145 145 0 24842 0
[pid=16535] vsize: 99948
Current children cumulated CPU time (s) 858.2
Current children cumulated vsize (Kb) 102072

[startup+870.084 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 25581 0 0 0 86641 175 0 0 25 0 1 0 1785401278 103739392 25186 4294967295 134512640 135094434 3221224448 3221223120 134556465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 25327 25186 145 145 0 25182 0
[pid=16535] vsize: 101308
Current children cumulated CPU time (s) 868.17
Current children cumulated vsize (Kb) 103432

[startup+880.085 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) T 16531 16531 9854 0 -1 0 25906 0 0 0 87635 176 0 0 25 0 1 0 1785401278 105058304 25511 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16535/statm): 25649 25511 145 145 0 25504 0
[pid=16535] vsize: 102596
Current children cumulated CPU time (s) 878.12
Current children cumulated vsize (Kb) 104720

[startup+890.085 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 26203 0 0 0 88629 179 0 0 25 0 1 0 1785401278 106266624 25808 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 25944 25808 145 145 0 25799 0
[pid=16535] vsize: 103776
Current children cumulated CPU time (s) 888.09
Current children cumulated vsize (Kb) 105900

[startup+900.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 26503 0 0 0 89623 181 0 0 25 0 1 0 1785401278 107491328 26108 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 26243 26108 145 145 0 26098 0
[pid=16535] vsize: 104972
Current children cumulated CPU time (s) 898.05
Current children cumulated vsize (Kb) 107096

[startup+910.087 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 26857 0 0 0 90617 184 0 0 25 0 1 0 1785401278 108933120 26462 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 26595 26462 145 145 0 26450 0
[pid=16535] vsize: 106380
Current children cumulated CPU time (s) 908.02
Current children cumulated vsize (Kb) 108504

[startup+920.088 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 27195 0 0 0 91612 186 0 0 25 0 1 0 1785401278 110309376 26800 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 26931 26800 145 145 0 26786 0
[pid=16535] vsize: 107724
Current children cumulated CPU time (s) 917.99
Current children cumulated vsize (Kb) 109848

[startup+930.088 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 27491 0 0 0 92606 188 0 0 25 0 1 0 1785401278 111513600 27096 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 27225 27096 145 145 0 27080 0
[pid=16535] vsize: 108900
Current children cumulated CPU time (s) 927.95
Current children cumulated vsize (Kb) 111024

[startup+940.089 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 27894 0 0 0 93599 192 0 0 25 0 1 0 1785401278 113156096 27499 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 27626 27499 145 145 0 27481 0
[pid=16535] vsize: 110504
Current children cumulated CPU time (s) 937.92
Current children cumulated vsize (Kb) 112628

[startup+950.091 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 28234 0 0 0 94593 194 0 0 25 0 1 0 1785401278 114544640 27839 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 27965 27839 145 145 0 27820 0
[pid=16535] vsize: 111860
Current children cumulated CPU time (s) 947.88
Current children cumulated vsize (Kb) 113984

[startup+960.092 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 28531 0 0 0 95587 197 0 0 25 0 1 0 1785401278 115752960 28136 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 28260 28136 145 145 0 28115 0
[pid=16535] vsize: 113040
Current children cumulated CPU time (s) 957.85
Current children cumulated vsize (Kb) 115164

[startup+970.093 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 28837 0 0 0 96583 199 0 0 25 0 1 0 1785401278 117002240 28442 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 28565 28442 145 145 0 28420 0
[pid=16535] vsize: 114260
Current children cumulated CPU time (s) 967.83
Current children cumulated vsize (Kb) 116384

[startup+980.093 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 29134 0 0 0 97577 201 0 0 25 0 1 0 1785401278 118734848 28739 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 28988 28739 145 145 0 28843 0
[pid=16535] vsize: 115952
Current children cumulated CPU time (s) 977.79
Current children cumulated vsize (Kb) 118076

[startup+990.094 s]
Raw data (loadavg): 1.00 1.00 1.00 1/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) T 16531 16531 9854 0 -1 0 29421 0 0 0 98572 203 0 0 25 0 1 0 1785401278 119906304 29026 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/16535/statm): 29274 29026 145 145 0 29129 0
[pid=16535] vsize: 117096
Current children cumulated CPU time (s) 987.76
Current children cumulated vsize (Kb) 119220

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 29776 0 0 0 99566 206 0 0 25 0 1 0 1785401278 121352192 29381 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 29627 29381 145 145 0 29482 0
[pid=16535] vsize: 118508
Current children cumulated CPU time (s) 997.73
Current children cumulated vsize (Kb) 120632

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 30079 0 0 0 100558 210 0 0 25 0 1 0 1785401278 122589184 29684 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 29929 29684 145 145 0 29784 0
[pid=16535] vsize: 119716
Current children cumulated CPU time (s) 1007.69
Current children cumulated vsize (Kb) 121840

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 30337 0 0 0 101554 212 0 0 25 0 1 0 1785401278 123641856 29942 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 30186 29942 145 145 0 30041 0
[pid=16535] vsize: 120744
Current children cumulated CPU time (s) 1017.67
Current children cumulated vsize (Kb) 122868

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 30603 0 0 0 102551 213 0 0 25 0 1 0 1785401278 124727296 30208 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 30451 30208 145 145 0 30306 0
[pid=16535] vsize: 121804
Current children cumulated CPU time (s) 1027.65
Current children cumulated vsize (Kb) 123928

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 30905 0 0 0 103546 216 0 0 25 0 1 0 1785401278 125964288 30510 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 30753 30510 145 145 0 30608 0
[pid=16535] vsize: 123012
Current children cumulated CPU time (s) 1037.63
Current children cumulated vsize (Kb) 125136

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 31191 0 0 0 104541 218 0 0 18 0 1 0 1785401278 127127552 30796 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 31037 30796 145 145 0 30892 0
[pid=16535] vsize: 124148
Current children cumulated CPU time (s) 1047.6
Current children cumulated vsize (Kb) 126272

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 31468 0 0 0 105535 220 0 0 25 0 1 0 1785401278 128253952 31073 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 31312 31073 145 145 0 31167 0
[pid=16535] vsize: 125248
Current children cumulated CPU time (s) 1057.56
Current children cumulated vsize (Kb) 127372

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 31739 0 0 0 106530 222 0 0 25 0 1 0 1785401278 129359872 31344 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 31582 31344 145 145 0 31437 0
[pid=16535] vsize: 126328
Current children cumulated CPU time (s) 1067.53
Current children cumulated vsize (Kb) 128452

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 32003 0 0 0 107526 223 0 0 25 0 1 0 1785401278 130445312 31608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 31847 31608 145 145 0 31702 0
[pid=16535] vsize: 127388
Current children cumulated CPU time (s) 1077.5
Current children cumulated vsize (Kb) 129512

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 32273 0 0 0 108522 224 0 0 25 0 1 0 1785401278 131559424 31878 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 32119 31878 145 145 0 31974 0
[pid=16535] vsize: 128476
Current children cumulated CPU time (s) 1087.47
Current children cumulated vsize (Kb) 130600

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 32535 0 0 0 109517 226 0 0 25 0 1 0 1785401278 132624384 32140 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 32379 32140 145 145 0 32234 0
[pid=16535] vsize: 129516
Current children cumulated CPU time (s) 1097.44
Current children cumulated vsize (Kb) 131640

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 32792 0 0 0 110513 228 0 0 25 0 1 0 1785401278 133668864 32397 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 32634 32397 145 145 0 32489 0
[pid=16535] vsize: 130536
Current children cumulated CPU time (s) 1107.42
Current children cumulated vsize (Kb) 132660

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 33046 0 0 0 111508 230 0 0 25 0 1 0 1785401278 134725632 32651 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 32892 32651 145 145 0 32747 0
[pid=16535] vsize: 131568
Current children cumulated CPU time (s) 1117.39
Current children cumulated vsize (Kb) 133692

[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 33279 0 0 0 112504 232 0 0 25 0 1 0 1785401278 135684096 32884 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 33126 32884 145 145 0 32981 0
[pid=16535] vsize: 132504
Current children cumulated CPU time (s) 1127.37
Current children cumulated vsize (Kb) 134628

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 33520 0 0 0 113500 234 0 0 25 0 1 0 1785401278 136663040 33125 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 33365 33125 145 145 0 33220 0
[pid=16535] vsize: 133460
Current children cumulated CPU time (s) 1137.35
Current children cumulated vsize (Kb) 135584

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 33859 0 0 0 114494 236 0 0 25 0 1 0 1785401278 138051584 33464 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 33704 33464 145 145 0 33559 0
[pid=16535] vsize: 134816
Current children cumulated CPU time (s) 1147.31
Current children cumulated vsize (Kb) 136940

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 34162 0 0 0 115489 238 0 0 25 0 1 0 1785401278 139300864 33767 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 34009 33767 145 145 0 33864 0
[pid=16535] vsize: 136036
Current children cumulated CPU time (s) 1157.28
Current children cumulated vsize (Kb) 138160

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 34443 0 0 0 116483 240 0 0 25 0 1 0 1785401278 140439552 34048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 34287 34048 145 145 0 34142 0
[pid=16535] vsize: 137148
Current children cumulated CPU time (s) 1167.24
Current children cumulated vsize (Kb) 139272

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 34704 0 0 0 117479 243 0 0 25 0 1 0 1785401278 141496320 34309 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 34545 34309 145 145 0 34400 0
[pid=16535] vsize: 138180
Current children cumulated CPU time (s) 1177.23
Current children cumulated vsize (Kb) 140304

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 34997 0 0 0 118473 245 0 0 25 0 1 0 1785401278 142696448 34602 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 34838 34602 145 145 0 34693 0
[pid=16535] vsize: 139352
Current children cumulated CPU time (s) 1187.19
Current children cumulated vsize (Kb) 141476

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 35293 0 0 0 119467 248 0 0 25 0 1 0 1785401278 143900672 34898 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16535/statm): 35132 34898 145 145 0 34987 0
[pid=16535] vsize: 140528
Current children cumulated CPU time (s) 1197.16
Current children cumulated vsize (Kb) 142652

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 35493 0 0 0 120463 249 0 0 25 0 1 0 1785401278 144715776 35098 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 35331 35098 145 145 0 35186 0
[pid=16535] vsize: 141324
Current children cumulated CPU time (s) 1207.13
Current children cumulated vsize (Kb) 143448



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 16535
Raw data (/proc/16531/stat): 16531 (minisat+_script) S 16530 16531 9854 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785401273 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16531/statm): 531 226 485 147 0 384 0
[pid=16531] vsize: 2124
Raw data (/proc/16535/stat): 16535 (minisat+_64-bit) R 16531 16531 9854 0 -1 0 35493 0 0 0 120464 249 0 0 25 0 1 0 1785401278 144715776 35098 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16535/statm): 35331 35098 145 145 0 35186 0
[pid=16535] vsize: 141324
Current children cumulated CPU time (s) 1207.14
Current children cumulated vsize (Kb) 143448

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

Child status: 10
Real time (s): 1210.19
CPU time (s): 1207.2
CPU user time (s): 1204.64
CPU system time (s): 2.56061
CPU usage (%): 99.7532
Max. virtual memory (cumulated for all children) (Kb): 143448

Verifier Data

ERROR: no interpretation found !