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-5.opb
MD5SUMa5354df485c2b6c1695d0d26c0cdb212
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -42
Optimality of the best value was proved NO
Number of terms in the objective function 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.16
Number of variables1534
Total number of constraints125982
Number of constraints which are clauses125982
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 2336

Launcher Data

LAUNCH ON wulflinc23 THE 2005-09-18 19:04:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2723 boxname=wulflinc23 idbench=379 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a5354df485c2b6c1695d0d26c0cdb212  /oldhome/oroussel/tmp/wulflinc23/normalized-frb59-26-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-frb59-26-5.opb
IDLAUNCH: 2723
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        910628 kB
Buffers:         33132 kB
Cached:          63180 kB
SwapCached:        792 kB
Active:          57020 kB
Inactive:        41944 kB
HighTotal:      131008 kB
HighFree:        64624 kB
LowTotal:       903652 kB
LowFree:        846004 kB
SwapTotal:     2097136 kB
SwapFree:      2095868 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            19436 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:24:44 (client local time) WITH STATUS 10 IN 1207.62 SECONDS
stats: 2723 7 1207.62 10

Solver Data

c Parsing PB file...
c Converting 125982 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 |  125982   251964 |   41994       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -42
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216721   464825 |   72240       0        0     nan |  0.000 % |
c |       100 |  215959   463222 |   79464      65      492     7.6 |  0.688 % |
c |       250 |  215163   461534 |   87410     185     1565     8.5 |  1.408 % |
c |       475 |  214472   460051 |   96151     367     3201     8.7 |  2.048 % |
c |       812 |  213299   457504 |  105766     663     6213     9.4 |  3.198 % |
c |      1318 |  210803   452048 |  116343    1052    10471    10.0 |  5.545 % |
c |      2078 |  206899   443392 |  127977    1632    16581    10.2 |  9.378 % |
c |      3217 |  199960   427819 |  140775    2503    25519    10.2 | 16.335 % |
c |      4925 |  192015   409778 |  154852    3695    39888    10.8 | 24.503 % |
c |      7488 |  180386   383175 |  170338    5442    62629    11.5 | 36.510 % |
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 |      9101 |  174218   369045 |   58072    6524    77488    11.9 | 36.510 % |
c |      9201 |  173612   367663 |   63879    6598    78260    11.9 | 43.746 % |
c |      9352 |  172254   364438 |   70267    6634    78701    11.9 | 45.220 % |
c |      9577 |  171126   361800 |   77293    6770    80672    11.9 | 46.408 % |
c |      9915 |  170107   359398 |   85023    7035    83170    11.8 | 47.468 % |
c |     10421 |  168416   355375 |   93525    7369    86547    11.7 | 49.288 % |
c |     11180 |  166329   350476 |  102878    7889    92417    11.7 | 51.500 % |
c |     12319 |  162134   340596 |  113165    8719   103213    11.8 | 56.044 % |
c |     14027 |  157622   329892 |  124482    9863   120023    12.2 | 60.978 % |
c |     16590 |  154141   321594 |  136930   11740   143012    12.2 | 64.795 % |
c |     20434 |  148827   308955 |  150623   14218   196223    13.8 | 70.642 % |
c |     26201 |  143510   296212 |  165686   18448   300139    16.3 | 76.485 % |
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 |     26706 |  143396   295898 |   47798   18911   307260    16.2 | 76.485 % |
c |     26807 |  143365   295823 |   52577   19010   309012    16.3 | 76.650 % |
c |     26957 |  143346   295776 |   57835   19153   311224    16.2 | 76.673 % |
c |     27182 |  143346   295776 |   63619   19378   315135    16.3 | 76.673 % |
c |     27519 |  143147   295303 |   69981   19597   320396    16.3 | 76.894 % |
c |     28026 |  143091   295163 |   76979   20091   335810    16.7 | 76.962 % |
c |     28786 |  142405   293484 |   84677   20635   354173    17.2 | 77.752 % |
c |     29925 |  142052   292643 |   93144   21385   377394    17.6 | 78.191 % |
c |     31633 |  141301   290830 |  102459   22900   434457    19.0 | 78.986 % |
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 |     32831 |  141162   290523 |   47054   23957   491822    20.5 | 78.986 % |
c |     32932 |  140811   289673 |   51759   23932   490747    20.5 | 79.557 % |
c |     33082 |  140811   289673 |   56935   24082   494759    20.5 | 79.557 % |
c |     33307 |  140758   289546 |   62628   24212   497422    20.5 | 79.617 % |
c |     33644 |  140708   289438 |   68891   24539   505279    20.6 | 79.664 % |
c |     34150 |  140708   289438 |   75780   25045   526109    21.0 | 79.664 % |
c ==============================================================================
c Found solution: -47
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34585 |  140706   289496 |   46902   25409   545666    21.5 | 79.664 % |
c |     34685 |  140631   289325 |   51592   25488   547741    21.5 | 79.790 % |
c |     34835 |  140502   289012 |   56751   25504   551262    21.6 | 79.937 % |
c |     35060 |  140402   288768 |   62426   25617   555828    21.7 | 80.050 % |
c |     35397 |  140196   288258 |   68669   25847   566341    21.9 | 80.291 % |
c |     35903 |  139974   287726 |   75536   26221   579362    22.1 | 80.531 % |
c |     36662 |  139868   287454 |   83089   26872   608330    22.6 | 80.663 % |
c |     37801 |  139004   285361 |   91398   27413   642062    23.4 | 81.628 % |
c |     39510 |  138731   284704 |  100538   28798   697757    24.2 | 81.934 % |
c |     42072 |  138129   283247 |  110592   30903   807101    26.1 | 82.604 % |
c |     45917 |  137418   281505 |  121651   33977   991265    29.2 | 83.419 % |
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 |     50963 |  136707   279714 |   45569   38071  1355297    35.6 | 83.419 % |
c |     51064 |  136665   279612 |   50125   38151  1356275    35.6 | 84.305 % |
c |     51214 |  136633   279530 |   55138   38260  1360588    35.6 | 84.344 % |
c |     51440 |  136573   279388 |   60652   38306  1366438    35.7 | 84.410 % |
c |     51777 |  136483   279176 |   66717   38425  1384832    36.0 | 84.508 % |
c |     52284 |  136441   279076 |   73389   38870  1410855    36.3 | 84.555 % |
c |     53044 |  136283   278706 |   80728   39261  1464008    37.3 | 84.726 % |
c |     54183 |  136243   278610 |   88801   40352  1545061    38.3 | 84.771 % |
c |     55891 |  136190   278485 |   97681   41887  1699101    40.6 | 84.827 % |
c |     58453 |  136091   278234 |  107449   44175  1922681    43.5 | 84.946 % |
c |     62297 |  136041   278108 |  118194   47904  2464514    51.4 | 85.006 % |
c |     68063 |  135763   277417 |  130013   53108  3155017    59.4 | 85.333 % |
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 |     72442 |  135783   277482 |   45261   57408  3652183    63.6 | 85.333 % |
c |     72542 |  135783   277482 |   49787   57508  3657004    63.6 | 85.319 % |
c |     72693 |  135749   277402 |   54765   57629  3661230    63.5 | 85.356 % |
c |     72918 |  135744   277391 |   60242   57848  3671369    63.5 | 85.361 % |
c |     73256 |  135732   277365 |   66266   58171  3703940    63.7 | 85.372 % |
c |     73763 |  135695   277274 |   72893   58562  3756826    64.2 | 85.416 % |
c |     74522 |  135611   277064 |   80182   59191  3786127    64.0 | 85.514 % |
c |     75662 |  135611   277064 |   88200   60331  3934420    65.2 | 85.514 % |
c |     77370 |  135597   277030 |   97020   62037  4154789    67.0 | 85.530 % |
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 |     78950 |  135575   276913 |   45191   62522  4231397    67.7 | 85.530 % |
c |     79050 |  135532   276799 |   49710   62546  4231449    67.7 | 85.609 % |
c |     79200 |  135532   276799 |   54681   62696  4238985    67.6 | 85.609 % |
c |     79425 |  135529   276792 |   60149   62920  4255939    67.6 | 85.613 % |
c |     79762 |  135529   276792 |   66164   63257  4304084    68.0 | 85.613 % |
c |     80270 |  135529   276792 |   72780   63765  4359392    68.4 | 85.613 % |
c |     81029 |  135444   276590 |   80058   64283  4405638    68.5 | 85.704 % |
c |     82168 |  135444   276590 |   88064   65422  4514282    69.0 | 85.704 % |
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 |     82761 |  135475   276684 |   45158   66015  4553481    69.0 | 85.704 % |
c |     82861 |  135465   276660 |   49673   66081  4556332    69.0 | 85.710 % |
c |     83011 |  135465   276660 |   54641   66231  4565254    68.9 | 85.710 % |
c |     83236 |  135465   276660 |   60105   66456  4570299    68.8 | 85.710 % |
c |     83573 |  135465   276660 |   66115   66793  4594919    68.8 | 85.710 % |
c |     84079 |  135342   276354 |   72727   67152  4631108    69.0 | 85.848 % |
c |     84839 |  135228   276086 |   80000   67812  4691309    69.2 | 85.972 % |
c |     85979 |  135203   276023 |   88000   68603  4777095    69.6 | 86.003 % |
c |     87687 |  135029   275598 |   96800   69732  4907965    70.4 | 86.203 % |
c |     90249 |  135029   275598 |  106480   72294  5274639    73.0 | 86.203 % |
c |     94093 |  134944   275390 |  117128   75951  5693190    75.0 | 86.301 % |
c |     99859 |  134883   275249 |  128841   81592  6421159    78.7 | 86.366 % |
c |    108508 |  134835   275135 |  141725   90163  7860535    87.2 | 86.419 % |
c |    121482 |  134799   275042 |  155897  102952  9664105    93.9 | 86.462 % |
c |    140943 |  134747   274910 |  171487  122344 13291931   108.6 | 86.526 % |
c |    170136 |  134672   274727 |  188636  151088 19209599   127.1 | 86.613 % |
c ==============================================================================
c Found solution: -52
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    186163 |  134612   274561 |   44870  165904 21520868   129.7 | 86.613 % |
c |    186263 |  134612   274561 |   49357   25515  2207333    86.5 | 86.684 % |
c |    186414 |  134601   274534 |   54292   25642  2217650    86.5 | 86.697 % |
c |    186639 |  134601   274534 |   59721   25867  2241685    86.7 | 86.697 % |
c |    186976 |  134524   274345 |   65694   26124  2249912    86.1 | 86.787 % |
c |    187482 |  134420   274095 |   72263   26616  2278339    85.6 | 86.903 % |
c |    188241 |  134420   274095 |   79489   27375  2319156    84.7 | 86.903 % |
c |    189380 |  134420   274095 |   87438   28514  2435373    85.4 | 86.903 % |
c |    191088 |  134420   274095 |   96182   30222  2600030    86.0 | 86.903 % |
c |    193650 |  134417   274088 |  105801   32781  3007387    91.7 | 86.906 % |
c |    197495 |  134364   273965 |  116381   36616  3563866    97.3 | 86.962 % |
c |    203261 |  134364   273965 |  128019   42382  4293921   101.3 | 86.962 % |
c |    211910 |  134328   273873 |  140821   51012  5544856   108.7 | 87.005 % |
c |    224884 |  134328   273873 |  154903   63986  7907749   123.6 | 87.005 % |
c |    244345 |  134328   273873 |  170393   83447 11620820   139.3 | 87.005 % |
c ==============================================================================
c Found solution: -53
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    251911 |  134341   273909 |   44780   90983 12874260   141.5 | 87.005 % |
c |    252011 |  134341   273909 |   49258   91083 12879997   141.4 | 87.002 % |
c |    252162 |  134341   273909 |   54183   91234 12893752   141.3 | 87.002 % |
c |    252387 |  134341   273909 |   59602   91459 12918345   141.2 | 87.002 % |
c |    252725 |  134341   273909 |   65562   91797 12950424   141.1 | 87.002 % |
c |    253231 |  134337   273899 |   72118   92302 12995661   140.8 | 87.007 % |
c |    253991 |  134323   273863 |   79330   93028 13081442   140.6 | 87.025 % |
c |    255130 |  134323   273863 |   87263   94167 13274461   141.0 | 87.025 % |
c |    256838 |  134323   273863 |   95989   95875 13445425   140.2 | 87.025 % |
c |    259400 |  134283   273763 |  105588   98400 13873992   141.0 | 87.073 % |
c |    263244 |  134283   273763 |  116147  102244 14537960   142.2 | 87.073 % |
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/13063/stat): 13063 (minisat+_script) R 13062 13063 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843643805 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13063/statm): 174 3 169 147 0 27 0
[pid=13063] 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=13064
New process pid=13065
New process pid=13066
execve syscall for /bin/sed executable
One traced child (pid=13065) 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=13066) exited with status: 0
One traced child (pid=13064) exited with status: 0
New process pid=13067
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-frb59-26-5.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 936 36 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 33852

[startup+20.0047 s]
Raw data (loadavg): 0.94 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 1935 36 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 19.72
Current children cumulated vsize (Kb) 33852

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 2935 36 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 29.72
Current children cumulated vsize (Kb) 33852

[startup+40.007 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 3935 36 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 33852

[startup+50.0086 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 4935 36 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 33852

[startup+60.0092 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 5935 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223088 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 33852

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 6935 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223136 134554715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 33852

[startup+80.0115 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 7935 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223152 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 33852

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 8936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 33852

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 9936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 99.74
Current children cumulated vsize (Kb) 33852

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 10936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 109.74
Current children cumulated vsize (Kb) 33852

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 11936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 33852

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 12936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 129.74
Current children cumulated vsize (Kb) 33852

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 13936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223120 134555566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 139.74
Current children cumulated vsize (Kb) 33852

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 14936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 149.74
Current children cumulated vsize (Kb) 33852

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 15936 37 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223120 134670081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 159.74
Current children cumulated vsize (Kb) 33852

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 16936 38 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 169.75
Current children cumulated vsize (Kb) 33852

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 17936 38 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 179.75
Current children cumulated vsize (Kb) 33852

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 18937 38 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223040 134552014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 189.76
Current children cumulated vsize (Kb) 33852

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7823 0 0 0 19936 38 0 0 25 0 1 0 1843643810 32489472 7810 4294967295 134512640 135094434 3221224448 3221223040 134556906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7932 7810 145 145 0 7787 0
[pid=13067] vsize: 31728
Current children cumulated CPU time (s) 199.75
Current children cumulated vsize (Kb) 33852

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 7881 0 0 0 20935 39 0 0 25 0 1 0 1843643810 32718848 7868 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 7988 7868 145 145 0 7843 0
[pid=13067] vsize: 31952
Current children cumulated CPU time (s) 209.75
Current children cumulated vsize (Kb) 34076

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 8129 0 0 0 21931 41 0 0 25 0 1 0 1843643810 33861632 8116 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 8267 8116 145 145 0 8122 0
[pid=13067] vsize: 33068
Current children cumulated CPU time (s) 219.73
Current children cumulated vsize (Kb) 35192

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 8385 0 0 0 22926 44 0 0 25 0 1 0 1843643810 34897920 8372 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 8520 8372 145 145 0 8375 0
[pid=13067] vsize: 34080
Current children cumulated CPU time (s) 229.71
Current children cumulated vsize (Kb) 36204

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 8791 0 0 0 23919 46 0 0 25 0 1 0 1843643810 36233216 8701 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 8846 8701 145 145 0 8701 0
[pid=13067] vsize: 35384
Current children cumulated CPU time (s) 239.66
Current children cumulated vsize (Kb) 37508

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 9164 0 0 0 24913 49 0 0 25 0 1 0 1843643810 37748736 9074 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 9216 9074 145 145 0 9071 0
[pid=13067] vsize: 36864
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 38988

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 9765 0 0 0 25902 53 0 0 25 0 1 0 1843643810 40194048 9675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 9813 9675 145 145 0 9668 0
[pid=13067] vsize: 39252
Current children cumulated CPU time (s) 259.56
Current children cumulated vsize (Kb) 41376

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 10198 0 0 0 26895 56 0 0 25 0 1 0 1843643810 41951232 10108 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 10242 10108 145 145 0 10097 0
[pid=13067] vsize: 40968
Current children cumulated CPU time (s) 269.52
Current children cumulated vsize (Kb) 43092

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 10637 0 0 0 27887 59 0 0 25 0 1 0 1843643810 43737088 10547 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 10678 10547 145 145 0 10533 0
[pid=13067] vsize: 42712
Current children cumulated CPU time (s) 279.47
Current children cumulated vsize (Kb) 44836

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 11120 0 0 0 28879 63 0 0 25 0 1 0 1843643810 45703168 11030 4294967295 134512640 135094434 3221224448 3221223040 134779242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 11158 11030 145 145 0 11013 0
[pid=13067] vsize: 44632
Current children cumulated CPU time (s) 289.43
Current children cumulated vsize (Kb) 46756

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 11483 0 0 0 29874 65 0 0 25 0 1 0 1843643810 46862336 11316 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 11441 11316 145 145 0 11296 0
[pid=13067] vsize: 45764
Current children cumulated CPU time (s) 299.4
Current children cumulated vsize (Kb) 47888

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 11935 0 0 0 30867 68 0 0 25 0 1 0 1843643810 48701440 11768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 11890 11768 145 145 0 11745 0
[pid=13067] vsize: 47560
Current children cumulated CPU time (s) 309.36
Current children cumulated vsize (Kb) 49684

[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 12182 0 0 0 31863 70 0 0 25 0 1 0 1843643810 49393664 11938 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 12059 11938 145 145 0 11914 0
[pid=13067] vsize: 48236
Current children cumulated CPU time (s) 319.34
Current children cumulated vsize (Kb) 50360

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 12460 0 0 0 32860 71 0 0 25 0 1 0 1843643810 50466816 12139 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 12321 12139 145 145 0 12176 0
[pid=13067] vsize: 49284
Current children cumulated CPU time (s) 329.32
Current children cumulated vsize (Kb) 51408

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 12690 0 0 0 33856 73 0 0 25 0 1 0 1843643810 51400704 12369 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 12549 12369 145 145 0 12404 0
[pid=13067] vsize: 50196
Current children cumulated CPU time (s) 339.3
Current children cumulated vsize (Kb) 52320

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 13002 0 0 0 34850 76 0 0 25 0 1 0 1843643810 52670464 12681 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 12859 12681 145 145 0 12714 0
[pid=13067] vsize: 51436
Current children cumulated CPU time (s) 349.27
Current children cumulated vsize (Kb) 53560

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 13369 0 0 0 35844 79 0 0 25 0 1 0 1843643810 54161408 13048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 13223 13048 145 145 0 13078 0
[pid=13067] vsize: 52892
Current children cumulated CPU time (s) 359.24
Current children cumulated vsize (Kb) 55016

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 13722 0 0 0 36837 82 0 0 25 0 1 0 1843643810 55599104 13401 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 13574 13401 145 145 0 13429 0
[pid=13067] vsize: 54296
Current children cumulated CPU time (s) 369.2
Current children cumulated vsize (Kb) 56420

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 14073 0 0 0 37833 85 0 0 25 0 1 0 1843643810 57024512 13752 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 13922 13752 145 145 0 13777 0
[pid=13067] vsize: 55688
Current children cumulated CPU time (s) 379.19
Current children cumulated vsize (Kb) 57812

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 14429 0 0 0 38825 87 0 0 25 0 1 0 1843643810 58474496 14108 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 14276 14108 145 145 0 14131 0
[pid=13067] vsize: 57104
Current children cumulated CPU time (s) 389.13
Current children cumulated vsize (Kb) 59228

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 14764 0 0 0 39817 91 0 0 25 0 1 0 1843643810 59834368 14443 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 14608 14443 145 145 0 14463 0
[pid=13067] vsize: 58432
Current children cumulated CPU time (s) 399.09
Current children cumulated vsize (Kb) 60556

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 15147 0 0 0 40809 95 0 0 25 0 1 0 1843643810 61394944 14826 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 14989 14826 145 145 0 14844 0
[pid=13067] vsize: 59956
Current children cumulated CPU time (s) 409.05
Current children cumulated vsize (Kb) 62080

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 15631 0 0 0 41800 98 0 0 25 0 1 0 1843643810 63369216 15310 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 15471 15310 145 145 0 15326 0
[pid=13067] vsize: 61884
Current children cumulated CPU time (s) 418.99
Current children cumulated vsize (Kb) 64008

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 16033 0 0 0 42793 101 0 0 25 0 1 0 1843643810 65007616 15712 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 15871 15712 145 145 0 15726 0
[pid=13067] vsize: 63484
Current children cumulated CPU time (s) 428.95
Current children cumulated vsize (Kb) 65608

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 16472 0 0 0 43787 103 0 0 25 0 1 0 1843643810 66793472 16151 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 16307 16151 145 145 0 16162 0
[pid=13067] vsize: 65228
Current children cumulated CPU time (s) 438.91
Current children cumulated vsize (Kb) 67352

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 16796 0 0 0 44783 105 0 0 25 0 1 0 1843643810 68112384 16475 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 16629 16475 145 145 0 16484 0
[pid=13067] vsize: 66516
Current children cumulated CPU time (s) 448.89
Current children cumulated vsize (Kb) 68640

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 17064 0 0 0 45778 107 0 0 25 0 1 0 1843643810 69201920 16743 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 16895 16743 145 145 0 16750 0
[pid=13067] vsize: 67580
Current children cumulated CPU time (s) 458.86
Current children cumulated vsize (Kb) 69704

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 17352 0 0 0 46771 110 0 0 25 0 1 0 1843643810 70373376 17031 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 17181 17031 145 145 0 17036 0
[pid=13067] vsize: 68724
Current children cumulated CPU time (s) 468.82
Current children cumulated vsize (Kb) 70848

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 17757 0 0 0 47762 114 0 0 25 0 1 0 1843643810 72024064 17436 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 17584 17436 145 145 0 17439 0
[pid=13067] vsize: 70336
Current children cumulated CPU time (s) 478.77
Current children cumulated vsize (Kb) 72460

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 18073 0 0 0 48756 118 0 0 25 0 1 0 1843643810 73310208 17752 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 17898 17752 145 145 0 17753 0
[pid=13067] vsize: 71592
Current children cumulated CPU time (s) 488.75
Current children cumulated vsize (Kb) 73716

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 18468 0 0 0 49749 120 0 0 25 0 1 0 1843643810 74919936 18147 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434789 0 0 17 0 0 0
Raw data (/proc/13067/statm): 18291 18147 145 145 0 18146 0
[pid=13067] vsize: 73164
Current children cumulated CPU time (s) 498.7
Current children cumulated vsize (Kb) 75288

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 18892 0 0 0 50741 124 0 0 25 0 1 0 1843643810 76648448 18571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 18713 18571 145 145 0 18568 0
[pid=13067] vsize: 74852
Current children cumulated CPU time (s) 508.66
Current children cumulated vsize (Kb) 76976

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 19327 0 0 0 51732 127 0 0 25 0 1 0 1843643810 78426112 19006 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 19147 19006 145 145 0 19002 0
[pid=13067] vsize: 76588
Current children cumulated CPU time (s) 518.6
Current children cumulated vsize (Kb) 78712

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 19566 0 0 0 52728 130 0 0 25 0 1 0 1843643810 79396864 19245 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 19384 19245 145 145 0 19239 0
[pid=13067] vsize: 77536
Current children cumulated CPU time (s) 528.59
Current children cumulated vsize (Kb) 79660

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 19883 0 0 0 53723 132 0 0 25 0 1 0 1843643810 80687104 19562 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 19699 19562 145 145 0 19554 0
[pid=13067] vsize: 78796
Current children cumulated CPU time (s) 538.56
Current children cumulated vsize (Kb) 80920

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 20253 0 0 0 54718 134 0 0 25 0 1 0 1843643810 82194432 19932 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 20067 19932 145 145 0 19922 0
[pid=13067] vsize: 80268
Current children cumulated CPU time (s) 548.53
Current children cumulated vsize (Kb) 82392

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 20601 0 0 0 55712 137 0 0 25 0 1 0 1843643810 83611648 20280 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 20413 20280 145 145 0 20268 0
[pid=13067] vsize: 81652
Current children cumulated CPU time (s) 558.5
Current children cumulated vsize (Kb) 83776

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 20958 0 0 0 56705 140 0 0 25 0 1 0 1843643810 85069824 20637 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 20769 20637 145 145 0 20624 0
[pid=13067] vsize: 83076
Current children cumulated CPU time (s) 568.46
Current children cumulated vsize (Kb) 85200

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 21313 0 0 0 57698 143 0 0 25 0 1 0 1843643810 86515712 20992 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 21122 20992 145 145 0 20977 0
[pid=13067] vsize: 84488
Current children cumulated CPU time (s) 578.42
Current children cumulated vsize (Kb) 86612

[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 21613 0 0 0 58693 145 0 0 25 0 1 0 1843643810 87736320 21292 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 21420 21292 145 145 0 21275 0
[pid=13067] vsize: 85680
Current children cumulated CPU time (s) 588.39
Current children cumulated vsize (Kb) 87804

[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 21876 0 0 0 59688 147 0 0 25 0 1 0 1843643810 88809472 21555 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 21682 21555 145 145 0 21537 0
[pid=13067] vsize: 86728
Current children cumulated CPU time (s) 598.36
Current children cumulated vsize (Kb) 88852

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 22158 0 0 0 60684 149 0 0 25 0 1 0 1843643810 89960448 21837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 21963 21837 145 145 0 21818 0
[pid=13067] vsize: 87852
Current children cumulated CPU time (s) 608.34
Current children cumulated vsize (Kb) 89976

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 22522 0 0 0 61677 153 0 0 25 0 1 0 1843643810 91443200 22201 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 22325 22201 145 145 0 22180 0
[pid=13067] vsize: 89300
Current children cumulated CPU time (s) 618.31
Current children cumulated vsize (Kb) 91424

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 22907 0 0 0 62671 155 0 0 25 0 1 0 1843643810 93016064 22586 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 22709 22586 145 145 0 22564 0
[pid=13067] vsize: 90836
Current children cumulated CPU time (s) 628.27
Current children cumulated vsize (Kb) 92960

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 23272 0 0 0 63665 157 0 0 25 0 1 0 1843643810 94502912 22951 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 23072 22951 145 145 0 22927 0
[pid=13067] vsize: 92288
Current children cumulated CPU time (s) 638.23
Current children cumulated vsize (Kb) 94412

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 23613 0 0 0 64659 160 0 0 25 0 1 0 1843643810 96419840 23292 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 23540 23292 145 145 0 23395 0
[pid=13067] vsize: 94160
Current children cumulated CPU time (s) 648.2
Current children cumulated vsize (Kb) 96284

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 23954 0 0 0 65654 162 0 0 25 0 1 0 1843643810 97812480 23633 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 23880 23633 145 145 0 23735 0
[pid=13067] vsize: 95520
Current children cumulated CPU time (s) 658.17
Current children cumulated vsize (Kb) 97644

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 24308 0 0 0 66649 164 0 0 25 0 1 0 1843643810 99254272 23987 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 24232 23987 145 145 0 24087 0
[pid=13067] vsize: 96928
Current children cumulated CPU time (s) 668.14
Current children cumulated vsize (Kb) 99052

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 24621 0 0 0 67644 166 0 0 25 0 1 0 1843643810 100532224 24300 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 24544 24300 145 145 0 24399 0
[pid=13067] vsize: 98176
Current children cumulated CPU time (s) 678.11
Current children cumulated vsize (Kb) 100300

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 24894 0 0 0 68640 168 0 0 25 0 1 0 1843643810 101646336 24573 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 24816 24573 145 145 0 24671 0
[pid=13067] vsize: 99264
Current children cumulated CPU time (s) 688.09
Current children cumulated vsize (Kb) 101388

[startup+700.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 25202 0 0 0 69635 171 0 0 25 0 1 0 1843643810 102903808 24881 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 25123 24881 145 145 0 24978 0
[pid=13067] vsize: 100492
Current children cumulated CPU time (s) 698.07
Current children cumulated vsize (Kb) 102616

[startup+710.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 25516 0 0 0 70629 172 0 0 25 0 1 0 1843643810 104185856 25195 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 25436 25195 145 145 0 25291 0
[pid=13067] vsize: 101744
Current children cumulated CPU time (s) 708.02
Current children cumulated vsize (Kb) 103868

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 25768 0 0 0 71627 173 0 0 25 0 1 0 1843643810 105218048 25447 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 25688 25447 145 145 0 25543 0
[pid=13067] vsize: 102752
Current children cumulated CPU time (s) 718.01
Current children cumulated vsize (Kb) 104876

[startup+730.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 26068 0 0 0 72621 176 0 0 25 0 1 0 1843643810 106438656 25747 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 25986 25747 145 145 0 25841 0
[pid=13067] vsize: 103944
Current children cumulated CPU time (s) 727.98
Current children cumulated vsize (Kb) 106068

[startup+740.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 26391 0 0 0 73615 178 0 0 25 0 1 0 1843643810 107761664 26070 4294967295 134512640 135094434 3221224448 3221222992 134562158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 26309 26070 145 145 0 26164 0
[pid=13067] vsize: 105236
Current children cumulated CPU time (s) 737.94
Current children cumulated vsize (Kb) 107360

[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 26712 0 0 0 74609 180 0 0 25 0 1 0 1843643810 109068288 26391 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 26628 26391 145 145 0 26483 0
[pid=13067] vsize: 106512
Current children cumulated CPU time (s) 747.9
Current children cumulated vsize (Kb) 108636

[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 26950 0 0 0 75605 182 0 0 25 0 1 0 1843643810 110039040 26629 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 26865 26629 145 145 0 26720 0
[pid=13067] vsize: 107460
Current children cumulated CPU time (s) 757.88
Current children cumulated vsize (Kb) 109584

[startup+770.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 27161 0 0 0 76601 184 0 0 25 0 1 0 1843643810 110899200 26840 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 27075 26840 145 145 0 26930 0
[pid=13067] vsize: 108300
Current children cumulated CPU time (s) 767.86
Current children cumulated vsize (Kb) 110424

[startup+780.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 27325 0 0 0 77598 185 0 0 25 0 1 0 1843643810 111562752 27004 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 27237 27004 145 145 0 27092 0
[pid=13067] vsize: 108948
Current children cumulated CPU time (s) 777.84
Current children cumulated vsize (Kb) 111072

[startup+790.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 27542 0 0 0 78594 187 0 0 25 0 1 0 1843643810 112447488 27221 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 27453 27221 145 145 0 27308 0
[pid=13067] vsize: 109812
Current children cumulated CPU time (s) 787.82
Current children cumulated vsize (Kb) 111936

[startup+800.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 27814 0 0 0 79590 188 0 0 25 0 1 0 1843643810 113553408 27493 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 27723 27493 145 145 0 27578 0
[pid=13067] vsize: 110892
Current children cumulated CPU time (s) 797.79
Current children cumulated vsize (Kb) 113016

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 28066 0 0 0 80585 190 0 0 25 0 1 0 1843643810 114581504 27745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 27974 27745 145 145 0 27829 0
[pid=13067] vsize: 111896
Current children cumulated CPU time (s) 807.76
Current children cumulated vsize (Kb) 114020

[startup+820.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 28269 0 0 0 81582 192 0 0 25 0 1 0 1843643810 115408896 27948 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 28176 27948 145 145 0 28031 0
[pid=13067] vsize: 112704
Current children cumulated CPU time (s) 817.75
Current children cumulated vsize (Kb) 114828

[startup+830.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 28493 0 0 0 82579 193 0 0 25 0 1 0 1843643810 116322304 28172 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 28399 28172 145 145 0 28254 0
[pid=13067] vsize: 113596
Current children cumulated CPU time (s) 827.73
Current children cumulated vsize (Kb) 115720

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 28737 0 0 0 83574 196 0 0 25 0 1 0 1843643810 117313536 28416 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 28641 28416 145 145 0 28496 0
[pid=13067] vsize: 114564
Current children cumulated CPU time (s) 837.71
Current children cumulated vsize (Kb) 116688

[startup+850.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 28976 0 0 0 84569 198 0 0 25 0 1 0 1843643810 118288384 28655 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 28879 28655 145 145 0 28734 0
[pid=13067] vsize: 115516
Current children cumulated CPU time (s) 847.68
Current children cumulated vsize (Kb) 117640

[startup+860.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 29228 0 0 0 85564 200 0 0 25 0 1 0 1843643810 119312384 28907 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 29129 28907 145 145 0 28984 0
[pid=13067] vsize: 116516
Current children cumulated CPU time (s) 857.65
Current children cumulated vsize (Kb) 118640

[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 29523 0 0 0 86556 204 0 0 25 0 1 0 1843643810 120516608 29202 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 29423 29202 145 145 0 29278 0
[pid=13067] vsize: 117692
Current children cumulated CPU time (s) 867.61
Current children cumulated vsize (Kb) 119816

[startup+880.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 29839 0 0 0 87550 208 0 0 25 0 1 0 1843643810 121806848 29518 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 29738 29518 145 145 0 29593 0
[pid=13067] vsize: 118952
Current children cumulated CPU time (s) 877.59
Current children cumulated vsize (Kb) 121076

[startup+890.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30140 0 0 0 88544 210 0 0 25 0 1 0 1843643810 123035648 29819 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30038 29819 145 145 0 29893 0
[pid=13067] vsize: 120152
Current children cumulated CPU time (s) 887.55
Current children cumulated vsize (Kb) 122276

[startup+900.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30374 0 0 0 89539 212 0 0 25 0 1 0 1843643810 123985920 30053 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30270 30053 145 145 0 30125 0
[pid=13067] vsize: 121080
Current children cumulated CPU time (s) 897.52
Current children cumulated vsize (Kb) 123204

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 90536 214 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 907.51
Current children cumulated vsize (Kb) 123508

[startup+920.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 91536 214 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 917.51
Current children cumulated vsize (Kb) 123508

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 92535 215 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223188 134559726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 927.51
Current children cumulated vsize (Kb) 123508

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 93535 216 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 937.52
Current children cumulated vsize (Kb) 123508

[startup+950.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 94534 216 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 947.51
Current children cumulated vsize (Kb) 123508

[startup+960.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 95534 217 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 957.52
Current children cumulated vsize (Kb) 123508

[startup+970.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 96533 217 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 967.51
Current children cumulated vsize (Kb) 123508

[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 97533 218 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 977.52
Current children cumulated vsize (Kb) 123508

[startup+990.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 98532 218 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 987.51
Current children cumulated vsize (Kb) 123508

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 99532 218 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 997.51
Current children cumulated vsize (Kb) 123508

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 100532 219 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1007.52
Current children cumulated vsize (Kb) 123508

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 101532 219 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223040 134556880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1017.52
Current children cumulated vsize (Kb) 123508

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 102531 219 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1027.51
Current children cumulated vsize (Kb) 123508

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 103531 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1037.52
Current children cumulated vsize (Kb) 123508

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 104531 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1047.52
Current children cumulated vsize (Kb) 123508

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 105532 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1057.53
Current children cumulated vsize (Kb) 123508

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 106532 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1067.53
Current children cumulated vsize (Kb) 123508

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 107532 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1077.53
Current children cumulated vsize (Kb) 123508

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 108532 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1087.53
Current children cumulated vsize (Kb) 123508

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 109532 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1097.53
Current children cumulated vsize (Kb) 123508

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 110533 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223040 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1107.54
Current children cumulated vsize (Kb) 123508

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 111533 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1117.54
Current children cumulated vsize (Kb) 123508

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 112533 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1127.54
Current children cumulated vsize (Kb) 123508

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 113533 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1137.54
Current children cumulated vsize (Kb) 123508

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 114533 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1147.54
Current children cumulated vsize (Kb) 123508

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 115534 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1157.55
Current children cumulated vsize (Kb) 123508

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 116534 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1167.55
Current children cumulated vsize (Kb) 123508

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 117534 220 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1177.55
Current children cumulated vsize (Kb) 123508

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 118534 221 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1187.56
Current children cumulated vsize (Kb) 123508

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 119534 221 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1197.56
Current children cumulated vsize (Kb) 123508

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 120535 221 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1207.57
Current children cumulated vsize (Kb) 123508



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13067
Raw data (/proc/13063/stat): 13063 (minisat+_script) S 13062 13063 5299 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843643805 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13063/statm): 531 226 485 147 0 384 0
[pid=13063] vsize: 2124
Raw data (/proc/13067/stat): 13067 (minisat+_64-bit) R 13063 13063 5299 0 -1 0 30527 0 0 0 120535 221 0 0 25 0 1 0 1843643810 124297216 30129 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13067/statm): 30346 30129 145 145 0 30201 0
[pid=13067] vsize: 121384
Current children cumulated CPU time (s) 1207.57
Current children cumulated vsize (Kb) 123508

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1207.62
CPU user time (s): 1205.35
CPU system time (s): 2.26965
CPU usage (%): 99.7896
Max. virtual memory (cumulated for all children) (Kb): 123508

Verifier Data

ERROR: no interpretation found !