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/frb45-21-opb/normalized-frb45-21-2.opb
MD5SUMa931f7e9a55cb6836807387327525e8b
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -36
Optimality of the best value was proved NO
Number of terms in the objective function 945
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 945
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 945
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.04
Number of variables945
Total number of constraints58624
Number of constraints which are clauses58624
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 2295

Launcher Data

LAUNCH ON wulflinc7 THE 2005-09-18 18:45:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2701 boxname=wulflinc7 idbench=357 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a931f7e9a55cb6836807387327525e8b  /oldhome/oroussel/tmp/wulflinc7/normalized-frb45-21-2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-frb45-21-2.opb
IDLAUNCH: 2701
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        913840 kB
Buffers:         35624 kB
Cached:          60536 kB
SwapCached:        740 kB
Active:          70156 kB
Inactive:        28616 kB
HighTotal:      131008 kB
HighFree:        68320 kB
LowTotal:       903652 kB
LowFree:        845520 kB
SwapTotal:     2097136 kB
SwapFree:      2095892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            16324 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:05:35 (client local time) WITH STATUS 10 IN 1208.32 SECONDS
stats: 2701 7 1208.32 10

Solver Data

c Parsing PB file...
c Converting 58624 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 |   58624   117248 |   19541       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  104213   224311 |   34737       0        0     nan |  0.000 % |
c |       100 |  103753   223355 |   38210      63      352     5.6 |  0.799 % |
c |       250 |  103075   221899 |   42031     184     1699     9.2 |  2.046 % |
c |       475 |  101685   218869 |   46234     359     3428     9.5 |  4.676 % |
c |       813 |   99941   215027 |   50858     624     5935     9.5 |  8.041 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1145 |   98367   211607 |   32789     875     9453    10.8 |  8.041 % |
c |      1246 |   97670   210062 |   36067     936    10041    10.7 | 12.509 % |
c |      1396 |   97202   209006 |   39674    1031    10925    10.6 | 13.452 % |
c |      1621 |   95987   206277 |   43642    1161    12048    10.4 | 15.877 % |
c |      1958 |   94801   203593 |   48006    1411    15086    10.7 | 18.255 % |
c |      2464 |   92142   197582 |   52807    1692    17509    10.3 | 23.612 % |
c |      3223 |   89622   191786 |   58087    2260    23288    10.3 | 28.835 % |
c |      4362 |   85515   182365 |   63896    3094    31899    10.3 | 37.082 % |
c |      6070 |   81641   173405 |   70286    4400    47324    10.8 | 45.054 % |
c |      8632 |   76140   160465 |   77314    6222    77175    12.4 | 56.811 % |
c |     12476 |   71881   150330 |   85046    9255   155440    16.8 | 66.013 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14307 |   70810   147891 |   23603   10753   201061    18.7 | 66.013 % |
c |     14407 |   70765   147784 |   25963   10841   202522    18.7 | 68.509 % |
c |     14557 |   70765   147784 |   28559   10991   207402    18.9 | 68.509 % |
c |     14783 |   70691   147602 |   31415   11185   216078    19.3 | 68.675 % |
c |     15120 |   70586   147358 |   34557   11507   227319    19.8 | 68.886 % |
c |     15626 |   70348   146787 |   38012   11951   241938    20.2 | 69.400 % |
c |     16385 |   70089   146154 |   41814   12648   271863    21.5 | 69.975 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16815 |   69891   145672 |   23297   13020   282802    21.7 | 69.975 % |
c |     16915 |   69891   145672 |   25626   13120   284893    21.7 | 70.395 % |
c |     17065 |   69891   145672 |   28189   13270   286399    21.6 | 70.395 % |
c |     17290 |   69827   145517 |   31008   13475   295467    21.9 | 70.532 % |
c |     17627 |   69734   145292 |   34109   13799   310942    22.5 | 70.743 % |
c |     18133 |   69371   144409 |   37520   14192   322561    22.7 | 71.538 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18277 |   69362   144430 |   23120   14335   325818    22.7 | 71.538 % |
c |     18377 |   69362   144430 |   25432   14435   332585    23.0 | 71.584 % |
c |     18527 |   69277   144233 |   27975   14556   347362    23.9 | 71.763 % |
c |     18752 |   69277   144233 |   30772   14781   367844    24.9 | 71.763 % |
c |     19089 |   69030   143626 |   33849   14950   374080    25.0 | 72.327 % |
c |     19596 |   68741   142905 |   37234   15398   392392    25.5 | 73.016 % |
c |     20355 |   68660   142718 |   40958   16081   432831    26.9 | 73.185 % |
c |     21494 |   68513   142365 |   45054   17165   509426    29.7 | 73.511 % |
c |     23202 |   68154   141510 |   49559   18653   641562    34.4 | 74.298 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23824 |   67852   140729 |   22617   19046   663777    34.9 | 74.298 % |
c |     23924 |   67766   140515 |   24878   19123   665280    34.8 | 75.183 % |
c |     24074 |   67714   140393 |   27366   19252   669804    34.8 | 75.292 % |
c |     24299 |   67714   140393 |   30103   19477   677322    34.8 | 75.292 % |
c |     24636 |   67714   140393 |   33113   19814   696585    35.2 | 75.292 % |
c |     25142 |   67678   140303 |   36424   20309   716491    35.3 | 75.375 % |
c |     25902 |   67425   139703 |   40067   20929   797034    38.1 | 75.917 % |
c |     27042 |   67212   139192 |   44074   21947   872312    39.7 | 76.383 % |
c |     28750 |   67142   139014 |   48481   23609  1034815    43.8 | 76.548 % |
c |     31312 |   67092   138893 |   53329   26102  1245314    47.7 | 76.657 % |
c |     35156 |   66477   137377 |   58662   29648  1507713    50.9 | 78.057 % |
c |     40922 |   66357   137092 |   64528   35234  2003265    56.9 | 78.315 % |
c |     49572 |   66165   136632 |   70981   43618  2849495    65.3 | 78.733 % |
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 |     53102 |   66131   136585 |   22043   46964  3239093    69.0 | 78.733 % |
c |     53203 |   66092   136494 |   24247   19870  1267667    63.8 | 78.977 % |
c |     53353 |   66092   136494 |   26672   20020  1277625    63.8 | 78.977 % |
c |     53578 |   66092   136494 |   29339   20245  1297647    64.1 | 78.977 % |
c |     53917 |   66083   136473 |   32273   20580  1329003    64.6 | 78.996 % |
c |     54424 |   66083   136473 |   35500   21087  1371465    65.0 | 78.996 % |
c |     55183 |   66081   136469 |   39050   21844  1449488    66.4 | 78.999 % |
c |     56322 |   66081   136469 |   42955   22983  1576964    68.6 | 78.999 % |
c |     58030 |   66081   136469 |   47251   24691  1727745    70.0 | 78.999 % |
c |     60592 |   65903   136032 |   51976   27218  1994366    73.3 | 79.390 % |
c |     64436 |   65748   135667 |   57173   31008  2368011    76.4 | 79.714 % |
c |     70202 |   65748   135667 |   62891   36774  3054028    83.0 | 79.714 % |
c |     78851 |   65630   135370 |   69180   45415  4281369    94.3 | 79.987 % |
c |     91825 |   65630   135370 |   76098   58389  6085540   104.2 | 79.987 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97446 |   65617   135317 |   21872   63942  6734885   105.3 | 79.987 % |
c |     97546 |   65521   135083 |   24059   19913  1776166    89.2 | 80.240 % |
c |     97696 |   65511   135059 |   26465   20062  1785837    89.0 | 80.262 % |
c |     97921 |   65485   134999 |   29111   20286  1798820    88.7 | 80.316 % |
c |     98258 |   65485   134999 |   32022   20623  1818617    88.2 | 80.316 % |
c |     98765 |   65485   134999 |   35225   21130  1863451    88.2 | 80.316 % |
c |     99525 |   65485   134999 |   38747   21890  1943719    88.8 | 80.316 % |
c |    100667 |   65432   134870 |   42622   23023  2052223    89.1 | 80.433 % |
c |    102376 |   65237   134387 |   46884   24634  2215179    89.9 | 80.881 % |
c |    104938 |   65233   134377 |   51573   27193  2439838    89.7 | 80.891 % |
c |    108784 |   65114   134084 |   56730   31017  2904470    93.6 | 81.164 % |
c |    114550 |   64872   133502 |   62403   36617  3619951    98.9 | 81.689 % |
c |    123199 |   64872   133502 |   68643   45266  4649642   102.7 | 81.689 % |
c |    136175 |   64810   133346 |   75508   58227  6774965   116.4 | 81.838 % |
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 |    150026 |   64829   133402 |   21609   72073  8627626   119.7 | 81.838 % |
c |    150126 |   64829   133402 |   23769   20486  1739332    84.9 | 81.817 % |
c |    150276 |   64829   133402 |   26146   20636  1744519    84.5 | 81.817 % |
c |    150501 |   64829   133402 |   28761   20861  1763472    84.5 | 81.817 % |
c |    150839 |   64720   133135 |   31637   21184  1776192    83.8 | 82.068 % |
c |    151345 |   64720   133135 |   34801   21690  1809498    83.4 | 82.068 % |
c |    152104 |   64667   133003 |   38281   22431  1868161    83.3 | 82.192 % |
c |    153244 |   64576   132788 |   42109   23332  1921393    82.4 | 82.385 % |
c |    154952 |   64519   132644 |   46320   25032  2128460    85.0 | 82.515 % |
c |    157514 |   64514   132633 |   50952   27592  2413144    87.5 | 82.525 % |
c |    161359 |   64514   132633 |   56048   31437  2830357    90.0 | 82.525 % |
c |    167125 |   64508   132619 |   61652   37198  3592888    96.6 | 82.538 % |
c |    175774 |   64484   132559 |   67818   45837  4744404   103.5 | 82.595 % |
c |    188750 |   64443   132458 |   74600   58799  6135883   104.4 | 82.690 % |
c |    208211 |   64435   132438 |   82060   78258  8346917   106.7 | 82.709 % |
c |    237404 |   64428   132421 |   90266  107448 11304159   105.2 | 82.725 % |
c |    281193 |   64313   132144 |   99292   56003  5085663    90.8 | 82.979 % |
c |    346877 |   64154   131750 |  109222  121446 12746175   105.0 | 83.347 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 C883 -C882 -C881 -C880 C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C26

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/26083/stat): 26083 (minisat+_script) R 26082 26083 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785314588 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26083/statm): 174 3 169 147 0 27 0
[pid=26083] 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=26084
New process pid=26085
New process pid=26086
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=26085) exited with status: 0
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=26086) exited with status: 0
One traced child (pid=26084) exited with status: 0
New process pid=26087
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-frb45-21-2.opb

[startup+10.0027 s]
Raw data (loadavg): 1.08 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 964 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0
[pid=26087] vsize: 15296
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 17420

[startup+20.0034 s]
Raw data (loadavg): 1.07 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 1964 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0
[pid=26087] vsize: 15296
Current children cumulated CPU time (s) 19.83
Current children cumulated vsize (Kb) 17420

[startup+30.004 s]
Raw data (loadavg): 1.06 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 2963 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0
[pid=26087] vsize: 15296
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 17420

[startup+40.0056 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 3963 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0
[pid=26087] vsize: 15296
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 17420

[startup+50.0063 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) T 26083 26083 15400 0 -1 0 3763 0 0 0 4963 19 0 0 25 0 1 0 1785314593 15810560 3750 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26087/statm): 3860 3750 145 145 0 3715 0
[pid=26087] vsize: 15440
Current children cumulated CPU time (s) 49.82
Current children cumulated vsize (Kb) 17564

[startup+60.0069 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 4114 0 0 0 5957 22 0 0 25 0 1 0 1785314593 16732160 3980 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 4085 3980 145 145 0 3940 0
[pid=26087] vsize: 16340
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 18464

[startup+70.0086 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 4570 0 0 0 6950 25 0 0 25 0 1 0 1785314593 18481152 4396 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 4512 4396 145 145 0 4367 0
[pid=26087] vsize: 18048
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 20172

[startup+80.0092 s]
Raw data (loadavg): 1.09 1.03 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 5144 0 0 0 7939 30 0 0 25 0 1 0 1785314593 20811776 4970 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 5081 4970 145 145 0 4936 0
[pid=26087] vsize: 20324
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 22448

[startup+90.0098 s]
Raw data (loadavg): 1.07 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 5564 0 0 0 8932 32 0 0 25 0 1 0 1785314593 22511616 5390 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 5496 5390 145 145 0 5351 0
[pid=26087] vsize: 21984
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 24108

[startup+100.01 s]
Raw data (loadavg): 1.06 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 6067 0 0 0 9925 35 0 0 25 0 1 0 1785314593 24686592 5893 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 6027 5893 145 145 0 5882 0
[pid=26087] vsize: 24108
Current children cumulated CPU time (s) 99.6
Current children cumulated vsize (Kb) 26232

[startup+110.011 s]
Raw data (loadavg): 1.05 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 6552 0 0 0 10917 39 0 0 25 0 1 0 1785314593 26652672 6378 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 6507 6378 145 145 0 6362 0
[pid=26087] vsize: 26028
Current children cumulated CPU time (s) 109.56
Current children cumulated vsize (Kb) 28152

[startup+120.013 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7076 0 0 0 11907 42 0 0 25 0 1 0 1785314593 28782592 6902 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 7027 6902 145 145 0 6882 0
[pid=26087] vsize: 28108
Current children cumulated CPU time (s) 119.49
Current children cumulated vsize (Kb) 30232

[startup+130.013 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7414 0 0 0 12901 45 0 0 25 0 1 0 1785314593 29990912 7199 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 7322 7199 145 145 0 7177 0
[pid=26087] vsize: 29288
Current children cumulated CPU time (s) 129.46
Current children cumulated vsize (Kb) 31412

[startup+140.014 s]
Raw data (loadavg): 1.03 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7414 0 0 0 13902 45 0 0 25 0 1 0 1785314593 29990912 7199 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 7322 7199 145 145 0 7177 0
[pid=26087] vsize: 29288
Current children cumulated CPU time (s) 139.47
Current children cumulated vsize (Kb) 31412

[startup+150.016 s]
Raw data (loadavg): 1.03 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7414 0 0 0 14902 45 0 0 25 0 1 0 1785314593 29990912 7199 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 7322 7199 145 145 0 7177 0
[pid=26087] vsize: 29288
Current children cumulated CPU time (s) 149.47
Current children cumulated vsize (Kb) 31412

[startup+160.016 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7415 0 0 0 15902 45 0 0 25 0 1 0 1785314593 29990912 7200 4294967295 134512640 135094434 3221224448 3221223120 134556434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 7322 7200 145 145 0 7177 0
[pid=26087] vsize: 29288
Current children cumulated CPU time (s) 159.47
Current children cumulated vsize (Kb) 31412

[startup+170.017 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7751 0 0 0 16897 47 0 0 25 0 1 0 1785314593 31367168 7536 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 7658 7536 145 145 0 7513 0
[pid=26087] vsize: 30632
Current children cumulated CPU time (s) 169.44
Current children cumulated vsize (Kb) 32756

[startup+180.018 s]
Raw data (loadavg): 1.01 1.02 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 8325 0 0 0 17888 50 0 0 25 0 1 0 1785314593 33718272 8110 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 8232 8110 145 145 0 8087 0
[pid=26087] vsize: 32928
Current children cumulated CPU time (s) 179.38
Current children cumulated vsize (Kb) 35052

[startup+190.018 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 8847 0 0 0 18878 54 0 0 25 0 1 0 1785314593 35852288 8632 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 8753 8632 145 145 0 8608 0
[pid=26087] vsize: 35012
Current children cumulated CPU time (s) 189.32
Current children cumulated vsize (Kb) 37136

[startup+200.019 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 9331 0 0 0 19870 57 0 0 25 0 1 0 1785314593 37822464 9116 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 9234 9116 145 145 0 9089 0
[pid=26087] vsize: 36936
Current children cumulated CPU time (s) 199.27
Current children cumulated vsize (Kb) 39060

[startup+210.019 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 9881 0 0 0 20860 61 0 0 25 0 1 0 1785314593 40062976 9666 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 9781 9666 145 145 0 9636 0
[pid=26087] vsize: 39124
Current children cumulated CPU time (s) 209.21
Current children cumulated vsize (Kb) 41248

[startup+220.021 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 10312 0 0 0 21852 65 0 0 25 0 1 0 1785314593 41816064 10097 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 10209 10097 145 145 0 10064 0
[pid=26087] vsize: 40836
Current children cumulated CPU time (s) 219.17
Current children cumulated vsize (Kb) 42960

[startup+230.022 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 10700 0 0 0 22845 67 0 0 25 0 1 0 1785314593 43397120 10485 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 10595 10485 145 145 0 10450 0
[pid=26087] vsize: 42380
Current children cumulated CPU time (s) 229.12
Current children cumulated vsize (Kb) 44504

[startup+240.022 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11086 0 0 0 23838 70 0 0 25 0 1 0 1785314593 44965888 10871 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 10978 10871 145 145 0 10833 0
[pid=26087] vsize: 43912
Current children cumulated CPU time (s) 239.08
Current children cumulated vsize (Kb) 46036

[startup+250.023 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 24835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223040 134551704 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 249.07
Current children cumulated vsize (Kb) 46368

[startup+260.024 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 25835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 259.07
Current children cumulated vsize (Kb) 46368

[startup+270.024 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 26835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 269.07
Current children cumulated vsize (Kb) 46368

[startup+280.025 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 27835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 279.07
Current children cumulated vsize (Kb) 46368

[startup+290.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 28835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 289.07
Current children cumulated vsize (Kb) 46368

[startup+300.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 29835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 299.07
Current children cumulated vsize (Kb) 46368

[startup+310.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 30836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223040 134557336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 309.08
Current children cumulated vsize (Kb) 46368

[startup+320.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 31836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 319.08
Current children cumulated vsize (Kb) 46368

[startup+330.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 32836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 329.08
Current children cumulated vsize (Kb) 46368

[startup+340.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 33836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0
[pid=26087] vsize: 44244
Current children cumulated CPU time (s) 339.08
Current children cumulated vsize (Kb) 46368

[startup+350.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11505 0 0 0 34832 74 0 0 25 0 1 0 1785314593 46514176 11249 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11356 11249 145 145 0 11211 0
[pid=26087] vsize: 45424
Current children cumulated CPU time (s) 349.06
Current children cumulated vsize (Kb) 47548

[startup+360.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11994 0 0 0 35824 77 0 0 25 0 1 0 1785314593 48517120 11738 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 11845 11738 145 145 0 11700 0
[pid=26087] vsize: 47380
Current children cumulated CPU time (s) 359.01
Current children cumulated vsize (Kb) 49504

[startup+370.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 12404 0 0 0 36816 81 0 0 25 0 1 0 1785314593 50450432 12148 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 12317 12148 145 145 0 12172 0
[pid=26087] vsize: 49268
Current children cumulated CPU time (s) 368.97
Current children cumulated vsize (Kb) 51392

[startup+380.032 s]
Raw data (loadavg): 1.00 1.00 0.93 3/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 12800 0 0 0 37809 84 0 0 25 0 1 0 1785314593 52064256 12544 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 12711 12544 145 145 0 12566 0
[pid=26087] vsize: 50844
Current children cumulated CPU time (s) 378.93
Current children cumulated vsize (Kb) 52968

[startup+390.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13142 0 0 0 38803 87 0 0 25 0 1 0 1785314593 53448704 12886 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13049 12886 145 145 0 12904 0
[pid=26087] vsize: 52196
Current children cumulated CPU time (s) 388.9
Current children cumulated vsize (Kb) 54320

[startup+400.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 39801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 398.89
Current children cumulated vsize (Kb) 54780

[startup+410.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 40801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 408.89
Current children cumulated vsize (Kb) 54780

[startup+420.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 41801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 418.89
Current children cumulated vsize (Kb) 54780

[startup+430.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 42801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 428.89
Current children cumulated vsize (Kb) 54780

[startup+440.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 43801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 438.89
Current children cumulated vsize (Kb) 54780

[startup+450.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 44801 89 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 448.9
Current children cumulated vsize (Kb) 54780

[startup+460.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 45801 89 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 458.9
Current children cumulated vsize (Kb) 54780

[startup+470.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 46801 89 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 468.9
Current children cumulated vsize (Kb) 54780

[startup+480.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 47801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 478.91
Current children cumulated vsize (Kb) 54780

[startup+490.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 48801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 488.91
Current children cumulated vsize (Kb) 54780

[startup+500.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 49801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 498.91
Current children cumulated vsize (Kb) 54780

[startup+510.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 50801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 508.91
Current children cumulated vsize (Kb) 54780

[startup+520.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13300 0 0 0 51802 90 0 0 25 0 1 0 1785314593 53919744 13003 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13003 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 518.92
Current children cumulated vsize (Kb) 54780

[startup+530.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13300 0 0 0 52802 90 0 0 25 0 1 0 1785314593 53919744 13003 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13003 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 528.92
Current children cumulated vsize (Kb) 54780

[startup+540.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13300 0 0 0 53802 90 0 0 25 0 1 0 1785314593 53919744 13003 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13003 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 538.92
Current children cumulated vsize (Kb) 54780

[startup+550.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13302 0 0 0 54802 90 0 0 25 0 1 0 1785314593 53919744 13005 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13005 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 548.92
Current children cumulated vsize (Kb) 54780

[startup+560.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13305 0 0 0 55802 90 0 0 25 0 1 0 1785314593 53919744 13008 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13164 13008 145 145 0 13019 0
[pid=26087] vsize: 52656
Current children cumulated CPU time (s) 558.92
Current children cumulated vsize (Kb) 54780

[startup+570.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13395 0 0 0 56800 91 0 0 25 0 1 0 1785314593 54280192 13098 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13252 13098 145 145 0 13107 0
[pid=26087] vsize: 53008
Current children cumulated CPU time (s) 568.91
Current children cumulated vsize (Kb) 55132

[startup+580.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13686 0 0 0 57795 93 0 0 25 0 1 0 1785314593 55463936 13389 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13541 13389 145 145 0 13396 0
[pid=26087] vsize: 54164
Current children cumulated CPU time (s) 578.88
Current children cumulated vsize (Kb) 56288

[startup+590.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13973 0 0 0 58790 95 0 0 25 0 1 0 1785314593 56627200 13676 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 13825 13676 145 145 0 13680 0
[pid=26087] vsize: 55300
Current children cumulated CPU time (s) 588.85
Current children cumulated vsize (Kb) 57424

[startup+600.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 14226 0 0 0 59784 98 0 0 25 0 1 0 1785314593 57667584 13929 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 14079 13929 145 145 0 13934 0
[pid=26087] vsize: 56316
Current children cumulated CPU time (s) 598.82
Current children cumulated vsize (Kb) 58440

[startup+610.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 14510 0 0 0 60779 100 0 0 25 0 1 0 1785314593 58826752 14213 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 14362 14213 145 145 0 14217 0
[pid=26087] vsize: 57448
Current children cumulated CPU time (s) 608.79
Current children cumulated vsize (Kb) 59572

[startup+620.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 14780 0 0 0 61775 103 0 0 25 0 1 0 1785314593 59920384 14483 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 14629 14483 145 145 0 14484 0
[pid=26087] vsize: 58516
Current children cumulated CPU time (s) 618.78
Current children cumulated vsize (Kb) 60640

[startup+630.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15029 0 0 0 62770 105 0 0 25 0 1 0 1785314593 60932096 14732 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 14876 14732 145 145 0 14731 0
[pid=26087] vsize: 59504
Current children cumulated CPU time (s) 628.75
Current children cumulated vsize (Kb) 61628

[startup+640.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15223 0 0 0 63765 107 0 0 25 0 1 0 1785314593 61718528 14926 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 15068 14926 145 145 0 14923 0
[pid=26087] vsize: 60272
Current children cumulated CPU time (s) 638.72
Current children cumulated vsize (Kb) 62396

[startup+650.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15446 0 0 0 64761 109 0 0 25 0 1 0 1785314593 62627840 15149 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 15290 15149 145 145 0 15145 0
[pid=26087] vsize: 61160
Current children cumulated CPU time (s) 648.7
Current children cumulated vsize (Kb) 63284

[startup+660.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15651 0 0 0 65758 110 0 0 25 0 1 0 1785314593 63471616 15354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 15496 15354 145 145 0 15351 0
[pid=26087] vsize: 61984
Current children cumulated CPU time (s) 658.68
Current children cumulated vsize (Kb) 64108

[startup+670.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15854 0 0 0 66755 112 0 0 25 0 1 0 1785314593 64294912 15557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 15697 15557 145 145 0 15552 0
[pid=26087] vsize: 62788
Current children cumulated CPU time (s) 668.67
Current children cumulated vsize (Kb) 64912

[startup+680.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16048 0 0 0 67751 113 0 0 25 0 1 0 1785314593 65085440 15751 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 15890 15751 145 145 0 15745 0
[pid=26087] vsize: 63560
Current children cumulated CPU time (s) 678.64
Current children cumulated vsize (Kb) 65684

[startup+690.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16244 0 0 0 68747 115 0 0 25 0 1 0 1785314593 65880064 15947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 16084 15947 145 145 0 15939 0
[pid=26087] vsize: 64336
Current children cumulated CPU time (s) 688.62
Current children cumulated vsize (Kb) 66460

[startup+700.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16423 0 0 0 69743 116 0 0 25 0 1 0 1785314593 66596864 16126 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 16259 16126 145 145 0 16114 0
[pid=26087] vsize: 65036
Current children cumulated CPU time (s) 698.59
Current children cumulated vsize (Kb) 67160

[startup+710.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16630 0 0 0 70740 117 0 0 25 0 1 0 1785314593 67436544 16333 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 16464 16333 145 145 0 16319 0
[pid=26087] vsize: 65856
Current children cumulated CPU time (s) 708.57
Current children cumulated vsize (Kb) 67980

[startup+720.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16860 0 0 0 71734 120 0 0 25 0 1 0 1785314593 68382720 16563 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 16695 16563 145 145 0 16550 0
[pid=26087] vsize: 66780
Current children cumulated CPU time (s) 718.54
Current children cumulated vsize (Kb) 68904

[startup+730.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17085 0 0 0 72730 122 0 0 25 0 1 0 1785314593 69292032 16788 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 16917 16788 145 145 0 16772 0
[pid=26087] vsize: 67668
Current children cumulated CPU time (s) 728.52
Current children cumulated vsize (Kb) 69792

[startup+740.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17310 0 0 0 73726 123 0 0 25 0 1 0 1785314593 70217728 17013 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17143 17013 145 145 0 16998 0
[pid=26087] vsize: 68572
Current children cumulated CPU time (s) 738.49
Current children cumulated vsize (Kb) 70696

[startup+750.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17527 0 0 0 74723 124 0 0 25 0 1 0 1785314593 71098368 17230 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17358 17230 145 145 0 17213 0
[pid=26087] vsize: 69432
Current children cumulated CPU time (s) 748.47
Current children cumulated vsize (Kb) 71556

[startup+760.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 75722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 758.47
Current children cumulated vsize (Kb) 71696

[startup+770.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 76722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 768.47
Current children cumulated vsize (Kb) 71696

[startup+780.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 77722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 778.47
Current children cumulated vsize (Kb) 71696

[startup+790.065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 78722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 788.47
Current children cumulated vsize (Kb) 71696

[startup+800.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 79723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 798.48
Current children cumulated vsize (Kb) 71696

[startup+810.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 80723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 808.48
Current children cumulated vsize (Kb) 71696

[startup+820.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 81723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 818.48
Current children cumulated vsize (Kb) 71696

[startup+830.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 82724 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 828.49
Current children cumulated vsize (Kb) 71696

[startup+840.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 83723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 838.48
Current children cumulated vsize (Kb) 71696

[startup+850.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 84723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 848.49
Current children cumulated vsize (Kb) 71696

[startup+860.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 85723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 858.49
Current children cumulated vsize (Kb) 71696

[startup+870.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 86723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 868.49
Current children cumulated vsize (Kb) 71696

[startup+880.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 87723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 878.49
Current children cumulated vsize (Kb) 71696

[startup+890.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 88723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 888.49
Current children cumulated vsize (Kb) 71696

[startup+900.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 89724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 898.5
Current children cumulated vsize (Kb) 71696

[startup+910.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 90724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 908.5
Current children cumulated vsize (Kb) 71696

[startup+920.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 91724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 918.5
Current children cumulated vsize (Kb) 71696

[startup+930.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 92724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 928.5
Current children cumulated vsize (Kb) 71696

[startup+940.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 93724 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 938.5
Current children cumulated vsize (Kb) 71696

[startup+950.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 94725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 948.51
Current children cumulated vsize (Kb) 71696

[startup+960.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 95725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 958.51
Current children cumulated vsize (Kb) 71696

[startup+970.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 96725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 968.51
Current children cumulated vsize (Kb) 71696

[startup+980.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 97725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 978.51
Current children cumulated vsize (Kb) 71696

[startup+990.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 98726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 988.52
Current children cumulated vsize (Kb) 71696

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 99726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 998.52
Current children cumulated vsize (Kb) 71696

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 100726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1008.52
Current children cumulated vsize (Kb) 71696

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 101726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1018.52
Current children cumulated vsize (Kb) 71696

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 102726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1028.52
Current children cumulated vsize (Kb) 71696

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 103727 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1038.53
Current children cumulated vsize (Kb) 71696

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 104726 127 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1048.53
Current children cumulated vsize (Kb) 71696

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 105726 127 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1058.53
Current children cumulated vsize (Kb) 71696

[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 106726 127 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1068.53
Current children cumulated vsize (Kb) 71696

[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 107726 128 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0
[pid=26087] vsize: 69572
Current children cumulated CPU time (s) 1078.54
Current children cumulated vsize (Kb) 71696

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17784 0 0 0 108722 130 0 0 25 0 1 0 1785314593 72142848 17487 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 17613 17487 145 145 0 17468 0
[pid=26087] vsize: 70452
Current children cumulated CPU time (s) 1088.52
Current children cumulated vsize (Kb) 72576

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18010 0 0 0 109718 131 0 0 25 0 1 0 1785314593 73064448 17713 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 17838 17713 145 145 0 17693 0
[pid=26087] vsize: 71352
Current children cumulated CPU time (s) 1098.49
Current children cumulated vsize (Kb) 73476

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18182 0 0 0 110715 133 0 0 25 0 1 0 1785314593 73777152 17885 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26087/statm): 18012 17885 145 145 0 17867 0
[pid=26087] vsize: 72048
Current children cumulated CPU time (s) 1108.48
Current children cumulated vsize (Kb) 74172

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18434 0 0 0 111708 135 0 0 25 0 1 0 1785314593 74813440 18137 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 18265 18137 145 145 0 18120 0
[pid=26087] vsize: 73060
Current children cumulated CPU time (s) 1118.43
Current children cumulated vsize (Kb) 75184

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 3/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18686 0 0 0 112704 137 0 0 25 0 1 0 1785314593 75845632 18389 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 18517 18389 145 145 0 18372 0
[pid=26087] vsize: 74068
Current children cumulated CPU time (s) 1128.41
Current children cumulated vsize (Kb) 76192

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18892 0 0 0 113700 139 0 0 25 0 1 0 1785314593 76689408 18595 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 18723 18595 145 145 0 18578 0
[pid=26087] vsize: 74892
Current children cumulated CPU time (s) 1138.39
Current children cumulated vsize (Kb) 77016

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19118 0 0 0 114696 140 0 0 25 0 1 0 1785314593 77606912 18821 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 18947 18821 145 145 0 18802 0
[pid=26087] vsize: 75788
Current children cumulated CPU time (s) 1148.36
Current children cumulated vsize (Kb) 77912

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19326 0 0 0 115692 142 0 0 25 0 1 0 1785314593 78454784 19029 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 19154 19029 145 145 0 19009 0
[pid=26087] vsize: 76616
Current children cumulated CPU time (s) 1158.34
Current children cumulated vsize (Kb) 78740

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19529 0 0 0 116688 144 0 0 25 0 1 0 1785314593 79802368 19232 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 19483 19232 145 145 0 19338 0
[pid=26087] vsize: 77932
Current children cumulated CPU time (s) 1168.32
Current children cumulated vsize (Kb) 80056

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19757 0 0 0 117684 146 0 0 25 0 1 0 1785314593 80732160 19460 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 19710 19460 145 145 0 19565 0
[pid=26087] vsize: 78840
Current children cumulated CPU time (s) 1178.3
Current children cumulated vsize (Kb) 80964

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20022 0 0 0 118681 148 0 0 25 0 1 0 1785314593 81809408 19725 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 19973 19725 145 145 0 19828 0
[pid=26087] vsize: 79892
Current children cumulated CPU time (s) 1188.29
Current children cumulated vsize (Kb) 82016

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20252 0 0 0 119677 149 0 0 25 0 1 0 1785314593 82743296 19955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 20201 19955 145 145 0 20056 0
[pid=26087] vsize: 80804
Current children cumulated CPU time (s) 1198.26
Current children cumulated vsize (Kb) 82928

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20267 0 0 0 120677 149 0 0 25 0 1 0 1785314593 82804736 19970 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 20216 19970 145 145 0 20071 0
[pid=26087] vsize: 80864
Current children cumulated CPU time (s) 1208.26
Current children cumulated vsize (Kb) 82988



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 26087
Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26083/statm): 531 226 485 147 0 384 0
[pid=26083] vsize: 2124
Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20267 0 0 0 120678 149 0 0 25 0 1 0 1785314593 82804736 19970 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26087/statm): 20216 19970 145 145 0 20071 0
[pid=26087] vsize: 80864
Current children cumulated CPU time (s) 1208.27
Current children cumulated vsize (Kb) 82988

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.32
CPU user time (s): 1206.78
CPU system time (s): 1.53877
CPU usage (%): 99.8498
Max. virtual memory (cumulated for all children) (Kb): 82988

Verifier Data

ERROR: no interpretation found !