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/frb53-24-opb/normalized-frb53-24-2.opb
MD5SUM45b026c6b351128e9764d865ca917a59
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -40
Optimality of the best value was proved NO
Number of terms in the objective function 1272
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 1272
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 1272
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 benchmark1206.13
Number of variables1272
Total number of constraints94289
Number of constraints which are clauses94289
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 2308

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        876664 kB
Buffers:         34136 kB
Cached:          96872 kB
SwapCached:        708 kB
Active:          67436 kB
Inactive:        66220 kB
HighTotal:      131008 kB
HighFree:        61068 kB
LowTotal:       903652 kB
LowFree:        815596 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18604 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:12:04 (client local time) WITH STATUS 10 IN 1207.23 SECONDS
stats: 2711 7 1207.23 10

Solver Data

c Parsing PB file...
c Converting 94289 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 |   94289   188578 |   31429       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:70300     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  169363   364695 |   56454       0        0     nan |  0.000 % |
c |       100 |  168931   363803 |   62099      75      961    12.8 |  0.464 % |
c |       251 |  168226   362304 |   68309     195     2080    10.7 |  1.241 % |
c |       477 |  166908   359478 |   75140     361     4481    12.4 |  2.716 % |
c |       814 |  165085   355491 |   82654     634     6941    10.9 |  4.833 % |
c |      1320 |  161650   347896 |   90919    1002    11746    11.7 |  8.903 % |
c |      2079 |  157439   338515 |  100011    1501    17642    11.8 | 13.952 % |
c |      3218 |  149574   320611 |  110012    2257    27487    12.2 | 23.762 % |
c |      4926 |  140077   298909 |  121014    3343    40938    12.2 | 35.604 % |
c |      7488 |  129263   273622 |  133115    4970    57038    11.5 | 49.390 % |
c |     11332 |  118074   247204 |  146427    7283    85078    11.7 | 64.089 % |
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 |     14173 |  112053   232947 |   37351    8812   110869    12.6 | 64.089 % |
c |     14273 |  111956   232718 |   41086    8872   112201    12.6 | 72.341 % |
c |     14423 |  111733   232187 |   45194    9002   114113    12.7 | 72.561 % |
c |     14649 |  111451   231507 |   49714    9151   118315    12.9 | 72.945 % |
c |     14986 |  111001   230402 |   54685    9390   121727    13.0 | 73.568 % |
c |     15492 |  110268   228664 |   60154    9746   131154    13.5 | 74.539 % |
c |     16252 |  109470   226728 |   66169   10246   139678    13.6 | 75.632 % |
c |     17391 |  108305   223901 |   72786   11038   156782    14.2 | 77.225 % |
c |     19099 |  106843   220411 |   80065   12116   192204    15.9 | 79.176 % |
c |     21662 |  105578   217316 |   88071   13811   254342    18.4 | 80.914 % |
c |     25506 |  104256   214065 |   96878   16859   438700    26.0 | 82.765 % |
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 |     29128 |  104139   213840 |   34713   20366   654650    32.1 | 82.765 % |
c |     29229 |  104025   213562 |   38184   20446   657035    32.1 | 83.099 % |
c |     29380 |  103872   213177 |   42002   20466   657976    32.1 | 83.323 % |
c |     29605 |  103872   213177 |   46203   20691   675471    32.6 | 83.323 % |
c |     29942 |  103872   213177 |   50823   21028   685274    32.6 | 83.323 % |
c |     30448 |  103722   212801 |   55905   21442   702839    32.8 | 83.539 % |
c |     31207 |  103261   211676 |   61496   21792   727090    33.4 | 84.177 % |
c |     32346 |  103261   211676 |   67645   22931   784028    34.2 | 84.177 % |
c ==============================================================================
c Found solution: -44
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33412 |  103252   211633 |   34417   23944   928774    38.8 | 84.177 % |
c |     33512 |  103242   211609 |   37858   24024   929884    38.7 | 84.207 % |
c |     33663 |  103242   211609 |   41644   24175   937156    38.8 | 84.207 % |
c |     33888 |  103242   211609 |   45809   24400   945982    38.8 | 84.207 % |
c |     34225 |  103106   211272 |   50389   24656   961580    39.0 | 84.396 % |
c |     34731 |  103096   211246 |   55428   25109   984488    39.2 | 84.412 % |
c |     35491 |  103053   211129 |   60971   25751  1012426    39.3 | 84.478 % |
c |     36631 |  102901   210759 |   67068   26726  1066796    39.9 | 84.686 % |
c |     38339 |  102881   210709 |   73775   28397  1192012    42.0 | 84.715 % |
c |     40901 |  102881   210709 |   81153   30959  1469684    47.5 | 84.715 % |
c |     44746 |  102871   210685 |   89268   34788  1844984    53.0 | 84.729 % |
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 |     49083 |  102808   210537 |   34269   39065  2552883    65.3 | 84.729 % |
c |     49183 |  102715   210319 |   37695   39094  2554059    65.3 | 84.952 % |
c |     49333 |  102715   210319 |   41465   39244  2564935    65.4 | 84.952 % |
c |     49559 |  102638   210132 |   45612   39228  2570691    65.5 | 85.059 % |
c |     49896 |  102638   210132 |   50173   39565  2591937    65.5 | 85.059 % |
c |     50403 |  102638   210132 |   55190   40072  2655788    66.3 | 85.059 % |
c |     51162 |  102638   210132 |   60709   40831  2713978    66.5 | 85.059 % |
c |     52301 |  102627   210103 |   66780   41795  2803087    67.1 | 85.076 % |
c |     54009 |  102492   209776 |   73458   43288  3004323    69.4 | 85.263 % |
c |     56573 |  102482   209754 |   80804   45807  3307196    72.2 | 85.275 % |
c |     60417 |  102434   209638 |   88884   49598  3816497    76.9 | 85.341 % |
c |     66183 |  102321   209365 |   97773   54712  4533488    82.9 | 85.496 % |
c |     74832 |  102098   208818 |  107550   62430  5539945    88.7 | 85.806 % |
c |     87807 |  101884   208284 |  118305   75224  8117231   107.9 | 86.117 % |
c ==============================================================================
c Found solution: -46
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89873 |  101873   208219 |   33957   77213  8366826   108.4 | 86.117 % |
c |     89973 |  101813   208079 |   37352   77250  8370963   108.4 | 86.209 % |
c |     90123 |  101813   208079 |   41087   77400  8384920   108.3 | 86.209 % |
c |     90348 |  101813   208079 |   45196   77625  8402830   108.2 | 86.209 % |
c |     90685 |  101813   208079 |   49716   77962  8425118   108.1 | 86.209 % |
c |     91191 |  101808   208066 |   54688   78418  8477500   108.1 | 86.217 % |
c |     91950 |  101769   207969 |   60156   79147  8535292   107.8 | 86.273 % |
c |     93089 |  101732   207878 |   66172   79954  8650341   108.2 | 86.324 % |
c |     94797 |  101691   207781 |   72789   81587  8836109   108.3 | 86.378 % |
c |     97360 |  101678   207750 |   80068   84139  9093070   108.1 | 86.396 % |
c |    101204 |  101587   207532 |   88075   87350  9467343   108.4 | 86.516 % |
c |    106970 |  101584   207525 |   96883   93115 10262644   110.2 | 86.520 % |
c |    115619 |  101584   207525 |  106571  101764 11400274   112.0 | 86.520 % |
c ==============================================================================
c Found solution: -47
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128246 |  101576   207519 |   33858  113993 13276183   116.5 | 86.520 % |
c |    128346 |  101576   207519 |   37243   20346  1966312    96.6 | 86.569 % |
c |    128496 |  101576   207519 |   40968   20496  1972565    96.2 | 86.569 % |
c |    128722 |  101576   207519 |   45064   20722  1990233    96.0 | 86.569 % |
c |    129059 |  101576   207519 |   49571   21059  2010034    95.4 | 86.569 % |
c |    129565 |  101573   207512 |   54528   21564  2043549    94.8 | 86.573 % |
c |    130325 |  101573   207512 |   59981   22324  2119304    94.9 | 86.573 % |
c |    131466 |  101573   207512 |   65979   23465  2227953    94.9 | 86.573 % |
c |    133174 |  101566   207497 |   72577   25171  2440505    97.0 | 86.580 % |
c |    135736 |  101564   207493 |   79835   27732  2748292    99.1 | 86.582 % |
c |    139581 |  101564   207493 |   87818   31577  3280586   103.9 | 86.582 % |
c |    145347 |  101564   207493 |   96600   37343  4140110   110.9 | 86.582 % |
c |    153996 |  101564   207493 |  106260   45992  5223572   113.6 | 86.582 % |
c |    166970 |  101517   207383 |  116886   58757  6847744   116.5 | 86.641 % |
c |    186431 |  101502   207348 |  128575   78195  9333628   119.4 | 86.660 % |
c |    215624 |  101465   207263 |  141433  107203 13487587   125.8 | 86.705 % |
c |    259413 |  101459   207249 |  155576  150988 19357146   128.2 | 86.712 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639

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/5871/stat): 5871 (minisat+_script) R 5870 5871 1333 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785349124 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5871/statm): 174 3 169 147 0 27 0
[pid=5871] 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=5872
New process pid=5873
New process pid=5874
execve syscall for /bin/sed executable
One traced child (pid=5873) 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=5874) exited with status: 0
One traced child (pid=5872) exited with status: 0
New process pid=5875
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-frb53-24-2.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 949 28 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 26588

[startup+20.0055 s]
Raw data (loadavg): 0.94 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 1949 28 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 19.78
Current children cumulated vsize (Kb) 26588

[startup+30.0072 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 2948 29 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223176 134538517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 26588

[startup+40.0078 s]
Raw data (loadavg): 0.96 0.96 0.97 3/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 3948 29 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 26588

[startup+50.0095 s]
Raw data (loadavg): 0.96 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 4948 29 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 26588

[startup+60.0101 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 5948 30 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 26588

[startup+70.0118 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 6947 30 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 69.78
Current children cumulated vsize (Kb) 26588

[startup+80.0125 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 7947 31 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 26588

[startup+90.0131 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 5926 0 0 0 8946 31 0 0 25 0 1 0 1785349129 25051136 5913 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6116 5913 145 145 0 5971 0
[pid=5875] vsize: 24464
Current children cumulated CPU time (s) 89.78
Current children cumulated vsize (Kb) 26588

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 6053 0 0 0 9944 33 0 0 25 0 1 0 1785349129 25952256 6040 4294967295 134512640 135094434 3221224448 3221223236 134553475 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6336 6040 145 145 0 6191 0
[pid=5875] vsize: 25344
Current children cumulated CPU time (s) 99.78
Current children cumulated vsize (Kb) 27468

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 6053 0 0 0 10943 34 0 0 25 0 1 0 1785349129 25952256 6040 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 6336 6040 145 145 0 6191 0
[pid=5875] vsize: 25344
Current children cumulated CPU time (s) 109.78
Current children cumulated vsize (Kb) 27468

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 6239 0 0 0 11940 35 0 0 25 0 1 0 1785349129 26710016 6226 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 6521 6226 145 145 0 6376 0
[pid=5875] vsize: 26084
Current children cumulated CPU time (s) 119.76
Current children cumulated vsize (Kb) 28208

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) T 5871 5871 1333 0 -1 0 6634 0 0 0 12935 39 0 0 25 0 1 0 1785349129 28164096 6570 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5875/statm): 6876 6570 145 145 0 6731 0
[pid=5875] vsize: 27504
Current children cumulated CPU time (s) 129.75
Current children cumulated vsize (Kb) 29628

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 7071 0 0 0 13929 41 0 0 25 0 1 0 1785349129 29728768 6957 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 7258 6957 145 145 0 7113 0
[pid=5875] vsize: 29032
Current children cumulated CPU time (s) 139.71
Current children cumulated vsize (Kb) 31156

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 7614 0 0 0 14917 46 0 0 25 0 1 0 1785349129 31928320 7500 4294967295 134512640 135094434 3221224448 3221223120 134556485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 7795 7500 145 145 0 7650 0
[pid=5875] vsize: 31180
Current children cumulated CPU time (s) 149.64
Current children cumulated vsize (Kb) 33304

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 8191 0 0 0 15908 50 0 0 25 0 1 0 1785349129 34402304 8077 4294967295 134512640 135094434 3221224448 3221223040 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 8399 8077 145 145 0 8254 0
[pid=5875] vsize: 33596
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 35720

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 8884 0 0 0 16897 55 0 0 25 0 1 0 1785349129 37023744 8720 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 9039 8720 145 145 0 8894 0
[pid=5875] vsize: 36156
Current children cumulated CPU time (s) 169.53
Current children cumulated vsize (Kb) 38280

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 9309 0 0 0 17888 58 0 0 25 0 1 0 1785349129 38748160 9145 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 9460 9145 145 145 0 9315 0
[pid=5875] vsize: 37840
Current children cumulated CPU time (s) 179.47
Current children cumulated vsize (Kb) 39964

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 9893 0 0 0 18877 63 0 0 25 0 1 0 1785349129 41127936 9729 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 10041 9729 145 145 0 9896 0
[pid=5875] vsize: 40164
Current children cumulated CPU time (s) 189.41
Current children cumulated vsize (Kb) 42288

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 10315 0 0 0 19868 66 0 0 25 0 1 0 1785349129 42840064 10151 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 10459 10151 145 145 0 10314 0
[pid=5875] vsize: 41836
Current children cumulated CPU time (s) 199.35
Current children cumulated vsize (Kb) 43960

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) T 5871 5871 1333 0 -1 0 10845 0 0 0 20859 70 0 0 25 0 1 0 1785349129 44998656 10681 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5875/statm): 10986 10681 145 145 0 10841 0
[pid=5875] vsize: 43944
Current children cumulated CPU time (s) 209.3
Current children cumulated vsize (Kb) 46068

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 11290 0 0 0 21852 73 0 0 25 0 1 0 1785349129 46809088 11126 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 11428 11126 145 145 0 11283 0
[pid=5875] vsize: 45712
Current children cumulated CPU time (s) 219.26
Current children cumulated vsize (Kb) 47836

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 11681 0 0 0 22845 75 0 0 18 0 1 0 1785349129 48402432 11517 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 11817 11517 145 145 0 11672 0
[pid=5875] vsize: 47268
Current children cumulated CPU time (s) 229.21
Current children cumulated vsize (Kb) 49392

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 11983 0 0 0 23840 77 0 0 25 0 1 0 1785349129 49631232 11819 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 12117 11819 145 145 0 11972 0
[pid=5875] vsize: 48468
Current children cumulated CPU time (s) 239.18
Current children cumulated vsize (Kb) 50592

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 12480 0 0 0 24833 80 0 0 25 0 1 0 1785349129 51912704 12316 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 12674 12316 145 145 0 12529 0
[pid=5875] vsize: 50696
Current children cumulated CPU time (s) 249.14
Current children cumulated vsize (Kb) 52820

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 13027 0 0 0 25824 83 0 0 21 0 1 0 1785349129 54145024 12863 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 13219 12863 145 145 0 13074 0
[pid=5875] vsize: 52876
Current children cumulated CPU time (s) 259.08
Current children cumulated vsize (Kb) 55000

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 13550 0 0 0 26813 88 0 0 25 0 1 0 1785349129 56274944 13386 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 13739 13386 145 145 0 13594 0
[pid=5875] vsize: 54956
Current children cumulated CPU time (s) 269.02
Current children cumulated vsize (Kb) 57080

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 14071 0 0 0 27804 92 0 0 25 0 1 0 1785349129 58400768 13907 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 14258 13907 145 145 0 14113 0
[pid=5875] vsize: 57032
Current children cumulated CPU time (s) 278.97
Current children cumulated vsize (Kb) 59156

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 14576 0 0 0 28795 95 0 0 25 0 1 0 1785349129 60461056 14412 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 14761 14412 145 145 0 14616 0
[pid=5875] vsize: 59044
Current children cumulated CPU time (s) 288.91
Current children cumulated vsize (Kb) 61168

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 14955 0 0 0 29789 98 0 0 25 0 1 0 1785349129 61800448 14741 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 15088 14741 145 145 0 14943 0
[pid=5875] vsize: 60352
Current children cumulated CPU time (s) 298.88
Current children cumulated vsize (Kb) 62476

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 15224 0 0 0 30784 99 0 0 25 0 1 0 1785349129 62894080 15010 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 15355 15010 145 145 0 15210 0
[pid=5875] vsize: 61420
Current children cumulated CPU time (s) 308.84
Current children cumulated vsize (Kb) 63544

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 15519 0 0 0 31778 102 0 0 25 0 1 0 1785349129 64090112 15305 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 15647 15305 145 145 0 15502 0
[pid=5875] vsize: 62588
Current children cumulated CPU time (s) 318.81
Current children cumulated vsize (Kb) 64712

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 15807 0 0 0 32774 104 0 0 25 0 1 0 1785349129 65261568 15593 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 15933 15593 145 145 0 15788 0
[pid=5875] vsize: 63732
Current children cumulated CPU time (s) 328.79
Current children cumulated vsize (Kb) 65856

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 16059 0 0 0 33768 106 0 0 25 0 1 0 1785349129 66285568 15845 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 16183 15845 145 145 0 16038 0
[pid=5875] vsize: 64732
Current children cumulated CPU time (s) 338.75
Current children cumulated vsize (Kb) 66856

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 16395 0 0 0 34763 108 0 0 25 0 1 0 1785349129 67653632 16181 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 16517 16181 145 145 0 16372 0
[pid=5875] vsize: 66068
Current children cumulated CPU time (s) 348.72
Current children cumulated vsize (Kb) 68192

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 16729 0 0 0 35757 110 0 0 25 0 1 0 1785349129 69013504 16515 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 16849 16515 145 145 0 16704 0
[pid=5875] vsize: 67396
Current children cumulated CPU time (s) 358.68
Current children cumulated vsize (Kb) 69520

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 17072 0 0 0 36751 112 0 0 25 0 1 0 1785349129 70410240 16858 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 17190 16858 145 145 0 17045 0
[pid=5875] vsize: 68760
Current children cumulated CPU time (s) 368.64
Current children cumulated vsize (Kb) 70884

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 17362 0 0 0 37746 114 0 0 25 0 1 0 1785349129 71589888 17148 4294967295 134512640 135094434 3221224448 3221223016 134562037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 17478 17148 145 145 0 17333 0
[pid=5875] vsize: 69912
Current children cumulated CPU time (s) 378.61
Current children cumulated vsize (Kb) 72036

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 17661 0 0 0 38740 117 0 0 25 0 1 0 1785349129 72806400 17447 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 17775 17447 145 145 0 17630 0
[pid=5875] vsize: 71100
Current children cumulated CPU time (s) 388.58
Current children cumulated vsize (Kb) 73224

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.97 3/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 17964 0 0 0 39736 118 0 0 25 0 1 0 1785349129 74039296 17750 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 18076 17750 145 145 0 17931 0
[pid=5875] vsize: 72304
Current children cumulated CPU time (s) 398.55
Current children cumulated vsize (Kb) 74428

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 18256 0 0 0 40730 120 0 0 25 0 1 0 1785349129 75227136 18042 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 18366 18042 145 145 0 18221 0
[pid=5875] vsize: 73464
Current children cumulated CPU time (s) 408.51
Current children cumulated vsize (Kb) 75588

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 18536 0 0 0 41725 122 0 0 25 0 1 0 1785349129 76365824 18322 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 18644 18322 145 145 0 18499 0
[pid=5875] vsize: 74576
Current children cumulated CPU time (s) 418.48
Current children cumulated vsize (Kb) 76700

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 18828 0 0 0 42719 124 0 0 25 0 1 0 1785349129 77553664 18614 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 18934 18614 145 145 0 18789 0
[pid=5875] vsize: 75736
Current children cumulated CPU time (s) 428.44
Current children cumulated vsize (Kb) 77860

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 19182 0 0 0 43713 126 0 0 25 0 1 0 1785349129 78995456 18968 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 19286 18968 145 145 0 19141 0
[pid=5875] vsize: 77144
Current children cumulated CPU time (s) 438.4
Current children cumulated vsize (Kb) 79268

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 19560 0 0 0 44706 129 0 0 25 0 1 0 1785349129 80535552 19346 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 19662 19346 145 145 0 19517 0
[pid=5875] vsize: 78648
Current children cumulated CPU time (s) 448.36
Current children cumulated vsize (Kb) 80772

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 19930 0 0 0 45700 131 0 0 25 0 1 0 1785349129 82042880 19716 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20030 19716 145 145 0 19885 0
[pid=5875] vsize: 80120
Current children cumulated CPU time (s) 458.32
Current children cumulated vsize (Kb) 82244

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 46697 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221222904 134782811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 468.31
Current children cumulated vsize (Kb) 83248

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 47697 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 478.31
Current children cumulated vsize (Kb) 83248

[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 48697 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223120 134556533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 488.31
Current children cumulated vsize (Kb) 83248

[startup+500.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 49698 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 498.32
Current children cumulated vsize (Kb) 83248

[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 50698 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223120 134555853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 508.32
Current children cumulated vsize (Kb) 83248

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 51698 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 518.32
Current children cumulated vsize (Kb) 83248

[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 52698 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 528.32
Current children cumulated vsize (Kb) 83248

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 53699 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 538.33
Current children cumulated vsize (Kb) 83248

[startup+550.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 54699 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 548.33
Current children cumulated vsize (Kb) 83248

[startup+560.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 55699 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 558.33
Current children cumulated vsize (Kb) 83248

[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 56699 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223040 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 568.33
Current children cumulated vsize (Kb) 83248

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 57699 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 578.33
Current children cumulated vsize (Kb) 83248

[startup+590.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 58700 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 588.34
Current children cumulated vsize (Kb) 83248

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 59700 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 598.34
Current children cumulated vsize (Kb) 83248

[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 60700 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 608.34
Current children cumulated vsize (Kb) 83248

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 61701 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 618.35
Current children cumulated vsize (Kb) 83248

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 62701 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 628.35
Current children cumulated vsize (Kb) 83248

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 63701 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 638.35
Current children cumulated vsize (Kb) 83248

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 64701 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 648.35
Current children cumulated vsize (Kb) 83248

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 65702 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 658.36
Current children cumulated vsize (Kb) 83248

[startup+670.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 66702 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 668.36
Current children cumulated vsize (Kb) 83248

[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 67702 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 678.36
Current children cumulated vsize (Kb) 83248

[startup+690.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 68702 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 688.36
Current children cumulated vsize (Kb) 83248

[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 69703 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 698.37
Current children cumulated vsize (Kb) 83248

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 70703 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 708.37
Current children cumulated vsize (Kb) 83248

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 71703 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 718.37
Current children cumulated vsize (Kb) 83248

[startup+730.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 72703 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 728.37
Current children cumulated vsize (Kb) 83248

[startup+740.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20232 0 0 0 73704 133 0 0 25 0 1 0 1785349129 83070976 19968 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20281 19968 145 145 0 20136 0
[pid=5875] vsize: 81124
Current children cumulated CPU time (s) 738.38
Current children cumulated vsize (Kb) 83248

[startup+750.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20358 0 0 0 74701 134 0 0 25 0 1 0 1785349129 83587072 20094 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20407 20094 145 145 0 20262 0
[pid=5875] vsize: 81628
Current children cumulated CPU time (s) 748.36
Current children cumulated vsize (Kb) 83752

[startup+760.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 20738 0 0 0 75695 137 0 0 25 0 1 0 1785349129 85147648 20474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 20788 20474 145 145 0 20643 0
[pid=5875] vsize: 83152
Current children cumulated CPU time (s) 758.33
Current children cumulated vsize (Kb) 85276

[startup+770.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 21004 0 0 0 76689 139 0 0 25 0 1 0 1785349129 86237184 20740 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 21054 20740 145 145 0 20909 0
[pid=5875] vsize: 84216
Current children cumulated CPU time (s) 768.29
Current children cumulated vsize (Kb) 86340

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 21279 0 0 0 77685 141 0 0 25 0 1 0 1785349129 87375872 21015 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 21332 21015 145 145 0 21187 0
[pid=5875] vsize: 85328
Current children cumulated CPU time (s) 778.27
Current children cumulated vsize (Kb) 87452

[startup+790.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 21554 0 0 0 78681 142 0 0 25 0 1 0 1785349129 88502272 21290 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 21607 21290 145 145 0 21462 0
[pid=5875] vsize: 86428
Current children cumulated CPU time (s) 788.24
Current children cumulated vsize (Kb) 88552

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 21810 0 0 0 79677 145 0 0 25 0 1 0 1785349129 89538560 21546 4294967295 134512640 135094434 3221224448 3221223120 134555797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 21860 21546 145 145 0 21715 0
[pid=5875] vsize: 87440
Current children cumulated CPU time (s) 798.23
Current children cumulated vsize (Kb) 89564

[startup+810.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 22134 0 0 0 80672 147 0 0 25 0 1 0 1785349129 90861568 21870 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 22183 21870 145 145 0 22038 0
[pid=5875] vsize: 88732
Current children cumulated CPU time (s) 808.2
Current children cumulated vsize (Kb) 90856

[startup+820.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 22412 0 0 0 81667 149 0 0 25 0 1 0 1785349129 91992064 22148 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 22459 22148 145 145 0 22314 0
[pid=5875] vsize: 89836
Current children cumulated CPU time (s) 818.17
Current children cumulated vsize (Kb) 91960

[startup+830.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 22708 0 0 0 82663 151 0 0 25 0 1 0 1785349129 93204480 22444 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 22755 22444 145 145 0 22610 0
[pid=5875] vsize: 91020
Current children cumulated CPU time (s) 828.15
Current children cumulated vsize (Kb) 93144

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 22969 0 0 0 83658 153 0 0 25 0 1 0 1785349129 94265344 22705 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 23014 22705 145 145 0 22869 0
[pid=5875] vsize: 92056
Current children cumulated CPU time (s) 838.12
Current children cumulated vsize (Kb) 94180

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 23241 0 0 0 84654 155 0 0 25 0 1 0 1785349129 95371264 22977 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 23284 22977 145 145 0 23139 0
[pid=5875] vsize: 93136
Current children cumulated CPU time (s) 848.1
Current children cumulated vsize (Kb) 95260

[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 23530 0 0 0 85648 157 0 0 25 0 1 0 1785349129 96546816 23266 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 23571 23266 145 145 0 23426 0
[pid=5875] vsize: 94284
Current children cumulated CPU time (s) 858.06
Current children cumulated vsize (Kb) 96408

[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 23808 0 0 0 86645 158 0 0 25 0 1 0 1785349129 98197504 23544 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 23974 23544 145 145 0 23829 0
[pid=5875] vsize: 95896
Current children cumulated CPU time (s) 868.04
Current children cumulated vsize (Kb) 98020

[startup+880.071 s]
Raw data (loadavg): 0.99 0.97 0.97 1/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) T 5871 5871 1333 0 -1 0 24087 0 0 0 87639 161 0 0 25 0 1 0 1785349129 99336192 23823 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5875/statm): 24252 23823 145 145 0 24107 0
[pid=5875] vsize: 97008
Current children cumulated CPU time (s) 878.01
Current children cumulated vsize (Kb) 99132

[startup+890.072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 24361 0 0 0 88635 163 0 0 25 0 1 0 1785349129 100450304 24097 4294967295 134512640 135094434 3221224448 3221223088 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 24524 24097 145 145 0 24379 0
[pid=5875] vsize: 98096
Current children cumulated CPU time (s) 887.99
Current children cumulated vsize (Kb) 100220

[startup+900.073 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 24629 0 0 0 89631 164 0 0 25 0 1 0 1785349129 101539840 24365 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 24790 24365 145 145 0 24645 0
[pid=5875] vsize: 99160
Current children cumulated CPU time (s) 897.96
Current children cumulated vsize (Kb) 101284

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 24885 0 0 0 90627 166 0 0 25 0 1 0 1785349129 102584320 24621 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 25045 24621 145 145 0 24900 0
[pid=5875] vsize: 100180
Current children cumulated CPU time (s) 907.94
Current children cumulated vsize (Kb) 102304

[startup+920.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 25149 0 0 0 91622 168 0 0 25 0 1 0 1785349129 103665664 24885 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 25309 24885 145 145 0 25164 0
[pid=5875] vsize: 101236
Current children cumulated CPU time (s) 917.91
Current children cumulated vsize (Kb) 103360

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 25386 0 0 0 92618 169 0 0 25 0 1 0 1785349129 104632320 25122 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 25545 25122 145 145 0 25400 0
[pid=5875] vsize: 102180
Current children cumulated CPU time (s) 927.88
Current children cumulated vsize (Kb) 104304

[startup+940.076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 25631 0 0 0 93613 172 0 0 25 0 1 0 1785349129 105627648 25367 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 25788 25367 145 145 0 25643 0
[pid=5875] vsize: 103152
Current children cumulated CPU time (s) 937.86
Current children cumulated vsize (Kb) 105276

[startup+950.077 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 25874 0 0 0 94607 174 0 0 25 0 1 0 1785349129 106610688 25610 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 26028 25610 145 145 0 25883 0
[pid=5875] vsize: 104112
Current children cumulated CPU time (s) 947.82
Current children cumulated vsize (Kb) 106236

[startup+960.077 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 26117 0 0 0 95602 176 0 0 25 0 1 0 1785349129 107606016 25853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 26271 25853 145 145 0 26126 0
[pid=5875] vsize: 105084
Current children cumulated CPU time (s) 957.79
Current children cumulated vsize (Kb) 107208

[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 26344 0 0 0 96597 179 0 0 25 0 1 0 1785349129 108552192 26080 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 26502 26080 145 145 0 26357 0
[pid=5875] vsize: 106008
Current children cumulated CPU time (s) 967.77
Current children cumulated vsize (Kb) 108132

[startup+980.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 26565 0 0 0 97592 181 0 0 25 0 1 0 1785349129 109449216 26301 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 26721 26301 145 145 0 26576 0
[pid=5875] vsize: 106884
Current children cumulated CPU time (s) 977.74
Current children cumulated vsize (Kb) 109008

[startup+990.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 26808 0 0 0 98589 183 0 0 25 0 1 0 1785349129 110456832 26544 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 26967 26544 145 145 0 26822 0
[pid=5875] vsize: 107868
Current children cumulated CPU time (s) 987.73
Current children cumulated vsize (Kb) 109992

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 27055 0 0 0 99583 185 0 0 25 0 1 0 1785349129 111460352 26791 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 27212 26791 145 145 0 27067 0
[pid=5875] vsize: 108848
Current children cumulated CPU time (s) 997.69
Current children cumulated vsize (Kb) 110972

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 27303 0 0 0 100580 186 0 0 25 0 1 0 1785349129 112472064 27039 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 27459 27039 145 145 0 27314 0
[pid=5875] vsize: 109836
Current children cumulated CPU time (s) 1007.67
Current children cumulated vsize (Kb) 111960

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 27539 0 0 0 101576 188 0 0 25 0 1 0 1785349129 113434624 27275 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 27694 27275 145 145 0 27549 0
[pid=5875] vsize: 110776
Current children cumulated CPU time (s) 1017.65
Current children cumulated vsize (Kb) 112900

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 27796 0 0 0 102571 190 0 0 25 0 1 0 1785349129 114483200 27532 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 27950 27532 145 145 0 27805 0
[pid=5875] vsize: 111800
Current children cumulated CPU time (s) 1027.62
Current children cumulated vsize (Kb) 113924

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 28040 0 0 0 103565 192 0 0 25 0 1 0 1785349129 115486720 27776 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 28195 27776 145 145 0 28050 0
[pid=5875] vsize: 112780
Current children cumulated CPU time (s) 1037.58
Current children cumulated vsize (Kb) 114904

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 28283 0 0 0 104561 194 0 0 25 0 1 0 1785349129 116473856 28019 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 28436 28019 145 145 0 28291 0
[pid=5875] vsize: 113744
Current children cumulated CPU time (s) 1047.56
Current children cumulated vsize (Kb) 115868

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 28530 0 0 0 105557 196 0 0 25 0 1 0 1785349129 117477376 28266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 28681 28266 145 145 0 28536 0
[pid=5875] vsize: 114724
Current children cumulated CPU time (s) 1057.54
Current children cumulated vsize (Kb) 116848

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 28766 0 0 0 106553 197 0 0 25 0 1 0 1785349129 118444032 28502 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 28917 28502 145 145 0 28772 0
[pid=5875] vsize: 115668
Current children cumulated CPU time (s) 1067.51
Current children cumulated vsize (Kb) 117792

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 29014 0 0 0 107548 199 0 0 25 0 1 0 1785349129 119451648 28750 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 29163 28750 145 145 0 29018 0
[pid=5875] vsize: 116652
Current children cumulated CPU time (s) 1077.48
Current children cumulated vsize (Kb) 118776

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 29261 0 0 0 108544 200 0 0 25 0 1 0 1785349129 120459264 28997 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5875/statm): 29409 28997 145 145 0 29264 0
[pid=5875] vsize: 117636
Current children cumulated CPU time (s) 1087.45
Current children cumulated vsize (Kb) 119760

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 29495 0 0 0 109541 202 0 0 25 0 1 0 1785349129 121405440 29231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 29640 29231 145 145 0 29495 0
[pid=5875] vsize: 118560
Current children cumulated CPU time (s) 1097.44
Current children cumulated vsize (Kb) 120684

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 29701 0 0 0 110537 203 0 0 25 0 1 0 1785349129 122241024 29437 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 29844 29437 145 145 0 29699 0
[pid=5875] vsize: 119376
Current children cumulated CPU time (s) 1107.41
Current children cumulated vsize (Kb) 121500

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 29886 0 0 0 111533 205 0 0 25 0 1 0 1785349129 123002880 29622 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 30030 29622 145 145 0 29885 0
[pid=5875] vsize: 120120
Current children cumulated CPU time (s) 1117.39
Current children cumulated vsize (Kb) 122244

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 30054 0 0 0 112529 206 0 0 25 0 1 0 1785349129 123686912 29790 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 30197 29790 145 145 0 30052 0
[pid=5875] vsize: 120788
Current children cumulated CPU time (s) 1127.36
Current children cumulated vsize (Kb) 122912

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 30229 0 0 0 113525 208 0 0 25 0 1 0 1785349129 124399616 29965 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 30371 29965 145 145 0 30226 0
[pid=5875] vsize: 121484
Current children cumulated CPU time (s) 1137.34
Current children cumulated vsize (Kb) 123608

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 30425 0 0 0 114521 210 0 0 25 0 1 0 1785349129 125198336 30161 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 30566 30161 145 145 0 30421 0
[pid=5875] vsize: 122264
Current children cumulated CPU time (s) 1147.32
Current children cumulated vsize (Kb) 124388

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 30607 0 0 0 115517 212 0 0 25 0 1 0 1785349129 125943808 30343 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 30748 30343 145 145 0 30603 0
[pid=5875] vsize: 122992
Current children cumulated CPU time (s) 1157.3
Current children cumulated vsize (Kb) 125116

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 30823 0 0 0 116513 214 0 0 25 0 1 0 1785349129 126820352 30559 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 30962 30559 145 145 0 30817 0
[pid=5875] vsize: 123848
Current children cumulated CPU time (s) 1167.28
Current children cumulated vsize (Kb) 125972

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 31084 0 0 0 117508 216 0 0 25 0 1 0 1785349129 127893504 30820 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 31224 30820 145 145 0 31079 0
[pid=5875] vsize: 124896
Current children cumulated CPU time (s) 1177.25
Current children cumulated vsize (Kb) 127020

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 31350 0 0 0 118502 219 0 0 25 0 1 0 1785349129 128978944 31086 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 31489 31086 145 145 0 31344 0
[pid=5875] vsize: 125956
Current children cumulated CPU time (s) 1187.22
Current children cumulated vsize (Kb) 128080

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 31595 0 0 0 119497 221 0 0 25 0 1 0 1785349129 129974272 31331 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 31732 31331 145 145 0 31587 0
[pid=5875] vsize: 126928
Current children cumulated CPU time (s) 1197.19
Current children cumulated vsize (Kb) 129052

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 31825 0 0 0 120492 224 0 0 25 0 1 0 1785349129 130916352 31561 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 31962 31561 145 145 0 31817 0
[pid=5875] vsize: 127848
Current children cumulated CPU time (s) 1207.17
Current children cumulated vsize (Kb) 129972



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 5875
Raw data (/proc/5871/stat): 5871 (minisat+_script) S 5870 5871 1333 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785349124 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5871/statm): 531 226 485 147 0 384 0
[pid=5871] vsize: 2124
Raw data (/proc/5875/stat): 5875 (minisat+_64-bit) R 5871 5871 1333 0 -1 0 31825 0 0 0 120492 224 0 0 25 0 1 0 1785349129 130916352 31561 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5875/statm): 31962 31561 145 145 0 31817 0
[pid=5875] vsize: 127848
Current children cumulated CPU time (s) 1207.17
Current children cumulated vsize (Kb) 129972

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1207.23
CPU user time (s): 1204.92
CPU system time (s): 2.30465
CPU usage (%): 99.7576
Max. virtual memory (cumulated for all children) (Kb): 129972

Verifier Data

ERROR: no interpretation found !