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-1.opb
MD5SUMaa1ea44fce5b7bfbe62733720f941ebb
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.05
Number of variables945
Total number of constraints59186
Number of constraints which are clauses59186
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 2294

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        910804 kB
Buffers:         34652 kB
Cached:          61576 kB
SwapCached:        536 kB
Active:          68340 kB
Inactive:        30496 kB
HighTotal:      131008 kB
HighFree:        67368 kB
LowTotal:       903652 kB
LowFree:        843436 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5864 kB
Slab:            19388 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:05:32 (client local time) WITH STATUS 10 IN 1208.58 SECONDS
stats: 2700 7 1208.58 10

Solver Data

c Parsing PB file...
c Converting 59186 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 |   59186   118372 |   19728       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 |  104775   225435 |   34925       0        0     nan |  0.000 % |
c |       100 |  104524   224914 |   38417      85     1066    12.5 |  0.436 % |
c |       250 |  103672   223098 |   42259     189     2294    12.1 |  2.065 % |
c |       475 |  102383   220255 |   46485     345     4840    14.0 |  4.529 % |
c |       812 |  100937   217141 |   51133     586     7419    12.7 |  7.149 % |
c |      1318 |   98182   211016 |   56247     955    12123    12.7 | 12.554 % |
c |      2077 |   95016   203912 |   61871    1479    18940    12.8 | 18.868 % |
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 |      2281 |   94270   202263 |   31423    1638    21254    13.0 | 18.868 % |
c |      2381 |   93557   200642 |   34565    1705    22268    13.1 | 21.898 % |
c |      2531 |   92946   199272 |   38021    1827    23369    12.8 | 23.109 % |
c |      2756 |   91830   196738 |   41824    1986    25232    12.7 | 25.365 % |
c |      3093 |   90546   193828 |   46006    2258    28068    12.4 | 27.941 % |
c |      3599 |   89135   190554 |   50607    2662    32253    12.1 | 30.930 % |
c |      4358 |   86431   184320 |   55667    3235    39718    12.3 | 36.339 % |
c |      5497 |   82098   174321 |   61234    4060    50083    12.3 | 45.224 % |
c |      7205 |   78759   166500 |   67357    5274    69800    13.2 | 52.309 % |
c |      9767 |   74447   156240 |   74093    7257   115053    15.9 | 61.626 % |
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 |     11855 |   72901   152602 |   24300    9007   171237    19.0 | 61.626 % |
c |     11956 |   72669   152047 |   26730    9026   173881    19.3 | 65.703 % |
c |     12106 |   72511   151662 |   29403    9103   175319    19.3 | 66.054 % |
c |     12332 |   71960   150355 |   32343    9214   178574    19.4 | 67.232 % |
c |     12669 |   71960   150355 |   35577    9551   186891    19.6 | 67.232 % |
c |     13175 |   71822   150026 |   39135   10017   198100    19.8 | 67.634 % |
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 |     13651 |   71767   149867 |   23922   10477   227070    21.7 | 67.634 % |
c |     13751 |   71635   149552 |   26314   10560   229754    21.8 | 67.952 % |
c |     13901 |   71495   149231 |   28945   10689   232692    21.8 | 68.240 % |
c |     14126 |   71495   149231 |   31840   10914   240590    22.0 | 68.240 % |
c |     14464 |   71301   148771 |   35024   11166   247387    22.2 | 68.658 % |
c |     14970 |   71096   148283 |   38526   11598   264285    22.8 | 69.105 % |
c |     15729 |   70692   147312 |   42379   12216   294929    24.1 | 70.005 % |
c |     16868 |   70606   147101 |   46617   13307   355598    26.7 | 70.197 % |
c |     18576 |   70013   145662 |   51278   14834   442373    29.8 | 71.487 % |
c |     21138 |   69860   145296 |   56406   17357   580759    33.5 | 71.822 % |
c |     24982 |   69186   143692 |   62047   21008   882895    42.0 | 73.271 % |
c |     30748 |   68669   142440 |   68252   26564  1266965    47.7 | 74.405 % |
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 |     36888 |   68477   142002 |   22825   32538  2350890    72.3 | 74.405 % |
c |     36989 |   68477   142002 |   25107   32639  2355889    72.2 | 74.863 % |
c |     37139 |   68477   142002 |   27618   32789  2364920    72.1 | 74.863 % |
c |     37364 |   68390   141794 |   30380   32976  2374435    72.0 | 75.048 % |
c |     37701 |   68208   141353 |   33418   33252  2387786    71.8 | 75.447 % |
c |     38207 |   68191   141312 |   36759   33737  2410028    71.4 | 75.485 % |
c |     38966 |   68191   141312 |   40435   34496  2508782    72.7 | 75.485 % |
c |     40105 |   67643   139988 |   44479   35447  2584380    72.9 | 76.710 % |
c |     41813 |   67533   139718 |   48927   36998  2681268    72.5 | 76.965 % |
c |     44377 |   67408   139415 |   53820   39481  2933313    74.3 | 77.249 % |
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 |     46463 |   67399   139347 |   22466   41488  3173600    76.5 | 77.249 % |
c |     46563 |   67366   139264 |   24712   41579  3178985    76.5 | 77.355 % |
c |     46714 |   67366   139264 |   27183   41730  3188195    76.4 | 77.355 % |
c |     46939 |   67366   139264 |   29902   41955  3203516    76.4 | 77.355 % |
c |     47277 |   67152   138734 |   32892   42197  3212016    76.1 | 77.856 % |
c |     47783 |   67024   138429 |   36181   42593  3256759    76.5 | 78.130 % |
c |     48542 |   66893   138094 |   39799   43247  3317085    76.7 | 78.440 % |
c |     49681 |   66773   137806 |   43779   44272  3468329    78.3 | 78.708 % |
c |     51389 |   66773   137806 |   48157   45980  3665783    79.7 | 78.708 % |
c |     53951 |   66773   137806 |   52973   48542  3874270    79.8 | 78.708 % |
c |     57795 |   66703   137642 |   58271   52249  4403144    84.3 | 78.858 % |
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 |     60959 |   66746   137780 |   22248   55413  4808677    86.8 | 78.858 % |
c |     61059 |   66746   137780 |   24472   19970  1491252    74.7 | 78.843 % |
c |     61209 |   66696   137659 |   26920   20112  1501421    74.7 | 78.955 % |
c |     61434 |   66655   137558 |   29612   20326  1508405    74.2 | 79.050 % |
c |     61772 |   66655   137558 |   32573   20664  1548997    75.0 | 79.050 % |
c |     62278 |   66641   137528 |   35830   21164  1579134    74.6 | 79.075 % |
c |     63038 |   66483   137145 |   39413   21877  1624906    74.3 | 79.428 % |
c |     64178 |   66436   137033 |   43355   23009  1706960    74.2 | 79.533 % |
c |     65886 |   66394   136940 |   47690   24715  1877964    76.0 | 79.612 % |
c |     68448 |   66394   136940 |   52459   27277  2138187    78.4 | 79.612 % |
c |     72292 |   66188   136448 |   57705   31053  2536364    81.7 | 80.060 % |
c |     78058 |   65990   135958 |   63476   36773  3108332    84.5 | 80.515 % |
c |     86708 |   65668   135177 |   69823   45315  4027181    88.9 | 81.214 % |
c |     99682 |   65663   135166 |   76806   58283  5489233    94.2 | 81.223 % |
c |    119143 |   65625   135078 |   84486   77730  8037334   103.4 | 81.303 % |
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 |    133656 |   65574   134927 |   21858   91840  9604872   104.6 | 81.303 % |
c |    133756 |   65574   134927 |   24043   23083  1518038    65.8 | 81.425 % |
c |    133906 |   65574   134927 |   26448   23233  1526900    65.7 | 81.425 % |
c |    134131 |   65574   134927 |   29092   23458  1544148    65.8 | 81.425 % |
c |    134468 |   65574   134927 |   32002   23795  1579065    66.4 | 81.425 % |
c |    134975 |   65574   134927 |   35202   24302  1634412    67.3 | 81.425 % |
c |    135734 |   65574   134927 |   38722   25061  1715989    68.5 | 81.425 % |
c |    136873 |   65574   134927 |   42595   26200  1819780    69.5 | 81.425 % |
c |    138581 |   65538   134839 |   46854   27898  1949053    69.9 | 81.507 % |
c |    141143 |   65538   134839 |   51540   30460  2313155    75.9 | 81.507 % |
c |    144987 |   65523   134802 |   56694   34301  2805082    81.8 | 81.542 % |
c |    150753 |   65475   134677 |   62363   40058  3378991    84.4 | 81.663 % |
c |    159402 |   65475   134677 |   68599   48707  4419954    90.7 | 81.663 % |
c |    172376 |   65475   134677 |   75459   61681  6333551   102.7 | 81.663 % |
c |    191837 |   65421   134551 |   83005   81127  9152518   112.8 | 81.778 % |
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 |    219923 |   65394   134505 |   21798  109183 12991111   119.0 | 81.778 % |
c |    220023 |   65338   134375 |   23977   22717  1789048    78.8 | 81.963 % |
c |    220174 |   65333   134362 |   26375   22867  1792281    78.4 | 81.976 % |
c |    220399 |   65333   134362 |   29013   23092  1806748    78.2 | 81.976 % |
c |    220736 |   65333   134362 |   31914   23429  1824678    77.9 | 81.976 % |
c |    221242 |   65333   134362 |   35105   23935  1866744    78.0 | 81.976 % |
c |    222002 |   65293   134272 |   38616   24652  1951243    79.2 | 82.055 % |
c |    223141 |   65286   134253 |   42478   25787  2104469    81.6 | 82.074 % |
c |    224849 |   65180   133992 |   46725   27472  2289235    83.3 | 82.319 % |
c |    227411 |   65176   133982 |   51398   30033  2573728    85.7 | 82.328 % |
c |    231255 |   65155   133933 |   56538   33873  3074425    90.8 | 82.373 % |
c |    237023 |   65155   133933 |   62192   39641  3661660    92.4 | 82.373 % |
c |    245672 |   65067   133711 |   68411   48265  4631228    96.0 | 82.585 % |
c |    258647 |   65059   133691 |   75252   61219  6278193   102.6 | 82.604 % |
c |    278108 |   65021   133594 |   82777   80669  8915752   110.5 | 82.696 % |
c |    307300 |   64872   133243 |   91055   25592  1556180    60.8 | 83.017 % |
c |    351089 |   64793   133051 |  100161   69306  6528778    94.2 | 83.195 % |
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 -C265

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/32703/stat): 32703 (minisat+_script) R 32702 32703 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843518547 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/32703/statm): 174 3 169 147 0 27 0
[pid=32703] 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=32704
New process pid=32705
New process pid=32706
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
One traced child (pid=32705) exited with status: 0
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=32706) exited with status: 0
One traced child (pid=32704) exited with status: 0
New process pid=32707
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-frb45-21-1.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 3763 0 0 0 968 16 0 0 25 0 1 0 1843518552 15798272 3750 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 3857 3750 145 145 0 3712 0
[pid=32707] vsize: 15428
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 17552

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 3763 0 0 0 1968 16 0 0 25 0 1 0 1843518552 15798272 3750 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 3857 3750 145 145 0 3712 0
[pid=32707] vsize: 15428
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 17552

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 3763 0 0 0 2967 17 0 0 25 0 1 0 1843518552 15798272 3750 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 3857 3750 145 145 0 3712 0
[pid=32707] vsize: 15428
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 17552

[startup+40.0065 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 3763 0 0 0 3967 17 0 0 25 0 1 0 1843518552 15798272 3750 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 3857 3750 145 145 0 3712 0
[pid=32707] vsize: 15428
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 17552

[startup+50.0072 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 3834 0 0 0 4967 17 0 0 25 0 1 0 1843518552 15929344 3780 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 3889 3780 145 145 0 3744 0
[pid=32707] vsize: 15556
Current children cumulated CPU time (s) 49.84
Current children cumulated vsize (Kb) 17680

[startup+60.0079 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 4211 0 0 0 5959 21 0 0 25 0 1 0 1843518552 17281024 4116 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 4219 4116 145 145 0 4074 0
[pid=32707] vsize: 16876
Current children cumulated CPU time (s) 59.8
Current children cumulated vsize (Kb) 19000

[startup+70.0096 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 4755 0 0 0 6949 25 0 0 25 0 1 0 1843518552 19546112 4660 4294967295 134512640 135094434 3221224448 3221223040 134557491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 4772 4660 145 145 0 4627 0
[pid=32707] vsize: 19088
Current children cumulated CPU time (s) 69.74
Current children cumulated vsize (Kb) 21212

[startup+80.0103 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 5209 0 0 0 7940 29 0 0 25 0 1 0 1843518552 21385216 5114 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 5221 5114 145 145 0 5076 0
[pid=32707] vsize: 20884
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 23008

[startup+90.0101 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 6108 0 0 0 8925 35 0 0 25 0 1 0 1843518552 25051136 6013 4294967295 134512640 135094434 3221224448 3221223040 134557234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 6116 6013 145 145 0 5971 0
[pid=32707] vsize: 24464
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 26588

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 6488 0 0 0 9920 37 0 0 25 0 1 0 1843518552 26566656 6353 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 6486 6353 145 145 0 6341 0
[pid=32707] vsize: 25944
Current children cumulated CPU time (s) 99.57
Current children cumulated vsize (Kb) 28068

[startup+110.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 6804 0 0 0 10913 40 0 0 25 0 1 0 1843518552 27844608 6669 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 6798 6669 145 145 0 6653 0
[pid=32707] vsize: 27192
Current children cumulated CPU time (s) 109.53
Current children cumulated vsize (Kb) 29316

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 7307 0 0 0 11902 46 0 0 25 0 1 0 1843518552 29720576 7131 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 7256 7131 145 145 0 7111 0
[pid=32707] vsize: 29024
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 31148

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 7657 0 0 0 12896 48 0 0 25 0 1 0 1843518552 31145984 7481 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 7604 7481 145 145 0 7459 0
[pid=32707] vsize: 30416
Current children cumulated CPU time (s) 129.44
Current children cumulated vsize (Kb) 32540

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 8076 0 0 0 13888 52 0 0 25 0 1 0 1843518552 32845824 7900 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8019 7900 145 145 0 7874 0
[pid=32707] vsize: 32076
Current children cumulated CPU time (s) 139.4
Current children cumulated vsize (Kb) 34200

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 8622 0 0 0 14879 56 0 0 25 0 1 0 1843518552 35065856 8446 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8561 8446 145 145 0 8416 0
[pid=32707] vsize: 34244
Current children cumulated CPU time (s) 149.35
Current children cumulated vsize (Kb) 36368

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 15871 59 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223108 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 159.3
Current children cumulated vsize (Kb) 37928

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 16870 60 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 169.3
Current children cumulated vsize (Kb) 37928

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 17870 60 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 179.3
Current children cumulated vsize (Kb) 37928

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 18869 61 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 189.3
Current children cumulated vsize (Kb) 37928

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 19869 61 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 199.3
Current children cumulated vsize (Kb) 37928

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 20868 62 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 209.3
Current children cumulated vsize (Kb) 37928

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 21868 62 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 37928

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9056 0 0 0 22867 63 0 0 25 0 1 0 1843518552 36663296 8839 4294967295 134512640 135094434 3221224448 3221223108 134555972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 8951 8839 145 145 0 8806 0
[pid=32707] vsize: 35804
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 37928

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9363 0 0 0 23860 66 0 0 25 0 1 0 1843518552 37920768 9146 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 9258 9146 145 145 0 9113 0
[pid=32707] vsize: 37032
Current children cumulated CPU time (s) 239.26
Current children cumulated vsize (Kb) 39156

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 9755 0 0 0 24854 69 0 0 25 0 1 0 1843518552 39522304 9538 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 9649 9538 145 145 0 9504 0
[pid=32707] vsize: 38596
Current children cumulated CPU time (s) 249.23
Current children cumulated vsize (Kb) 40720

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 10122 0 0 0 25848 71 0 0 25 0 1 0 1843518552 41013248 9905 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 10013 9905 145 145 0 9868 0
[pid=32707] vsize: 40052
Current children cumulated CPU time (s) 259.19
Current children cumulated vsize (Kb) 42176

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 10508 0 0 0 26841 74 0 0 25 0 1 0 1843518552 42582016 10291 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 10396 10291 145 145 0 10251 0
[pid=32707] vsize: 41584
Current children cumulated CPU time (s) 269.15
Current children cumulated vsize (Kb) 43708

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 10959 0 0 0 27833 78 0 0 25 0 1 0 1843518552 44675072 10742 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 10907 10742 145 145 0 10762 0
[pid=32707] vsize: 43628
Current children cumulated CPU time (s) 279.11
Current children cumulated vsize (Kb) 45752

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 11511 0 0 0 28823 82 0 0 25 0 1 0 1843518552 46927872 11294 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 11457 11294 145 145 0 11312 0
[pid=32707] vsize: 45828
Current children cumulated CPU time (s) 289.05
Current children cumulated vsize (Kb) 47952

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 11866 0 0 0 29816 85 0 0 25 0 1 0 1843518552 48373760 11649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 11810 11649 145 145 0 11665 0
[pid=32707] vsize: 47240
Current children cumulated CPU time (s) 299.01
Current children cumulated vsize (Kb) 49364

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 12309 0 0 0 30809 88 0 0 25 0 1 0 1843518552 50176000 12092 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 12250 12092 145 145 0 12105 0
[pid=32707] vsize: 49000
Current children cumulated CPU time (s) 308.97
Current children cumulated vsize (Kb) 51124

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 12703 0 0 0 31800 91 0 0 25 0 1 0 1843518552 51777536 12486 4294967295 134512640 135094434 3221224448 3221223040 134551757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 12641 12486 145 145 0 12496 0
[pid=32707] vsize: 50564
Current children cumulated CPU time (s) 318.91
Current children cumulated vsize (Kb) 52688

[startup+330.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 13064 0 0 0 32795 94 0 0 25 0 1 0 1843518552 53252096 12847 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 13001 12847 145 145 0 12856 0
[pid=32707] vsize: 52004
Current children cumulated CPU time (s) 328.89
Current children cumulated vsize (Kb) 54128

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 13398 0 0 0 33789 96 0 0 25 0 1 0 1843518552 54611968 13181 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 13333 13181 145 145 0 13188 0
[pid=32707] vsize: 53332
Current children cumulated CPU time (s) 338.85
Current children cumulated vsize (Kb) 55456

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 13652 0 0 0 34784 98 0 0 25 0 1 0 1843518552 55640064 13435 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 13584 13435 145 145 0 13439 0
[pid=32707] vsize: 54336
Current children cumulated CPU time (s) 348.82
Current children cumulated vsize (Kb) 56460

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 13966 0 0 0 35779 101 0 0 25 0 1 0 1843518552 56930304 13749 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 13899 13749 145 145 0 13754 0
[pid=32707] vsize: 55596
Current children cumulated CPU time (s) 358.8
Current children cumulated vsize (Kb) 57720

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14309 0 0 0 36773 104 0 0 25 0 1 0 1843518552 58322944 14092 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14239 14092 145 145 0 14094 0
[pid=32707] vsize: 56956
Current children cumulated CPU time (s) 368.77
Current children cumulated vsize (Kb) 59080

[startup+380.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 37772 104 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 378.76
Current children cumulated vsize (Kb) 59332

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 38772 104 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 388.76
Current children cumulated vsize (Kb) 59332

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 39772 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 59332

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 40772 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 408.77
Current children cumulated vsize (Kb) 59332

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 41772 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 418.77
Current children cumulated vsize (Kb) 59332

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 42773 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 428.78
Current children cumulated vsize (Kb) 59332

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 43773 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 438.78
Current children cumulated vsize (Kb) 59332

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 44773 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 448.78
Current children cumulated vsize (Kb) 59332

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 45773 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 458.78
Current children cumulated vsize (Kb) 59332

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 46773 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223120 134556198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 468.78
Current children cumulated vsize (Kb) 59332

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 47774 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 478.79
Current children cumulated vsize (Kb) 59332

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 48774 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 488.79
Current children cumulated vsize (Kb) 59332

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 49774 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 498.79
Current children cumulated vsize (Kb) 59332

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 50774 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 508.79
Current children cumulated vsize (Kb) 59332

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 51775 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 518.8
Current children cumulated vsize (Kb) 59332

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 52775 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 528.8
Current children cumulated vsize (Kb) 59332

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 53775 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 538.8
Current children cumulated vsize (Kb) 59332

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14413 0 0 0 54775 105 0 0 25 0 1 0 1843518552 58580992 14155 4294967295 134512640 135094434 3221224448 3221223040 134557375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14302 14155 145 145 0 14157 0
[pid=32707] vsize: 57208
Current children cumulated CPU time (s) 548.8
Current children cumulated vsize (Kb) 59332

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14595 0 0 0 55773 106 0 0 25 0 1 0 1843518552 59326464 14337 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14484 14337 145 145 0 14339 0
[pid=32707] vsize: 57936
Current children cumulated CPU time (s) 558.79
Current children cumulated vsize (Kb) 60060

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 14930 0 0 0 56766 108 0 0 25 0 1 0 1843518552 60698624 14672 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 14819 14672 145 145 0 14674 0
[pid=32707] vsize: 59276
Current children cumulated CPU time (s) 568.74
Current children cumulated vsize (Kb) 61400

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 15280 0 0 0 57761 110 0 0 25 0 1 0 1843518552 62132224 15022 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 15169 15022 145 145 0 15024 0
[pid=32707] vsize: 60676
Current children cumulated CPU time (s) 578.71
Current children cumulated vsize (Kb) 62800

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 15646 0 0 0 58755 112 0 0 25 0 1 0 1843518552 63623168 15388 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 15533 15388 145 145 0 15388 0
[pid=32707] vsize: 62132
Current children cumulated CPU time (s) 588.67
Current children cumulated vsize (Kb) 64256

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 16036 0 0 0 59748 115 0 0 25 0 1 0 1843518552 65228800 15778 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 15925 15778 145 145 0 15780 0
[pid=32707] vsize: 63700
Current children cumulated CPU time (s) 598.63
Current children cumulated vsize (Kb) 65824

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 16330 0 0 0 60742 118 0 0 25 0 1 0 1843518552 66424832 16072 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 16217 16072 145 145 0 16072 0
[pid=32707] vsize: 64868
Current children cumulated CPU time (s) 608.6
Current children cumulated vsize (Kb) 66992

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 16581 0 0 0 61738 120 0 0 25 0 1 0 1843518552 67465216 16323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 16471 16323 145 145 0 16326 0
[pid=32707] vsize: 65884
Current children cumulated CPU time (s) 618.58
Current children cumulated vsize (Kb) 68008

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 16843 0 0 0 62732 123 0 0 25 0 1 0 1843518552 68530176 16585 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 16731 16585 145 145 0 16586 0
[pid=32707] vsize: 66924
Current children cumulated CPU time (s) 628.55
Current children cumulated vsize (Kb) 69048

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 17166 0 0 0 63729 124 0 0 25 0 1 0 1843518552 69849088 16908 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17053 16908 145 145 0 16908 0
[pid=32707] vsize: 68212
Current children cumulated CPU time (s) 638.53
Current children cumulated vsize (Kb) 70336

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 17505 0 0 0 64722 126 0 0 25 0 1 0 1843518552 71229440 17247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17390 17247 145 145 0 17245 0
[pid=32707] vsize: 69560
Current children cumulated CPU time (s) 648.48
Current children cumulated vsize (Kb) 71684

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 17829 0 0 0 65716 129 0 0 25 0 1 0 1843518552 72544256 17571 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17711 17571 145 145 0 17566 0
[pid=32707] vsize: 70844
Current children cumulated CPU time (s) 658.45
Current children cumulated vsize (Kb) 72968

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 66710 130 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 668.4
Current children cumulated vsize (Kb) 73924

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 67709 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 678.4
Current children cumulated vsize (Kb) 73924

[startup+690.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 68710 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 688.41
Current children cumulated vsize (Kb) 73924

[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 69710 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 698.41
Current children cumulated vsize (Kb) 73924

[startup+710.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 70710 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 708.41
Current children cumulated vsize (Kb) 73924

[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 71710 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 718.41
Current children cumulated vsize (Kb) 73924

[startup+730.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 72710 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223120 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 728.41
Current children cumulated vsize (Kb) 73924

[startup+740.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 73711 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 738.42
Current children cumulated vsize (Kb) 73924

[startup+750.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 74711 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 748.42
Current children cumulated vsize (Kb) 73924

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 75711 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 758.42
Current children cumulated vsize (Kb) 73924

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 76711 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223120 134556517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 768.42
Current children cumulated vsize (Kb) 73924

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 77711 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 778.42
Current children cumulated vsize (Kb) 73924

[startup+790.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 78712 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 788.43
Current children cumulated vsize (Kb) 73924

[startup+800.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 79712 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 798.43
Current children cumulated vsize (Kb) 73924

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 80712 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 808.43
Current children cumulated vsize (Kb) 73924

[startup+820.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 81712 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 818.43
Current children cumulated vsize (Kb) 73924

[startup+830.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 82713 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 828.44
Current children cumulated vsize (Kb) 73924

[startup+840.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 83713 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 838.44
Current children cumulated vsize (Kb) 73924

[startup+850.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 84713 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 848.44
Current children cumulated vsize (Kb) 73924

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 85713 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 858.44
Current children cumulated vsize (Kb) 73924

[startup+870.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18109 0 0 0 86714 131 0 0 25 0 1 0 1843518552 73523200 17811 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17811 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 868.45
Current children cumulated vsize (Kb) 73924

[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 87714 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 878.45
Current children cumulated vsize (Kb) 73924

[startup+890.075 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 88714 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 888.45
Current children cumulated vsize (Kb) 73924

[startup+900.075 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 89714 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 898.45
Current children cumulated vsize (Kb) 73924

[startup+910.076 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 90715 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 908.46
Current children cumulated vsize (Kb) 73924

[startup+920.078 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 91715 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 918.46
Current children cumulated vsize (Kb) 73924

[startup+930.078 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 92715 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 928.46
Current children cumulated vsize (Kb) 73924

[startup+940.079 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 93715 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 938.46
Current children cumulated vsize (Kb) 73924

[startup+950.08 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 94716 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 948.47
Current children cumulated vsize (Kb) 73924

[startup+960.081 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 95716 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 958.47
Current children cumulated vsize (Kb) 73924

[startup+970.082 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18110 0 0 0 96716 131 0 0 25 0 1 0 1843518552 73523200 17812 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17812 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 968.47
Current children cumulated vsize (Kb) 73924

[startup+980.083 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 97716 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 978.47
Current children cumulated vsize (Kb) 73924

[startup+990.083 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 98716 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 988.47
Current children cumulated vsize (Kb) 73924

[startup+1000.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 99716 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 998.47
Current children cumulated vsize (Kb) 73924

[startup+1010.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 100717 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1008.48
Current children cumulated vsize (Kb) 73924

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 101717 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1018.48
Current children cumulated vsize (Kb) 73924

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 102717 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1028.48
Current children cumulated vsize (Kb) 73924

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 103717 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1038.48
Current children cumulated vsize (Kb) 73924

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 104718 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1048.49
Current children cumulated vsize (Kb) 73924

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 105718 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1058.49
Current children cumulated vsize (Kb) 73924

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 106718 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1068.49
Current children cumulated vsize (Kb) 73924

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 107718 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1078.49
Current children cumulated vsize (Kb) 73924

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 108719 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223136 134554715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1088.5
Current children cumulated vsize (Kb) 73924

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 109719 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1098.5
Current children cumulated vsize (Kb) 73924

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 110719 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1108.5
Current children cumulated vsize (Kb) 73924

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 111720 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223136 134554700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1118.51
Current children cumulated vsize (Kb) 73924

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 112720 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1128.51
Current children cumulated vsize (Kb) 73924

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 113720 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1138.51
Current children cumulated vsize (Kb) 73924

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 114720 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1148.51
Current children cumulated vsize (Kb) 73924

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 115720 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1158.51
Current children cumulated vsize (Kb) 73924

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 116721 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1168.52
Current children cumulated vsize (Kb) 73924

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 117721 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1178.52
Current children cumulated vsize (Kb) 73924

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 118721 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1188.52
Current children cumulated vsize (Kb) 73924

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 119721 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1198.52
Current children cumulated vsize (Kb) 73924

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 120722 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1208.53
Current children cumulated vsize (Kb) 73924



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 32707
Raw data (/proc/32703/stat): 32703 (minisat+_script) S 32702 32703 21452 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843518547 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32703/statm): 531 226 485 147 0 384 0
[pid=32703] vsize: 2124
Raw data (/proc/32707/stat): 32707 (minisat+_64-bit) R 32703 32703 21452 0 -1 0 18111 0 0 0 120722 131 0 0 25 0 1 0 1843518552 73523200 17813 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32707/statm): 17950 17813 145 145 0 17805 0
[pid=32707] vsize: 71800
Current children cumulated CPU time (s) 1208.53
Current children cumulated vsize (Kb) 73924

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.58
CPU user time (s): 1207.23
CPU system time (s): 1.34979
CPU usage (%): 99.8707
Max. virtual memory (cumulated for all children) (Kb): 73924

Verifier Data

ERROR: no interpretation found !