Some explanations

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

General information on the benchmark

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-4.opb
MD5SUMb85a90571dde4fe12541342d5605d680
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -39
Optimality of the best value was proved NO
Number of terms in the objective function 1150
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1150
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1150
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.05
Number of variables1150
Total number of constraints80258
Number of constraints which are clauses80258
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 2304

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        896456 kB
Buffers:         38660 kB
Cached:          59192 kB
SwapCached:        544 kB
Active:          68676 kB
Inactive:        41376 kB
HighTotal:      131008 kB
HighFree:        71820 kB
LowTotal:       903652 kB
LowFree:        824636 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22508 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:10:53 (client local time) WITH STATUS 10 IN 1207.99 SECONDS
stats: 2707 7 1207.99 10

Solver Data

c Parsing PB file...
c Converting 80258 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 |   80258   160516 |   26752       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148144   319772 |   49381       0        0     nan |  0.000 % |
c |       100 |  147820   319103 |   54319      84      567     6.8 |  0.388 % |
c |       250 |  147145   317664 |   59751     188     1432     7.6 |  1.214 % |
c |       476 |  146024   315267 |   65726     361     3068     8.5 |  2.595 % |
c |       813 |  143729   310234 |   72298     619     5841     9.4 |  5.557 % |
c |      1319 |  140833   303816 |   79528     968     9121     9.4 |  9.437 % |
c |      2079 |  136692   294527 |   87481    1586    15869    10.0 | 15.004 % |
c |      3218 |  131314   282313 |   96229    2417    27902    11.5 | 22.323 % |
c |      4926 |  122752   262701 |  105852    3528    39936    11.3 | 34.222 % |
c |      7488 |  112044   237857 |  116437    5289    62605    11.8 | 49.090 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7928 |  111198   235994 |   37066    5633    66805    11.9 | 49.090 % |
c |      8028 |  110897   235287 |   40772    5710    67536    11.8 | 50.901 % |
c |      8178 |  110452   234225 |   44849    5792    68387    11.8 | 51.548 % |
c |      8403 |  109585   232234 |   49334    5952    71118    11.9 | 52.759 % |
c |      8741 |  108728   230226 |   54268    6208    74433    12.0 | 53.995 % |
c |      9247 |  107763   227961 |   59695    6556    79030    12.1 | 55.393 % |
c |     10006 |  106198   224277 |   65664    7058    87476    12.4 | 57.665 % |
c |     11146 |  103552   218006 |   72231    7914   103965    13.1 | 61.514 % |
c |     12854 |  100400   210497 |   79454    9088   124554    13.7 | 66.138 % |
c |     15416 |   97019   202392 |   87399   10804   161729    15.0 | 71.090 % |
c |     19260 |   94852   197144 |   96139   14054   253306    18.0 | 74.363 % |
c |     25026 |   93592   194098 |  105753   19178   576284    30.0 | 76.268 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29121 |   92780   192183 |   30926   22895   940622    41.1 | 76.268 % |
c |     29221 |   92677   191930 |   34018   22961   941837    41.0 | 77.647 % |
c |     29371 |   92612   191776 |   37420   23105   945249    40.9 | 77.742 % |
c |     29597 |   92612   191776 |   41162   23331   954744    40.9 | 77.742 % |
c |     29934 |   92495   191494 |   45278   23662   962311    40.7 | 77.917 % |
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 |     30329 |   92131   190575 |   30710   23891   984433    41.2 | 77.917 % |
c |     30429 |   92064   190426 |   33781   23974   986115    41.1 | 78.509 % |
c |     30579 |   91949   190146 |   37159   24115   994438    41.2 | 78.683 % |
c |     30804 |   91850   189911 |   40875   24280  1003798    41.3 | 78.828 % |
c |     31141 |   91766   189701 |   44962   24546  1013462    41.3 | 78.962 % |
c |     31647 |   91650   189414 |   49458   25021  1032977    41.3 | 79.143 % |
c |     32406 |   91601   189300 |   54404   25733  1089814    42.4 | 79.212 % |
c |     33545 |   91498   189059 |   59845   26813  1189985    44.4 | 79.358 % |
c |     35253 |   91064   187999 |   65829   28271  1265964    44.8 | 80.005 % |
c |     37817 |   90592   186879 |   72412   30523  1417125    46.4 | 80.691 % |
c |     41661 |   90247   186028 |   79653   34043  1688146    49.6 | 81.219 % |
c |     47427 |   89873   185101 |   87619   39490  2309222    58.5 | 81.806 % |
c ==============================================================================
c Found solution: -43
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55522 |   89822   185003 |   29940   47545  3314007    69.7 | 81.806 % |
c |     55622 |   89822   185003 |   32934   47645  3321718    69.7 | 81.930 % |
c |     55772 |   89822   185003 |   36227   47795  3326427    69.6 | 81.931 % |
c |     55998 |   89822   185003 |   39850   48021  3341366    69.6 | 81.930 % |
c |     56336 |   89822   185003 |   43835   48359  3370021    69.7 | 81.931 % |
c |     56842 |   89822   185003 |   48218   48865  3409651    69.8 | 81.930 % |
c |     57601 |   89177   183450 |   53040   48863  3434237    70.3 | 82.894 % |
c |     58740 |   89177   183450 |   58344   50002  3579676    71.6 | 82.894 % |
c |     60448 |   89117   183296 |   64179   51669  3732132    72.2 | 82.996 % |
c |     63011 |   89039   183106 |   70596   54124  3965144    73.3 | 83.114 % |
c |     66855 |   89039   183106 |   77656   57968  4599226    79.3 | 83.114 % |
c |     72622 |   88752   182402 |   85422   63069  5112366    81.1 | 83.557 % |
c |     81271 |   88748   182392 |   93964   71717  6426102    89.6 | 83.564 % |
c |     94245 |   88748   182392 |  103361   84691  8009047    94.6 | 83.564 % |
c |    113707 |   88741   182375 |  113697  104135 11319413   108.7 | 83.574 % |
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 |    140871 |   88488   181720 |   29496  130980 15028721   114.7 | 83.574 % |
c |    140971 |   88488   181720 |   32445   23657  1604034    67.8 | 83.975 % |
c |    141121 |   88488   181720 |   35690   23807  1613264    67.8 | 83.975 % |
c |    141346 |   88488   181720 |   39259   24032  1631251    67.9 | 83.975 % |
c |    141683 |   88328   181322 |   43185   24359  1642586    67.4 | 84.221 % |
c |    142189 |   88328   181322 |   47503   24865  1700627    68.4 | 84.221 % |
c |    142948 |   88328   181322 |   52253   25624  1787151    69.7 | 84.221 % |
c |    144087 |   88328   181322 |   57479   26763  1947089    72.8 | 84.221 % |
c |    145797 |   88226   181078 |   63227   28458  2159705    75.9 | 84.369 % |
c |    148359 |   88221   181067 |   69550   31016  2379812    76.7 | 84.375 % |
c |    152203 |   88221   181067 |   76505   34860  2924276    83.9 | 84.375 % |
c |    157969 |   88221   181067 |   84155   40626  3769186    92.8 | 84.375 % |
c |    166618 |   88180   180970 |   92571   49077  4992109   101.7 | 84.436 % |
c |    179592 |   88139   180873 |  101828   61925  6663510   107.6 | 84.496 % |
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 |    193053 |   88160   180935 |   29386   75386  9039640   119.9 | 84.496 % |
c |    193153 |   88154   180921 |   32324   20076  2226072   110.9 | 84.484 % |
c |    193303 |   88149   180908 |   35557   20222  2233119   110.4 | 84.492 % |
c |    193528 |   88149   180908 |   39112   20447  2240695   109.6 | 84.492 % |
c |    193865 |   87960   180457 |   43024   20704  2251356   108.7 | 84.765 % |
c |    194373 |   87960   180457 |   47326   21212  2285864   107.8 | 84.765 % |
c |    195133 |   87928   180387 |   52059   21969  2317828   105.5 | 84.806 % |
c |    196272 |   87928   180387 |   57265   23108  2390481   103.4 | 84.806 % |
c |    197981 |   87877   180262 |   62991   24808  2557155   103.1 | 84.886 % |
c |    200543 |   87877   180262 |   69290   27370  2839758   103.8 | 84.886 % |
c |    204387 |   87859   180218 |   76219   31206  3310018   106.1 | 84.914 % |
c |    210154 |   87728   179913 |   83841   36956  3914827   105.9 | 85.101 % |
c |    218803 |   87618   179642 |   92225   45444  4968749   109.3 | 85.273 % |
c |    231778 |   87612   179628 |  101448   58416  6873546   117.7 | 85.281 % |
c |    251240 |   87602   179602 |  111593   77876  9366492   120.3 | 85.299 % |
c |    280433 |   87500   179360 |  122752  106975 13247285   123.8 | 85.449 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 C4

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/25273/stat): 25273 (minisat+_script) R 25272 25273 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785310562 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/25273/statm): 174 3 169 147 0 27 0
[pid=25273] 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=25274
New process pid=25275
New process pid=25276
One traced child (pid=25275) 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=25276) exited with status: 0
One traced child (pid=25274) exited with status: 0
New process pid=25277
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-frb50-23-4.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 960 20 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0
[pid=25277] vsize: 21184
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 23308

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 1959 20 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0
[pid=25277] vsize: 21184
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 23308

[startup+30.0068 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 2959 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0
[pid=25277] vsize: 21184
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 23308

[startup+40.0076 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 3958 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0
[pid=25277] vsize: 21184
Current children cumulated CPU time (s) 39.79
Current children cumulated vsize (Kb) 23308

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 4959 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0
[pid=25277] vsize: 21184
Current children cumulated CPU time (s) 49.8
Current children cumulated vsize (Kb) 23308

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 5959 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0
[pid=25277] vsize: 21184
Current children cumulated CPU time (s) 59.8
Current children cumulated vsize (Kb) 23308

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5342 0 0 0 6958 22 0 0 25 0 1 0 1785310567 23666688 5329 4294967295 134512640 135094434 3221224448 3221223200 134559238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5778 5329 145 145 0 5633 0
[pid=25277] vsize: 23112
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 25236

[startup+80.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5345 0 0 0 7958 22 0 0 25 0 1 0 1785310567 23666688 5332 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5778 5332 145 145 0 5633 0
[pid=25277] vsize: 23112
Current children cumulated CPU time (s) 79.8
Current children cumulated vsize (Kb) 25236

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5345 0 0 0 8958 22 0 0 25 0 1 0 1785310567 23666688 5332 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 5778 5332 145 145 0 5633 0
[pid=25277] vsize: 23112
Current children cumulated CPU time (s) 89.8
Current children cumulated vsize (Kb) 25236

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5645 0 0 0 9953 24 0 0 25 0 1 0 1785310567 24952832 5632 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 6092 5632 145 145 0 5947 0
[pid=25277] vsize: 24368
Current children cumulated CPU time (s) 99.77
Current children cumulated vsize (Kb) 26492

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 6204 0 0 0 10943 29 0 0 25 0 1 0 1785310567 27029504 6143 4294967295 134512640 135094434 3221224448 3221223236 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 6599 6143 145 145 0 6454 0
[pid=25277] vsize: 26396
Current children cumulated CPU time (s) 109.72
Current children cumulated vsize (Kb) 28520

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 6542 0 0 0 11936 32 0 0 25 0 1 0 1785310567 28213248 6436 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 6888 6436 145 145 0 6743 0
[pid=25277] vsize: 27552
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 29676

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 6857 0 0 0 12930 34 0 0 25 0 1 0 1785310567 29487104 6751 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 7199 6751 145 145 0 7054 0
[pid=25277] vsize: 28796
Current children cumulated CPU time (s) 129.64
Current children cumulated vsize (Kb) 30920

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 7271 0 0 0 13924 37 0 0 25 0 1 0 1785310567 31297536 7165 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 7641 7165 145 145 0 7496 0
[pid=25277] vsize: 30564
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 32688

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 7770 0 0 0 14916 40 0 0 25 0 1 0 1785310567 33320960 7664 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 8135 7664 145 145 0 7990 0
[pid=25277] vsize: 32540
Current children cumulated CPU time (s) 149.56
Current children cumulated vsize (Kb) 34664

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 8259 0 0 0 15907 42 0 0 25 0 1 0 1785310567 35307520 8153 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 8620 8153 145 145 0 8475 0
[pid=25277] vsize: 34480
Current children cumulated CPU time (s) 159.49
Current children cumulated vsize (Kb) 36604

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 8790 0 0 0 16897 46 0 0 25 0 1 0 1785310567 37466112 8684 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 9147 8684 145 145 0 9002 0
[pid=25277] vsize: 36588
Current children cumulated CPU time (s) 169.43
Current children cumulated vsize (Kb) 38712

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 9058 0 0 0 17893 48 0 0 25 0 1 0 1785310567 38367232 8905 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 9367 8905 145 145 0 9222 0
[pid=25277] vsize: 37468
Current children cumulated CPU time (s) 179.41
Current children cumulated vsize (Kb) 39592

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 9456 0 0 0 18886 51 0 0 25 0 1 0 1785310567 39981056 9303 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 9761 9303 145 145 0 9616 0
[pid=25277] vsize: 39044
Current children cumulated CPU time (s) 189.37
Current children cumulated vsize (Kb) 41168

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 10007 0 0 0 19875 56 0 0 25 0 1 0 1785310567 42221568 9854 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 10308 9854 145 145 0 10163 0
[pid=25277] vsize: 41232
Current children cumulated CPU time (s) 199.31
Current children cumulated vsize (Kb) 43356

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 10379 0 0 0 20869 59 0 0 25 0 1 0 1785310567 43737088 10226 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 10678 10226 145 145 0 10533 0
[pid=25277] vsize: 42712
Current children cumulated CPU time (s) 209.28
Current children cumulated vsize (Kb) 44836

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 10741 0 0 0 21862 62 0 0 25 0 1 0 1785310567 45207552 10588 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 11037 10588 145 145 0 10892 0
[pid=25277] vsize: 44148
Current children cumulated CPU time (s) 219.24
Current children cumulated vsize (Kb) 46272

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 11221 0 0 0 22853 66 0 0 25 0 1 0 1785310567 47161344 11068 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 11514 11068 145 145 0 11369 0
[pid=25277] vsize: 46056
Current children cumulated CPU time (s) 229.19
Current children cumulated vsize (Kb) 48180

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 11694 0 0 0 23845 70 0 0 25 0 1 0 1785310567 49348608 11541 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 12048 11541 145 145 0 11903 0
[pid=25277] vsize: 48192
Current children cumulated CPU time (s) 239.15
Current children cumulated vsize (Kb) 50316

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 12129 0 0 0 24837 73 0 0 25 0 1 0 1785310567 51118080 11976 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 12480 11976 145 145 0 12335 0
[pid=25277] vsize: 49920
Current children cumulated CPU time (s) 249.1
Current children cumulated vsize (Kb) 52044

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 12586 0 0 0 25828 77 0 0 25 0 1 0 1785310567 52977664 12433 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 12934 12433 145 145 0 12789 0
[pid=25277] vsize: 51736
Current children cumulated CPU time (s) 259.05
Current children cumulated vsize (Kb) 53860

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 12936 0 0 0 26823 79 0 0 25 0 1 0 1785310567 54398976 12783 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 13281 12783 145 145 0 13136 0
[pid=25277] vsize: 53124
Current children cumulated CPU time (s) 269.02
Current children cumulated vsize (Kb) 55248

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 13279 0 0 0 27817 81 0 0 25 0 1 0 1785310567 55795712 13126 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 13622 13126 145 145 0 13477 0
[pid=25277] vsize: 54488
Current children cumulated CPU time (s) 278.98
Current children cumulated vsize (Kb) 56612

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 13671 0 0 0 28810 84 0 0 25 0 1 0 1785310567 57389056 13518 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 14011 13518 145 145 0 13866 0
[pid=25277] vsize: 56044
Current children cumulated CPU time (s) 288.94
Current children cumulated vsize (Kb) 58168

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 14024 0 0 0 29803 88 0 0 25 0 1 0 1785310567 58822656 13871 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 14361 13871 145 145 0 14216 0
[pid=25277] vsize: 57444
Current children cumulated CPU time (s) 298.91
Current children cumulated vsize (Kb) 59568

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 14369 0 0 0 30796 90 0 0 25 0 1 0 1785310567 60227584 14216 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 14704 14216 145 145 0 14559 0
[pid=25277] vsize: 58816
Current children cumulated CPU time (s) 308.86
Current children cumulated vsize (Kb) 60940

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 14764 0 0 0 31790 93 0 0 25 0 1 0 1785310567 61833216 14611 4294967295 134512640 135094434 3221224448 3221223120 134556329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 15096 14611 145 145 0 14951 0
[pid=25277] vsize: 60384
Current children cumulated CPU time (s) 318.83
Current children cumulated vsize (Kb) 62508

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 15130 0 0 0 32784 96 0 0 25 0 1 0 1785310567 63324160 14977 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 15460 14977 145 145 0 15315 0
[pid=25277] vsize: 61840
Current children cumulated CPU time (s) 328.8
Current children cumulated vsize (Kb) 63964

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 15492 0 0 0 33777 98 0 0 25 0 1 0 1785310567 64798720 15339 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 15820 15339 145 145 0 15675 0
[pid=25277] vsize: 63280
Current children cumulated CPU time (s) 338.75
Current children cumulated vsize (Kb) 65404

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 15879 0 0 0 34769 101 0 0 25 0 1 0 1785310567 66375680 15726 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 16205 15726 145 145 0 16060 0
[pid=25277] vsize: 64820
Current children cumulated CPU time (s) 348.7
Current children cumulated vsize (Kb) 66944

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 16301 0 0 0 35762 105 0 0 25 0 1 0 1785310567 68096000 16148 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 16625 16148 145 145 0 16480 0
[pid=25277] vsize: 66500
Current children cumulated CPU time (s) 358.67
Current children cumulated vsize (Kb) 68624

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 16669 0 0 0 36754 109 0 0 25 0 1 0 1785310567 69595136 16516 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 16991 16516 145 145 0 16846 0
[pid=25277] vsize: 67964
Current children cumulated CPU time (s) 368.63
Current children cumulated vsize (Kb) 70088

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 17055 0 0 0 37747 112 0 0 25 0 1 0 1785310567 71168000 16902 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 17375 16902 145 145 0 17230 0
[pid=25277] vsize: 69500
Current children cumulated CPU time (s) 378.59
Current children cumulated vsize (Kb) 71624

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 17414 0 0 0 38740 115 0 0 25 0 1 0 1785310567 72634368 17261 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 17733 17261 145 145 0 17588 0
[pid=25277] vsize: 70932
Current children cumulated CPU time (s) 388.55
Current children cumulated vsize (Kb) 73056

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 17695 0 0 0 39734 117 0 0 25 0 1 0 1785310567 73781248 17542 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 18013 17542 145 145 0 17868 0
[pid=25277] vsize: 72052
Current children cumulated CPU time (s) 398.51
Current children cumulated vsize (Kb) 74176

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 18007 0 0 0 40729 119 0 0 25 0 1 0 1785310567 75046912 17854 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 18322 17854 145 145 0 18177 0
[pid=25277] vsize: 73288
Current children cumulated CPU time (s) 408.48
Current children cumulated vsize (Kb) 75412

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 18362 0 0 0 41722 122 0 0 25 0 1 0 1785310567 76492800 18209 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 18675 18209 145 145 0 18530 0
[pid=25277] vsize: 74700
Current children cumulated CPU time (s) 418.44
Current children cumulated vsize (Kb) 76824

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 18717 0 0 0 42716 124 0 0 25 0 1 0 1785310567 77942784 18564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 19029 18564 145 145 0 18884 0
[pid=25277] vsize: 76116
Current children cumulated CPU time (s) 428.4
Current children cumulated vsize (Kb) 78240

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19122 0 0 0 43709 128 0 0 25 0 1 0 1785310567 79593472 18969 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 19432 18969 145 145 0 19287 0
[pid=25277] vsize: 77728
Current children cumulated CPU time (s) 438.37
Current children cumulated vsize (Kb) 79852

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19481 0 0 0 44703 130 0 0 25 0 1 0 1785310567 81055744 19328 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 19789 19328 145 145 0 19644 0
[pid=25277] vsize: 79156
Current children cumulated CPU time (s) 448.33
Current children cumulated vsize (Kb) 81280

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19727 0 0 0 45698 132 0 0 25 0 1 0 1785310567 82055168 19574 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 20033 19574 145 145 0 19888 0
[pid=25277] vsize: 80132
Current children cumulated CPU time (s) 458.3
Current children cumulated vsize (Kb) 82256

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19996 0 0 0 46693 134 0 0 25 0 1 0 1785310567 83148800 19843 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 20300 19843 145 145 0 20155 0
[pid=25277] vsize: 81200
Current children cumulated CPU time (s) 468.27
Current children cumulated vsize (Kb) 83324

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20258 0 0 0 47688 137 0 0 25 0 1 0 1785310567 84217856 20105 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 20561 20105 145 145 0 20416 0
[pid=25277] vsize: 82244
Current children cumulated CPU time (s) 478.25
Current children cumulated vsize (Kb) 84368

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20516 0 0 0 48682 139 0 0 25 0 1 0 1785310567 85266432 20363 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 20817 20363 145 145 0 20672 0
[pid=25277] vsize: 83268
Current children cumulated CPU time (s) 488.21
Current children cumulated vsize (Kb) 85392

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20768 0 0 0 49678 142 0 0 25 0 1 0 1785310567 86290432 20615 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21067 20615 145 145 0 20922 0
[pid=25277] vsize: 84268
Current children cumulated CPU time (s) 498.2
Current children cumulated vsize (Kb) 86392

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20939 0 0 0 50675 143 0 0 25 0 1 0 1785310567 86990848 20786 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21238 20786 145 145 0 21093 0
[pid=25277] vsize: 84952
Current children cumulated CPU time (s) 508.18
Current children cumulated vsize (Kb) 87076

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21195 0 0 0 51670 145 0 0 24 0 1 0 1785310567 88035328 21042 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21493 21042 145 145 0 21348 0
[pid=25277] vsize: 85972
Current children cumulated CPU time (s) 518.15
Current children cumulated vsize (Kb) 88096

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 52665 148 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134784942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 528.13
Current children cumulated vsize (Kb) 88900

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 53665 148 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 538.13
Current children cumulated vsize (Kb) 88900

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 54665 148 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 548.13
Current children cumulated vsize (Kb) 88900

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 55664 149 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 558.13
Current children cumulated vsize (Kb) 88900

[startup+570.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 56664 149 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 568.13
Current children cumulated vsize (Kb) 88900

[startup+580.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 57664 150 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 578.14
Current children cumulated vsize (Kb) 88900

[startup+590.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 58663 150 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 588.13
Current children cumulated vsize (Kb) 88900

[startup+600.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 59663 150 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 598.13
Current children cumulated vsize (Kb) 88900

[startup+610.06 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 60663 151 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 608.14
Current children cumulated vsize (Kb) 88900

[startup+620.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 61662 151 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 618.13
Current children cumulated vsize (Kb) 88900

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 62662 152 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 628.14
Current children cumulated vsize (Kb) 88900

[startup+640.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 63662 152 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 638.14
Current children cumulated vsize (Kb) 88900

[startup+650.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 64661 152 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223120 134555830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 648.13
Current children cumulated vsize (Kb) 88900

[startup+660.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 65661 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 658.14
Current children cumulated vsize (Kb) 88900

[startup+670.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 66660 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 668.13
Current children cumulated vsize (Kb) 88900

[startup+680.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 67661 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 678.14
Current children cumulated vsize (Kb) 88900

[startup+690.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 68661 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 688.14
Current children cumulated vsize (Kb) 88900

[startup+700.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 69661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223120 134555576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 698.15
Current children cumulated vsize (Kb) 88900

[startup+710.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 70661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 708.15
Current children cumulated vsize (Kb) 88900

[startup+720.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 71661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 718.15
Current children cumulated vsize (Kb) 88900

[startup+730.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 72661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 728.15
Current children cumulated vsize (Kb) 88900

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 73661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 738.15
Current children cumulated vsize (Kb) 88900

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 74662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 748.16
Current children cumulated vsize (Kb) 88900

[startup+760.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 75662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 758.16
Current children cumulated vsize (Kb) 88900

[startup+770.079 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 76662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 768.16
Current children cumulated vsize (Kb) 88900

[startup+780.08 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 77662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 778.16
Current children cumulated vsize (Kb) 88900

[startup+790.081 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 78662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 788.16
Current children cumulated vsize (Kb) 88900

[startup+800.081 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 79662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 798.16
Current children cumulated vsize (Kb) 88900

[startup+810.083 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 80663 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 808.17
Current children cumulated vsize (Kb) 88900

[startup+820.084 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 81663 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223088 134538541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 818.17
Current children cumulated vsize (Kb) 88900

[startup+830.086 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 82663 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 828.18
Current children cumulated vsize (Kb) 88900

[startup+840.086 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 83663 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 838.18
Current children cumulated vsize (Kb) 88900

[startup+850.086 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 84663 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 848.18
Current children cumulated vsize (Kb) 88900

[startup+860.087 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 85664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 858.19
Current children cumulated vsize (Kb) 88900

[startup+870.088 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 86664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 868.19
Current children cumulated vsize (Kb) 88900

[startup+880.089 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 87664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 878.19
Current children cumulated vsize (Kb) 88900

[startup+890.09 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 88664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 888.19
Current children cumulated vsize (Kb) 88900

[startup+900.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 89664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 898.19
Current children cumulated vsize (Kb) 88900

[startup+910.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 90665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 908.2
Current children cumulated vsize (Kb) 88900

[startup+920.092 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 91665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 918.2
Current children cumulated vsize (Kb) 88900

[startup+930.093 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 92665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 928.2
Current children cumulated vsize (Kb) 88900

[startup+940.094 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 93665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 938.2
Current children cumulated vsize (Kb) 88900

[startup+950.095 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 94666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 948.21
Current children cumulated vsize (Kb) 88900

[startup+960.095 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 95666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 958.21
Current children cumulated vsize (Kb) 88900

[startup+970.096 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 96666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 968.21
Current children cumulated vsize (Kb) 88900

[startup+980.097 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 97666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 978.21
Current children cumulated vsize (Kb) 88900

[startup+990.098 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 98666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 988.21
Current children cumulated vsize (Kb) 88900

[startup+1000.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 99665 156 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 998.21
Current children cumulated vsize (Kb) 88900

[startup+1010.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 100665 156 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 1008.21
Current children cumulated vsize (Kb) 88900

[startup+1020.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 101665 156 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 1018.21
Current children cumulated vsize (Kb) 88900

[startup+1030.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21445 0 0 0 102665 156 0 0 25 0 1 0 1785310567 88858624 21245 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21245 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 1028.21
Current children cumulated vsize (Kb) 88900

[startup+1040.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21445 0 0 0 103666 156 0 0 25 0 1 0 1785310567 88858624 21245 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21245 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 1038.22
Current children cumulated vsize (Kb) 88900

[startup+1050.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21445 0 0 0 104666 156 0 0 25 0 1 0 1785310567 88858624 21245 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21694 21245 145 145 0 21549 0
[pid=25277] vsize: 86776
Current children cumulated CPU time (s) 1048.22
Current children cumulated vsize (Kb) 88900

[startup+1060.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21456 0 0 0 105666 156 0 0 25 0 1 0 1785310567 88903680 21256 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21705 21256 145 145 0 21560 0
[pid=25277] vsize: 86820
Current children cumulated CPU time (s) 1058.22
Current children cumulated vsize (Kb) 88944

[startup+1070.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21712 0 0 0 106661 159 0 0 25 0 1 0 1785310567 89952256 21512 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 21961 21512 145 145 0 21816 0
[pid=25277] vsize: 87844
Current children cumulated CPU time (s) 1068.2
Current children cumulated vsize (Kb) 89968

[startup+1080.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21940 0 0 0 107658 160 0 0 25 0 1 0 1785310567 90886144 21740 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 22189 21740 145 145 0 22044 0
[pid=25277] vsize: 88756
Current children cumulated CPU time (s) 1078.18
Current children cumulated vsize (Kb) 90880

[startup+1090.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22121 0 0 0 108654 162 0 0 25 0 1 0 1785310567 91627520 21921 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 22370 21921 145 145 0 22225 0
[pid=25277] vsize: 89480
Current children cumulated CPU time (s) 1088.16
Current children cumulated vsize (Kb) 91604

[startup+1100.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22341 0 0 0 109651 164 0 0 25 0 1 0 1785310567 92532736 22141 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 22591 22141 145 145 0 22446 0
[pid=25277] vsize: 90364
Current children cumulated CPU time (s) 1098.15
Current children cumulated vsize (Kb) 92488

[startup+1110.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22580 0 0 0 110646 166 0 0 25 0 1 0 1785310567 93515776 22380 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 22831 22380 145 145 0 22686 0
[pid=25277] vsize: 91324
Current children cumulated CPU time (s) 1108.12
Current children cumulated vsize (Kb) 93448

[startup+1120.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22806 0 0 0 111642 169 0 0 25 0 1 0 1785310567 94961664 22606 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 23184 22606 145 145 0 23039 0
[pid=25277] vsize: 92736
Current children cumulated CPU time (s) 1118.11
Current children cumulated vsize (Kb) 94860

[startup+1130.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23019 0 0 0 112638 171 0 0 25 0 1 0 1785310567 95825920 22819 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 23395 22819 145 145 0 23250 0
[pid=25277] vsize: 93580
Current children cumulated CPU time (s) 1128.09
Current children cumulated vsize (Kb) 95704

[startup+1140.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23226 0 0 0 113634 173 0 0 25 0 1 0 1785310567 96665600 23026 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 23600 23026 145 145 0 23455 0
[pid=25277] vsize: 94400
Current children cumulated CPU time (s) 1138.07
Current children cumulated vsize (Kb) 96524

[startup+1150.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23426 0 0 0 114631 175 0 0 25 0 1 0 1785310567 97476608 23226 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 23798 23226 145 145 0 23653 0
[pid=25277] vsize: 95192
Current children cumulated CPU time (s) 1148.06
Current children cumulated vsize (Kb) 97316

[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23612 0 0 0 115628 176 0 0 25 0 1 0 1785310567 98242560 23412 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 23985 23412 145 145 0 23840 0
[pid=25277] vsize: 95940
Current children cumulated CPU time (s) 1158.04
Current children cumulated vsize (Kb) 98064

[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23796 0 0 0 116624 178 0 0 25 0 1 0 1785310567 98996224 23596 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 24169 23596 145 145 0 24024 0
[pid=25277] vsize: 96676
Current children cumulated CPU time (s) 1168.02
Current children cumulated vsize (Kb) 98800

[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23983 0 0 0 117620 179 0 0 25 0 1 0 1785310567 99753984 23783 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 24354 23783 145 145 0 24209 0
[pid=25277] vsize: 97416
Current children cumulated CPU time (s) 1177.99
Current children cumulated vsize (Kb) 99540

[startup+1190.12 s]
Raw data (loadavg): 1.00 0.99 0.91 3/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24110 0 0 0 118618 180 0 0 25 0 1 0 1785310567 100286464 23910 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 24484 23910 145 145 0 24339 0
[pid=25277] vsize: 97936
Current children cumulated CPU time (s) 1187.98
Current children cumulated vsize (Kb) 100060

[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24329 0 0 0 119615 181 0 0 25 0 1 0 1785310567 101183488 24129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 24703 24129 145 145 0 24558 0
[pid=25277] vsize: 98812
Current children cumulated CPU time (s) 1197.96
Current children cumulated vsize (Kb) 100936

[startup+1210.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24570 0 0 0 120610 183 0 0 25 0 1 0 1785310567 102178816 24370 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 24946 24370 145 145 0 24801 0
[pid=25277] vsize: 99784
Current children cumulated CPU time (s) 1207.93
Current children cumulated vsize (Kb) 101908



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 25277
Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/25273/statm): 531 226 485 147 0 384 0
[pid=25273] vsize: 2124
Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24570 0 0 0 120610 183 0 0 25 0 1 0 1785310567 102178816 24370 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25277/statm): 24946 24370 145 145 0 24801 0
[pid=25277] vsize: 99784
Current children cumulated CPU time (s) 1207.93
Current children cumulated vsize (Kb) 101908

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1207.99
CPU user time (s): 1206.11
CPU system time (s): 1.88371
CPU usage (%): 99.8198
Max. virtual memory (cumulated for all children) (Kb): 101908

Verifier Data

ERROR: no interpretation found !