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-5.opb
MD5SUM54f6acf3ab92bda8abb11350f74de20e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -38
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 constraints80035
Number of constraints which are clauses80035
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 2305

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        914332 kB
Buffers:         35320 kB
Cached:          49992 kB
SwapCached:        844 kB
Active:          68000 kB
Inactive:        19896 kB
HighTotal:      131008 kB
HighFree:        78120 kB
LowTotal:       903652 kB
LowFree:        836212 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26784 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:10:55 (client local time) WITH STATUS 10 IN 1208 SECONDS
stats: 2708 7 1208 10

Solver Data

c Parsing PB file...
c Converting 80035 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 |   80035   160070 |   26678       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  147951   319392 |   49317       0        0     nan |  0.000 % |
c |       100 |  147312   318040 |   54248      57     1282    22.5 |  0.772 % |
c |       251 |  146773   316900 |   59673     187     2917    15.6 |  1.422 % |
c |       476 |  145213   313544 |   65640     368     5352    14.5 |  3.429 % |
c |       813 |  143505   309796 |   72205     621     8354    13.5 |  5.644 % |
c |      1320 |  139677   301273 |   79425    1008    13306    13.2 | 10.638 % |
c |      2079 |  135693   292365 |   87368    1543    19391    12.6 | 15.964 % |
c |      3218 |  129784   278974 |   96104    2359    29829    12.6 | 24.035 % |
c |      4926 |  122432   262085 |  105715    3616    48944    13.5 | 34.279 % |
c |      7488 |  111938   237654 |  116286    5258    69109    13.1 | 49.006 % |
c |     11332 |  101310   212553 |  127915    7785   111547    14.3 | 64.438 % |
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 |     14084 |   96816   201835 |   32272    9412   143299    15.2 | 64.438 % |
c |     14184 |   96772   201727 |   35499    9499   144028    15.2 | 71.052 % |
c |     14334 |   96570   201231 |   39049    9550   144833    15.2 | 71.359 % |
c |     14560 |   96295   200569 |   42954    9703   147277    15.2 | 71.772 % |
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 |     14788 |   96036   200007 |   32012    9819   147145    15.0 | 71.772 % |
c |     14888 |   96036   200007 |   35213    9919   148330    15.0 | 72.243 % |
c |     15038 |   96036   200007 |   38734   10069   149721    14.9 | 72.243 % |
c |     15263 |   96036   200007 |   42607   10294   154570    15.0 | 72.243 % |
c |     15600 |   95761   199378 |   46868   10569   160536    15.2 | 72.625 % |
c |     16106 |   95153   197892 |   51555   10886   169202    15.5 | 73.553 % |
c |     16865 |   94758   196946 |   56711   11525   181628    15.8 | 74.144 % |
c |     18004 |   94310   195868 |   62382   12430   205545    16.5 | 74.813 % |
c |     19713 |   94001   195126 |   68620   13894   265668    19.1 | 75.275 % |
c |     22276 |   92381   191245 |   75482   15687   319719    20.4 | 77.691 % |
c |     26120 |   91522   189173 |   83030   19074   495885    26.0 | 78.980 % |
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 |     27853 |   91077   188149 |   30359   20461   588458    28.8 | 78.980 % |
c |     27953 |   91077   188149 |   33394   20561   590686    28.7 | 79.629 % |
c |     28103 |   91026   188021 |   36734   20631   592469    28.7 | 79.706 % |
c |     28328 |   91026   188021 |   40407   20856   599678    28.8 | 79.706 % |
c |     28665 |   91026   188021 |   44448   21193   622260    29.4 | 79.706 % |
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 |     28969 |   90731   187263 |   30243   21322   628608    29.5 | 79.706 % |
c |     29069 |   90722   187240 |   33267   21414   632006    29.5 | 80.173 % |
c |     29219 |   90593   186934 |   36594   21396   633325    29.6 | 80.358 % |
c |     29445 |   90536   186795 |   40253   21617   652375    30.2 | 80.447 % |
c |     29782 |   90499   186706 |   44278   21904   668251    30.5 | 80.503 % |
c |     30289 |   90299   186216 |   48706   22108   682253    30.9 | 80.809 % |
c |     31048 |   90231   186060 |   53577   22782   711877    31.2 | 80.904 % |
c |     32187 |   89778   184940 |   58935   23599   766824    32.5 | 81.598 % |
c |     33896 |   89773   184929 |   64828   25280   869667    34.4 | 81.605 % |
c |     36458 |   89601   184511 |   71311   27781  1104154    39.7 | 81.868 % |
c |     40303 |   89001   183057 |   78442   30883  1452224    47.0 | 82.782 % |
c |     46069 |   88653   182193 |   86286   36261  1909440    52.7 | 83.326 % |
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 |     53577 |   88651   182222 |   29550   43705  2561808    58.6 | 83.326 % |
c |     53677 |   88651   182222 |   32505   43805  2563789    58.5 | 83.359 % |
c |     53827 |   88622   182151 |   35755   43811  2568576    58.6 | 83.404 % |
c |     54052 |   88622   182151 |   39331   44036  2589935    58.8 | 83.404 % |
c |     54389 |   88537   181938 |   43264   44316  2602581    58.7 | 83.542 % |
c |     54895 |   88502   181851 |   47590   44743  2640960    59.0 | 83.598 % |
c |     55654 |   88489   181818 |   52349   45410  2688658    59.2 | 83.620 % |
c |     56795 |   88255   181245 |   57584   46245  2798146    60.5 | 83.970 % |
c |     58504 |   88255   181245 |   63343   47954  2931810    61.1 | 83.970 % |
c |     61066 |   88117   180910 |   69677   50021  3189748    63.8 | 84.181 % |
c |     64910 |   88088   180842 |   76645   53834  3616238    67.2 | 84.220 % |
c |     70676 |   88083   180831 |   84309   59598  4123646    69.2 | 84.226 % |
c ==============================================================================
c Found solution: -45
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76602 |   87920   180446 |   29306   64994  4731142    72.8 | 84.226 % |
c |     76704 |   87920   180446 |   32236   65096  4739491    72.8 | 84.488 % |
c |     76855 |   87920   180446 |   35460   65247  4745429    72.7 | 84.488 % |
c |     77080 |   87920   180446 |   39006   65472  4759519    72.7 | 84.488 % |
c |     77417 |   87920   180446 |   42906   65809  4783089    72.7 | 84.488 % |
c |     77924 |   87920   180446 |   47197   66316  4834519    72.9 | 84.488 % |
c |     78684 |   87915   180435 |   51917   67073  4915209    73.3 | 84.494 % |
c |     79823 |   87782   180128 |   57109   67701  5020176    74.2 | 84.681 % |
c |     81531 |   87629   179763 |   62820   69363  5207979    75.1 | 84.907 % |
c |     84093 |   87629   179763 |   69102   71925  5462668    75.9 | 84.907 % |
c |     87937 |   87629   179763 |   76012   75769  5852613    77.2 | 84.907 % |
c |     93703 |   87615   179727 |   83613   81487  6335995    77.8 | 84.931 % |
c |    102352 |   87615   179727 |   91974   90136  7289858    80.9 | 84.931 % |
c |    115328 |   87613   179723 |  101172  103111  8798918    85.3 | 84.933 % |
c |    134790 |   87540   179550 |  111289  122522 11000809    89.8 | 85.040 % |
c |    163982 |   87270   178893 |  122418  150898 14231492    94.3 | 85.455 % |
c |    207771 |   87197   178706 |  134660   54694  5876777   107.4 | 85.578 % |
c |    273455 |   87182   178671 |  148126  120376 10322069    85.7 | 85.599 % |
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/5448/stat): 5448 (minisat+_script) R 5447 5448 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843516560 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5448/statm): 174 3 169 147 0 27 0
[pid=5448] 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=5449
New process pid=5450
New process pid=5451
execve syscall for /bin/sed executable
One traced child (pid=5450) 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=5451) exited with status: 0
One traced child (pid=5449) exited with status: 0
New process pid=5452
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-frb50-23-5.opb

[startup+10.0035 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 957 24 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0
[pid=5452] vsize: 21124
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 23248

[startup+20.0044 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 1957 24 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0
[pid=5452] vsize: 21124
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 23248

[startup+30.0064 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 2956 25 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0
[pid=5452] vsize: 21124
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 23248

[startup+40.0073 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 3956 25 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223116 134553438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0
[pid=5452] vsize: 21124
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 23248

[startup+50.0092 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 4955 26 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0
[pid=5452] vsize: 21124
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 23248

[startup+60.0101 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5061 0 0 0 5955 26 0 0 25 0 1 0 1843516564 21630976 5048 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5281 5048 145 145 0 5136 0
[pid=5452] vsize: 21124
Current children cumulated CPU time (s) 59.81
Current children cumulated vsize (Kb) 23248

[startup+70.0111 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5075 0 0 0 6954 26 0 0 25 0 1 0 1843516564 21688320 5062 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5295 5062 145 145 0 5150 0
[pid=5452] vsize: 21180
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 23304

[startup+80.013 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5107 0 0 0 7954 27 0 0 25 0 1 0 1843516564 21843968 5094 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5333 5094 145 145 0 5188 0
[pid=5452] vsize: 21332
Current children cumulated CPU time (s) 79.81
Current children cumulated vsize (Kb) 23456

[startup+90.0139 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5411 0 0 0 8952 29 0 0 25 0 1 0 1843516564 23953408 5398 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5848 5398 145 145 0 5703 0
[pid=5452] vsize: 23392
Current children cumulated CPU time (s) 89.81
Current children cumulated vsize (Kb) 25516

[startup+100.016 s]
Raw data (loadavg): 1.09 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5465 0 0 0 9950 30 0 0 25 0 1 0 1843516564 24158208 5452 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 5898 5452 145 145 0 5753 0
[pid=5452] vsize: 23592
Current children cumulated CPU time (s) 99.8
Current children cumulated vsize (Kb) 25716

[startup+110.018 s]
Raw data (loadavg): 1.08 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5865 0 0 0 10945 32 0 0 25 0 1 0 1843516564 25649152 5805 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 6262 5805 145 145 0 6117 0
[pid=5452] vsize: 25048
Current children cumulated CPU time (s) 109.77
Current children cumulated vsize (Kb) 27172

[startup+120.019 s]
Raw data (loadavg): 1.06 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 6202 0 0 0 11939 35 0 0 25 0 1 0 1843516564 26824704 6096 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 6549 6096 145 145 0 6404 0
[pid=5452] vsize: 26196
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 28320

[startup+130.02 s]
Raw data (loadavg): 1.05 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 6777 0 0 0 12929 39 0 0 25 0 1 0 1843516564 29163520 6671 4294967295 134512640 135094434 3221224448 3221223120 134556528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 7120 6671 145 145 0 6975 0
[pid=5452] vsize: 28480
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 30604

[startup+140.021 s]
Raw data (loadavg): 1.05 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 7187 0 0 0 13922 42 0 0 25 0 1 0 1843516564 30957568 7081 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 7558 7081 145 145 0 7413 0
[pid=5452] vsize: 30232
Current children cumulated CPU time (s) 139.64
Current children cumulated vsize (Kb) 32356

[startup+150.022 s]
Raw data (loadavg): 1.04 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 7577 0 0 0 14914 45 0 0 25 0 1 0 1843516564 32530432 7471 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 7942 7471 145 145 0 7797 0
[pid=5452] vsize: 31768
Current children cumulated CPU time (s) 149.59
Current children cumulated vsize (Kb) 33892

[startup+160.023 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 8104 0 0 0 15905 49 0 0 25 0 1 0 1843516564 34480128 7951 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 8418 7951 145 145 0 8273 0
[pid=5452] vsize: 33672
Current children cumulated CPU time (s) 159.54
Current children cumulated vsize (Kb) 35796

[startup+170.024 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 8385 0 0 0 16900 50 0 0 25 0 1 0 1843516564 35618816 8232 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 8696 8232 145 145 0 8551 0
[pid=5452] vsize: 34784
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 36908

[startup+180.025 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 8810 0 0 0 17892 54 0 0 25 0 1 0 1843516564 37347328 8657 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 9118 8657 145 145 0 8973 0
[pid=5452] vsize: 36472
Current children cumulated CPU time (s) 179.46
Current children cumulated vsize (Kb) 38596

[startup+190.026 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 9289 0 0 0 18881 59 0 0 25 0 1 0 1843516564 39288832 9136 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 9592 9136 145 145 0 9447 0
[pid=5452] vsize: 38368
Current children cumulated CPU time (s) 189.4
Current children cumulated vsize (Kb) 40492

[startup+200.027 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 9679 0 0 0 19875 62 0 0 25 0 1 0 1843516564 40873984 9526 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 9979 9526 145 145 0 9834 0
[pid=5452] vsize: 39916
Current children cumulated CPU time (s) 199.37
Current children cumulated vsize (Kb) 42040

[startup+210.028 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 10120 0 0 0 20866 65 0 0 25 0 1 0 1843516564 42663936 9967 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 10416 9967 145 145 0 10271 0
[pid=5452] vsize: 41664
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 43788

[startup+220.029 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 10405 0 0 0 21862 68 0 0 25 0 1 0 1843516564 43823104 10252 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 10699 10252 145 145 0 10554 0
[pid=5452] vsize: 42796
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 44920

[startup+230.03 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 10758 0 0 0 22855 71 0 0 25 0 1 0 1843516564 45330432 10559 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 11067 10559 145 145 0 10922 0
[pid=5452] vsize: 44268
Current children cumulated CPU time (s) 229.26
Current children cumulated vsize (Kb) 46392

[startup+240.031 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11073 0 0 0 23848 74 0 0 25 0 1 0 1843516564 46612480 10874 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 11380 10874 145 145 0 11235 0
[pid=5452] vsize: 45520
Current children cumulated CPU time (s) 239.22
Current children cumulated vsize (Kb) 47644

[startup+250.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11413 0 0 0 24841 77 0 0 25 0 1 0 1843516564 47988736 11214 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 11716 11214 145 145 0 11571 0
[pid=5452] vsize: 46864
Current children cumulated CPU time (s) 249.18
Current children cumulated vsize (Kb) 48988

[startup+260.033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11724 0 0 0 25834 80 0 0 25 0 1 0 1843516564 49254400 11525 4294967295 134512640 135094434 3221224448 3221223120 134555547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 12025 11525 145 145 0 11880 0
[pid=5452] vsize: 48100
Current children cumulated CPU time (s) 259.14
Current children cumulated vsize (Kb) 50224

[startup+270.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11994 0 0 0 26830 82 0 0 25 0 1 0 1843516564 50348032 11795 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 12292 11795 145 145 0 12147 0
[pid=5452] vsize: 49168
Current children cumulated CPU time (s) 269.12
Current children cumulated vsize (Kb) 51292

[startup+280.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 12318 0 0 0 27824 84 0 0 25 0 1 0 1843516564 51662848 12119 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 12613 12119 145 145 0 12468 0
[pid=5452] vsize: 50452
Current children cumulated CPU time (s) 279.08
Current children cumulated vsize (Kb) 52576

[startup+290.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 12602 0 0 0 28819 86 0 0 25 0 1 0 1843516564 52813824 12403 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 12894 12403 145 145 0 12749 0
[pid=5452] vsize: 51576
Current children cumulated CPU time (s) 289.05
Current children cumulated vsize (Kb) 53700

[startup+300.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 12916 0 0 0 29814 88 0 0 25 0 1 0 1843516564 54087680 12717 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 13205 12717 145 145 0 13060 0
[pid=5452] vsize: 52820
Current children cumulated CPU time (s) 299.02
Current children cumulated vsize (Kb) 54944

[startup+310.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 13318 0 0 0 30806 91 0 0 25 0 1 0 1843516564 55726080 13119 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 13605 13119 145 145 0 13460 0
[pid=5452] vsize: 54420
Current children cumulated CPU time (s) 308.97
Current children cumulated vsize (Kb) 56544

[startup+320.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 13641 0 0 0 31799 95 0 0 25 0 1 0 1843516564 57036800 13442 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 13925 13442 145 145 0 13780 0
[pid=5452] vsize: 55700
Current children cumulated CPU time (s) 318.94
Current children cumulated vsize (Kb) 57824

[startup+330.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14004 0 0 0 32791 98 0 0 25 0 1 0 1843516564 58511360 13805 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 14285 13805 145 145 0 14140 0
[pid=5452] vsize: 57140
Current children cumulated CPU time (s) 328.89
Current children cumulated vsize (Kb) 59264

[startup+340.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14321 0 0 0 33785 100 0 0 25 0 1 0 1843516564 59801600 14122 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 14600 14122 145 145 0 14455 0
[pid=5452] vsize: 58400
Current children cumulated CPU time (s) 338.85
Current children cumulated vsize (Kb) 60524

[startup+350.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14606 0 0 0 34780 102 0 0 25 0 1 0 1843516564 60964864 14407 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 14884 14407 145 145 0 14739 0
[pid=5452] vsize: 59536
Current children cumulated CPU time (s) 348.82
Current children cumulated vsize (Kb) 61660

[startup+360.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14888 0 0 0 35774 105 0 0 25 0 1 0 1843516564 62107648 14689 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 15163 14689 145 145 0 15018 0
[pid=5452] vsize: 60652
Current children cumulated CPU time (s) 358.79
Current children cumulated vsize (Kb) 62776

[startup+370.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 15115 0 0 0 36768 107 0 0 25 0 1 0 1843516564 63025152 14916 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 15387 14916 145 145 0 15242 0
[pid=5452] vsize: 61548
Current children cumulated CPU time (s) 368.75
Current children cumulated vsize (Kb) 63672

[startup+380.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 15441 0 0 0 37761 110 0 0 25 0 1 0 1843516564 64352256 15242 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 15711 15242 145 145 0 15566 0
[pid=5452] vsize: 62844
Current children cumulated CPU time (s) 378.71
Current children cumulated vsize (Kb) 64968

[startup+390.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 15701 0 0 0 38756 113 0 0 25 0 1 0 1843516564 65404928 15502 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 15968 15502 145 145 0 15823 0
[pid=5452] vsize: 63872
Current children cumulated CPU time (s) 388.69
Current children cumulated vsize (Kb) 65996

[startup+400.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16034 0 0 0 39748 116 0 0 25 0 1 0 1843516564 66760704 15835 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 16299 15835 145 145 0 16154 0
[pid=5452] vsize: 65196
Current children cumulated CPU time (s) 398.64
Current children cumulated vsize (Kb) 67320

[startup+410.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16352 0 0 0 40739 120 0 0 25 0 1 0 1843516564 68050944 16153 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 16614 16153 145 145 0 16469 0
[pid=5452] vsize: 66456
Current children cumulated CPU time (s) 408.59
Current children cumulated vsize (Kb) 68580

[startup+420.052 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16626 0 0 0 41732 124 0 0 25 0 1 0 1843516564 69165056 16427 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 16886 16427 145 145 0 16741 0
[pid=5452] vsize: 67544
Current children cumulated CPU time (s) 418.56
Current children cumulated vsize (Kb) 69668

[startup+430.054 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16864 0 0 0 42728 126 0 0 25 0 1 0 1843516564 70131712 16665 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 17122 16665 145 145 0 16977 0
[pid=5452] vsize: 68488
Current children cumulated CPU time (s) 428.54
Current children cumulated vsize (Kb) 70612

[startup+440.055 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) T 5448 5448 31027 0 -1 0 17119 0 0 0 43721 128 0 0 25 0 1 0 1843516564 71168000 16920 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/5452/statm): 17375 16920 145 145 0 17230 0
[pid=5452] vsize: 69500
Current children cumulated CPU time (s) 438.49
Current children cumulated vsize (Kb) 71624

[startup+450.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17355 0 0 0 44718 129 0 0 25 0 1 0 1843516564 72126464 17156 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 17609 17156 145 145 0 17464 0
[pid=5452] vsize: 70436
Current children cumulated CPU time (s) 448.47
Current children cumulated vsize (Kb) 72560

[startup+460.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17620 0 0 0 45713 131 0 0 25 0 1 0 1843516564 73207808 17421 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 17873 17421 145 145 0 17728 0
[pid=5452] vsize: 71492
Current children cumulated CPU time (s) 458.44
Current children cumulated vsize (Kb) 73616

[startup+470.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17784 0 0 0 46710 133 0 0 25 0 1 0 1843516564 73883648 17585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 18038 17585 145 145 0 17893 0
[pid=5452] vsize: 72152
Current children cumulated CPU time (s) 468.43
Current children cumulated vsize (Kb) 74276

[startup+480.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17961 0 0 0 47706 134 0 0 25 0 1 0 1843516564 74596352 17762 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 18212 17762 145 145 0 18067 0
[pid=5452] vsize: 72848
Current children cumulated CPU time (s) 478.4
Current children cumulated vsize (Kb) 74972

[startup+490.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 18227 0 0 0 48700 136 0 0 25 0 1 0 1843516564 75677696 18028 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 18476 18028 145 145 0 18331 0
[pid=5452] vsize: 73904
Current children cumulated CPU time (s) 488.36
Current children cumulated vsize (Kb) 76028

[startup+500.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 18584 0 0 0 49692 140 0 0 25 0 1 0 1843516564 77651968 18385 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 18958 18385 145 145 0 18813 0
[pid=5452] vsize: 75832
Current children cumulated CPU time (s) 498.32
Current children cumulated vsize (Kb) 77956

[startup+510.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 18855 0 0 0 50687 143 0 0 25 0 1 0 1843516564 78753792 18656 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 19227 18656 145 145 0 19082 0
[pid=5452] vsize: 76908
Current children cumulated CPU time (s) 508.3
Current children cumulated vsize (Kb) 79032

[startup+520.067 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19151 0 0 0 51681 145 0 0 25 0 1 0 1843516564 79958016 18952 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 19521 18952 145 145 0 19376 0
[pid=5452] vsize: 78084
Current children cumulated CPU time (s) 518.26
Current children cumulated vsize (Kb) 80208

[startup+530.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19435 0 0 0 52675 148 0 0 25 0 1 0 1843516564 81108992 19236 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 19802 19236 145 145 0 19657 0
[pid=5452] vsize: 79208
Current children cumulated CPU time (s) 528.23
Current children cumulated vsize (Kb) 81332

[startup+540.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19725 0 0 0 53671 149 0 0 25 0 1 0 1843516564 82292736 19526 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 20091 19526 145 145 0 19946 0
[pid=5452] vsize: 80364
Current children cumulated CPU time (s) 538.2
Current children cumulated vsize (Kb) 82488

[startup+550.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19997 0 0 0 54665 152 0 0 25 0 1 0 1843516564 83406848 19798 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 20363 19798 145 145 0 20218 0
[pid=5452] vsize: 81452
Current children cumulated CPU time (s) 548.17
Current children cumulated vsize (Kb) 83576

[startup+560.073 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20186 0 0 0 55662 153 0 0 25 0 1 0 1843516564 84180992 19987 4294967295 134512640 135094434 3221224448 3221223040 134557287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 20552 19987 145 145 0 20407 0
[pid=5452] vsize: 82208
Current children cumulated CPU time (s) 558.15
Current children cumulated vsize (Kb) 84332

[startup+570.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20327 0 0 0 56659 154 0 0 25 0 1 0 1843516564 84754432 20128 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 20692 20128 145 145 0 20547 0
[pid=5452] vsize: 82768
Current children cumulated CPU time (s) 568.13
Current children cumulated vsize (Kb) 84892

[startup+580.076 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20523 0 0 0 57654 157 0 0 25 0 1 0 1843516564 85557248 20324 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 20888 20324 145 145 0 20743 0
[pid=5452] vsize: 83552
Current children cumulated CPU time (s) 578.11
Current children cumulated vsize (Kb) 85676

[startup+590.077 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20732 0 0 0 58650 159 0 0 25 0 1 0 1843516564 86417408 20533 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 21098 20533 145 145 0 20953 0
[pid=5452] vsize: 84392
Current children cumulated CPU time (s) 588.09
Current children cumulated vsize (Kb) 86516

[startup+600.079 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20926 0 0 0 59646 160 0 0 25 0 1 0 1843516564 87203840 20727 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 21290 20727 145 145 0 21145 0
[pid=5452] vsize: 85160
Current children cumulated CPU time (s) 598.06
Current children cumulated vsize (Kb) 87284

[startup+610.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21132 0 0 0 60642 162 0 0 25 0 1 0 1843516564 88039424 20933 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 21494 20933 145 145 0 21349 0
[pid=5452] vsize: 85976
Current children cumulated CPU time (s) 608.04
Current children cumulated vsize (Kb) 88100

[startup+620.081 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21343 0 0 0 61638 164 0 0 25 0 1 0 1843516564 88899584 21144 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 21704 21144 145 145 0 21559 0
[pid=5452] vsize: 86816
Current children cumulated CPU time (s) 618.02
Current children cumulated vsize (Kb) 88940

[startup+630.082 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21551 0 0 0 62634 166 0 0 25 0 1 0 1843516564 89735168 21352 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 21908 21352 145 145 0 21763 0
[pid=5452] vsize: 87632
Current children cumulated CPU time (s) 628
Current children cumulated vsize (Kb) 89756

[startup+640.083 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21772 0 0 0 63628 169 0 0 25 0 1 0 1843516564 90632192 21573 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22127 21573 145 145 0 21982 0
[pid=5452] vsize: 88508
Current children cumulated CPU time (s) 637.97
Current children cumulated vsize (Kb) 90632

[startup+650.085 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22061 0 0 0 64625 171 0 0 25 0 1 0 1843516564 91811840 21862 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22415 21862 145 145 0 22270 0
[pid=5452] vsize: 89660
Current children cumulated CPU time (s) 647.96
Current children cumulated vsize (Kb) 91784

[startup+660.086 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22316 0 0 0 65619 174 0 0 25 0 1 0 1843516564 92848128 22117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22668 22117 145 145 0 22523 0
[pid=5452] vsize: 90672
Current children cumulated CPU time (s) 657.93
Current children cumulated vsize (Kb) 92796

[startup+670.087 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 66616 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221222480 134562780 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 667.91
Current children cumulated vsize (Kb) 93660

[startup+680.088 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 67617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 677.92
Current children cumulated vsize (Kb) 93660

[startup+690.089 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 68617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 687.92
Current children cumulated vsize (Kb) 93660

[startup+700.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 69617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 697.92
Current children cumulated vsize (Kb) 93660

[startup+710.091 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 70617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 707.92
Current children cumulated vsize (Kb) 93660

[startup+720.092 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 71618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 717.93
Current children cumulated vsize (Kb) 93660

[startup+730.093 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 72618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 727.93
Current children cumulated vsize (Kb) 93660

[startup+740.094 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 73618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 737.93
Current children cumulated vsize (Kb) 93660

[startup+750.095 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 74618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 747.93
Current children cumulated vsize (Kb) 93660

[startup+760.096 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 75617 176 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223120 134555853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 757.93
Current children cumulated vsize (Kb) 93660

[startup+770.097 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 76617 176 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 767.93
Current children cumulated vsize (Kb) 93660

[startup+780.099 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 77617 176 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 777.93
Current children cumulated vsize (Kb) 93660

[startup+790.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 78616 177 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 787.93
Current children cumulated vsize (Kb) 93660

[startup+800.101 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 79616 177 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 797.93
Current children cumulated vsize (Kb) 93660

[startup+810.103 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 80615 177 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 807.92
Current children cumulated vsize (Kb) 93660

[startup+820.104 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 81615 178 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 817.93
Current children cumulated vsize (Kb) 93660

[startup+830.106 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 82615 178 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 827.93
Current children cumulated vsize (Kb) 93660

[startup+840.108 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 83614 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 837.93
Current children cumulated vsize (Kb) 93660

[startup+850.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 84614 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 847.93
Current children cumulated vsize (Kb) 93660

[startup+860.111 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 85614 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 857.93
Current children cumulated vsize (Kb) 93660

[startup+870.112 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 86613 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 867.92
Current children cumulated vsize (Kb) 93660

[startup+880.114 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 87613 180 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 877.93
Current children cumulated vsize (Kb) 93660

[startup+890.115 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 88613 180 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 887.93
Current children cumulated vsize (Kb) 93660

[startup+900.117 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 89612 181 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 897.93
Current children cumulated vsize (Kb) 93660

[startup+910.118 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 90612 181 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 907.93
Current children cumulated vsize (Kb) 93660

[startup+920.119 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 91612 181 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 917.93
Current children cumulated vsize (Kb) 93660

[startup+930.12 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 92611 182 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 927.93
Current children cumulated vsize (Kb) 93660

[startup+940.121 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 93611 182 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 937.93
Current children cumulated vsize (Kb) 93660

[startup+950.123 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 94611 182 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 947.93
Current children cumulated vsize (Kb) 93660

[startup+960.125 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 95610 183 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 957.93
Current children cumulated vsize (Kb) 93660

[startup+970.126 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 96610 183 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 967.93
Current children cumulated vsize (Kb) 93660

[startup+980.128 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 97609 183 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 977.92
Current children cumulated vsize (Kb) 93660

[startup+990.129 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 98609 184 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 987.93
Current children cumulated vsize (Kb) 93660

[startup+1000.13 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 99608 184 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 997.92
Current children cumulated vsize (Kb) 93660

[startup+1010.13 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 100608 184 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1007.92
Current children cumulated vsize (Kb) 93660

[startup+1020.13 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 101608 185 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1017.93
Current children cumulated vsize (Kb) 93660

[startup+1030.13 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 102608 185 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1027.93
Current children cumulated vsize (Kb) 93660

[startup+1040.13 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 103608 185 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1037.93
Current children cumulated vsize (Kb) 93660

[startup+1050.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 104607 186 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1047.93
Current children cumulated vsize (Kb) 93660

[startup+1060.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 105607 186 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1057.93
Current children cumulated vsize (Kb) 93660

[startup+1070.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 106606 187 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1067.93
Current children cumulated vsize (Kb) 93660

[startup+1080.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 107606 187 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1077.93
Current children cumulated vsize (Kb) 93660

[startup+1090.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 108605 187 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1087.92
Current children cumulated vsize (Kb) 93660

[startup+1100.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 109605 188 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1097.93
Current children cumulated vsize (Kb) 93660

[startup+1110.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 110605 188 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1107.93
Current children cumulated vsize (Kb) 93660

[startup+1120.14 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 111604 189 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1117.93
Current children cumulated vsize (Kb) 93660

[startup+1130.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 112604 189 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1127.93
Current children cumulated vsize (Kb) 93660

[startup+1140.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 113604 189 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223136 134554717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1137.93
Current children cumulated vsize (Kb) 93660

[startup+1150.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 114604 190 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1147.94
Current children cumulated vsize (Kb) 93660

[startup+1160.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 115604 190 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1157.94
Current children cumulated vsize (Kb) 93660

[startup+1170.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 116604 190 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1167.94
Current children cumulated vsize (Kb) 93660

[startup+1180.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 117604 191 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1177.95
Current children cumulated vsize (Kb) 93660

[startup+1190.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 118603 191 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1187.94
Current children cumulated vsize (Kb) 93660

[startup+1200.15 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 119603 192 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1197.95
Current children cumulated vsize (Kb) 93660

[startup+1210.16 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 120603 192 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1207.95
Current children cumulated vsize (Kb) 93660



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.16 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 5452
Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5448/statm): 531 226 485 147 0 384 0
[pid=5448] vsize: 2124
Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 120603 192 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0
[pid=5452] vsize: 91536
Current children cumulated CPU time (s) 1207.95
Current children cumulated vsize (Kb) 93660

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

Child status: 10
Real time (s): 1210.21
CPU time (s): 1208
CPU user time (s): 1206.04
CPU system time (s): 1.9637
CPU usage (%): 99.8177
Max. virtual memory (cumulated for all children) (Kb): 93660

Verifier Data

ERROR: no interpretation found !