Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb56-25-opb/normalized-frb56-25-3.opb
MD5SUM3f087816af6a7fb75be2e9f81cc24df7
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -43
Optimality of the best value was proved NO
Number of terms in the objective function 1400
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1400
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1400
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1203.19
Number of variables1400
Total number of constraints109379
Number of constraints which are clauses109379
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 2332

Launcher Data

LAUNCH ON wulflinc19 THE 2005-09-18 18:59:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2719 boxname=wulflinc19 idbench=375 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3f087816af6a7fb75be2e9f81cc24df7  /oldhome/oroussel/tmp/wulflinc19/normalized-frb56-25-3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-frb56-25-3.opb
IDLAUNCH: 2719
/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:        919992 kB
Buffers:         34528 kB
Cached:          52904 kB
SwapCached:        832 kB
Active:          62924 kB
Inactive:        27052 kB
HighTotal:      131008 kB
HighFree:        77420 kB
LowTotal:       903652 kB
LowFree:        842572 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19132 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:19:57 (client local time) WITH STATUS 10 IN 1207.53 SECONDS
stats: 2719 7 1207.53 10

Solver Data

c Parsing PB file...
c Converting 109379 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 |  109379   218758 |   36459       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:78076     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  193072   415055 |   64357       0        0     nan |  0.000 % |
c |       100 |  192289   413380 |   70792      76      438     5.8 |  0.796 % |
c |       250 |  191308   411295 |   77871     154     1089     7.1 |  1.765 % |
c |       475 |  189986   408459 |   85659     332     3281     9.9 |  3.095 % |
c |       812 |  188252   404641 |   94225     591     5859     9.9 |  4.924 % |
c |      1318 |  185282   398055 |  103647     966    10783    11.2 |  8.159 % |
c |      2077 |  180838   388205 |  114012    1540    17472    11.3 | 12.913 % |
c |      3216 |  174564   374091 |  125413    2383    27299    11.5 | 19.709 % |
c |      4924 |  165519   353508 |  137954    3677    43819    11.9 | 29.753 % |
c |      7486 |  155664   330749 |  151750    5389    63888    11.9 | 40.969 % |
c ==============================================================================
c Found solution: -42
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7678 |  155277   329891 |   51759    5555    66399    12.0 | 40.969 % |
c |      7778 |  155112   329513 |   56934    5646    67027    11.9 | 41.617 % |
c |      7928 |  154703   328544 |   62628    5760    68552    11.9 | 42.108 % |
c |      8153 |  153653   326101 |   68891    5917    70305    11.9 | 43.312 % |
c |      8491 |  152864   324267 |   75780    6136    73256    11.9 | 44.216 % |
c |      8997 |  150953   319781 |   83358    6468    76139    11.8 | 46.384 % |
c |      9756 |  148474   313934 |   91694    6960    82237    11.8 | 49.283 % |
c |     10895 |  144799   305265 |  100863    7805    92930    11.9 | 53.569 % |
c |     12603 |  139793   293375 |  110950    8870   106020    12.0 | 59.496 % |
c |     15165 |  135051   282169 |  122045   10462   131410    12.6 | 65.125 % |
c |     19010 |  129965   270060 |  134249   13548   195200    14.4 | 71.137 % |
c |     24776 |  126588   261988 |  147674   18369   339931    18.5 | 75.205 % |
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 |     32090 |  124714   257528 |   41571   24908   642270    25.8 | 75.205 % |
c |     32190 |  124620   257302 |   45728   24877   642286    25.8 | 77.650 % |
c |     32340 |  124503   257023 |   50300   24964   645321    25.9 | 77.792 % |
c |     32565 |  124503   257023 |   55331   25189   657624    26.1 | 77.792 % |
c |     32902 |  124248   256413 |   60864   25322   668588    26.4 | 78.100 % |
c |     33409 |  124048   255923 |   66950   25747   685296    26.6 | 78.349 % |
c |     34169 |  123814   255346 |   73645   26344   707362    26.9 | 78.659 % |
c |     35308 |  123314   254145 |   81010   26766   734139    27.4 | 79.251 % |
c |     37016 |  122980   253317 |   89111   28310   800471    28.3 | 79.671 % |
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 |     38041 |  122955   253294 |   40985   29330   878435    30.0 | 79.671 % |
c |     38141 |  122908   253175 |   45083   29428   881494    30.0 | 79.772 % |
c |     38292 |  122808   252938 |   49591   29459   884935    30.0 | 79.889 % |
c |     38517 |  122701   252678 |   54551   29640   893182    30.1 | 80.022 % |
c |     38854 |  122469   252128 |   60006   29755   899984    30.2 | 80.300 % |
c |     39360 |  122418   251995 |   66006   30229   921921    30.5 | 80.369 % |
c |     40120 |  122408   251969 |   72607   30944   953783    30.8 | 80.383 % |
c |     41259 |  121915   250781 |   79868   31596  1004535    31.8 | 80.976 % |
c |     42967 |  121553   249906 |   87854   32982  1091208    33.1 | 81.405 % |
c ==============================================================================
c Found solution: -46
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43880 |  120877   248170 |   40292   33490  1122781    33.5 | 81.405 % |
c |     43981 |  120746   247855 |   44321   33468  1122634    33.5 | 82.436 % |
c |     44131 |  120643   247601 |   48753   33534  1125930    33.6 | 82.568 % |
c |     44356 |  120639   247591 |   53628   33757  1134632    33.6 | 82.573 % |
c |     44694 |  120639   247591 |   58991   34095  1167457    34.2 | 82.573 % |
c |     45202 |  120555   247389 |   64890   34455  1205966    35.0 | 82.676 % |
c |     45961 |  120449   247139 |   71379   35097  1268003    36.1 | 82.802 % |
c |     47100 |  120449   247139 |   78517   36236  1343983    37.1 | 82.802 % |
c |     48808 |  120381   246969 |   86369   37873  1461540    38.6 | 82.891 % |
c |     51370 |  120381   246969 |   95006   40435  1758124    43.5 | 82.891 % |
c |     55214 |  120194   246508 |  104507   44166  2049429    46.4 | 83.131 % |
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 |     59419 |  120236   246644 |   40078   48283  2571328    53.3 | 83.131 % |
c |     59519 |  120236   246644 |   44085   48383  2577827    53.3 | 83.121 % |
c |     59669 |  120046   246170 |   48494   48153  2573782    53.5 | 83.366 % |
c |     59894 |  120046   246170 |   53343   48378  2587917    53.5 | 83.366 % |
c |     60231 |  120046   246170 |   58678   48715  2610106    53.6 | 83.366 % |
c |     60737 |  119972   245994 |   64546   49150  2641554    53.7 | 83.455 % |
c |     61496 |  119972   245994 |   71000   49909  2689717    53.9 | 83.455 % |
c |     62635 |  119972   245994 |   78100   51048  2778866    54.4 | 83.455 % |
c |     64345 |  119928   245882 |   85910   52609  2939154    55.9 | 83.512 % |
c |     66908 |  119762   245470 |   94501   54951  3124242    56.9 | 83.722 % |
c |     70752 |  119678   245269 |  103952   58681  3464776    59.0 | 83.821 % |
c |     76518 |  119245   244229 |  114347   63705  4075621    64.0 | 84.345 % |
c |     85167 |  119220   244168 |  125781   72202  4873608    67.5 | 84.377 % |
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 |     89191 |  119133   243922 |   39711   75689  5308024    70.1 | 84.377 % |
c |     89293 |  119097   243838 |   43682   75747  5308704    70.1 | 84.538 % |
c |     89443 |  119097   243838 |   48050   75897  5313532    70.0 | 84.538 % |
c |     89668 |  119097   243838 |   52855   76122  5343666    70.2 | 84.538 % |
c |     90005 |  119097   243838 |   58140   76459  5376009    70.3 | 84.538 % |
c |     90511 |  119097   243838 |   63954   76965  5418238    70.4 | 84.538 % |
c |     91270 |  119092   243827 |   70350   77719  5484685    70.6 | 84.543 % |
c |     92410 |  119061   243749 |   77385   78821  5576081    70.7 | 84.583 % |
c |     94119 |  119009   243626 |   85124   79969  5732669    71.7 | 84.641 % |
c |     96681 |  118880   243323 |   93636   82103  6068614    73.9 | 84.793 % |
c |    100525 |  118867   243294 |  103000   85937  6618201    77.0 | 84.807 % |
c |    106291 |  118844   243239 |  113300   91697  7472440    81.5 | 84.835 % |
c |    114941 |  118836   243219 |  124630  100333  8787645    87.6 | 84.845 % |
c |    127915 |  118830   243203 |  137093  113301 10621442    93.7 | 84.854 % |
c |    147376 |  118811   243160 |  150802  132530 13627869   102.8 | 84.875 % |
c |    176568 |  118770   243067 |  165882  161493 19013368   117.7 | 84.920 % |
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 |    194891 |  118792   243133 |   39597  179816 22236738   123.7 | 84.920 % |
c |    194991 |  118792   243133 |   43556   25721  2608842   101.4 | 84.904 % |
c |    195141 |  118792   243133 |   47912   25871  2618895   101.2 | 84.904 % |
c |    195366 |  118792   243133 |   52703   26096  2633968   100.9 | 84.904 % |
c |    195703 |  118792   243133 |   57973   26433  2658439   100.6 | 84.904 % |
c |    196209 |  118746   243016 |   63771   26900  2696719   100.2 | 84.960 % |
c |    196968 |  118746   243016 |   70148   27659  2783846   100.6 | 84.960 % |
c |    198107 |  118746   243016 |   77163   28798  2904085   100.8 | 84.960 % |
c |    199815 |  118708   242922 |   84879   30503  3038914    99.6 | 85.009 % |
c |    202377 |  118561   242559 |   93367   33010  3263398    98.9 | 85.195 % |
c |    206221 |  118438   242259 |  102704   36848  3708724   100.6 | 85.347 % |
c |    211987 |  118423   242224 |  112974   42603  4394753   103.2 | 85.365 % |
c |    220636 |  118399   242168 |  124272   51236  5537942   108.1 | 85.393 % |
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 |    229090 |  118286   241857 |   39428   59647  6700392   112.3 | 85.393 % |
c |    229190 |  118286   241857 |   43370   59747  6707785   112.3 | 85.535 % |
c |    229342 |  118286   241857 |   47707   59899  6717998   112.2 | 85.535 % |
c |    229567 |  118286   241857 |   52478   60124  6753812   112.3 | 85.535 % |
c |    229904 |  118286   241857 |   57726   60461  6781159   112.2 | 85.535 % |
c |    230410 |  118286   241857 |   63499   60967  6854467   112.4 | 85.535 % |
c |    231169 |  118286   241857 |   69849   61726  6920330   112.1 | 85.535 % |
c |    232308 |  118286   241857 |   76834   62865  7085436   112.7 | 85.535 % |
c |    234016 |  118286   241857 |   84517   64573  7329189   113.5 | 85.535 % |
c |    236578 |  118280   241843 |   92969   67081  7761358   115.7 | 85.542 % |
c |    240423 |  118280   241843 |  102266   70926  8364204   117.9 | 85.542 % |
c |    246189 |  118195   241640 |  112492   76643  9241235   120.6 | 85.644 % |
c |    254838 |  118192   241633 |  123741   85290 10512072   123.3 | 85.648 % |
c |    267813 |  118081   241357 |  136116   98069 12211460   124.5 | 85.791 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 C1387 -C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 C1177 -C1176 -C1175 -C1174 C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 C854 -C853 -C852 -C851 -C850 -C849 C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 C704 -C703 -C702 -C701 -C700 C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 C606 -C605 -C604 -C603 -C602 -C601 -C600 C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 C502 -C501 -C500 -C499 -C498 -C497 -C496 C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 C452 -C451 -C450 C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 C327 -C326 -C325 -C324 -C323 -C322 C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 C103 -C102 -C1

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/12864/stat): 12864 (minisat+_script) R 12863 12864 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843588559 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12864/statm): 174 3 169 147 0 27 0
[pid=12864] 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=12865
New process pid=12866
New process pid=12867
One traced child (pid=12866) exited with status: 0
execve syscall for /bin/sed executable
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=12867) exited with status: 0
One traced child (pid=12865) exited with status: 0
New process pid=12868
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-frb56-25-3.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.95 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 947 27 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 30048

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 1947 27 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 19.75
Current children cumulated vsize (Kb) 30048

[startup+30.007 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 2946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 30048

[startup+40.0078 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 3946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 30048

[startup+50.0096 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 4946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 30048

[startup+60.0104 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 5946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 30048

[startup+70.0122 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 6946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 30048

[startup+80.013 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 7946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223132 134553432 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 79.75
Current children cumulated vsize (Kb) 30048

[startup+90.0138 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 8947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 89.76
Current children cumulated vsize (Kb) 30048

[startup+100.015 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 9947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 30048

[startup+110.015 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 10947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 109.76
Current children cumulated vsize (Kb) 30048

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 11947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 119.76
Current children cumulated vsize (Kb) 30048

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 12948 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 129.77
Current children cumulated vsize (Kb) 30048

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 13948 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0
[pid=12868] vsize: 27924
Current children cumulated CPU time (s) 139.77
Current children cumulated vsize (Kb) 30048

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6963 0 0 0 14946 29 0 0 25 0 1 0 1843588564 29122560 6950 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 7110 6950 145 145 0 6965 0
[pid=12868] vsize: 28440
Current children cumulated CPU time (s) 149.76
Current children cumulated vsize (Kb) 30564

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 7288 0 0 0 15941 31 0 0 25 0 1 0 1843588564 30146560 7200 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12868/statm): 7360 7200 145 145 0 7215 0
[pid=12868] vsize: 29440
Current children cumulated CPU time (s) 159.73
Current children cumulated vsize (Kb) 31564

[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 7591 0 0 0 16936 34 0 0 25 0 1 0 1843588564 31076352 7427 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12868/statm): 7587 7427 145 145 0 7442 0
[pid=12868] vsize: 30348
Current children cumulated CPU time (s) 169.71
Current children cumulated vsize (Kb) 32472

[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 7832 0 0 0 17931 35 0 0 25 0 1 0 1843588564 32190464 7668 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 7859 7668 145 145 0 7714 0
[pid=12868] vsize: 31436
Current children cumulated CPU time (s) 179.67
Current children cumulated vsize (Kb) 33560

[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 8174 0 0 0 18926 38 0 0 25 0 1 0 1843588564 33271808 7935 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 8123 7935 145 145 0 7978 0
[pid=12868] vsize: 32492
Current children cumulated CPU time (s) 189.65
Current children cumulated vsize (Kb) 34616

[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 8676 0 0 0 19917 41 0 0 25 0 1 0 1843588564 35307520 8437 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 8620 8437 145 145 0 8475 0
[pid=12868] vsize: 34480
Current children cumulated CPU time (s) 199.59
Current children cumulated vsize (Kb) 36604

[startup+210.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 9072 0 0 0 20910 45 0 0 25 0 1 0 1843588564 36913152 8833 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 9012 8833 145 145 0 8867 0
[pid=12868] vsize: 36048
Current children cumulated CPU time (s) 209.56
Current children cumulated vsize (Kb) 38172

[startup+220.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 9615 0 0 0 21901 49 0 0 25 0 1 0 1843588564 38813696 9300 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 9476 9300 145 145 0 9331 0
[pid=12868] vsize: 37904
Current children cumulated CPU time (s) 219.51
Current children cumulated vsize (Kb) 40028

[startup+230.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 9975 0 0 0 22896 51 0 0 25 0 1 0 1843588564 40271872 9660 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 9832 9660 145 145 0 9687 0
[pid=12868] vsize: 39328
Current children cumulated CPU time (s) 229.48
Current children cumulated vsize (Kb) 41452

[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 10297 0 0 0 23890 53 0 0 25 0 1 0 1843588564 41578496 9982 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 10151 9982 145 145 0 10006 0
[pid=12868] vsize: 40604
Current children cumulated CPU time (s) 239.44
Current children cumulated vsize (Kb) 42728

[startup+250.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 10606 0 0 0 24883 55 0 0 25 0 1 0 1843588564 42831872 10291 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 10457 10291 145 145 0 10312 0
[pid=12868] vsize: 41828
Current children cumulated CPU time (s) 249.39
Current children cumulated vsize (Kb) 43952

[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 11038 0 0 0 25877 58 0 0 25 0 1 0 1843588564 44593152 10723 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12868/statm): 10887 10723 145 145 0 10742 0
[pid=12868] vsize: 43548
Current children cumulated CPU time (s) 259.36
Current children cumulated vsize (Kb) 45672

[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 11375 0 0 0 26870 61 0 0 25 0 1 0 1843588564 45957120 11060 4294967295 134512640 135094434 3221224448 3221223104 134561720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 11220 11060 145 145 0 11075 0
[pid=12868] vsize: 44880
Current children cumulated CPU time (s) 269.32
Current children cumulated vsize (Kb) 47004

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 11745 0 0 0 27863 64 0 0 25 0 1 0 1843588564 47718400 11430 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 11650 11430 145 145 0 11505 0
[pid=12868] vsize: 46600
Current children cumulated CPU time (s) 279.28
Current children cumulated vsize (Kb) 48724

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 12124 0 0 0 28857 67 0 0 25 0 1 0 1843588564 49258496 11809 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 12026 11809 145 145 0 11881 0
[pid=12868] vsize: 48104
Current children cumulated CPU time (s) 289.25
Current children cumulated vsize (Kb) 50228

[startup+300.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 12481 0 0 0 29849 71 0 0 25 0 1 0 1843588564 50708480 12166 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 12380 12166 145 145 0 12235 0
[pid=12868] vsize: 49520
Current children cumulated CPU time (s) 299.21
Current children cumulated vsize (Kb) 51644

[startup+310.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 12844 0 0 0 30843 73 0 0 25 0 1 0 1843588564 51879936 12454 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 12666 12454 145 145 0 12521 0
[pid=12868] vsize: 50664
Current children cumulated CPU time (s) 309.17
Current children cumulated vsize (Kb) 52788

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 13128 0 0 0 31839 75 0 0 25 0 1 0 1843588564 53035008 12738 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 12948 12738 145 145 0 12803 0
[pid=12868] vsize: 51792
Current children cumulated CPU time (s) 319.15
Current children cumulated vsize (Kb) 53916

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 13467 0 0 0 32833 78 0 0 25 0 1 0 1843588564 54415360 13077 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 13285 13077 145 145 0 13140 0
[pid=12868] vsize: 53140
Current children cumulated CPU time (s) 329.12
Current children cumulated vsize (Kb) 55264

[startup+340.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 13888 0 0 0 33826 80 0 0 25 0 1 0 1843588564 56127488 13498 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 13703 13498 145 145 0 13558 0
[pid=12868] vsize: 54812
Current children cumulated CPU time (s) 339.07
Current children cumulated vsize (Kb) 56936

[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 14189 0 0 0 34822 82 0 0 25 0 1 0 1843588564 57352192 13799 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 14002 13799 145 145 0 13857 0
[pid=12868] vsize: 56008
Current children cumulated CPU time (s) 349.05
Current children cumulated vsize (Kb) 58132

[startup+360.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 14607 0 0 0 35815 85 0 0 25 0 1 0 1843588564 59056128 14217 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 14418 14217 145 145 0 14273 0
[pid=12868] vsize: 57672
Current children cumulated CPU time (s) 359.01
Current children cumulated vsize (Kb) 59796

[startup+370.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 15001 0 0 0 36809 87 0 0 25 0 1 0 1843588564 60657664 14611 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 14809 14611 145 145 0 14664 0
[pid=12868] vsize: 59236
Current children cumulated CPU time (s) 368.97
Current children cumulated vsize (Kb) 61360

[startup+380.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 15347 0 0 0 37802 91 0 0 25 0 1 0 1843588564 62066688 14957 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 15153 14957 145 145 0 15008 0
[pid=12868] vsize: 60612
Current children cumulated CPU time (s) 378.94
Current children cumulated vsize (Kb) 62736

[startup+390.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 15726 0 0 0 38795 93 0 0 25 0 1 0 1843588564 63606784 15336 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 15529 15336 145 145 0 15384 0
[pid=12868] vsize: 62116
Current children cumulated CPU time (s) 388.89
Current children cumulated vsize (Kb) 64240

[startup+400.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 16141 0 0 0 39788 96 0 0 25 0 1 0 1843588564 65298432 15751 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 15942 15751 145 145 0 15797 0
[pid=12868] vsize: 63768
Current children cumulated CPU time (s) 398.85
Current children cumulated vsize (Kb) 65892

[startup+410.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 16488 0 0 0 40783 98 0 0 25 0 1 0 1843588564 66711552 16098 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 16287 16098 145 145 0 16142 0
[pid=12868] vsize: 65148
Current children cumulated CPU time (s) 408.82
Current children cumulated vsize (Kb) 67272

[startup+420.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 16788 0 0 0 41777 100 0 0 25 0 1 0 1843588564 67932160 16398 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 16585 16398 145 145 0 16440 0
[pid=12868] vsize: 66340
Current children cumulated CPU time (s) 418.78
Current children cumulated vsize (Kb) 68464

[startup+430.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 17116 0 0 0 42773 101 0 0 25 0 1 0 1843588564 69267456 16726 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 16911 16726 145 145 0 16766 0
[pid=12868] vsize: 67644
Current children cumulated CPU time (s) 428.75
Current children cumulated vsize (Kb) 69768

[startup+440.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 17433 0 0 0 43767 104 0 0 25 0 1 0 1843588564 70553600 17043 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 17225 17043 145 145 0 17080 0
[pid=12868] vsize: 68900
Current children cumulated CPU time (s) 438.72
Current children cumulated vsize (Kb) 71024

[startup+450.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 17810 0 0 0 44760 107 0 0 25 0 1 0 1843588564 72089600 17420 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 17600 17420 145 145 0 17455 0
[pid=12868] vsize: 70400
Current children cumulated CPU time (s) 448.68
Current children cumulated vsize (Kb) 72524

[startup+460.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 18179 0 0 0 45752 110 0 0 25 0 1 0 1843588564 73592832 17789 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 17967 17789 145 145 0 17822 0
[pid=12868] vsize: 71868
Current children cumulated CPU time (s) 458.63
Current children cumulated vsize (Kb) 73992

[startup+470.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 18444 0 0 0 46748 112 0 0 25 0 1 0 1843588564 74674176 18054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 18231 18054 145 145 0 18086 0
[pid=12868] vsize: 72924
Current children cumulated CPU time (s) 468.61
Current children cumulated vsize (Kb) 75048

[startup+480.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 18799 0 0 0 47740 116 0 0 25 0 1 0 1843588564 76124160 18409 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12868/statm): 18585 18409 145 145 0 18440 0
[pid=12868] vsize: 74340
Current children cumulated CPU time (s) 478.57
Current children cumulated vsize (Kb) 76464

[startup+490.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 19136 0 0 0 48734 120 0 0 25 0 1 0 1843588564 77496320 18746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 18920 18746 145 145 0 18775 0
[pid=12868] vsize: 75680
Current children cumulated CPU time (s) 488.55
Current children cumulated vsize (Kb) 77804

[startup+500.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 19406 0 0 0 49729 121 0 0 25 0 1 0 1843588564 78594048 19016 4294967295 134512640 135094434 3221224448 3221223120 134555821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 19188 19016 145 145 0 19043 0
[pid=12868] vsize: 76752
Current children cumulated CPU time (s) 498.51
Current children cumulated vsize (Kb) 78876

[startup+510.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 19736 0 0 0 50724 124 0 0 25 0 1 0 1843588564 79937536 19346 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 19516 19346 145 145 0 19371 0
[pid=12868] vsize: 78064
Current children cumulated CPU time (s) 508.49
Current children cumulated vsize (Kb) 80188

[startup+520.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 20033 0 0 0 51719 127 0 0 25 0 1 0 1843588564 81145856 19643 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 19811 19643 145 145 0 19666 0
[pid=12868] vsize: 79244
Current children cumulated CPU time (s) 518.47
Current children cumulated vsize (Kb) 81368

[startup+530.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 20327 0 0 0 52713 129 0 0 25 0 1 0 1843588564 82345984 19937 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 20104 19937 145 145 0 19959 0
[pid=12868] vsize: 80416
Current children cumulated CPU time (s) 528.43
Current children cumulated vsize (Kb) 82540

[startup+540.058 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 20682 0 0 0 53706 132 0 0 25 0 1 0 1843588564 83791872 20292 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12868/statm): 20457 20292 145 145 0 20312 0
[pid=12868] vsize: 81828
Current children cumulated CPU time (s) 538.39
Current children cumulated vsize (Kb) 83952

[startup+550.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 20974 0 0 0 54701 134 0 0 25 0 1 0 1843588564 84979712 20584 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 20747 20584 145 145 0 20602 0
[pid=12868] vsize: 82988
Current children cumulated CPU time (s) 548.36
Current children cumulated vsize (Kb) 85112

[startup+560.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 21241 0 0 0 55697 136 0 0 25 0 1 0 1843588564 86065152 20851 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 21012 20851 145 145 0 20867 0
[pid=12868] vsize: 84048
Current children cumulated CPU time (s) 558.34
Current children cumulated vsize (Kb) 86172

[startup+570.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 21494 0 0 0 56692 139 0 0 25 0 1 0 1843588564 87621632 21104 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 21392 21104 145 145 0 21247 0
[pid=12868] vsize: 85568
Current children cumulated CPU time (s) 568.32
Current children cumulated vsize (Kb) 87692

[startup+580.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 21759 0 0 0 57688 140 0 0 25 0 1 0 1843588564 88698880 21369 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 21655 21369 145 145 0 21510 0
[pid=12868] vsize: 86620
Current children cumulated CPU time (s) 578.29
Current children cumulated vsize (Kb) 88744

[startup+590.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22037 0 0 0 58683 142 0 0 25 0 1 0 1843588564 89829376 21647 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 21931 21647 145 145 0 21786 0
[pid=12868] vsize: 87724
Current children cumulated CPU time (s) 588.26
Current children cumulated vsize (Kb) 89848

[startup+600.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22319 0 0 0 59679 143 0 0 25 0 1 0 1843588564 90980352 21929 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 22212 21929 145 145 0 22067 0
[pid=12868] vsize: 88848
Current children cumulated CPU time (s) 598.23
Current children cumulated vsize (Kb) 90972

[startup+610.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22608 0 0 0 60674 146 0 0 25 0 1 0 1843588564 92155904 22218 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 22499 22218 145 145 0 22354 0
[pid=12868] vsize: 89996
Current children cumulated CPU time (s) 608.21
Current children cumulated vsize (Kb) 92120

[startup+620.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22885 0 0 0 61670 148 0 0 25 0 1 0 1843588564 93286400 22495 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 22775 22495 145 145 0 22630 0
[pid=12868] vsize: 91100
Current children cumulated CPU time (s) 618.19
Current children cumulated vsize (Kb) 93224

[startup+630.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 23231 0 0 0 62663 151 0 0 25 0 1 0 1843588564 94699520 22841 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 23120 22841 145 145 0 22975 0
[pid=12868] vsize: 92480
Current children cumulated CPU time (s) 628.15
Current children cumulated vsize (Kb) 94604

[startup+640.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 23640 0 0 0 63656 154 0 0 25 0 1 0 1843588564 96370688 23250 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 23528 23250 145 145 0 23383 0
[pid=12868] vsize: 94112
Current children cumulated CPU time (s) 638.11
Current children cumulated vsize (Kb) 96236

[startup+650.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 23927 0 0 0 64651 156 0 0 25 0 1 0 1843588564 97538048 23537 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 23813 23537 145 145 0 23668 0
[pid=12868] vsize: 95252
Current children cumulated CPU time (s) 648.08
Current children cumulated vsize (Kb) 97376

[startup+660.069 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 24199 0 0 0 65646 158 0 0 25 0 1 0 1843588564 98648064 23809 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 24084 23809 145 145 0 23939 0
[pid=12868] vsize: 96336
Current children cumulated CPU time (s) 658.05
Current children cumulated vsize (Kb) 98460

[startup+670.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 24504 0 0 0 66640 161 0 0 25 0 1 0 1843588564 99889152 24114 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 24387 24114 145 145 0 24242 0
[pid=12868] vsize: 97548
Current children cumulated CPU time (s) 668.02
Current children cumulated vsize (Kb) 99672

[startup+680.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 24811 0 0 0 67634 163 0 0 25 0 1 0 1843588564 101142528 24421 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 24693 24421 145 145 0 24548 0
[pid=12868] vsize: 98772
Current children cumulated CPU time (s) 677.98
Current children cumulated vsize (Kb) 100896

[startup+690.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 25158 0 0 0 68627 166 0 0 25 0 1 0 1843588564 102555648 24768 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 25038 24768 145 145 0 24893 0
[pid=12868] vsize: 100152
Current children cumulated CPU time (s) 687.94
Current children cumulated vsize (Kb) 102276

[startup+700.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 25485 0 0 0 69622 167 0 0 25 0 1 0 1843588564 103890944 25095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 25364 25095 145 145 0 25219 0
[pid=12868] vsize: 101456
Current children cumulated CPU time (s) 697.9
Current children cumulated vsize (Kb) 103580

[startup+710.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 25801 0 0 0 70618 168 0 0 25 0 1 0 1843588564 105181184 25411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 25679 25411 145 145 0 25534 0
[pid=12868] vsize: 102716
Current children cumulated CPU time (s) 707.87
Current children cumulated vsize (Kb) 104840

[startup+720.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 26074 0 0 0 71613 170 0 0 25 0 1 0 1843588564 106295296 25684 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 25951 25684 145 145 0 25806 0
[pid=12868] vsize: 103804
Current children cumulated CPU time (s) 717.84
Current children cumulated vsize (Kb) 105928

[startup+730.076 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 26371 0 0 0 72607 172 0 0 25 0 1 0 1843588564 107507712 25981 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12868/statm): 26247 25981 145 145 0 26102 0
[pid=12868] vsize: 104988
Current children cumulated CPU time (s) 727.8
Current children cumulated vsize (Kb) 107112

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 26645 0 0 0 73603 174 0 0 25 0 1 0 1843588564 108621824 26255 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 26519 26255 145 145 0 26374 0
[pid=12868] vsize: 106076
Current children cumulated CPU time (s) 737.78
Current children cumulated vsize (Kb) 108200

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 26911 0 0 0 74598 176 0 0 25 0 1 0 1843588564 109703168 26521 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 26783 26521 145 145 0 26638 0
[pid=12868] vsize: 107132
Current children cumulated CPU time (s) 747.75
Current children cumulated vsize (Kb) 109256

[startup+760.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27170 0 0 0 75595 177 0 0 25 0 1 0 1843588564 110759936 26780 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 27041 26780 145 145 0 26896 0
[pid=12868] vsize: 108164
Current children cumulated CPU time (s) 757.73
Current children cumulated vsize (Kb) 110288

[startup+770.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27423 0 0 0 76591 179 0 0 25 0 1 0 1843588564 111788032 27033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 27292 27033 145 145 0 27147 0
[pid=12868] vsize: 109168
Current children cumulated CPU time (s) 767.71
Current children cumulated vsize (Kb) 111292

[startup+780.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27665 0 0 0 77586 181 0 0 25 0 1 0 1843588564 112775168 27275 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 27533 27275 145 145 0 27388 0
[pid=12868] vsize: 110132
Current children cumulated CPU time (s) 777.68
Current children cumulated vsize (Kb) 112256

[startup+790.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27921 0 0 0 78581 184 0 0 25 0 1 0 1843588564 113819648 27531 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 27788 27531 145 145 0 27643 0
[pid=12868] vsize: 111152
Current children cumulated CPU time (s) 787.66
Current children cumulated vsize (Kb) 113276

[startup+800.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 28255 0 0 0 79576 186 0 0 25 0 1 0 1843588564 115187712 27865 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12868/statm): 28122 27865 145 145 0 27977 0
[pid=12868] vsize: 112488
Current children cumulated CPU time (s) 797.63
Current children cumulated vsize (Kb) 114612

[startup+810.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 28530 0 0 0 80571 189 0 0 25 0 1 0 1843588564 116305920 28140 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 28395 28140 145 145 0 28250 0
[pid=12868] vsize: 113580
Current children cumulated CPU time (s) 807.61
Current children cumulated vsize (Kb) 115704

[startup+820.084 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 28805 0 0 0 81567 190 0 0 25 0 1 0 1843588564 117420032 28415 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 28667 28415 145 145 0 28522 0
[pid=12868] vsize: 114668
Current children cumulated CPU time (s) 817.58
Current children cumulated vsize (Kb) 116792

[startup+830.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29114 0 0 0 82561 193 0 0 25 0 1 0 1843588564 118685696 28724 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 28976 28724 145 145 0 28831 0
[pid=12868] vsize: 115904
Current children cumulated CPU time (s) 827.55
Current children cumulated vsize (Kb) 118028

[startup+840.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29419 0 0 0 83556 195 0 0 25 0 1 0 1843588564 119926784 29029 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 29279 29029 145 145 0 29134 0
[pid=12868] vsize: 117116
Current children cumulated CPU time (s) 837.52
Current children cumulated vsize (Kb) 119240

[startup+850.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29666 0 0 0 84552 197 0 0 25 0 1 0 1843588564 120930304 29276 4294967295 134512640 135094434 3221224448 3221223040 134556951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 29524 29276 145 145 0 29379 0
[pid=12868] vsize: 118096
Current children cumulated CPU time (s) 847.5
Current children cumulated vsize (Kb) 120220

[startup+860.087 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29958 0 0 0 85547 198 0 0 25 0 1 0 1843588564 122122240 29568 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 29815 29568 145 145 0 29670 0
[pid=12868] vsize: 119260
Current children cumulated CPU time (s) 857.46
Current children cumulated vsize (Kb) 121384

[startup+870.088 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30282 0 0 0 86541 201 0 0 25 0 1 0 1843588564 123441152 29892 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30137 29892 145 145 0 29992 0
[pid=12868] vsize: 120548
Current children cumulated CPU time (s) 867.43
Current children cumulated vsize (Kb) 122672

[startup+880.089 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 87536 202 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223236 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 877.39
Current children cumulated vsize (Kb) 123932

[startup+890.089 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 88536 202 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 887.39
Current children cumulated vsize (Kb) 123932

[startup+900.091 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 89535 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134551873 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 897.39
Current children cumulated vsize (Kb) 123932

[startup+910.093 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 90536 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 907.4
Current children cumulated vsize (Kb) 123932

[startup+920.094 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 91536 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 917.4
Current children cumulated vsize (Kb) 123932

[startup+930.095 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 92536 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 927.4
Current children cumulated vsize (Kb) 123932

[startup+940.095 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 93537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 937.41
Current children cumulated vsize (Kb) 123932

[startup+950.096 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 94537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 947.41
Current children cumulated vsize (Kb) 123932

[startup+960.097 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 95537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 957.41
Current children cumulated vsize (Kb) 123932

[startup+970.098 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 96537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 967.41
Current children cumulated vsize (Kb) 123932

[startup+980.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 97537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 977.41
Current children cumulated vsize (Kb) 123932

[startup+990.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 98538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 987.42
Current children cumulated vsize (Kb) 123932

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 99538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 997.42
Current children cumulated vsize (Kb) 123932

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 100538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1007.42
Current children cumulated vsize (Kb) 123932

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 101538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1017.42
Current children cumulated vsize (Kb) 123932

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 102539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1027.43
Current children cumulated vsize (Kb) 123932

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 103539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1037.43
Current children cumulated vsize (Kb) 123932

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 104539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223008 134562165 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1047.43
Current children cumulated vsize (Kb) 123932

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 105539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1057.43
Current children cumulated vsize (Kb) 123932

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 106539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1067.43
Current children cumulated vsize (Kb) 123932

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 107540 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1077.44
Current children cumulated vsize (Kb) 123932

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 108540 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1087.44
Current children cumulated vsize (Kb) 123932

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 109540 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1097.44
Current children cumulated vsize (Kb) 123932

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 110540 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1107.45
Current children cumulated vsize (Kb) 123932

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 111540 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1117.45
Current children cumulated vsize (Kb) 123932

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 112541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1127.46
Current children cumulated vsize (Kb) 123932

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 113541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1137.46
Current children cumulated vsize (Kb) 123932

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 114541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223120 134556502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1147.46
Current children cumulated vsize (Kb) 123932

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 115541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134555980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1157.46
Current children cumulated vsize (Kb) 123932

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 116541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1167.46
Current children cumulated vsize (Kb) 123932

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 117542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1177.47
Current children cumulated vsize (Kb) 123932

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 118542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223088 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1187.47
Current children cumulated vsize (Kb) 123932

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 119542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1197.47
Current children cumulated vsize (Kb) 123932

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 120542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1207.47
Current children cumulated vsize (Kb) 123932



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12868
Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12864/statm): 531 226 485 147 0 384 0
[pid=12864] vsize: 2124
Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 120542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0
[pid=12868] vsize: 121808
Current children cumulated CPU time (s) 1207.47
Current children cumulated vsize (Kb) 123932

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

Child status: 10
Real time (s): 1210.19
CPU time (s): 1207.53
CPU user time (s): 1205.43
CPU system time (s): 2.09968
CPU usage (%): 99.7807
Max. virtual memory (cumulated for all children) (Kb): 123932

Verifier Data

ERROR: no interpretation found !