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-2.opb
MD5SUMfe7ff8b16c276b409b25a87eed31b6f9
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -40
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 constraints80851
Number of constraints which are clauses80851
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 2303

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        905764 kB
Buffers:         37512 kB
Cached:          61116 kB
SwapCached:        788 kB
Active:          67508 kB
Inactive:        33784 kB
HighTotal:      131008 kB
HighFree:        69104 kB
LowTotal:       903652 kB
LowFree:        836660 kB
SwapTotal:     2097892 kB
SwapFree:      2096636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            22020 kB
Committed_AS:    64136 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:09:58 (client local time) WITH STATUS 10 IN 1207.48 SECONDS
stats: 2706 7 1207.48 10

Solver Data

c Parsing PB file...
c Converting 80851 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 |   80851   161702 |   26950       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 |  148737   320958 |   49579       0        0     nan |  0.000 % |
c |       101 |  148366   320193 |   54536      85      765     9.0 |  0.441 % |
c |       252 |  148029   319484 |   59990     220     3072    14.0 |  0.844 % |
c |       477 |  147140   317584 |   65989     414     5422    13.1 |  1.937 % |
c |       814 |  145503   314007 |   72588     695    10180    14.6 |  4.025 % |
c |      1320 |  141871   306005 |   79847    1052    14339    13.6 |  8.753 % |
c |      2079 |  136023   292923 |   87832    1565    21384    13.7 | 16.582 % |
c |      3218 |  130632   280671 |   96615    2487    32283    13.0 | 23.974 % |
c |      4926 |  123081   263362 |  106276    3797    51144    13.5 | 34.454 % |
c |      7488 |  115042   244888 |  116904    5568    76837    13.8 | 45.531 % |
c |     11332 |  106902   225592 |  128595    8647   126243    14.6 | 57.367 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12189 |  105355   221989 |   35118    9206   138743    15.1 | 57.367 % |
c |     12292 |  105334   221942 |   38629    9300   142332    15.3 | 59.672 % |
c |     12442 |  105154   221511 |   42492    9437   144616    15.3 | 59.940 % |
c |     12668 |  104547   220088 |   46742    9550   146897    15.4 | 60.812 % |
c |     13005 |  104266   219414 |   51416    9700   149137    15.4 | 61.231 % |
c |     13511 |  102353   214845 |   56557    9851   154585    15.7 | 64.142 % |
c |     14271 |  101471   212704 |   62213   10471   168910    16.1 | 65.388 % |
c |     15410 |  100525   210483 |   68435   11341   190635    16.8 | 66.819 % |
c |     17118 |   98376   205358 |   75278   12589   222288    17.7 | 69.882 % |
c |     19680 |   97425   203063 |   82806   14811   278397    18.8 | 71.285 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19987 |   96638   201152 |   32212   14981   283316    18.9 | 71.285 % |
c |     20087 |   96638   201152 |   35433   15081   285189    18.9 | 72.422 % |
c |     20237 |   96439   200654 |   38976   15146   288150    19.0 | 72.733 % |
c |     20462 |   96306   200334 |   42874   15335   293321    19.1 | 72.932 % |
c |     20799 |   95886   199340 |   47161   15583   300834    19.3 | 73.553 % |
c |     21306 |   95774   199086 |   51877   16064   315316    19.6 | 73.706 % |
c |     22066 |   95551   198555 |   57065   16757   339492    20.3 | 74.033 % |
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 |     22573 |   95160   197669 |   31720   17015   350326    20.6 | 74.033 % |
c |     22673 |   95160   197669 |   34892   17115   356501    20.8 | 74.686 % |
c |     22823 |   95106   197535 |   38381   17261   360565    20.9 | 74.772 % |
c |     23049 |   95013   197310 |   42219   17466   365076    20.9 | 74.910 % |
c |     23386 |   94966   197201 |   46441   17776   378604    21.3 | 74.975 % |
c |     23892 |   94961   197190 |   51085   18276   390433    21.4 | 74.981 % |
c |     24652 |   94399   195810 |   56193   18675   406360    21.8 | 75.842 % |
c |     25792 |   94283   195526 |   61813   19618   439777    22.4 | 76.021 % |
c |     27501 |   93887   194570 |   67994   21188   551252    26.0 | 76.623 % |
c |     30063 |   93580   193835 |   74794   23586   661515    28.0 | 77.085 % |
c |     33907 |   92526   191288 |   82273   26622   855765    32.1 | 78.683 % |
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 |     34660 |   92501   191256 |   30833   27346   890259    32.6 | 78.683 % |
c |     34760 |   92374   190951 |   33916   27407   892203    32.6 | 78.925 % |
c |     34910 |   92374   190951 |   37307   27557   897352    32.6 | 78.925 % |
c |     35135 |   92325   190828 |   41038   27771   909011    32.7 | 78.996 % |
c |     35472 |   92325   190828 |   45142   28108   929804    33.1 | 78.996 % |
c |     35978 |   92325   190828 |   49656   28614   952436    33.3 | 78.996 % |
c |     36737 |   91933   189887 |   54622   29190   998234    34.2 | 79.580 % |
c |     37877 |   91668   189231 |   60084   30184  1050966    34.8 | 79.977 % |
c |     39585 |   91179   188051 |   66093   31104  1123554    36.1 | 80.703 % |
c |     42147 |   90991   187592 |   72702   33536  1352386    40.3 | 80.990 % |
c |     45991 |   90915   187410 |   79972   37245  1889303    50.7 | 81.102 % |
c |     51757 |   90762   187040 |   87970   42879  2343683    54.7 | 81.333 % |
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 |     52914 |   90753   186986 |   30251   43937  2470581    56.2 | 81.333 % |
c |     53014 |   90753   186986 |   33276   44037  2472887    56.2 | 81.351 % |
c |     53164 |   90753   186986 |   36603   44187  2487369    56.3 | 81.351 % |
c |     53390 |   90753   186986 |   40264   44413  2502524    56.3 | 81.351 % |
c |     53727 |   90753   186986 |   44290   44750  2517712    56.3 | 81.351 % |
c |     54234 |   90712   186891 |   48719   45092  2552226    56.6 | 81.407 % |
c |     54995 |   90712   186891 |   53591   45853  2626768    57.3 | 81.407 % |
c |     56134 |   90698   186857 |   58950   46911  2726470    58.1 | 81.429 % |
c |     57843 |   90611   186643 |   64845   48530  2837380    58.5 | 81.556 % |
c |     60405 |   90521   186429 |   71330   50928  3048163    59.9 | 81.685 % |
c |     64249 |   90508   186398 |   78463   54678  3459802    63.3 | 81.705 % |
c |     70016 |   90366   186066 |   86309   60273  4054487    67.3 | 81.907 % |
c |     78665 |   90114   185438 |   94940   68614  5012115    73.0 | 82.308 % |
c |     91640 |   89808   184690 |  104434   80924  6476449    80.0 | 82.780 % |
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 |    101349 |   89784   184660 |   29928   90515  7625234    84.2 | 82.780 % |
c |    101449 |   89740   184546 |   32920   23637  1615649    68.4 | 82.927 % |
c |    101600 |   89736   184536 |   36212   23784  1622993    68.2 | 82.933 % |
c |    101825 |   89736   184536 |   39834   24009  1640600    68.3 | 82.933 % |
c |    102162 |   89658   184344 |   43817   24307  1661876    68.4 | 83.056 % |
c |    102668 |   89497   183949 |   48199   24754  1694957    68.5 | 83.305 % |
c |    103427 |   89497   183949 |   53019   25513  1767199    69.3 | 83.305 % |
c |    104566 |   89497   183949 |   58321   26652  1884370    70.7 | 83.305 % |
c |    106275 |   89373   183652 |   64153   28323  2061056    72.8 | 83.490 % |
c |    108837 |   89373   183652 |   70568   30885  2343424    75.9 | 83.490 % |
c |    112681 |   89339   183568 |   77625   34664  2898101    83.6 | 83.544 % |
c |    118447 |   88995   182758 |   85388   40297  3742322    92.9 | 84.037 % |
c |    127096 |   88992   182751 |   93926   48945  4973106   101.6 | 84.041 % |
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 |    128864 |   88967   182666 |   29655   50677  5251581   103.6 | 84.041 % |
c |    128964 |   88962   182655 |   32620   50775  5256860   103.5 | 84.087 % |
c |    129114 |   88962   182655 |   35882   50925  5267190   103.4 | 84.087 % |
c |    129339 |   88962   182655 |   39470   51150  5283543   103.3 | 84.087 % |
c |    129677 |   88962   182655 |   43417   51488  5324792   103.4 | 84.087 % |
c |    130183 |   88962   182655 |   47759   51994  5375997   103.4 | 84.087 % |
c |    130942 |   88962   182655 |   52535   52753  5461119   103.5 | 84.087 % |
c |    132081 |   88962   182655 |   57789   53892  5567309   103.3 | 84.087 % |
c |    133790 |   88962   182655 |   63568   55601  5753628   103.5 | 84.087 % |
c |    136353 |   88870   182433 |   69924   58139  6016906   103.5 | 84.220 % |
c |    140197 |   88770   182167 |   76917   61962  6470826   104.4 | 84.399 % |
c |    145963 |   88768   182163 |   84609   67727  7108180   105.0 | 84.401 % |
c |    154612 |   88725   182047 |   93070   76332  8360934   109.5 | 84.474 % |
c |    167586 |   88673   181922 |  102377   89282 10392161   116.4 | 84.554 % |
c |    187048 |   88609   181774 |  112614  108730 13218100   121.6 | 84.644 % |
c |    216240 |   88592   181733 |  123876  137917 17842959   129.4 | 84.670 % |
c |    260030 |   88397   181266 |  136263   36498  4124381   113.0 | 84.963 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 C625 -C624 -C623 -C622 C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/13813/stat): 13813 (minisat+_script) R 13812 13813 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843532065 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/13813/statm): 174 3 169 147 0 27 0
[pid=13813] 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=13814
New process pid=13815
New process pid=13816
execve syscall for /bin/sed executable
One traced child (pid=13815) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=13816) exited with status: 0
One traced child (pid=13814) exited with status: 0
New process pid=13817
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-frb50-23-2.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.95 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5113 0 0 0 959 21 0 0 25 0 1 0 1843532070 21848064 5100 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5334 5100 145 145 0 5189 0
[pid=13817] vsize: 21336
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 23460

[startup+20.0055 s]
Raw data (loadavg): 0.94 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5113 0 0 0 1959 21 0 0 25 0 1 0 1843532070 21848064 5100 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5334 5100 145 145 0 5189 0
[pid=13817] vsize: 21336
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 23460

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5113 0 0 0 2959 21 0 0 25 0 1 0 1843532070 21848064 5100 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5334 5100 145 145 0 5189 0
[pid=13817] vsize: 21336
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 23460

[startup+40.0071 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5113 0 0 0 3959 21 0 0 25 0 1 0 1843532070 21848064 5100 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5334 5100 145 145 0 5189 0
[pid=13817] vsize: 21336
Current children cumulated CPU time (s) 39.8
Current children cumulated vsize (Kb) 23460

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5113 0 0 0 4959 21 0 0 25 0 1 0 1843532070 21848064 5100 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5334 5100 145 145 0 5189 0
[pid=13817] vsize: 21336
Current children cumulated CPU time (s) 49.8
Current children cumulated vsize (Kb) 23460

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5113 0 0 0 5959 21 0 0 25 0 1 0 1843532070 21848064 5100 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5334 5100 145 145 0 5189 0
[pid=13817] vsize: 21336
Current children cumulated CPU time (s) 59.8
Current children cumulated vsize (Kb) 23460

[startup+70.0106 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5124 0 0 0 6959 21 0 0 25 0 1 0 1843532070 21913600 5111 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13817/statm): 5350 5111 145 145 0 5205 0
[pid=13817] vsize: 21400
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 23524

[startup+80.0113 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5420 0 0 0 7957 22 0 0 25 0 1 0 1843532070 23990272 5407 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13817/statm): 5857 5407 145 145 0 5712 0
[pid=13817] vsize: 23428
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 25552

[startup+90.0111 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5424 0 0 0 8956 22 0 0 25 0 1 0 1843532070 23990272 5411 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 5857 5411 145 145 0 5712 0
[pid=13817] vsize: 23428
Current children cumulated CPU time (s) 89.78
Current children cumulated vsize (Kb) 25552

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5667 0 0 0 9953 24 0 0 25 0 1 0 1843532070 24649728 5560 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 6018 5560 145 145 0 5873 0
[pid=13817] vsize: 24072
Current children cumulated CPU time (s) 99.77
Current children cumulated vsize (Kb) 26196

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 5990 0 0 0 10947 27 0 0 21 0 1 0 1843532070 25952256 5883 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 6336 5883 145 145 0 6191 0
[pid=13817] vsize: 25344
Current children cumulated CPU time (s) 109.74
Current children cumulated vsize (Kb) 27468

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 6329 0 0 0 11943 29 0 0 25 0 1 0 1843532070 27136000 6175 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 6625 6175 145 145 0 6480 0
[pid=13817] vsize: 26500
Current children cumulated CPU time (s) 119.72
Current children cumulated vsize (Kb) 28624

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 6625 0 0 0 12937 31 0 0 25 0 1 0 1843532070 28332032 6471 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 6917 6471 145 145 0 6772 0
[pid=13817] vsize: 27668
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 29792

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 7238 0 0 0 13926 35 0 0 25 0 1 0 1843532070 30957568 7084 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 7558 7084 145 145 0 7413 0
[pid=13817] vsize: 30232
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 32356

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 7732 0 0 0 14918 38 0 0 25 0 1 0 1843532070 32960512 7578 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 8047 7578 145 145 0 7902 0
[pid=13817] vsize: 32188
Current children cumulated CPU time (s) 149.56
Current children cumulated vsize (Kb) 34312

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 8189 0 0 0 15911 41 0 0 25 0 1 0 1843532070 34631680 7990 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 8455 7990 145 145 0 8310 0
[pid=13817] vsize: 33820
Current children cumulated CPU time (s) 159.52
Current children cumulated vsize (Kb) 35944

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 8554 0 0 0 16903 45 0 0 25 0 1 0 1843532070 36110336 8355 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13817/statm): 8816 8355 145 145 0 8671 0
[pid=13817] vsize: 35264
Current children cumulated CPU time (s) 169.48
Current children cumulated vsize (Kb) 37388

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 8968 0 0 0 17896 49 0 0 25 0 1 0 1843532070 37785600 8769 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 9225 8769 145 145 0 9080 0
[pid=13817] vsize: 36900
Current children cumulated CPU time (s) 179.45
Current children cumulated vsize (Kb) 39024

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 9370 0 0 0 18888 51 0 0 25 0 1 0 1843532070 39419904 9171 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 9624 9171 145 145 0 9479 0
[pid=13817] vsize: 38496
Current children cumulated CPU time (s) 189.39
Current children cumulated vsize (Kb) 40620

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 9791 0 0 0 19881 55 0 0 25 0 1 0 1843532070 41132032 9592 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 10042 9592 145 145 0 9897 0
[pid=13817] vsize: 40168
Current children cumulated CPU time (s) 199.36
Current children cumulated vsize (Kb) 42292

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 10175 0 0 0 20874 58 0 0 25 0 1 0 1843532070 42692608 9976 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 10423 9976 145 145 0 10278 0
[pid=13817] vsize: 41692
Current children cumulated CPU time (s) 209.32
Current children cumulated vsize (Kb) 43816

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 10571 0 0 0 21864 63 0 0 25 0 1 0 1843532070 44564480 10372 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 10880 10372 145 145 0 10735 0
[pid=13817] vsize: 43520
Current children cumulated CPU time (s) 219.27
Current children cumulated vsize (Kb) 45644

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 10950 0 0 0 22857 66 0 0 25 0 1 0 1843532070 46100480 10751 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 11255 10751 145 145 0 11110 0
[pid=13817] vsize: 45020
Current children cumulated CPU time (s) 229.23
Current children cumulated vsize (Kb) 47144

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 11329 0 0 0 23851 68 0 0 25 0 1 0 1843532070 47644672 11130 4294967295 134512640 135094434 3221224448 3221223108 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 11632 11130 145 145 0 11487 0
[pid=13817] vsize: 46528
Current children cumulated CPU time (s) 239.19
Current children cumulated vsize (Kb) 48652

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 11692 0 0 0 24845 71 0 0 25 0 1 0 1843532070 49119232 11493 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 11992 11493 145 145 0 11847 0
[pid=13817] vsize: 47968
Current children cumulated CPU time (s) 249.16
Current children cumulated vsize (Kb) 50092

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 12045 0 0 0 25838 74 0 0 25 0 1 0 1843532070 50552832 11846 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 12342 11846 145 145 0 12197 0
[pid=13817] vsize: 49368
Current children cumulated CPU time (s) 259.12
Current children cumulated vsize (Kb) 51492

[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 12435 0 0 0 26830 77 0 0 25 0 1 0 1843532070 52137984 12236 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 12729 12236 145 145 0 12584 0
[pid=13817] vsize: 50916
Current children cumulated CPU time (s) 269.07
Current children cumulated vsize (Kb) 53040

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 12650 0 0 0 27827 78 0 0 25 0 1 0 1843532070 53010432 12451 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 12942 12451 145 145 0 12797 0
[pid=13817] vsize: 51768
Current children cumulated CPU time (s) 279.05
Current children cumulated vsize (Kb) 53892

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 12953 0 0 0 28822 80 0 0 25 0 1 0 1843532070 54243328 12754 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13243 12754 145 145 0 13098 0
[pid=13817] vsize: 52972
Current children cumulated CPU time (s) 289.02
Current children cumulated vsize (Kb) 55096

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.97 3/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13357 0 0 0 29814 83 0 0 25 0 1 0 1843532070 55885824 13158 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13644 13158 145 145 0 13499 0
[pid=13817] vsize: 54576
Current children cumulated CPU time (s) 298.97
Current children cumulated vsize (Kb) 56700

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 30808 86 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 308.94
Current children cumulated vsize (Kb) 57960

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 31808 86 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 318.94
Current children cumulated vsize (Kb) 57960

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 32808 86 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 328.94
Current children cumulated vsize (Kb) 57960

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 33808 86 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 338.94
Current children cumulated vsize (Kb) 57960

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 34808 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 348.95
Current children cumulated vsize (Kb) 57960

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 35809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 358.96
Current children cumulated vsize (Kb) 57960

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 36809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 368.96
Current children cumulated vsize (Kb) 57960

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 37809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 378.96
Current children cumulated vsize (Kb) 57960

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 38809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 388.96
Current children cumulated vsize (Kb) 57960

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 39809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 398.96
Current children cumulated vsize (Kb) 57960

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 40809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 408.96
Current children cumulated vsize (Kb) 57960

[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 41809 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 418.96
Current children cumulated vsize (Kb) 57960

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 42810 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223080 134539534 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 428.97
Current children cumulated vsize (Kb) 57960

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 43810 87 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 438.97
Current children cumulated vsize (Kb) 57960

[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 13719 0 0 0 44810 88 0 0 25 0 1 0 1843532070 57176064 13475 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 13959 13475 145 145 0 13814 0
[pid=13817] vsize: 55836
Current children cumulated CPU time (s) 448.98
Current children cumulated vsize (Kb) 57960

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 14123 0 0 0 45804 90 0 0 25 0 1 0 1843532070 58830848 13879 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 14363 13879 145 145 0 14218 0
[pid=13817] vsize: 57452
Current children cumulated CPU time (s) 458.94
Current children cumulated vsize (Kb) 59576

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 14486 0 0 0 46797 92 0 0 25 0 1 0 1843532070 60317696 14242 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 14726 14242 145 145 0 14581 0
[pid=13817] vsize: 58904
Current children cumulated CPU time (s) 468.89
Current children cumulated vsize (Kb) 61028

[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 14817 0 0 0 47791 95 0 0 25 0 1 0 1843532070 61673472 14573 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 15057 14573 145 145 0 14912 0
[pid=13817] vsize: 60228
Current children cumulated CPU time (s) 478.86
Current children cumulated vsize (Kb) 62352

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 15103 0 0 0 48786 97 0 0 25 0 1 0 1843532070 62844928 14859 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 15343 14859 145 145 0 15198 0
[pid=13817] vsize: 61372
Current children cumulated CPU time (s) 488.83
Current children cumulated vsize (Kb) 63496

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 15490 0 0 0 49780 100 0 0 25 0 1 0 1843532070 64430080 15246 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 15730 15246 145 145 0 15585 0
[pid=13817] vsize: 62920
Current children cumulated CPU time (s) 498.8
Current children cumulated vsize (Kb) 65044

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 15875 0 0 0 50772 103 0 0 25 0 1 0 1843532070 66011136 15631 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 16116 15631 145 145 0 15971 0
[pid=13817] vsize: 64464
Current children cumulated CPU time (s) 508.75
Current children cumulated vsize (Kb) 66588

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 16327 0 0 0 51763 106 0 0 25 0 1 0 1843532070 67862528 16083 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 16568 16083 145 145 0 16423 0
[pid=13817] vsize: 66272
Current children cumulated CPU time (s) 518.69
Current children cumulated vsize (Kb) 68396

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 16751 0 0 0 52755 110 0 0 25 0 1 0 1843532070 69599232 16507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 16992 16507 145 145 0 16847 0
[pid=13817] vsize: 67968
Current children cumulated CPU time (s) 528.65
Current children cumulated vsize (Kb) 70092

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 17116 0 0 0 53748 113 0 0 25 0 1 0 1843532070 71090176 16872 4294967295 134512640 135094434 3221224448 3221223040 134557234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 17356 16872 145 145 0 17211 0
[pid=13817] vsize: 69424
Current children cumulated CPU time (s) 538.61
Current children cumulated vsize (Kb) 71548

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 17472 0 0 0 54743 115 0 0 25 0 1 0 1843532070 72536064 17228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 17709 17228 145 145 0 17564 0
[pid=13817] vsize: 70836
Current children cumulated CPU time (s) 548.58
Current children cumulated vsize (Kb) 72960

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 17755 0 0 0 55737 118 0 0 25 0 1 0 1843532070 73691136 17511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 17991 17511 145 145 0 17846 0
[pid=13817] vsize: 71964
Current children cumulated CPU time (s) 558.55
Current children cumulated vsize (Kb) 74088

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 18099 0 0 0 56730 121 0 0 25 0 1 0 1843532070 75096064 17855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 18334 17855 145 145 0 18189 0
[pid=13817] vsize: 73336
Current children cumulated CPU time (s) 568.51
Current children cumulated vsize (Kb) 75460

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 18411 0 0 0 57724 123 0 0 25 0 1 0 1843532070 76361728 18167 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 18643 18167 145 145 0 18498 0
[pid=13817] vsize: 74572
Current children cumulated CPU time (s) 578.47
Current children cumulated vsize (Kb) 76696

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 18752 0 0 0 58718 125 0 0 25 0 1 0 1843532070 77750272 18508 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 18982 18508 145 145 0 18837 0
[pid=13817] vsize: 75928
Current children cumulated CPU time (s) 588.43
Current children cumulated vsize (Kb) 78052

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 19047 0 0 0 59714 127 0 0 25 0 1 0 1843532070 78954496 18803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 19276 18803 145 145 0 19131 0
[pid=13817] vsize: 77104
Current children cumulated CPU time (s) 598.41
Current children cumulated vsize (Kb) 79228

[startup+610.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 19355 0 0 0 60708 130 0 0 25 0 1 0 1843532070 80211968 19111 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 19583 19111 145 145 0 19438 0
[pid=13817] vsize: 78332
Current children cumulated CPU time (s) 608.38
Current children cumulated vsize (Kb) 80456

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 19697 0 0 0 61704 132 0 0 25 0 1 0 1843532070 81604608 19453 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 19923 19453 145 145 0 19778 0
[pid=13817] vsize: 79692
Current children cumulated CPU time (s) 618.36
Current children cumulated vsize (Kb) 81816

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 19935 0 0 0 62698 134 0 0 25 0 1 0 1843532070 82583552 19691 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 20162 19691 145 145 0 20017 0
[pid=13817] vsize: 80648
Current children cumulated CPU time (s) 628.32
Current children cumulated vsize (Kb) 82772

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 20197 0 0 0 63694 136 0 0 25 0 1 0 1843532070 83648512 19953 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 20422 19953 145 145 0 20277 0
[pid=13817] vsize: 81688
Current children cumulated CPU time (s) 638.3
Current children cumulated vsize (Kb) 83812

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 20426 0 0 0 64690 138 0 0 25 0 1 0 1843532070 84582400 20182 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 20650 20182 145 145 0 20505 0
[pid=13817] vsize: 82600
Current children cumulated CPU time (s) 648.28
Current children cumulated vsize (Kb) 84724

[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 20682 0 0 0 65684 140 0 0 25 0 1 0 1843532070 85622784 20438 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 20904 20438 145 145 0 20759 0
[pid=13817] vsize: 83616
Current children cumulated CPU time (s) 658.24
Current children cumulated vsize (Kb) 85740

[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 20928 0 0 0 66680 142 0 0 25 0 1 0 1843532070 86622208 20684 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 21148 20684 145 145 0 21003 0
[pid=13817] vsize: 84592
Current children cumulated CPU time (s) 668.22
Current children cumulated vsize (Kb) 86716

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 21192 0 0 0 67676 144 0 0 25 0 1 0 1843532070 87695360 20948 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 21410 20948 145 145 0 21265 0
[pid=13817] vsize: 85640
Current children cumulated CPU time (s) 678.2
Current children cumulated vsize (Kb) 87764

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 21479 0 0 0 68669 147 0 0 25 0 1 0 1843532070 88870912 21235 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 21697 21235 145 145 0 21552 0
[pid=13817] vsize: 86788
Current children cumulated CPU time (s) 688.16
Current children cumulated vsize (Kb) 88912

[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 21801 0 0 0 69664 149 0 0 25 0 1 0 1843532070 90181632 21557 4294967295 134512640 135094434 3221224448 3221223040 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 22017 21557 145 145 0 21872 0
[pid=13817] vsize: 88068
Current children cumulated CPU time (s) 698.13
Current children cumulated vsize (Kb) 90192

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 22098 0 0 0 70659 150 0 0 25 0 1 0 1843532070 91389952 21854 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 22312 21854 145 145 0 22167 0
[pid=13817] vsize: 89248
Current children cumulated CPU time (s) 708.09
Current children cumulated vsize (Kb) 91372

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 22422 0 0 0 71654 153 0 0 25 0 1 0 1843532070 92712960 22178 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 22635 22178 145 145 0 22490 0
[pid=13817] vsize: 90540
Current children cumulated CPU time (s) 718.07
Current children cumulated vsize (Kb) 92664

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 22744 0 0 0 72649 155 0 0 25 0 1 0 1843532070 94023680 22500 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 22955 22500 145 145 0 22810 0
[pid=13817] vsize: 91820
Current children cumulated CPU time (s) 728.04
Current children cumulated vsize (Kb) 93944

[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 23063 0 0 0 73644 157 0 0 25 0 1 0 1843532070 95846400 22819 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 23400 22819 145 145 0 23255 0
[pid=13817] vsize: 93600
Current children cumulated CPU time (s) 738.01
Current children cumulated vsize (Kb) 95724

[startup+750.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 23387 0 0 0 74637 160 0 0 25 0 1 0 1843532070 97169408 23143 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 23723 23143 145 145 0 23578 0
[pid=13817] vsize: 94892
Current children cumulated CPU time (s) 747.97
Current children cumulated vsize (Kb) 97016

[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 23732 0 0 0 75632 163 0 0 25 0 1 0 1843532070 98578432 23488 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 24067 23488 145 145 0 23922 0
[pid=13817] vsize: 96268
Current children cumulated CPU time (s) 757.95
Current children cumulated vsize (Kb) 98392

[startup+770.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 24061 0 0 0 76626 166 0 0 25 0 1 0 1843532070 99921920 23817 4294967295 134512640 135094434 3221224448 3221223104 134555975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13817/statm): 24395 23817 145 145 0 24250 0
[pid=13817] vsize: 97580
Current children cumulated CPU time (s) 767.92
Current children cumulated vsize (Kb) 99704

[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 24341 0 0 0 77619 168 0 0 25 0 1 0 1843532070 101064704 24097 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 24674 24097 145 145 0 24529 0
[pid=13817] vsize: 98696
Current children cumulated CPU time (s) 777.87
Current children cumulated vsize (Kb) 100820

[startup+790.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 24646 0 0 0 78613 170 0 0 25 0 1 0 1843532070 102322176 24402 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 24981 24402 145 145 0 24836 0
[pid=13817] vsize: 99924
Current children cumulated CPU time (s) 787.83
Current children cumulated vsize (Kb) 102048

[startup+800.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 24873 0 0 0 79608 172 0 0 25 0 1 0 1843532070 103251968 24629 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 25208 24629 145 145 0 25063 0
[pid=13817] vsize: 100832
Current children cumulated CPU time (s) 797.8
Current children cumulated vsize (Kb) 102956

[startup+810.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 25134 0 0 0 80604 174 0 0 25 0 1 0 1843532070 104312832 24890 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 25467 24890 145 145 0 25322 0
[pid=13817] vsize: 101868
Current children cumulated CPU time (s) 807.78
Current children cumulated vsize (Kb) 103992

[startup+820.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 25347 0 0 0 81600 175 0 0 25 0 1 0 1843532070 105177088 25103 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 25678 25103 145 145 0 25533 0
[pid=13817] vsize: 102712
Current children cumulated CPU time (s) 817.75
Current children cumulated vsize (Kb) 104836

[startup+830.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 25584 0 0 0 82596 177 0 0 25 0 1 0 1843532070 106147840 25340 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 25915 25340 145 145 0 25770 0
[pid=13817] vsize: 103660
Current children cumulated CPU time (s) 827.73
Current children cumulated vsize (Kb) 105784

[startup+840.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 25839 0 0 0 83592 179 0 0 25 0 1 0 1843532070 107188224 25595 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 26169 25595 145 145 0 26024 0
[pid=13817] vsize: 104676
Current children cumulated CPU time (s) 837.71
Current children cumulated vsize (Kb) 106800

[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 26066 0 0 0 84588 182 0 0 25 0 1 0 1843532070 108113920 25822 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 26395 25822 145 145 0 26250 0
[pid=13817] vsize: 105580
Current children cumulated CPU time (s) 847.7
Current children cumulated vsize (Kb) 107704

[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 26277 0 0 0 85585 183 0 0 25 0 1 0 1843532070 108978176 26033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 26606 26033 145 145 0 26461 0
[pid=13817] vsize: 106424
Current children cumulated CPU time (s) 857.68
Current children cumulated vsize (Kb) 108548

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 26596 0 0 0 86579 186 0 0 25 0 1 0 1843532070 110280704 26352 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 26924 26352 145 145 0 26779 0
[pid=13817] vsize: 107696
Current children cumulated CPU time (s) 867.65
Current children cumulated vsize (Kb) 109820

[startup+880.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 26847 0 0 0 87575 188 0 0 25 0 1 0 1843532070 111304704 26603 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 27174 26603 145 145 0 27029 0
[pid=13817] vsize: 108696
Current children cumulated CPU time (s) 877.63
Current children cumulated vsize (Kb) 110820

[startup+890.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 27090 0 0 0 88570 190 0 0 25 0 1 0 1843532070 112295936 26846 4294967295 134512640 135094434 3221224448 3221223072 134557633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 27416 26846 145 145 0 27271 0
[pid=13817] vsize: 109664
Current children cumulated CPU time (s) 887.6
Current children cumulated vsize (Kb) 111788

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 27335 0 0 0 89566 192 0 0 25 0 1 0 1843532070 113291264 27091 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 27659 27091 145 145 0 27514 0
[pid=13817] vsize: 110636
Current children cumulated CPU time (s) 897.58
Current children cumulated vsize (Kb) 112760

[startup+910.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 27590 0 0 0 90561 194 0 0 25 0 1 0 1843532070 114331648 27346 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 27913 27346 145 145 0 27768 0
[pid=13817] vsize: 111652
Current children cumulated CPU time (s) 907.55
Current children cumulated vsize (Kb) 113776

[startup+920.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 27857 0 0 0 91558 195 0 0 19 0 1 0 1843532070 115417088 27613 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 28178 27613 145 145 0 28033 0
[pid=13817] vsize: 112712
Current children cumulated CPU time (s) 917.53
Current children cumulated vsize (Kb) 114836

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 28087 0 0 0 92554 197 0 0 25 0 1 0 1843532070 116355072 27843 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 28407 27843 145 145 0 28262 0
[pid=13817] vsize: 113628
Current children cumulated CPU time (s) 927.51
Current children cumulated vsize (Kb) 115752

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 28310 0 0 0 93550 198 0 0 25 0 1 0 1843532070 117260288 28066 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 28628 28066 145 145 0 28483 0
[pid=13817] vsize: 114512
Current children cumulated CPU time (s) 937.48
Current children cumulated vsize (Kb) 116636

[startup+950.072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 28569 0 0 0 94546 200 0 0 25 0 1 0 1843532070 118317056 28325 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 28886 28325 145 145 0 28741 0
[pid=13817] vsize: 115544
Current children cumulated CPU time (s) 947.46
Current children cumulated vsize (Kb) 117668

[startup+960.073 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 28814 0 0 0 95543 202 0 0 25 0 1 0 1843532070 119312384 28570 4294967295 134512640 135094434 3221224448 3221223120 134555792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29129 28570 145 145 0 28984 0
[pid=13817] vsize: 116516
Current children cumulated CPU time (s) 957.45
Current children cumulated vsize (Kb) 118640

[startup+970.075 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29044 0 0 0 96539 203 0 0 25 0 1 0 1843532070 120254464 28800 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29359 28800 145 145 0 29214 0
[pid=13817] vsize: 117436
Current children cumulated CPU time (s) 967.42
Current children cumulated vsize (Kb) 119560

[startup+980.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) T 13813 13813 5245 0 -1 0 29323 0 0 0 97534 205 0 0 25 0 1 0 1843532070 121389056 29079 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29636 29079 145 145 0 29491 0
[pid=13817] vsize: 118544
Current children cumulated CPU time (s) 977.39
Current children cumulated vsize (Kb) 120668

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 98533 205 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 987.38
Current children cumulated vsize (Kb) 120780

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 99533 205 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221222992 134562146 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 997.38
Current children cumulated vsize (Kb) 120780

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 100533 205 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1007.38
Current children cumulated vsize (Kb) 120780

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 101533 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1017.39
Current children cumulated vsize (Kb) 120780

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 102532 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1027.38
Current children cumulated vsize (Kb) 120780

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 103532 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1037.38
Current children cumulated vsize (Kb) 120780

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 104532 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1047.38
Current children cumulated vsize (Kb) 120780

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 105533 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1057.39
Current children cumulated vsize (Kb) 120780

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 106533 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1067.39
Current children cumulated vsize (Kb) 120780

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 107533 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1077.39
Current children cumulated vsize (Kb) 120780

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 108534 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1087.4
Current children cumulated vsize (Kb) 120780

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 109534 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1097.4
Current children cumulated vsize (Kb) 120780

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 110534 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1107.4
Current children cumulated vsize (Kb) 120780

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29352 0 0 0 111534 206 0 0 25 0 1 0 1843532070 121503744 29108 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29108 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1117.4
Current children cumulated vsize (Kb) 120780

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 112533 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1127.4
Current children cumulated vsize (Kb) 120780

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 113533 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1137.4
Current children cumulated vsize (Kb) 120780

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 114533 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1147.4
Current children cumulated vsize (Kb) 120780

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 115533 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1157.4
Current children cumulated vsize (Kb) 120780

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 116534 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1167.41
Current children cumulated vsize (Kb) 120780

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 117534 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1177.41
Current children cumulated vsize (Kb) 120780

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 118534 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1187.41
Current children cumulated vsize (Kb) 120780

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 119534 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1197.41
Current children cumulated vsize (Kb) 120780

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 120534 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1207.41
Current children cumulated vsize (Kb) 120780



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 13817
Raw data (/proc/13813/stat): 13813 (minisat+_script) S 13812 13813 5245 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843532065 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13813/statm): 531 226 485 147 0 384 0
[pid=13813] vsize: 2124
Raw data (/proc/13817/stat): 13817 (minisat+_64-bit) R 13813 13813 5245 0 -1 0 29353 0 0 0 120534 207 0 0 25 0 1 0 1843532070 121503744 29109 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13817/statm): 29664 29109 145 145 0 29519 0
[pid=13817] vsize: 118656
Current children cumulated CPU time (s) 1207.41
Current children cumulated vsize (Kb) 120780

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1207.48
CPU user time (s): 1205.35
CPU system time (s): 2.13168
CPU usage (%): 99.7791
Max. virtual memory (cumulated for all children) (Kb): 120780

Verifier Data

ERROR: no interpretation found !