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-3.opb
MD5SUMbaa7b619e2dc55a18c674a719d78c00c
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -41
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 benchmark1195.05
Number of variables1272
Total number of constraints94127
Number of constraints which are clauses94127
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 2311

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915124 kB
Buffers:         34976 kB
Cached:          56556 kB
SwapCached:        744 kB
Active:          69064 kB
Inactive:        25140 kB
HighTotal:      131008 kB
HighFree:        71288 kB
LowTotal:       903652 kB
LowFree:        843836 kB
SwapTotal:     2097892 kB
SwapFree:      2096644 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            19680 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:13:10 (client local time) WITH STATUS 10 IN 1208.14 SECONDS
stats: 2714 7 1208.14 10

Solver Data

c Parsing PB file...
c Converting 94127 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 |   94127   188254 |   31375       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:70300     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  169206   364382 |   56402       0        0     nan |  0.000 % |
c |       100 |  168601   363114 |   62042      60      642    10.7 |  0.650 % |
c |       250 |  168197   362272 |   68246     188     1787     9.5 |  1.078 % |
c |       475 |  166779   359205 |   75071     353     5149    14.6 |  2.687 % |
c |       812 |  164849   355011 |   82578     614     8125    13.2 |  4.901 % |
c |      1318 |  161915   348511 |   90835    1007    11889    11.8 |  8.388 % |
c |      2078 |  157298   338163 |   99919    1514    19611    13.0 | 13.974 % |
c |      3217 |  150383   322519 |  109911    2361    27149    11.5 | 22.504 % |
c |      4925 |  142177   303723 |  120902    3455    43440    12.6 | 32.802 % |
c ==============================================================================
c Found solution: -39
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6002 |  136029   289832 |   45343    4064    51113    12.6 | 32.802 % |
c |      6102 |  135501   288616 |   49877    4094    51418    12.6 | 41.228 % |
c |      6252 |  134830   287062 |   54865    4169    52253    12.5 | 42.056 % |
c |      6477 |  133556   284073 |   60351    4284    53504    12.5 | 43.681 % |
c |      6815 |  131508   279252 |   66386    4352    53518    12.3 | 46.324 % |
c |      7321 |  129404   274330 |   73025    4686    58304    12.4 | 49.004 % |
c |      8080 |  124550   262767 |   80327    5020    62499    12.4 | 55.415 % |
c |      9219 |  120847   253969 |   88360    5639    70773    12.6 | 60.316 % |
c |     10927 |  116439   243527 |   97196    6740    85038    12.6 | 66.140 % |
c |     13489 |  111872   232610 |  106916    8109   102853    12.7 | 72.176 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15449 |  108663   224875 |   36221    9239   125727    13.6 | 72.176 % |
c |     15549 |  108599   224717 |   39843    9321   126476    13.6 | 76.650 % |
c |     15699 |  108565   224641 |   43827    9450   128114    13.6 | 76.691 % |
c |     15924 |  107849   222933 |   48210    9505   128963    13.6 | 77.658 % |
c |     16261 |  107296   221602 |   53031    9592   132052    13.8 | 78.413 % |
c |     16767 |  107016   220928 |   58334   10007   142853    14.3 | 78.791 % |
c |     17527 |  106385   219426 |   64167   10577   155481    14.7 | 79.638 % |
c |     18668 |  105298   216803 |   70584   11375   176705    15.5 | 81.105 % |
c |     20376 |  104074   213784 |   77642   12323   199977    16.2 | 82.788 % |
c |     22938 |  103716   212925 |   85407   14593   321534    22.0 | 83.276 % |
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 |     24986 |  102854   210754 |   34284   15664   393625    25.1 | 83.276 % |
c |     25086 |  102732   210450 |   37712   15436   390882    25.3 | 84.654 % |
c |     25236 |  102684   210340 |   41483   15542   394868    25.4 | 84.714 % |
c |     25461 |  102641   210233 |   45632   15714   406285    25.9 | 84.776 % |
c |     25798 |  102629   210201 |   50195   16042   422226    26.3 | 84.796 % |
c |     26304 |  102576   210078 |   55214   16509   466638    28.3 | 84.864 % |
c |     27063 |  102576   210078 |   60736   17268   503954    29.2 | 84.864 % |
c |     28202 |  102576   210078 |   66809   18407   593877    32.3 | 84.864 % |
c |     29911 |  102443   209761 |   73490   20018   684978    34.2 | 85.044 % |
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 |     31856 |  102356   209564 |   34118   21852   815129    37.3 | 85.044 % |
c |     31956 |  102268   209345 |   37529   21860   814537    37.3 | 85.339 % |
c |     32106 |  102228   209247 |   41282   21838   815492    37.3 | 85.394 % |
c |     32333 |  102223   209236 |   45411   22016   831326    37.8 | 85.400 % |
c |     32671 |  102209   209200 |   49952   22306   856533    38.4 | 85.421 % |
c |     33177 |  102197   209172 |   54947   22741   873272    38.4 | 85.437 % |
c |     33937 |  102094   208924 |   60442   23330   930681    39.9 | 85.575 % |
c |     35077 |  102019   208744 |   66486   24242   985516    40.7 | 85.676 % |
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 |     35607 |  102009   208691 |   34003   24540   995539    40.6 | 85.676 % |
c |     35708 |  101928   208492 |   37403   24624   997833    40.5 | 85.803 % |
c |     35858 |  101928   208492 |   41143   24774  1006585    40.6 | 85.803 % |
c |     36083 |  101928   208492 |   45257   24999  1014501    40.6 | 85.803 % |
c |     36420 |  101784   208131 |   49783   24930  1033808    41.5 | 86.003 % |
c |     36928 |  101784   208131 |   54762   25438  1056708    41.5 | 86.003 % |
c |     37689 |  101770   208097 |   60238   26110  1110764    42.5 | 86.023 % |
c |     38828 |  101692   207908 |   66262   27180  1189071    43.7 | 86.128 % |
c |     40536 |  101664   207836 |   72888   28873  1410165    48.8 | 86.171 % |
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 |     40771 |  101685   207899 |   33895   29108  1431870    49.2 | 86.171 % |
c |     40871 |  101599   207692 |   37284   29151  1433947    49.2 | 86.268 % |
c |     41022 |  101583   207656 |   41012   29204  1437736    49.2 | 86.288 % |
c |     41247 |  101583   207656 |   45114   29429  1451214    49.3 | 86.288 % |
c |     41585 |  101579   207646 |   49625   29759  1468341    49.3 | 86.294 % |
c |     42091 |  101579   207646 |   54588   30265  1514920    50.1 | 86.294 % |
c |     42850 |  101579   207646 |   60047   31024  1566731    50.5 | 86.294 % |
c |     43989 |  101522   207517 |   66051   32004  1690247    52.8 | 86.364 % |
c |     45697 |  101519   207510 |   72656   33657  1837966    54.6 | 86.368 % |
c |     48259 |  101514   207497 |   79922   36156  2069775    57.2 | 86.375 % |
c |     52103 |  101425   207284 |   87914   39754  2565923    64.5 | 86.496 % |
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 |     56071 |  101328   207015 |   33776   42986  3027810    70.4 | 86.496 % |
c |     56171 |  101160   206601 |   37153   42581  3019786    70.9 | 86.866 % |
c |     56322 |  101122   206513 |   40868   42554  3024513    71.1 | 86.915 % |
c |     56547 |  101122   206513 |   44955   42779  3039749    71.1 | 86.915 % |
c |     56886 |  101122   206513 |   49451   43118  3064538    71.1 | 86.915 % |
c |     57392 |  101122   206513 |   54396   43624  3101898    71.1 | 86.915 % |
c |     58152 |  101122   206513 |   59836   44384  3194510    72.0 | 86.915 % |
c |     59291 |  101046   206333 |   65819   45208  3294689    72.9 | 87.014 % |
c |     60999 |  101046   206333 |   72401   46916  3533061    75.3 | 87.014 % |
c |     63561 |  101046   206333 |   79642   49478  3883031    78.5 | 87.014 % |
c |     67406 |  100914   205999 |   87606   53044  4385925    82.7 | 87.206 % |
c |     73172 |  100806   205737 |   96366   58558  5046095    86.2 | 87.354 % |
c |     81821 |  100711   205504 |  106003   67011  6093036    90.9 | 87.486 % |
c |     94795 |  100700   205477 |  116603   79939  7520194    94.1 | 87.502 % |
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 |    105865 |  100598   205249 |   33532   90227  8874178    98.4 | 87.502 % |
c |    105965 |  100593   205238 |   36885   20901  1600986    76.6 | 87.670 % |
c |    106117 |  100593   205238 |   40573   21053  1614859    76.7 | 87.670 % |
c |    106344 |  100593   205238 |   44631   21280  1631167    76.7 | 87.670 % |
c |    106681 |  100593   205238 |   49094   21617  1672760    77.4 | 87.670 % |
c |    107187 |  100593   205238 |   54003   22123  1718568    77.7 | 87.670 % |
c |    107946 |  100593   205238 |   59403   22882  1790790    78.3 | 87.670 % |
c |    109085 |  100552   205131 |   65344   23996  1881654    78.4 | 87.734 % |
c |    110794 |  100507   205018 |   71878   25649  2041000    79.6 | 87.798 % |
c |    113356 |  100507   205018 |   79066   28211  2385755    84.6 | 87.798 % |
c |    117201 |  100363   204678 |   86973   31966  2747854    86.0 | 87.983 % |
c |    122969 |  100363   204678 |   95670   37734  3327649    88.2 | 87.983 % |
c |    131618 |  100361   204672 |  105237   46377  4057930    87.5 | 87.986 % |
c |    144592 |  100361   204672 |  115761   59351  5417520    91.3 | 87.986 % |
c |    164053 |  100361   204672 |  127337   78812  7374147    93.6 | 87.986 % |
c ==============================================================================
c Found solution: -48
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    180700 |  100336   204592 |   33445   95355  9046564    94.9 | 87.986 % |
c |    180800 |  100336   204592 |   36789   20047  1291344    64.4 | 88.022 % |
c |    180953 |  100336   204592 |   40468   20200  1303202    64.5 | 88.022 % |
c |    181179 |  100336   204592 |   44515   20426  1316828    64.5 | 88.022 % |
c |    181517 |  100336   204592 |   48966   20764  1335170    64.3 | 88.022 % |
c |    182023 |  100336   204592 |   53863   21270  1379477    64.9 | 88.022 % |
c |    182782 |  100336   204592 |   59249   22029  1465852    66.5 | 88.022 % |
c |    183921 |  100336   204592 |   65174   23168  1572637    67.9 | 88.022 % |
c |    185630 |  100336   204592 |   71692   24877  1715016    68.9 | 88.022 % |
c |    188194 |  100315   204537 |   78861   27433  1979748    72.2 | 88.055 % |
c |    192038 |  100261   204411 |   86747   31274  2434565    77.8 | 88.125 % |
c |    197805 |  100261   204411 |   95422   37041  2947613    79.6 | 88.125 % |
c |    206454 |  100261   204411 |  104964   45690  3968544    86.9 | 88.125 % |
c |    219428 |  100230   204344 |  115461   58628  5032265    85.8 | 88.160 % |
c |    238890 |  100163   204183 |  127007   78084  6825521    87.4 | 88.251 % |
c |    268082 |  100162   204180 |  139708  107224 10345801    96.5 | 88.253 % |
c |    311871 |  100159   204173 |  153678  151012 13666617    90.5 | 88.257 % |
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 -C

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/26127/stat): 26127 (minisat+_script) R 26126 26127 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843564313 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26127/statm): 174 3 169 147 0 27 0
[pid=26127] 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=26128
New process pid=26129
New process pid=26130
execve syscall for /bin/sed executable
One traced child (pid=26129) 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=26130) exited with status: 0
One traced child (pid=26128) exited with status: 0
New process pid=26131
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-frb53-24-3.opb

[startup+10.0029 s]
Raw data (loadavg): 0.93 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 5914 0 0 0 951 26 0 0 25 0 1 0 1843564318 24997888 5901 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 6103 5901 145 145 0 5958 0
[pid=26131] vsize: 24412
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 26536

[startup+20.0047 s]
Raw data (loadavg): 0.94 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 5914 0 0 0 1951 26 0 0 25 0 1 0 1843564318 24997888 5901 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 6103 5901 145 145 0 5958 0
[pid=26131] vsize: 24412
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 26536

[startup+30.0053 s]
Raw data (loadavg): 0.95 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 5914 0 0 0 2950 27 0 0 25 0 1 0 1843564318 24997888 5901 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 6103 5901 145 145 0 5958 0
[pid=26131] vsize: 24412
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 26536

[startup+40.006 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 5914 0 0 0 3950 27 0 0 25 0 1 0 1843564318 24997888 5901 4294967295 134512640 135094434 3221224448 3221223108 134553475 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 6103 5901 145 145 0 5958 0
[pid=26131] vsize: 24412
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 26536

[startup+50.0077 s]
Raw data (loadavg): 0.96 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 5914 0 0 0 4950 27 0 0 25 0 1 0 1843564318 24997888 5901 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6103 5901 145 145 0 5958 0
[pid=26131] vsize: 24412
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 26536

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 5914 0 0 0 5951 27 0 0 25 0 1 0 1843564318 24997888 5901 4294967295 134512640 135094434 3221224448 3221223124 134553524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6103 5901 145 145 0 5958 0
[pid=26131] vsize: 24412
Current children cumulated CPU time (s) 59.78
Current children cumulated vsize (Kb) 26536

[startup+70.0091 s]
Raw data (loadavg): 0.97 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6028 0 0 0 6950 28 0 0 25 0 1 0 1843564318 25731072 6015 4294967295 134512640 135094434 3221224448 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6282 6015 145 145 0 6137 0
[pid=26131] vsize: 25128
Current children cumulated CPU time (s) 69.78
Current children cumulated vsize (Kb) 27252

[startup+80.0098 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6028 0 0 0 7950 28 0 0 25 0 1 0 1843564318 25731072 6015 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6282 6015 145 145 0 6137 0
[pid=26131] vsize: 25128
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 27252

[startup+90.0105 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6028 0 0 0 8950 28 0 0 25 0 1 0 1843564318 25731072 6015 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6282 6015 145 145 0 6137 0
[pid=26131] vsize: 25128
Current children cumulated CPU time (s) 89.78
Current children cumulated vsize (Kb) 27252

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6028 0 0 0 9950 28 0 0 25 0 1 0 1843564318 25731072 6015 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6282 6015 145 145 0 6137 0
[pid=26131] vsize: 25128
Current children cumulated CPU time (s) 99.78
Current children cumulated vsize (Kb) 27252

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6028 0 0 0 10950 28 0 0 25 0 1 0 1843564318 25731072 6015 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6282 6015 145 145 0 6137 0
[pid=26131] vsize: 25128
Current children cumulated CPU time (s) 109.78
Current children cumulated vsize (Kb) 27252

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6040 0 0 0 11950 28 0 0 25 0 1 0 1843564318 25772032 6027 4294967295 134512640 135094434 3221224448 3221223152 134559007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6292 6027 145 145 0 6147 0
[pid=26131] vsize: 25168
Current children cumulated CPU time (s) 119.78
Current children cumulated vsize (Kb) 27292

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6405 0 0 0 12945 31 0 0 25 0 1 0 1843564318 27119616 6341 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 6621 6341 145 145 0 6476 0
[pid=26131] vsize: 26484
Current children cumulated CPU time (s) 129.76
Current children cumulated vsize (Kb) 28608

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 6909 0 0 0 13937 35 0 0 25 0 1 0 1843564318 28954624 6795 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 7069 6795 145 145 0 6924 0
[pid=26131] vsize: 28276
Current children cumulated CPU time (s) 139.72
Current children cumulated vsize (Kb) 30400

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 7310 0 0 0 14930 38 0 0 25 0 1 0 1843564318 30371840 7145 4294967295 134512640 135094434 3221224448 3221223040 134557128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 7415 7145 145 145 0 7270 0
[pid=26131] vsize: 29660
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 31784

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 7841 0 0 0 15920 42 0 0 25 0 1 0 1843564318 32325632 7626 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 7892 7626 145 145 0 7747 0
[pid=26131] vsize: 31568
Current children cumulated CPU time (s) 159.62
Current children cumulated vsize (Kb) 33692

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 8332 0 0 0 16911 46 0 0 25 0 1 0 1843564318 34447360 8117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 8410 8117 145 145 0 8265 0
[pid=26131] vsize: 33640
Current children cumulated CPU time (s) 169.57
Current children cumulated vsize (Kb) 35764

[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 8856 0 0 0 17902 49 0 0 25 0 1 0 1843564318 36577280 8641 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 8930 8641 145 145 0 8785 0
[pid=26131] vsize: 35720
Current children cumulated CPU time (s) 179.51
Current children cumulated vsize (Kb) 37844

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 9434 0 0 0 18891 54 0 0 25 0 1 0 1843564318 38723584 9168 4294967295 134512640 135094434 3221224448 3221223108 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 9454 9168 145 145 0 9309 0
[pid=26131] vsize: 37816
Current children cumulated CPU time (s) 189.45
Current children cumulated vsize (Kb) 39940

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 9794 0 0 0 19884 57 0 0 25 0 1 0 1843564318 40189952 9528 4294967295 134512640 135094434 3221224448 3221223120 134555241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 9812 9528 145 145 0 9667 0
[pid=26131] vsize: 39248
Current children cumulated CPU time (s) 199.41
Current children cumulated vsize (Kb) 41372

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 10295 0 0 0 20873 62 0 0 25 0 1 0 1843564318 42225664 10029 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 10309 10029 145 145 0 10164 0
[pid=26131] vsize: 41236
Current children cumulated CPU time (s) 209.35
Current children cumulated vsize (Kb) 43360

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 10700 0 0 0 21865 65 0 0 25 0 1 0 1843564318 43872256 10434 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 10711 10434 145 145 0 10566 0
[pid=26131] vsize: 42844
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 44968

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 11176 0 0 0 22858 68 0 0 25 0 1 0 1843564318 45809664 10910 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 11184 10910 145 145 0 11039 0
[pid=26131] vsize: 44736
Current children cumulated CPU time (s) 229.26
Current children cumulated vsize (Kb) 46860

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 11539 0 0 0 23851 71 0 0 25 0 1 0 1843564318 47284224 11273 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 11544 11273 145 145 0 11399 0
[pid=26131] vsize: 46176
Current children cumulated CPU time (s) 239.22
Current children cumulated vsize (Kb) 48300

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 11945 0 0 0 24844 74 0 0 25 0 1 0 1843564318 48934912 11679 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 11947 11679 145 145 0 11802 0
[pid=26131] vsize: 47788
Current children cumulated CPU time (s) 249.18
Current children cumulated vsize (Kb) 49912

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 12299 0 0 0 25837 77 0 0 25 0 1 0 1843564318 50376704 12033 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 12299 12033 145 145 0 12154 0
[pid=26131] vsize: 49196
Current children cumulated CPU time (s) 259.14
Current children cumulated vsize (Kb) 51320

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 12673 0 0 0 26830 81 0 0 25 0 1 0 1843564318 52158464 12407 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 12734 12407 145 145 0 12589 0
[pid=26131] vsize: 50936
Current children cumulated CPU time (s) 269.11
Current children cumulated vsize (Kb) 53060

[startup+280.023 s]
Raw data (loadavg): 1.07 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 13038 0 0 0 27824 84 0 0 25 0 1 0 1843564318 53641216 12772 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 13096 12772 145 145 0 12951 0
[pid=26131] vsize: 52384
Current children cumulated CPU time (s) 279.08
Current children cumulated vsize (Kb) 54508

[startup+290.024 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 13351 0 0 0 28818 87 0 0 25 0 1 0 1843564318 54910976 13085 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 13406 13085 145 145 0 13261 0
[pid=26131] vsize: 53624
Current children cumulated CPU time (s) 289.05
Current children cumulated vsize (Kb) 55748

[startup+300.025 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 13618 0 0 0 29812 90 0 0 25 0 1 0 1843564318 55996416 13352 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 13671 13352 145 145 0 13526 0
[pid=26131] vsize: 54684
Current children cumulated CPU time (s) 299.02
Current children cumulated vsize (Kb) 56808

[startup+310.025 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 13883 0 0 0 30806 92 0 0 25 0 1 0 1843564318 57073664 13617 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 13934 13617 145 145 0 13789 0
[pid=26131] vsize: 55736
Current children cumulated CPU time (s) 308.98
Current children cumulated vsize (Kb) 57860

[startup+320.026 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 14144 0 0 0 31801 94 0 0 25 0 1 0 1843564318 58134528 13878 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 14193 13878 145 145 0 14048 0
[pid=26131] vsize: 56772
Current children cumulated CPU time (s) 318.95
Current children cumulated vsize (Kb) 58896

[startup+330.026 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 14445 0 0 0 32795 97 0 0 25 0 1 0 1843564318 59355136 14179 4294967295 134512640 135094434 3221224448 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 14491 14179 145 145 0 14346 0
[pid=26131] vsize: 57964
Current children cumulated CPU time (s) 328.92
Current children cumulated vsize (Kb) 60088

[startup+340.027 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 14723 0 0 0 33789 99 0 0 25 0 1 0 1843564318 60485632 14457 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 14767 14457 145 145 0 14622 0
[pid=26131] vsize: 59068
Current children cumulated CPU time (s) 338.88
Current children cumulated vsize (Kb) 61192

[startup+350.028 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15055 0 0 0 34783 101 0 0 25 0 1 0 1843564318 61837312 14789 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15097 14789 145 145 0 14952 0
[pid=26131] vsize: 60388
Current children cumulated CPU time (s) 348.84
Current children cumulated vsize (Kb) 62512

[startup+360.028 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15372 0 0 0 35777 103 0 0 25 0 1 0 1843564318 63127552 15106 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 15412 15106 145 145 0 15267 0
[pid=26131] vsize: 61648
Current children cumulated CPU time (s) 358.8
Current children cumulated vsize (Kb) 63772

[startup+370.029 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 36770 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 368.77
Current children cumulated vsize (Kb) 64792

[startup+380.03 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 37770 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 378.77
Current children cumulated vsize (Kb) 64792

[startup+390.03 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 38770 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 388.77
Current children cumulated vsize (Kb) 64792

[startup+400.031 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 39770 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 64792

[startup+410.032 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 40771 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 408.78
Current children cumulated vsize (Kb) 64792

[startup+420.032 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 41771 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 418.78
Current children cumulated vsize (Kb) 64792

[startup+430.033 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 42771 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 428.78
Current children cumulated vsize (Kb) 64792

[startup+440.034 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 43771 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 438.78
Current children cumulated vsize (Kb) 64792

[startup+450.035 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 44771 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 448.78
Current children cumulated vsize (Kb) 64792

[startup+460.034 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 45772 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 458.79
Current children cumulated vsize (Kb) 64792

[startup+470.036 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 46772 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 468.79
Current children cumulated vsize (Kb) 64792

[startup+480.037 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 47772 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 478.79
Current children cumulated vsize (Kb) 64792

[startup+490.037 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 48772 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 488.79
Current children cumulated vsize (Kb) 64792

[startup+500.038 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 49773 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 498.8
Current children cumulated vsize (Kb) 64792

[startup+510.039 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 50773 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 508.8
Current children cumulated vsize (Kb) 64792

[startup+520.039 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 51773 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 518.8
Current children cumulated vsize (Kb) 64792

[startup+530.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 52773 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 528.8
Current children cumulated vsize (Kb) 64792

[startup+540.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 53773 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 538.8
Current children cumulated vsize (Kb) 64792

[startup+550.043 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 54774 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 548.81
Current children cumulated vsize (Kb) 64792

[startup+560.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 55774 107 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 558.81
Current children cumulated vsize (Kb) 64792

[startup+570.044 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 56774 108 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221222992 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 568.82
Current children cumulated vsize (Kb) 64792

[startup+580.045 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 15680 0 0 0 57774 108 0 0 25 0 1 0 1843564318 64172032 15363 4294967295 134512640 135094434 3221224448 3221223040 134557143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 15667 15363 145 145 0 15522 0
[pid=26131] vsize: 62668
Current children cumulated CPU time (s) 578.82
Current children cumulated vsize (Kb) 64792

[startup+590.045 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16018 0 0 0 58769 110 0 0 25 0 1 0 1843564318 65544192 15701 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16002 15701 145 145 0 15857 0
[pid=26131] vsize: 64008
Current children cumulated CPU time (s) 588.79
Current children cumulated vsize (Kb) 66132

[startup+600.046 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 59766 111 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223060 134563094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 598.77
Current children cumulated vsize (Kb) 66736

[startup+610.047 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 60766 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 608.78
Current children cumulated vsize (Kb) 66736

[startup+620.047 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 61766 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 618.78
Current children cumulated vsize (Kb) 66736

[startup+630.048 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 62766 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 628.78
Current children cumulated vsize (Kb) 66736

[startup+640.05 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 63766 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 638.78
Current children cumulated vsize (Kb) 66736

[startup+650.051 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 64767 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 648.79
Current children cumulated vsize (Kb) 66736

[startup+660.051 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 65767 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223072 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 658.79
Current children cumulated vsize (Kb) 66736

[startup+670.052 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 66767 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 668.79
Current children cumulated vsize (Kb) 66736

[startup+680.053 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 67767 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223024 134552441 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 678.79
Current children cumulated vsize (Kb) 66736

[startup+690.054 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 68767 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 688.79
Current children cumulated vsize (Kb) 66736

[startup+700.055 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 69767 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 698.79
Current children cumulated vsize (Kb) 66736

[startup+710.056 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 70768 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 708.8
Current children cumulated vsize (Kb) 66736

[startup+720.056 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 71768 112 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 718.8
Current children cumulated vsize (Kb) 66736

[startup+730.057 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 72768 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223040 134785278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 728.81
Current children cumulated vsize (Kb) 66736

[startup+740.058 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 73768 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223040 134557302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 738.81
Current children cumulated vsize (Kb) 66736

[startup+750.058 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 74769 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 748.82
Current children cumulated vsize (Kb) 66736

[startup+760.059 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 75769 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 758.82
Current children cumulated vsize (Kb) 66736

[startup+770.06 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 76769 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 768.82
Current children cumulated vsize (Kb) 66736

[startup+780.061 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 77769 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223040 134557256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 778.82
Current children cumulated vsize (Kb) 66736

[startup+790.061 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 78769 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 788.82
Current children cumulated vsize (Kb) 66736

[startup+800.062 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 79770 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 798.83
Current children cumulated vsize (Kb) 66736

[startup+810.063 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16222 0 0 0 80770 113 0 0 25 0 1 0 1843564318 66162688 15854 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16153 15854 145 145 0 16008 0
[pid=26131] vsize: 64612
Current children cumulated CPU time (s) 808.83
Current children cumulated vsize (Kb) 66736

[startup+820.064 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16283 0 0 0 81769 113 0 0 25 0 1 0 1843564318 66404352 15915 4294967295 134512640 135094434 3221224448 3221223072 134557614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16212 15915 145 145 0 16067 0
[pid=26131] vsize: 64848
Current children cumulated CPU time (s) 818.82
Current children cumulated vsize (Kb) 66972

[startup+830.065 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16574 0 0 0 82764 115 0 0 25 0 1 0 1843564318 67592192 16206 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 16502 16206 145 145 0 16357 0
[pid=26131] vsize: 66008
Current children cumulated CPU time (s) 828.79
Current children cumulated vsize (Kb) 68132

[startup+840.066 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 16884 0 0 0 83758 117 0 0 25 0 1 0 1843564318 68853760 16516 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26131/statm): 16810 16516 145 145 0 16665 0
[pid=26131] vsize: 67240
Current children cumulated CPU time (s) 838.75
Current children cumulated vsize (Kb) 69364

[startup+850.067 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 17209 0 0 0 84752 120 0 0 25 0 1 0 1843564318 70176768 16841 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 17133 16841 145 145 0 16988 0
[pid=26131] vsize: 68532
Current children cumulated CPU time (s) 848.72
Current children cumulated vsize (Kb) 70656

[startup+860.067 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 17517 0 0 0 85747 122 0 0 25 0 1 0 1843564318 71434240 17149 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 17440 17149 145 145 0 17295 0
[pid=26131] vsize: 69760
Current children cumulated CPU time (s) 858.69
Current children cumulated vsize (Kb) 71884

[startup+870.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 17790 0 0 0 86740 125 0 0 25 0 1 0 1843564318 72540160 17422 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 17710 17422 145 145 0 17565 0
[pid=26131] vsize: 70840
Current children cumulated CPU time (s) 868.65
Current children cumulated vsize (Kb) 72964

[startup+880.068 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 18049 0 0 0 87736 127 0 0 25 0 1 0 1843564318 73584640 17681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 17965 17681 145 145 0 17820 0
[pid=26131] vsize: 71860
Current children cumulated CPU time (s) 878.63
Current children cumulated vsize (Kb) 73984

[startup+890.069 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 18273 0 0 0 88731 128 0 0 25 0 1 0 1843564318 74493952 17905 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 18187 17905 145 145 0 18042 0
[pid=26131] vsize: 72748
Current children cumulated CPU time (s) 888.59
Current children cumulated vsize (Kb) 74872

[startup+900.07 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 18487 0 0 0 89727 130 0 0 25 0 1 0 1843564318 75358208 18119 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 18398 18119 145 145 0 18253 0
[pid=26131] vsize: 73592
Current children cumulated CPU time (s) 898.57
Current children cumulated vsize (Kb) 75716

[startup+910.071 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 18697 0 0 0 90723 131 0 0 25 0 1 0 1843564318 76210176 18329 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 18606 18329 145 145 0 18461 0
[pid=26131] vsize: 74424
Current children cumulated CPU time (s) 908.54
Current children cumulated vsize (Kb) 76548

[startup+920.071 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 18886 0 0 0 91720 132 0 0 25 0 1 0 1843564318 76976128 18518 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 18793 18518 145 145 0 18648 0
[pid=26131] vsize: 75172
Current children cumulated CPU time (s) 918.52
Current children cumulated vsize (Kb) 77296

[startup+930.072 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 19085 0 0 0 92716 134 0 0 25 0 1 0 1843564318 77795328 18717 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 18993 18717 145 145 0 18848 0
[pid=26131] vsize: 75972
Current children cumulated CPU time (s) 928.5
Current children cumulated vsize (Kb) 78096

[startup+940.073 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 19281 0 0 0 93713 135 0 0 25 0 1 0 1843564318 78598144 18913 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 19189 18913 145 145 0 19044 0
[pid=26131] vsize: 76756
Current children cumulated CPU time (s) 938.48
Current children cumulated vsize (Kb) 78880

[startup+950.073 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 19440 0 0 0 94710 136 0 0 25 0 1 0 1843564318 79253504 19072 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 19349 19072 145 145 0 19204 0
[pid=26131] vsize: 77396
Current children cumulated CPU time (s) 948.46
Current children cumulated vsize (Kb) 79520

[startup+960.074 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 19603 0 0 0 95706 138 0 0 25 0 1 0 1843564318 79908864 19235 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 19509 19235 145 145 0 19364 0
[pid=26131] vsize: 78036
Current children cumulated CPU time (s) 958.44
Current children cumulated vsize (Kb) 80160

[startup+970.075 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 19804 0 0 0 96703 139 0 0 25 0 1 0 1843564318 81248256 19436 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 19836 19436 145 145 0 19691 0
[pid=26131] vsize: 79344
Current children cumulated CPU time (s) 968.42
Current children cumulated vsize (Kb) 81468

[startup+980.075 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 19983 0 0 0 97700 140 0 0 25 0 1 0 1843564318 81973248 19615 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20013 19615 145 145 0 19868 0
[pid=26131] vsize: 80052
Current children cumulated CPU time (s) 978.4
Current children cumulated vsize (Kb) 82176

[startup+990.077 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 20145 0 0 0 98698 142 0 0 25 0 1 0 1843564318 82628608 19777 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20173 19777 145 145 0 20028 0
[pid=26131] vsize: 80692
Current children cumulated CPU time (s) 988.4
Current children cumulated vsize (Kb) 82816

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 20296 0 0 0 99695 143 0 0 25 0 1 0 1843564318 83238912 19928 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20322 19928 145 145 0 20177 0
[pid=26131] vsize: 81288
Current children cumulated CPU time (s) 998.38
Current children cumulated vsize (Kb) 83412

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.96 1/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) T 26127 26127 20728 0 -1 0 20467 0 0 0 100692 143 0 0 25 0 1 0 1843564318 83931136 20099 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20491 20099 145 145 0 20346 0
[pid=26131] vsize: 81964
Current children cumulated CPU time (s) 1008.35
Current children cumulated vsize (Kb) 84088

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 20590 0 0 0 101690 144 0 0 25 0 1 0 1843564318 84426752 20222 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20612 20222 145 145 0 20467 0
[pid=26131] vsize: 82448
Current children cumulated CPU time (s) 1018.34
Current children cumulated vsize (Kb) 84572

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 20740 0 0 0 102688 145 0 0 25 0 1 0 1843564318 85032960 20372 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20760 20372 145 145 0 20615 0
[pid=26131] vsize: 83040
Current children cumulated CPU time (s) 1028.33
Current children cumulated vsize (Kb) 85164

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 20878 0 0 0 103686 146 0 0 25 0 1 0 1843564318 85594112 20510 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 20897 20510 145 145 0 20752 0
[pid=26131] vsize: 83588
Current children cumulated CPU time (s) 1038.32
Current children cumulated vsize (Kb) 85712

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21003 0 0 0 104684 147 0 0 25 0 1 0 1843564318 86102016 20635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21021 20635 145 145 0 20876 0
[pid=26131] vsize: 84084
Current children cumulated CPU time (s) 1048.31
Current children cumulated vsize (Kb) 86208

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21124 0 0 0 105682 148 0 0 25 0 1 0 1843564318 86589440 20756 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21140 20756 145 145 0 20995 0
[pid=26131] vsize: 84560
Current children cumulated CPU time (s) 1058.3
Current children cumulated vsize (Kb) 86684

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21236 0 0 0 106680 149 0 0 25 0 1 0 1843564318 87044096 20868 4294967295 134512640 135094434 3221224448 3221223120 134556460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21251 20868 145 145 0 21106 0
[pid=26131] vsize: 85004
Current children cumulated CPU time (s) 1068.29
Current children cumulated vsize (Kb) 87128

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21348 0 0 0 107678 150 0 0 25 0 1 0 1843564318 87490560 20980 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21360 20980 145 145 0 21215 0
[pid=26131] vsize: 85440
Current children cumulated CPU time (s) 1078.28
Current children cumulated vsize (Kb) 87564

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21451 0 0 0 108676 151 0 0 25 0 1 0 1843564318 87908352 21083 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21462 21083 145 145 0 21317 0
[pid=26131] vsize: 85848
Current children cumulated CPU time (s) 1088.27
Current children cumulated vsize (Kb) 87972

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21554 0 0 0 109675 152 0 0 25 0 1 0 1843564318 88322048 21186 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21563 21186 145 145 0 21418 0
[pid=26131] vsize: 86252
Current children cumulated CPU time (s) 1098.27
Current children cumulated vsize (Kb) 88376

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21648 0 0 0 110674 152 0 0 25 0 1 0 1843564318 88698880 21280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21655 21280 145 145 0 21510 0
[pid=26131] vsize: 86620
Current children cumulated CPU time (s) 1108.26
Current children cumulated vsize (Kb) 88744

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 21836 0 0 0 111670 153 0 0 25 0 1 0 1843564318 89489408 21468 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 21848 21468 145 145 0 21703 0
[pid=26131] vsize: 87392
Current children cumulated CPU time (s) 1118.23
Current children cumulated vsize (Kb) 89516

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 22017 0 0 0 112667 155 0 0 25 0 1 0 1843564318 90222592 21649 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 22027 21649 145 145 0 21882 0
[pid=26131] vsize: 88108
Current children cumulated CPU time (s) 1128.22
Current children cumulated vsize (Kb) 90232

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 22177 0 0 0 113664 156 0 0 25 0 1 0 1843564318 90869760 21809 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 22185 21809 145 145 0 22040 0
[pid=26131] vsize: 88740
Current children cumulated CPU time (s) 1138.2
Current children cumulated vsize (Kb) 90864

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 22367 0 0 0 114662 157 0 0 25 0 1 0 1843564318 91639808 21999 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 22373 21999 145 145 0 22228 0
[pid=26131] vsize: 89492
Current children cumulated CPU time (s) 1148.19
Current children cumulated vsize (Kb) 91616

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 22537 0 0 0 115658 158 0 0 25 0 1 0 1843564318 92327936 22169 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 22541 22169 145 145 0 22396 0
[pid=26131] vsize: 90164
Current children cumulated CPU time (s) 1158.16
Current children cumulated vsize (Kb) 92288

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 22711 0 0 0 116655 159 0 0 25 0 1 0 1843564318 93036544 22343 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 22714 22343 145 145 0 22569 0
[pid=26131] vsize: 90856
Current children cumulated CPU time (s) 1168.14
Current children cumulated vsize (Kb) 92980

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 22892 0 0 0 117653 161 0 0 25 0 1 0 1843564318 93777920 22524 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 22895 22524 145 145 0 22750 0
[pid=26131] vsize: 91580
Current children cumulated CPU time (s) 1178.14
Current children cumulated vsize (Kb) 93704

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 23084 0 0 0 118650 162 0 0 25 0 1 0 1843564318 94556160 22716 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 23085 22716 145 145 0 22940 0
[pid=26131] vsize: 92340
Current children cumulated CPU time (s) 1188.12
Current children cumulated vsize (Kb) 94464

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 23275 0 0 0 119647 164 0 0 25 0 1 0 1843564318 95342592 22907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 23277 22907 145 145 0 23132 0
[pid=26131] vsize: 93108
Current children cumulated CPU time (s) 1198.11
Current children cumulated vsize (Kb) 95232

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 23462 0 0 0 120644 165 0 0 25 0 1 0 1843564318 96108544 23094 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 23464 23094 145 145 0 23319 0
[pid=26131] vsize: 93856
Current children cumulated CPU time (s) 1208.09
Current children cumulated vsize (Kb) 95980



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 26131
Raw data (/proc/26127/stat): 26127 (minisat+_script) S 26126 26127 20728 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843564313 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26127/statm): 531 226 485 147 0 384 0
[pid=26127] vsize: 2124
Raw data (/proc/26131/stat): 26131 (minisat+_64-bit) R 26127 26127 20728 0 -1 0 23462 0 0 0 120644 165 0 0 25 0 1 0 1843564318 96108544 23094 4294967295 134512640 135094434 3221224448 3221223008 134550333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26131/statm): 23464 23094 145 145 0 23319 0
[pid=26131] vsize: 93856
Current children cumulated CPU time (s) 1208.09
Current children cumulated vsize (Kb) 95980

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1208.14
CPU user time (s): 1206.45
CPU system time (s): 1.69574
CPU usage (%): 99.8339
Max. virtual memory (cumulated for all children) (Kb): 95980

Verifier Data

ERROR: no interpretation found !