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/frb56-25-opb/normalized-frb56-25-4.opb
MD5SUMe21d47f954166f353681a275b560afba
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -41
Optimality of the best value was proved NO
Number of terms in the objective function 1400
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 1400
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1400
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1203.66
Number of variables1400
Total number of constraints110038
Number of constraints which are clauses110038
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 2315

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        917268 kB
Buffers:         35108 kB
Cached:          55308 kB
SwapCached:        228 kB
Active:          68832 kB
Inactive:        24536 kB
HighTotal:      131008 kB
HighFree:        71904 kB
LowTotal:       903652 kB
LowFree:        845364 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18396 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:13:19 (client local time) WITH STATUS 10 IN 1207.22 SECONDS
stats: 2717 7 1207.22 10

Solver Data

c Parsing PB file...
c Converting 110038 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 |  110038   220076 |   36679       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:78076     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  193767   416453 |   64589       0        0     nan |  0.000 % |
c |       100 |  193211   415303 |   71047      71      567     8.0 |  0.523 % |
c |       250 |  192296   413340 |   78152     193     1687     8.7 |  1.443 % |
c |       475 |  190686   409826 |   85967     345     4411    12.8 |  3.114 % |
c |       812 |  189125   406459 |   94564     630     6997    11.1 |  4.700 % |
c |      1318 |  186296   400188 |  104021    1000    11394    11.4 |  7.721 % |
c |      2077 |  181158   388688 |  114423    1569    17663    11.3 | 13.295 % |
c |      3216 |  173643   371821 |  125865    2397    27786    11.6 | 21.467 % |
c |      4924 |  165143   352394 |  138452    3575    41683    11.7 | 30.985 % |
c |      7486 |  153437   325407 |  152297    5345    66987    12.5 | 44.181 % |
c |     11330 |  141122   296343 |  167527    7819    99133    12.7 | 58.622 % |
c |     17097 |  130209   270346 |  184279   11567   161806    14.0 | 71.611 % |
c ==============================================================================
c Found solution: -42
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18566 |  128729   266792 |   42909   12571   182083    14.5 | 71.611 % |
c |     18666 |  128551   266373 |   47199   12611   182963    14.5 | 73.626 % |
c |     18816 |  128445   266115 |   51919   12742   184752    14.5 | 73.759 % |
c |     19041 |  127939   264905 |   57111   12835   186093    14.5 | 74.370 % |
c |     19378 |  127939   264905 |   62823   13172   193447    14.7 | 74.370 % |
c |     19884 |  127611   264143 |   69105   13513   204336    15.1 | 74.751 % |
c |     20644 |  127200   263140 |   76015   14084   218616    15.5 | 75.260 % |
c |     21783 |  126721   261991 |   83617   15017   237295    15.8 | 75.841 % |
c ==============================================================================
c Found solution: -43
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22546 |  126525   261588 |   42175   15588   259656    16.7 | 75.841 % |
c |     22647 |  126182   260749 |   46392   15599   260038    16.7 | 76.562 % |
c |     22799 |  126172   260725 |   51031   15750   262977    16.7 | 76.574 % |
c |     23024 |  126057   260455 |   56134   15916   268753    16.9 | 76.707 % |
c |     23361 |  126057   260455 |   61748   16253   280191    17.2 | 76.707 % |
c |     23867 |  125749   259709 |   67923   16626   292865    17.6 | 77.086 % |
c |     24628 |  125481   259056 |   74715   17132   307189    17.9 | 77.420 % |
c |     25767 |  125214   258403 |   82187   18114   345667    19.1 | 77.751 % |
c ==============================================================================
c Found solution: -44
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27463 |  124678   257111 |   41559   19343   381365    19.7 | 77.751 % |
c |     27563 |  124664   257081 |   45714   19429   383445    19.7 | 78.418 % |
c |     27713 |  124617   256960 |   50286   19546   386496    19.8 | 78.483 % |
c |     27938 |  124421   256474 |   55315   19639   390151    19.9 | 78.735 % |
c |     28275 |  124368   256346 |   60846   19905   399588    20.1 | 78.800 % |
c |     28781 |  124219   255995 |   66931   20357   418681    20.6 | 78.976 % |
c |     29540 |  123568   254406 |   73624   20735   434974    21.0 | 79.786 % |
c |     30679 |  123324   253817 |   80986   21711   475126    21.9 | 80.080 % |
c |     32387 |  123105   253279 |   89085   23245   534203    23.0 | 80.353 % |
c |     34949 |  122598   252034 |   97993   25509   655764    25.7 | 80.984 % |
c |     38794 |  122155   250955 |  107793   29028   828204    28.5 | 81.525 % |
c ==============================================================================
c Found solution: -45
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42330 |  122073   250778 |   40691   32394  1050976    32.4 | 81.525 % |
c |     42430 |  121963   250525 |   44760   32424  1051305    32.4 | 81.759 % |
c |     42580 |  121924   250432 |   49236   32452  1053238    32.5 | 81.807 % |
c |     42805 |  121916   250414 |   54159   32642  1059551    32.5 | 81.815 % |
c |     43142 |  121909   250399 |   59575   32975  1079180    32.7 | 81.822 % |
c |     43649 |  121762   250044 |   65533   33418  1099764    32.9 | 82.003 % |
c |     44409 |  121635   249732 |   72086   34086  1132460    33.2 | 82.160 % |
c |     45549 |  121592   249637 |   79295   35182  1198499    34.1 | 82.206 % |
c ==============================================================================
c Found solution: -46
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46735 |  121306   248888 |   40435   35907  1285951    35.8 | 82.206 % |
c |     46835 |  121264   248786 |   44478   35960  1288209    35.8 | 82.623 % |
c |     46985 |  121264   248786 |   48926   36110  1295337    35.9 | 82.623 % |
c |     47211 |  121125   248464 |   53818   36215  1301784    35.9 | 82.782 % |
c |     47548 |  121125   248464 |   59200   36552  1323780    36.2 | 82.782 % |
c |     48056 |  121085   248366 |   65120   37018  1357054    36.7 | 82.831 % |
c |     48816 |  121038   248253 |   71633   37741  1396995    37.0 | 82.889 % |
c |     49957 |  121038   248253 |   78796   38882  1491934    38.4 | 82.889 % |
c |     51665 |  120776   247607 |   86676   40316  1593143    39.5 | 83.220 % |
c |     54227 |  120578   247108 |   95343   42660  1731750    40.6 | 83.482 % |
c |     58071 |  120466   246838 |  104877   46186  2175305    47.1 | 83.621 % |
c ==============================================================================
c Found solution: -47
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60431 |  120513   246983 |   40171   48546  2396212    49.4 | 83.621 % |
c |     60532 |  120390   246680 |   44188   48589  2397470    49.3 | 83.755 % |
c |     60682 |  120383   246663 |   48606   48619  2401968    49.4 | 83.763 % |
c |     60908 |  120383   246663 |   53467   48845  2416094    49.5 | 83.763 % |
c |     61245 |  120379   246653 |   58814   49181  2436369    49.5 | 83.769 % |
c |     61751 |  120334   246550 |   64695   49651  2463070    49.6 | 83.819 % |
c |     62510 |  120334   246550 |   71165   50410  2525544    50.1 | 83.819 % |
c |     63649 |  120329   246539 |   78281   51547  2594009    50.3 | 83.824 % |
c |     65357 |  120324   246528 |   86110   53252  2746627    51.6 | 83.830 % |
c |     67920 |  120284   246428 |   94721   55627  3049475    54.8 | 83.880 % |
c |     71764 |  120284   246428 |  104193   59471  3664380    61.6 | 83.880 % |
c |     77531 |  120274   246404 |  114612   65223  4262331    65.4 | 83.893 % |
c |     86180 |  120039   245833 |  126073   73304  5452615    74.4 | 84.182 % |
c |     99154 |  119824   245314 |  138681   85604  7053597    82.4 | 84.444 % |
c |    118615 |  119399   244284 |  152549  104335  9894511    94.8 | 84.960 % |
c ==============================================================================
c Found solution: -48
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131166 |  119128   243585 |   39709  115450 11394890    98.7 | 84.960 % |
c |    131266 |  119128   243585 |   43679   25589  1732926    67.7 | 85.318 % |
c |    131416 |  119109   243538 |   48047   25717  1737032    67.5 | 85.343 % |
c |    131641 |  119109   243538 |   52852   25942  1754432    67.6 | 85.343 % |
c |    131978 |  119109   243538 |   58137   26279  1788678    68.1 | 85.343 % |
c |    132485 |  119109   243538 |   63951   26786  1831948    68.4 | 85.343 % |
c |    133246 |  119103   243524 |   70346   27545  1879086    68.2 | 85.350 % |
c |    134385 |  119103   243524 |   77381   28684  2005655    69.9 | 85.350 % |
c |    136093 |  119103   243524 |   85119   30392  2181580    71.8 | 85.350 % |
c |    138655 |  119018   243320 |   93631   32806  2505869    76.4 | 85.453 % |
c |    142499 |  118947   243149 |  102994   36618  2957459    80.8 | 85.540 % |
c |    148265 |  118904   243048 |  113294   42373  3999187    94.4 | 85.591 % |
c |    156914 |  118778   242752 |  124623   50901  5151512   101.2 | 85.739 % |
c |    169890 |  118778   242752 |  137086   63877  7363093   115.3 | 85.739 % |
c |    189352 |  118712   242584 |  150794   83215 10573767   127.1 | 85.828 % |
c ==============================================================================
c Found solution: -49
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192438 |  118734   242648 |   39578   86301 11024722   127.7 | 85.828 % |
c |    192538 |  118734   242648 |   43535   86401 11032497   127.7 | 85.811 % |
c |    192688 |  118734   242648 |   47889   86551 11044645   127.6 | 85.811 % |
c |    192914 |  118734   242648 |   52678   86777 11050467   127.3 | 85.811 % |
c |    193252 |  118660   242476 |   57946   87109 11062072   127.0 | 85.897 % |
c |    193758 |  118660   242476 |   63740   87615 11140756   127.2 | 85.897 % |
c |    194517 |  118651   242455 |   70114   88372 11223980   127.0 | 85.907 % |
c |    195660 |  118651   242455 |   77126   89515 11423672   127.6 | 85.907 % |
c |    197369 |  118651   242455 |   84838   91224 11599410   127.2 | 85.907 % |
c |    199931 |  118651   242455 |   93322   93786 11943051   127.3 | 85.907 % |
c |    203776 |  118619   242379 |  102655   97621 12547536   128.5 | 85.946 % |
c |    209542 |  118619   242379 |  112920  103387 13545077   131.0 | 85.946 % |
c |    218192 |  118619   242379 |  124212  112037 14738228   131.5 | 85.946 % |
c |    231166 |  118619   242379 |  136633  125011 16463619   131.7 | 85.946 % |
c |    250628 |  118619   242379 |  150297  144473 19099031   132.2 | 85.946 % |
c |    279820 |  118619   242379 |  165327  173665 23277081   134.0 | 85.946 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 -C1383 -C1382 C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -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 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C1

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/31341/stat): 31341 (minisat+_script) R 31340 31341 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785373497 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/31341/statm): 174 3 169 147 0 27 0
[pid=31341] 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=31342
New process pid=31343
New process pid=31344
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=31343) exited with status: 0
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=31344) exited with status: 0
One traced child (pid=31342) exited with status: 0
New process pid=31345
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-frb56-25-4.opb

[startup+10.0035 s]
Raw data (loadavg): 0.95 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 944 31 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 30216

[startup+20.004 s]
Raw data (loadavg): 0.96 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 1943 31 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 30216

[startup+30.0056 s]
Raw data (loadavg): 0.97 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 2943 32 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 30216

[startup+40.0061 s]
Raw data (loadavg): 0.97 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 3942 32 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 30216

[startup+50.0077 s]
Raw data (loadavg): 0.97 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 4942 33 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 30216

[startup+60.0083 s]
Raw data (loadavg): 0.98 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 5942 33 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 30216

[startup+70.0088 s]
Raw data (loadavg): 0.98 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 6941 33 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 69.74
Current children cumulated vsize (Kb) 30216

[startup+80.0104 s]
Raw data (loadavg): 0.98 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 7941 34 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 79.75
Current children cumulated vsize (Kb) 30216

[startup+90.0109 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 8940 34 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223124 134553436 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 30216

[startup+100.013 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 9940 35 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 99.75
Current children cumulated vsize (Kb) 30216

[startup+110.013 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 10939 36 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 109.75
Current children cumulated vsize (Kb) 30216

[startup+120.014 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 11939 36 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 119.75
Current children cumulated vsize (Kb) 30216

[startup+130.014 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 12938 37 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 129.75
Current children cumulated vsize (Kb) 30216

[startup+140.015 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6869 0 0 0 13938 37 0 0 25 0 1 0 1785373502 28766208 6856 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 7023 6856 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 139.75
Current children cumulated vsize (Kb) 30216

[startup+150.016 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 6916 0 0 0 14939 37 0 0 25 0 1 0 1785373502 28766208 6865 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 7023 6865 145 145 0 6878 0
[pid=31345] vsize: 28092
Current children cumulated CPU time (s) 149.76
Current children cumulated vsize (Kb) 30216

[startup+160.017 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 7070 0 0 0 15936 38 0 0 25 0 1 0 1785373502 29396992 7019 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 7177 7019 145 145 0 7032 0
[pid=31345] vsize: 28708
Current children cumulated CPU time (s) 159.74
Current children cumulated vsize (Kb) 30832

[startup+170.016 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 7395 0 0 0 16929 41 0 0 25 0 1 0 1785373502 30728192 7344 4294967295 134512640 135094434 3221224448 3221223040 134557494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7502 7344 145 145 0 7357 0
[pid=31345] vsize: 30008
Current children cumulated CPU time (s) 169.7
Current children cumulated vsize (Kb) 32132

[startup+180.017 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 7803 0 0 0 17922 43 0 0 25 0 1 0 1785373502 32219136 7677 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 7866 7677 145 145 0 7721 0
[pid=31345] vsize: 31464
Current children cumulated CPU time (s) 179.65
Current children cumulated vsize (Kb) 33588

[startup+190.019 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 8187 0 0 0 18915 45 0 0 25 0 1 0 1785373502 33472512 7986 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 8172 7986 145 145 0 8027 0
[pid=31345] vsize: 32688
Current children cumulated CPU time (s) 189.6
Current children cumulated vsize (Kb) 34812

[startup+200.019 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 8528 0 0 0 19908 49 0 0 25 0 1 0 1785373502 34852864 8327 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 8509 8327 145 145 0 8364 0
[pid=31345] vsize: 34036
Current children cumulated CPU time (s) 199.57
Current children cumulated vsize (Kb) 36160

[startup+210.02 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 9022 0 0 0 20899 53 0 0 25 0 1 0 1785373502 36859904 8821 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 8999 8821 145 145 0 8854 0
[pid=31345] vsize: 35996
Current children cumulated CPU time (s) 209.52
Current children cumulated vsize (Kb) 38120

[startup+220.02 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 9465 0 0 0 21891 56 0 0 25 0 1 0 1785373502 38350848 9189 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 9363 9189 145 145 0 9218 0
[pid=31345] vsize: 37452
Current children cumulated CPU time (s) 219.47
Current children cumulated vsize (Kb) 39576

[startup+230.021 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 9850 0 0 0 22885 60 0 0 25 0 1 0 1785373502 39907328 9574 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 9743 9574 145 145 0 9598 0
[pid=31345] vsize: 38972
Current children cumulated CPU time (s) 229.45
Current children cumulated vsize (Kb) 41096

[startup+240.021 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 10347 0 0 0 23875 63 0 0 25 0 1 0 1785373502 41926656 10071 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 10236 10071 145 145 0 10091 0
[pid=31345] vsize: 40944
Current children cumulated CPU time (s) 239.38
Current children cumulated vsize (Kb) 43068

[startup+250.021 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 10895 0 0 0 24865 67 0 0 25 0 1 0 1785373502 44158976 10619 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 10781 10619 145 145 0 10636 0
[pid=31345] vsize: 43124
Current children cumulated CPU time (s) 249.32
Current children cumulated vsize (Kb) 45248

[startup+260.021 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 11281 0 0 0 25858 70 0 0 25 0 1 0 1785373502 45727744 11005 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 11164 11005 145 145 0 11019 0
[pid=31345] vsize: 44656
Current children cumulated CPU time (s) 259.28
Current children cumulated vsize (Kb) 46780

[startup+270.021 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 11648 0 0 0 26852 72 0 0 25 0 1 0 1785373502 47480832 11372 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 11592 11372 145 145 0 11447 0
[pid=31345] vsize: 46368
Current children cumulated CPU time (s) 269.24
Current children cumulated vsize (Kb) 48492

[startup+280.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 12104 0 0 0 27845 76 0 0 25 0 1 0 1785373502 49336320 11828 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 12045 11828 145 145 0 11900 0
[pid=31345] vsize: 48180
Current children cumulated CPU time (s) 279.21
Current children cumulated vsize (Kb) 50304

[startup+290.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 12594 0 0 0 28835 80 0 0 25 0 1 0 1785373502 51335168 12318 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 12533 12318 145 145 0 12388 0
[pid=31345] vsize: 50132
Current children cumulated CPU time (s) 289.15
Current children cumulated vsize (Kb) 52256

[startup+300.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 12966 0 0 0 29827 83 0 0 25 0 1 0 1785373502 52846592 12690 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 12902 12690 145 145 0 12757 0
[pid=31345] vsize: 51608
Current children cumulated CPU time (s) 299.1
Current children cumulated vsize (Kb) 53732

[startup+310.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 13334 0 0 0 30820 86 0 0 25 0 1 0 1785373502 54341632 13058 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 13267 13058 145 145 0 13122 0
[pid=31345] vsize: 53068
Current children cumulated CPU time (s) 309.06
Current children cumulated vsize (Kb) 55192

[startup+320.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 13615 0 0 0 31815 88 0 0 25 0 1 0 1785373502 55484416 13339 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 13546 13339 145 145 0 13401 0
[pid=31345] vsize: 54184
Current children cumulated CPU time (s) 319.03
Current children cumulated vsize (Kb) 56308

[startup+330.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 14031 0 0 0 32808 91 0 0 25 0 1 0 1785373502 57176064 13755 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 13959 13755 145 145 0 13814 0
[pid=31345] vsize: 55836
Current children cumulated CPU time (s) 328.99
Current children cumulated vsize (Kb) 57960

[startup+340.023 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 14452 0 0 0 33799 95 0 0 25 0 1 0 1785373502 58892288 14176 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 14378 14176 145 145 0 14233 0
[pid=31345] vsize: 57512
Current children cumulated CPU time (s) 338.94
Current children cumulated vsize (Kb) 59636

[startup+350.022 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 14774 0 0 0 34793 98 0 0 25 0 1 0 1785373502 60198912 14498 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 14697 14498 145 145 0 14552 0
[pid=31345] vsize: 58788
Current children cumulated CPU time (s) 348.91
Current children cumulated vsize (Kb) 60912

[startup+360.023 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 15172 0 0 0 35786 100 0 0 25 0 1 0 1785373502 61816832 14896 4294967295 134512640 135094434 3221224448 3221223040 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 15092 14896 145 145 0 14947 0
[pid=31345] vsize: 60368
Current children cumulated CPU time (s) 358.86
Current children cumulated vsize (Kb) 62492

[startup+370.024 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 15517 0 0 0 36779 103 0 0 25 0 1 0 1785373502 63221760 15241 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 15435 15241 145 145 0 15290 0
[pid=31345] vsize: 61740
Current children cumulated CPU time (s) 368.82
Current children cumulated vsize (Kb) 63864

[startup+380.024 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 16080 0 0 0 37769 108 0 0 25 0 1 0 1785373502 65519616 15804 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 15996 15804 145 145 0 15851 0
[pid=31345] vsize: 63984
Current children cumulated CPU time (s) 378.77
Current children cumulated vsize (Kb) 66108

[startup+390.025 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 16430 0 0 0 38763 111 0 0 25 0 1 0 1785373502 66945024 16154 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 16344 16154 145 145 0 16199 0
[pid=31345] vsize: 65376
Current children cumulated CPU time (s) 388.74
Current children cumulated vsize (Kb) 67500

[startup+400.025 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 16762 0 0 0 39758 113 0 0 25 0 1 0 1785373502 68296704 16486 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 16674 16486 145 145 0 16529 0
[pid=31345] vsize: 66696
Current children cumulated CPU time (s) 398.71
Current children cumulated vsize (Kb) 68820

[startup+410.026 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 17173 0 0 0 40751 115 0 0 25 0 1 0 1785373502 69971968 16897 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 17083 16897 145 145 0 16938 0
[pid=31345] vsize: 68332
Current children cumulated CPU time (s) 408.66
Current children cumulated vsize (Kb) 70456

[startup+420.025 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 17333 0 0 0 41749 116 0 0 25 0 1 0 1785373502 70623232 17057 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 17242 17057 145 145 0 17097 0
[pid=31345] vsize: 68968
Current children cumulated CPU time (s) 418.65
Current children cumulated vsize (Kb) 71092

[startup+430.027 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 17616 0 0 0 42744 118 0 0 25 0 1 0 1785373502 71770112 17340 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 17522 17340 145 145 0 17377 0
[pid=31345] vsize: 70088
Current children cumulated CPU time (s) 428.62
Current children cumulated vsize (Kb) 72212

[startup+440.028 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 17700 0 0 0 43742 118 0 0 25 0 1 0 1785373502 72110080 17424 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 17605 17424 145 145 0 17460 0
[pid=31345] vsize: 70420
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 72544

[startup+450.027 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 18165 0 0 0 44734 121 0 0 25 0 1 0 1785373502 74006528 17889 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 18068 17889 145 145 0 17923 0
[pid=31345] vsize: 72272
Current children cumulated CPU time (s) 448.55
Current children cumulated vsize (Kb) 74396

[startup+460.028 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 18542 0 0 0 45727 124 0 0 25 0 1 0 1785373502 75542528 18266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 18443 18266 145 145 0 18298 0
[pid=31345] vsize: 73772
Current children cumulated CPU time (s) 458.51
Current children cumulated vsize (Kb) 75896

[startup+470.028 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 18849 0 0 0 46721 126 0 0 25 0 1 0 1785373502 76791808 18573 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 18748 18573 145 145 0 18603 0
[pid=31345] vsize: 74992
Current children cumulated CPU time (s) 468.47
Current children cumulated vsize (Kb) 77116

[startup+480.029 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19129 0 0 0 47717 128 0 0 25 0 1 0 1785373502 77930496 18853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19026 18853 145 145 0 18881 0
[pid=31345] vsize: 76104
Current children cumulated CPU time (s) 478.45
Current children cumulated vsize (Kb) 78228

[startup+490.029 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 48716 128 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 488.44
Current children cumulated vsize (Kb) 78456

[startup+500.03 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 49716 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 498.45
Current children cumulated vsize (Kb) 78456

[startup+510.03 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 50716 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 508.45
Current children cumulated vsize (Kb) 78456

[startup+520.031 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 51717 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 518.46
Current children cumulated vsize (Kb) 78456

[startup+530.032 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 52717 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223120 134556505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 528.46
Current children cumulated vsize (Kb) 78456

[startup+540.032 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 53717 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 538.46
Current children cumulated vsize (Kb) 78456

[startup+550.032 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 54717 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 548.46
Current children cumulated vsize (Kb) 78456

[startup+560.032 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 55718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 558.47
Current children cumulated vsize (Kb) 78456

[startup+570.033 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 56718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 568.47
Current children cumulated vsize (Kb) 78456

[startup+580.033 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 57718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 578.47
Current children cumulated vsize (Kb) 78456

[startup+590.034 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 58718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 588.47
Current children cumulated vsize (Kb) 78456

[startup+600.034 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 59718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 598.47
Current children cumulated vsize (Kb) 78456

[startup+610.034 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 60718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 608.47
Current children cumulated vsize (Kb) 78456

[startup+620.034 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 61718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 618.47
Current children cumulated vsize (Kb) 78456

[startup+630.034 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 62719 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 628.48
Current children cumulated vsize (Kb) 78456

[startup+640.035 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 63719 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 638.48
Current children cumulated vsize (Kb) 78456

[startup+650.035 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 64719 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 648.48
Current children cumulated vsize (Kb) 78456

[startup+660.036 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 65719 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 658.48
Current children cumulated vsize (Kb) 78456

[startup+670.035 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 66719 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 668.48
Current children cumulated vsize (Kb) 78456

[startup+680.036 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 67720 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 678.49
Current children cumulated vsize (Kb) 78456

[startup+690.037 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19262 0 0 0 68718 129 0 0 25 0 1 0 1785373502 78163968 18911 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 19083 18911 145 145 0 18938 0
[pid=31345] vsize: 76332
Current children cumulated CPU time (s) 688.47
Current children cumulated vsize (Kb) 78456

[startup+700.036 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19539 0 0 0 69712 132 0 0 25 0 1 0 1785373502 79298560 19188 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31345/statm): 19360 19188 145 145 0 19215 0
[pid=31345] vsize: 77440
Current children cumulated CPU time (s) 698.44
Current children cumulated vsize (Kb) 79564

[startup+710.038 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 19883 0 0 0 70705 134 0 0 25 0 1 0 1785373502 80707584 19532 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 19704 19532 145 145 0 19559 0
[pid=31345] vsize: 78816
Current children cumulated CPU time (s) 708.39
Current children cumulated vsize (Kb) 80940

[startup+720.038 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 20218 0 0 0 71699 137 0 0 24 0 1 0 1785373502 82079744 19867 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 20039 19867 145 145 0 19894 0
[pid=31345] vsize: 80156
Current children cumulated CPU time (s) 718.36
Current children cumulated vsize (Kb) 82280

[startup+730.039 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 20568 0 0 0 72693 139 0 0 25 0 1 0 1785373502 83513344 20217 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 20389 20217 145 145 0 20244 0
[pid=31345] vsize: 81556
Current children cumulated CPU time (s) 728.32
Current children cumulated vsize (Kb) 83680

[startup+740.039 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 20904 0 0 0 73688 141 0 0 25 0 1 0 1785373502 84889600 20553 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 20725 20553 145 145 0 20580 0
[pid=31345] vsize: 82900
Current children cumulated CPU time (s) 738.29
Current children cumulated vsize (Kb) 85024

[startup+750.04 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 21255 0 0 0 74682 143 0 0 25 0 1 0 1785373502 86327296 20904 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 21076 20904 145 145 0 20931 0
[pid=31345] vsize: 84304
Current children cumulated CPU time (s) 748.25
Current children cumulated vsize (Kb) 86428

[startup+760.04 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 21616 0 0 0 75675 147 0 0 25 0 1 0 1785373502 87805952 21265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 21437 21265 145 145 0 21292 0
[pid=31345] vsize: 85748
Current children cumulated CPU time (s) 758.22
Current children cumulated vsize (Kb) 87872

[startup+770.041 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 21906 0 0 0 76670 150 0 0 25 0 1 0 1785373502 88993792 21555 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 21727 21555 145 145 0 21582 0
[pid=31345] vsize: 86908
Current children cumulated CPU time (s) 768.2
Current children cumulated vsize (Kb) 89032

[startup+780.042 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 22161 0 0 0 77665 152 0 0 25 0 1 0 1785373502 90038272 21810 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 21982 21810 145 145 0 21837 0
[pid=31345] vsize: 87928
Current children cumulated CPU time (s) 778.17
Current children cumulated vsize (Kb) 90052

[startup+790.042 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 22460 0 0 0 78661 153 0 0 25 0 1 0 1785373502 91262976 22109 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 22281 22109 145 145 0 22136 0
[pid=31345] vsize: 89124
Current children cumulated CPU time (s) 788.14
Current children cumulated vsize (Kb) 91248

[startup+800.042 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 22743 0 0 0 79656 155 0 0 25 0 1 0 1785373502 92422144 22392 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 22564 22392 145 145 0 22419 0
[pid=31345] vsize: 90256
Current children cumulated CPU time (s) 798.11
Current children cumulated vsize (Kb) 92380

[startup+810.042 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 22970 0 0 0 80652 157 0 0 25 0 1 0 1785373502 93351936 22619 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 22791 22619 145 145 0 22646 0
[pid=31345] vsize: 91164
Current children cumulated CPU time (s) 808.09
Current children cumulated vsize (Kb) 93288

[startup+820.043 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 23295 0 0 0 81646 160 0 0 25 0 1 0 1785373502 94687232 22944 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 23117 22944 145 145 0 22972 0
[pid=31345] vsize: 92468
Current children cumulated CPU time (s) 818.06
Current children cumulated vsize (Kb) 94592

[startup+830.043 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 23564 0 0 0 82641 162 0 0 25 0 1 0 1785373502 95780864 23213 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 23384 23213 145 145 0 23239 0
[pid=31345] vsize: 93536
Current children cumulated CPU time (s) 828.03
Current children cumulated vsize (Kb) 95660

[startup+840.044 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 23846 0 0 0 83636 164 0 0 25 0 1 0 1785373502 96927744 23495 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 23664 23495 145 145 0 23519 0
[pid=31345] vsize: 94656
Current children cumulated CPU time (s) 838
Current children cumulated vsize (Kb) 96780

[startup+850.045 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 24106 0 0 0 84631 166 0 0 25 0 1 0 1785373502 97984512 23755 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 23922 23755 145 145 0 23777 0
[pid=31345] vsize: 95688
Current children cumulated CPU time (s) 847.97
Current children cumulated vsize (Kb) 97812

[startup+860.045 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 24370 0 0 0 85626 167 0 0 25 0 1 0 1785373502 99061760 24019 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 24185 24019 145 145 0 24040 0
[pid=31345] vsize: 96740
Current children cumulated CPU time (s) 857.93
Current children cumulated vsize (Kb) 98864

[startup+870.046 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 24592 0 0 0 86622 169 0 0 25 0 1 0 1785373502 99966976 24241 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 24406 24241 145 145 0 24261 0
[pid=31345] vsize: 97624
Current children cumulated CPU time (s) 867.91
Current children cumulated vsize (Kb) 99748

[startup+880.046 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 24813 0 0 0 87618 171 0 0 25 0 1 0 1785373502 100868096 24462 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 24626 24462 145 145 0 24481 0
[pid=31345] vsize: 98504
Current children cumulated CPU time (s) 877.89
Current children cumulated vsize (Kb) 100628

[startup+890.047 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 25081 0 0 0 88613 173 0 0 25 0 1 0 1785373502 101961728 24730 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 24893 24730 145 145 0 24748 0
[pid=31345] vsize: 99572
Current children cumulated CPU time (s) 887.86
Current children cumulated vsize (Kb) 101696

[startup+900.046 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 25341 0 0 0 89608 175 0 0 25 0 1 0 1785373502 103542784 24990 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 25279 24990 145 145 0 25134 0
[pid=31345] vsize: 101116
Current children cumulated CPU time (s) 897.83
Current children cumulated vsize (Kb) 103240

[startup+910.047 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 25600 0 0 0 90604 177 0 0 25 0 1 0 1785373502 104595456 25249 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 25536 25249 145 145 0 25391 0
[pid=31345] vsize: 102144
Current children cumulated CPU time (s) 907.81
Current children cumulated vsize (Kb) 104268

[startup+920.048 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 25857 0 0 0 91599 179 0 0 25 0 1 0 1785373502 105639936 25506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 25791 25506 145 145 0 25646 0
[pid=31345] vsize: 103164
Current children cumulated CPU time (s) 917.78
Current children cumulated vsize (Kb) 105288

[startup+930.048 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 26125 0 0 0 92595 181 0 0 25 0 1 0 1785373502 106733568 25774 4294967295 134512640 135094434 3221224448 3221223104 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 26058 25774 145 145 0 25913 0
[pid=31345] vsize: 104232
Current children cumulated CPU time (s) 927.76
Current children cumulated vsize (Kb) 106356

[startup+940.049 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 26367 0 0 0 93591 183 0 0 25 0 1 0 1785373502 107712512 26016 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 26297 26016 145 145 0 26152 0
[pid=31345] vsize: 105188
Current children cumulated CPU time (s) 937.74
Current children cumulated vsize (Kb) 107312

[startup+950.049 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 26667 0 0 0 94587 185 0 0 25 0 1 0 1785373502 108924928 26316 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 26593 26316 145 145 0 26448 0
[pid=31345] vsize: 106372
Current children cumulated CPU time (s) 947.72
Current children cumulated vsize (Kb) 108496

[startup+960.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 26945 0 0 0 95581 187 0 0 25 0 1 0 1785373502 110059520 26594 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 26870 26594 145 145 0 26725 0
[pid=31345] vsize: 107480
Current children cumulated CPU time (s) 957.68
Current children cumulated vsize (Kb) 109604

[startup+970.049 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 27217 0 0 0 96576 189 0 0 25 0 1 0 1785373502 111165440 26866 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 27140 26866 145 145 0 26995 0
[pid=31345] vsize: 108560
Current children cumulated CPU time (s) 967.65
Current children cumulated vsize (Kb) 110684

[startup+980.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 27446 0 0 0 97572 191 0 0 25 0 1 0 1785373502 112095232 27095 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 27367 27095 145 145 0 27222 0
[pid=31345] vsize: 109468
Current children cumulated CPU time (s) 977.63
Current children cumulated vsize (Kb) 111592

[startup+990.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 27643 0 0 0 98569 193 0 0 25 0 1 0 1785373502 112898048 27292 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 27563 27292 145 145 0 27418 0
[pid=31345] vsize: 110252
Current children cumulated CPU time (s) 987.62
Current children cumulated vsize (Kb) 112376

[startup+1000.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 27871 0 0 0 99565 195 0 0 25 0 1 0 1785373502 113823744 27520 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 27789 27520 145 145 0 27644 0
[pid=31345] vsize: 111156
Current children cumulated CPU time (s) 997.6
Current children cumulated vsize (Kb) 113280

[startup+1010.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 28045 0 0 0 100561 196 0 0 25 0 1 0 1785373502 114532352 27694 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 27962 27694 145 145 0 27817 0
[pid=31345] vsize: 111848
Current children cumulated CPU time (s) 1007.57
Current children cumulated vsize (Kb) 113972

[startup+1020.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 28251 0 0 0 101558 197 0 0 25 0 1 0 1785373502 115367936 27900 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 28166 27900 145 145 0 28021 0
[pid=31345] vsize: 112664
Current children cumulated CPU time (s) 1017.55
Current children cumulated vsize (Kb) 114788

[startup+1030.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 28494 0 0 0 102554 198 0 0 25 0 1 0 1785373502 116355072 28143 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 28407 28143 145 145 0 28262 0
[pid=31345] vsize: 113628
Current children cumulated CPU time (s) 1027.52
Current children cumulated vsize (Kb) 115752

[startup+1040.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 28761 0 0 0 103551 200 0 0 25 0 1 0 1785373502 117448704 28410 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 28674 28410 145 145 0 28529 0
[pid=31345] vsize: 114696
Current children cumulated CPU time (s) 1037.51
Current children cumulated vsize (Kb) 116820

[startup+1050.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 29026 0 0 0 104546 202 0 0 25 0 1 0 1785373502 118525952 28675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 28937 28675 145 145 0 28792 0
[pid=31345] vsize: 115748
Current children cumulated CPU time (s) 1047.48
Current children cumulated vsize (Kb) 117872

[startup+1060.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 29271 0 0 0 105542 204 0 0 25 0 1 0 1785373502 119525376 28920 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 29181 28920 145 145 0 29036 0
[pid=31345] vsize: 116724
Current children cumulated CPU time (s) 1057.46
Current children cumulated vsize (Kb) 118848

[startup+1070.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 29524 0 0 0 106537 206 0 0 25 0 1 0 1785373502 120553472 29173 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 29432 29173 145 145 0 29287 0
[pid=31345] vsize: 117728
Current children cumulated CPU time (s) 1067.43
Current children cumulated vsize (Kb) 119852

[startup+1080.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 29749 0 0 0 107533 208 0 0 25 0 1 0 1785373502 121470976 29398 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 29656 29398 145 145 0 29511 0
[pid=31345] vsize: 118624
Current children cumulated CPU time (s) 1077.41
Current children cumulated vsize (Kb) 120748

[startup+1090.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 29958 0 0 0 108530 209 0 0 25 0 1 0 1785373502 122327040 29607 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 29865 29607 145 145 0 29720 0
[pid=31345] vsize: 119460
Current children cumulated CPU time (s) 1087.39
Current children cumulated vsize (Kb) 121584

[startup+1100.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 30172 0 0 0 109527 211 0 0 25 0 1 0 1785373502 123195392 29821 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 30077 29821 145 145 0 29932 0
[pid=31345] vsize: 120308
Current children cumulated CPU time (s) 1097.38
Current children cumulated vsize (Kb) 122432

[startup+1110.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 30388 0 0 0 110524 212 0 0 25 0 1 0 1785373502 124076032 30037 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 30292 30037 145 145 0 30147 0
[pid=31345] vsize: 121168
Current children cumulated CPU time (s) 1107.36
Current children cumulated vsize (Kb) 123292

[startup+1120.05 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 30595 0 0 0 111521 214 0 0 25 0 1 0 1785373502 124919808 30244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 30498 30244 145 145 0 30353 0
[pid=31345] vsize: 121992
Current children cumulated CPU time (s) 1117.35
Current children cumulated vsize (Kb) 124116

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 30824 0 0 0 112517 215 0 0 25 0 1 0 1785373502 125849600 30473 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 30725 30473 145 145 0 30580 0
[pid=31345] vsize: 122900
Current children cumulated CPU time (s) 1127.32
Current children cumulated vsize (Kb) 125024

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 31031 0 0 0 113513 217 0 0 25 0 1 0 1785373502 126693376 30680 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 30931 30680 145 145 0 30786 0
[pid=31345] vsize: 123724
Current children cumulated CPU time (s) 1137.3
Current children cumulated vsize (Kb) 125848

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 31246 0 0 0 114510 218 0 0 25 0 1 0 1785373502 127569920 30895 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 31145 30895 145 145 0 31000 0
[pid=31345] vsize: 124580
Current children cumulated CPU time (s) 1147.28
Current children cumulated vsize (Kb) 126704

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 31466 0 0 0 115506 220 0 0 25 0 1 0 1785373502 128466944 31115 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 31364 31115 145 145 0 31219 0
[pid=31345] vsize: 125456
Current children cumulated CPU time (s) 1157.26
Current children cumulated vsize (Kb) 127580

[startup+1170.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 31677 0 0 0 116503 221 0 0 25 0 1 0 1785373502 129323008 31326 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 31573 31326 145 145 0 31428 0
[pid=31345] vsize: 126292
Current children cumulated CPU time (s) 1167.24
Current children cumulated vsize (Kb) 128416

[startup+1180.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 31884 0 0 0 117498 223 0 0 25 0 1 0 1785373502 130170880 31533 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 31780 31533 145 145 0 31635 0
[pid=31345] vsize: 127120
Current children cumulated CPU time (s) 1177.21
Current children cumulated vsize (Kb) 129244

[startup+1190.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 32093 0 0 0 118495 224 0 0 25 0 1 0 1785373502 131026944 31742 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 31989 31742 145 145 0 31844 0
[pid=31345] vsize: 127956
Current children cumulated CPU time (s) 1187.19
Current children cumulated vsize (Kb) 130080

[startup+1200.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 32346 0 0 0 119491 226 0 0 25 0 1 0 1785373502 132059136 31995 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 32241 31995 145 145 0 32096 0
[pid=31345] vsize: 128964
Current children cumulated CPU time (s) 1197.17
Current children cumulated vsize (Kb) 131088

[startup+1210.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 32572 0 0 0 120488 227 0 0 25 0 1 0 1785373502 132972544 32221 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 32464 32221 145 145 0 32319 0
[pid=31345] vsize: 129856
Current children cumulated CPU time (s) 1207.15
Current children cumulated vsize (Kb) 131980



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.06 s]
Raw data (loadavg): 0.99 0.99 0.98 2/57 31345
Raw data (/proc/31341/stat): 31341 (minisat+_script) S 31340 31341 22582 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785373497 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31341/statm): 531 226 485 147 0 384 0
[pid=31341] vsize: 2124
Raw data (/proc/31345/stat): 31345 (minisat+_64-bit) R 31341 31341 22582 0 -1 0 32572 0 0 0 120488 227 0 0 25 0 1 0 1785373502 132972544 32221 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31345/statm): 32464 32221 145 145 0 32319 0
[pid=31345] vsize: 129856
Current children cumulated CPU time (s) 1207.15
Current children cumulated vsize (Kb) 131980

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1207.22
CPU user time (s): 1204.88
CPU system time (s): 2.33864
CPU usage (%): 99.7601
Max. virtual memory (cumulated for all children) (Kb): 131980

Verifier Data

ERROR: no interpretation found !