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/frb59-26-opb/normalized-frb59-26-2.opb
MD5SUM5b8ef604a7452dcb7c7d749b75aed566
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -45
Optimality of the best value was proved NO
Number of terms in the objective function 1534
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 1534
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 1534
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 benchmark1204.55
Number of variables1534
Total number of constraints126163
Number of constraints which are clauses126163
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 2334

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        927448 kB
Buffers:         33908 kB
Cached:          44888 kB
SwapCached:        696 kB
Active:          63724 kB
Inactive:        17660 kB
HighTotal:      131008 kB
HighFree:        82460 kB
LowTotal:       903652 kB
LowFree:        844988 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            20224 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:23:14 (client local time) WITH STATUS 10 IN 1206.76 SECONDS
stats: 2721 7 1206.76 10

Solver Data

c Parsing PB file...
c Converting 126163 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 |  126163   252326 |   42054       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -42
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216902   465187 |   72300       0        0     nan |  0.000 % |
c |       100 |  216378   464089 |   79530      71     1045    14.7 |  0.476 % |
c |       250 |  215666   462590 |   87483     197     2307    11.7 |  1.110 % |
c |       475 |  214693   460491 |   96231     382     4569    12.0 |  2.022 % |
c |       812 |  212890   456566 |  105854     654     7279    11.1 |  3.734 % |
c |      1318 |  210422   451160 |  116439    1060    10851    10.2 |  6.157 % |
c |      2077 |  206393   442217 |  128083    1635    16954    10.4 | 10.063 % |
c |      3216 |  198975   425552 |  140892    2422    25813    10.7 | 17.559 % |
c |      4924 |  190640   406622 |  154981    3664    40208    11.0 | 26.087 % |
c |      7486 |  179470   381025 |  170479    5477    62777    11.5 | 37.698 % |
c |     11330 |  166692   351158 |  187527    8259    96088    11.6 | 51.142 % |
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 |     14201 |  159762   334804 |   53254   10383   124904    12.0 | 51.142 % |
c |     14301 |  159518   334234 |   58579   10463   126556    12.1 | 59.111 % |
c |     14451 |  159171   333401 |   64437   10595   128502    12.1 | 59.497 % |
c |     14676 |  158480   331759 |   70881   10678   129458    12.1 | 60.258 % |
c |     15013 |  158174   331032 |   77969   10915   133832    12.3 | 60.595 % |
c |     15520 |  157341   329073 |   85766   11321   139331    12.3 | 61.505 % |
c |     16280 |  155349   324351 |   94342   11703   145801    12.5 | 63.687 % |
c |     17419 |  153760   320544 |  103776   12549   161675    12.9 | 65.453 % |
c |     19127 |  152453   317467 |  114154   13881   182702    13.2 | 66.863 % |
c |     21689 |  148743   308640 |  125570   15567   217965    14.0 | 70.881 % |
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 |     24382 |  145456   300817 |   48485   17375   249367    14.4 | 70.881 % |
c |     24483 |  145363   300588 |   53333   17440   251246    14.4 | 74.648 % |
c |     24633 |  145288   300407 |   58666   17551   251739    14.3 | 74.732 % |
c |     24858 |  144991   299696 |   64533   17581   253807    14.4 | 75.065 % |
c |     25195 |  144671   298897 |   70986   17767   260713    14.7 | 75.446 % |
c |     25702 |  144071   297413 |   78085   18002   268321    14.9 | 76.147 % |
c |     26461 |  143083   295047 |   85894   18367   278416    15.2 | 77.238 % |
c |     27600 |  142217   292945 |   94483   19129   300433    15.7 | 78.224 % |
c |     29308 |  141140   290360 |  103931   20436   345754    16.9 | 79.432 % |
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 |     30862 |  140267   288181 |   46755   21633   397822    18.4 | 79.432 % |
c |     30963 |  140267   288181 |   51430   21734   399242    18.4 | 80.416 % |
c |     31114 |  140168   287935 |   56573   21806   400090    18.3 | 80.529 % |
c |     31339 |  140168   287935 |   62230   22031   412550    18.7 | 80.529 % |
c |     31676 |  140023   287590 |   68453   22256   418337    18.8 | 80.689 % |
c |     32183 |  140023   287590 |   75299   22763   438437    19.3 | 80.689 % |
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 |     32937 |  140085   287791 |   46695   23512   471006    20.0 | 80.689 % |
c |     33037 |  140085   287791 |   51364   23612   474023    20.1 | 80.668 % |
c |     33188 |  139985   287565 |   56500   23703   476332    20.1 | 80.768 % |
c |     33413 |  139925   287414 |   62151   23901   482389    20.2 | 80.840 % |
c |     33750 |  139819   287160 |   68366   24223   491372    20.3 | 80.958 % |
c |     34257 |  139501   286378 |   75202   24523   504115    20.6 | 81.320 % |
c |     35016 |  139221   285698 |   82723   25080   519407    20.7 | 81.634 % |
c |     36155 |  138949   285015 |   90995   26080   578152    22.2 | 81.958 % |
c |     37863 |  138937   284987 |  100094   27753   670991    24.2 | 81.971 % |
c |     40425 |  138358   283576 |  110104   29587   808674    27.3 | 82.622 % |
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 |     41630 |  138147   283085 |   46049   30685   883161    28.8 | 82.622 % |
c |     41730 |  138092   282958 |   50653   30763   884351    28.7 | 82.933 % |
c |     41880 |  137941   282583 |   55719   30835   887360    28.8 | 83.109 % |
c |     42105 |  137901   282493 |   61291   31052   893326    28.8 | 83.149 % |
c |     42442 |  137895   282479 |   67420   31375   909461    29.0 | 83.155 % |
c |     42948 |  137873   282425 |   74162   31874   947781    29.7 | 83.181 % |
c |     43707 |  137873   282425 |   81578   32633   990787    30.4 | 83.181 % |
c |     44846 |  137866   282408 |   89736   33764  1042346    30.9 | 83.189 % |
c |     46554 |  137539   281618 |   98710   35123  1108640    31.6 | 83.556 % |
c |     49116 |  137311   281072 |  108581   37144  1292520    34.8 | 83.810 % |
c |     52960 |  137157   280708 |  119439   40856  1598714    39.1 | 83.978 % |
c |     58727 |  136513   279109 |  131383   45613  1978665    43.4 | 84.730 % |
c ==============================================================================
c Found solution: -50
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64383 |  136428   278853 |   45476   50690  2426715    47.9 | 84.730 % |
c |     64483 |  136372   278721 |   50023   50704  2426821    47.9 | 84.888 % |
c |     64633 |  136372   278721 |   55025   50854  2434364    47.9 | 84.888 % |
c |     64858 |  136372   278721 |   60528   51079  2451936    48.0 | 84.888 % |
c |     65195 |  136354   278679 |   66581   51330  2465308    48.0 | 84.907 % |
c |     65701 |  136354   278679 |   73239   51836  2497084    48.2 | 84.907 % |
c |     66460 |  136315   278575 |   80563   52539  2537278    48.3 | 84.952 % |
c |     67599 |  136315   278575 |   88619   53678  2687895    50.1 | 84.952 % |
c |     69307 |  136315   278575 |   97481   55386  2882870    52.1 | 84.952 % |
c |     71869 |  136315   278575 |  107230   57948  3297295    56.9 | 84.952 % |
c ==============================================================================
c Found solution: -51
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74103 |  136106   278085 |   45368   59809  3485256    58.3 | 84.952 % |
c |     74203 |  136106   278085 |   49904   59909  3491775    58.3 | 85.223 % |
c |     74353 |  136063   277970 |   54895   59670  3485850    58.4 | 85.278 % |
c |     74578 |  136063   277970 |   60384   59895  3498842    58.4 | 85.278 % |
c |     74916 |  136058   277957 |   66423   60226  3530651    58.6 | 85.284 % |
c |     75422 |  135994   277802 |   73065   60597  3563296    58.8 | 85.355 % |
c |     76181 |  135950   277698 |   80372   61179  3620235    59.2 | 85.403 % |
c |     77320 |  135945   277687 |   88409   62293  3702636    59.4 | 85.408 % |
c |     79028 |  135928   277644 |   97250   63981  3892624    60.8 | 85.429 % |
c |     81590 |  135691   277063 |  106975   65768  4131868    62.8 | 85.702 % |
c |     85436 |  135590   276824 |  117672   69157  4565212    66.0 | 85.813 % |
c |     91202 |  135583   276807 |  129440   74866  5415516    72.3 | 85.821 % |
c |     99851 |  135540   276704 |  142384   83045  6414369    77.2 | 85.869 % |
c |    112826 |  135455   276509 |  156622   95875  8314958    86.7 | 85.957 % |
c ==============================================================================
c Found solution: -52
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127962 |  135394   276336 |   45131  109446 11574582   105.8 | 85.957 % |
c |    128062 |  135394   276336 |   49644   22310  3255192   145.9 | 86.028 % |
c |    128212 |  135295   276100 |   54608   22395  3259721   145.6 | 86.136 % |
c |    128437 |  135290   276089 |   60069   22610  3275212   144.9 | 86.141 % |
c |    128775 |  135238   275955 |   66076   22938  3289266   143.4 | 86.207 % |
c |    129281 |  135204   275877 |   72683   23429  3310280   141.3 | 86.242 % |
c |    130040 |  135194   275853 |   79952   24166  3344207   138.4 | 86.253 % |
c |    131179 |  135186   275835 |   87947   25295  3433065   135.7 | 86.261 % |
c |    132888 |  135178   275815 |   96742   26972  3689589   136.8 | 86.271 % |
c |    135450 |  135123   275675 |  106416   29433  4012571   136.3 | 86.338 % |
c |    139294 |  135123   275675 |  117058   33277  4564286   137.2 | 86.338 % |
c |    145060 |  134993   275371 |  128764   38714  5165896   133.4 | 86.475 % |
c |    153709 |  134993   275371 |  141640   47363  7432043   156.9 | 86.475 % |
c |    166684 |  134984   275352 |  155804   60336  9779793   162.1 | 86.483 % |
c |    186146 |  134984   275352 |  171384   79798 13225885   165.7 | 86.483 % |
c |    215338 |  134936   275238 |  188523  108912 18650008   171.2 | 86.536 % |
c |    259127 |  134911   275179 |  207375  152675 26672713   174.7 | 86.563 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 -C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 -C1518 -C1517 -C1516 -C1515 -C1514 -C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 -C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 -C1493 -C1492 -C1491 -C1490 C1489 -C1488 -C1487 -C1486 -C1485 -C1484 -C1483 -C1482 -C1481 -C1480 -C1479 -C1478 -C1477 -C1476 -C1475 -C1474 -C1473 -C1472 -C1471 -C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 -C1458 -C1457 -C1456 -C1455 -C1454 -C1453 -C1452 -C1451 -C1450 -C1449 C1448 -C1447 -C1446 -C1445 -C1444 -C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 -C1424 -C1423 -C1422 C1421 -C1420 -C1419 -C1418 -C1417 -C1416 -C1415 -C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 -C1401 -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 -C25

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/2278/stat): 2278 (minisat+_script) R 2277 2278 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843634753 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/2278/statm): 174 3 169 147 0 27 0
[pid=2278] 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=2279
New process pid=2280
New process pid=2281
execve syscall for /bin/sed executable
One traced child (pid=2280) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=2281) exited with status: 0
One traced child (pid=2279) exited with status: 0
New process pid=2282
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-frb59-26-2.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 941 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 33940

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 1940 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 33940

[startup+30.0068 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 2941 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 33940

[startup+40.0065 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 3940 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 33940

[startup+50.0082 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 4940 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223120 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 33940

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 5941 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 33940

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 6941 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 33940

[startup+80.0112 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 7941 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 79.75
Current children cumulated vsize (Kb) 33940

[startup+90.0119 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 8941 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 89.75
Current children cumulated vsize (Kb) 33940

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 9942 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 33940

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 10942 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 109.76
Current children cumulated vsize (Kb) 33940

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 11942 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 119.76
Current children cumulated vsize (Kb) 33940

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 12942 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 129.76
Current children cumulated vsize (Kb) 33940

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 13942 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 139.76
Current children cumulated vsize (Kb) 33940

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 14943 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 149.77
Current children cumulated vsize (Kb) 33940

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 15943 33 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 159.77
Current children cumulated vsize (Kb) 33940

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 16942 34 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 169.77
Current children cumulated vsize (Kb) 33940

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 17941 34 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223104 134561479 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 179.76
Current children cumulated vsize (Kb) 33940

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7844 0 0 0 18941 34 0 0 25 0 1 0 1843634758 32579584 7831 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7954 7831 145 145 0 7809 0
[pid=2282] vsize: 31816
Current children cumulated CPU time (s) 189.76
Current children cumulated vsize (Kb) 33940

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 7872 0 0 0 19941 34 0 0 25 0 1 0 1843634758 32681984 7859 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 7979 7859 145 145 0 7834 0
[pid=2282] vsize: 31916
Current children cumulated CPU time (s) 199.76
Current children cumulated vsize (Kb) 34040

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 8286 0 0 0 20934 37 0 0 25 0 1 0 1843634758 34189312 8196 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 8347 8196 145 145 0 8202 0
[pid=2282] vsize: 33388
Current children cumulated CPU time (s) 209.72
Current children cumulated vsize (Kb) 35512

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 8600 0 0 0 21929 39 0 0 25 0 1 0 1843634758 35459072 8510 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 8657 8510 145 145 0 8512 0
[pid=2282] vsize: 34628
Current children cumulated CPU time (s) 219.69
Current children cumulated vsize (Kb) 36752

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 8994 0 0 0 22922 41 0 0 25 0 1 0 1843634758 37056512 8904 4294967295 134512640 135094434 3221224448 3221223040 134557215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 9047 8904 145 145 0 8902 0
[pid=2282] vsize: 36188
Current children cumulated CPU time (s) 229.64
Current children cumulated vsize (Kb) 38312

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 9340 0 0 0 23916 44 0 0 25 0 1 0 1843634758 38457344 9250 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 9389 9250 145 145 0 9244 0
[pid=2282] vsize: 37556
Current children cumulated CPU time (s) 239.61
Current children cumulated vsize (Kb) 39680

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 9783 0 0 0 24910 46 0 0 25 0 1 0 1843634758 40255488 9693 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 9828 9693 145 145 0 9683 0
[pid=2282] vsize: 39312
Current children cumulated CPU time (s) 249.57
Current children cumulated vsize (Kb) 41436

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 10131 0 0 0 25906 48 0 0 25 0 1 0 1843634758 41353216 9964 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 10096 9964 145 145 0 9951 0
[pid=2282] vsize: 40384
Current children cumulated CPU time (s) 259.55
Current children cumulated vsize (Kb) 42508

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 10710 0 0 0 26895 52 0 0 25 0 1 0 1843634758 43708416 10543 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 10671 10543 145 145 0 10526 0
[pid=2282] vsize: 42684
Current children cumulated CPU time (s) 269.48
Current children cumulated vsize (Kb) 44808

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 11060 0 0 0 27891 54 0 0 25 0 1 0 1843634758 45129728 10893 4294967295 134512640 135094434 3221224448 3221223136 134785033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 11018 10893 145 145 0 10873 0
[pid=2282] vsize: 44072
Current children cumulated CPU time (s) 279.46
Current children cumulated vsize (Kb) 46196

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 11376 0 0 0 28886 56 0 0 25 0 1 0 1843634758 46100480 11132 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 11255 11132 145 145 0 11110 0
[pid=2282] vsize: 45020
Current children cumulated CPU time (s) 289.43
Current children cumulated vsize (Kb) 47144

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 11677 0 0 0 29882 58 0 0 25 0 1 0 1843634758 47325184 11433 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 11554 11433 145 145 0 11409 0
[pid=2282] vsize: 46216
Current children cumulated CPU time (s) 299.41
Current children cumulated vsize (Kb) 48340

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 12006 0 0 0 30876 59 0 0 25 0 1 0 1843634758 48922624 11762 4294967295 134512640 135094434 3221224448 3221223072 134557616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 11944 11762 145 145 0 11799 0
[pid=2282] vsize: 47776
Current children cumulated CPU time (s) 309.36
Current children cumulated vsize (Kb) 49900

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 12435 0 0 0 31869 62 0 0 25 0 1 0 1843634758 50667520 12191 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 12370 12191 145 145 0 12225 0
[pid=2282] vsize: 49480
Current children cumulated CPU time (s) 319.32
Current children cumulated vsize (Kb) 51604

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 12879 0 0 0 32860 65 0 0 25 0 1 0 1843634758 52473856 12635 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 12811 12635 145 145 0 12666 0
[pid=2282] vsize: 51244
Current children cumulated CPU time (s) 329.26
Current children cumulated vsize (Kb) 53368

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 13397 0 0 0 33851 69 0 0 25 0 1 0 1843634758 54583296 13153 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 13326 13153 145 145 0 13181 0
[pid=2282] vsize: 53304
Current children cumulated CPU time (s) 339.21
Current children cumulated vsize (Kb) 55428

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 13755 0 0 0 34843 72 0 0 25 0 1 0 1843634758 56037376 13511 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434789 0 0 17 0 0 0
Raw data (/proc/2282/statm): 13681 13511 145 145 0 13536 0
[pid=2282] vsize: 54724
Current children cumulated CPU time (s) 349.16
Current children cumulated vsize (Kb) 56848

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 14077 0 0 0 35838 73 0 0 25 0 1 0 1843634758 57348096 13833 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 14001 13833 145 145 0 13856 0
[pid=2282] vsize: 56004
Current children cumulated CPU time (s) 359.12
Current children cumulated vsize (Kb) 58128

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 14489 0 0 0 36831 76 0 0 25 0 1 0 1843634758 59023360 14245 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 14410 14245 145 145 0 14265 0
[pid=2282] vsize: 57640
Current children cumulated CPU time (s) 369.08
Current children cumulated vsize (Kb) 59764

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 14929 0 0 0 37822 81 0 0 25 0 1 0 1843634758 60817408 14685 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 14848 14685 145 145 0 14703 0
[pid=2282] vsize: 59392
Current children cumulated CPU time (s) 379.04
Current children cumulated vsize (Kb) 61516

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 15226 0 0 0 38817 83 0 0 25 0 1 0 1843634758 62021632 14982 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 15142 14982 145 145 0 14997 0
[pid=2282] vsize: 60568
Current children cumulated CPU time (s) 389.01
Current children cumulated vsize (Kb) 62692

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 15636 0 0 0 39810 86 0 0 25 0 1 0 1843634758 63692800 15392 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 15550 15392 145 145 0 15405 0
[pid=2282] vsize: 62200
Current children cumulated CPU time (s) 398.97
Current children cumulated vsize (Kb) 64324

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 16136 0 0 0 40800 90 0 0 24 0 1 0 1843634758 65728512 15892 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 16047 15892 145 145 0 15902 0
[pid=2282] vsize: 64188
Current children cumulated CPU time (s) 408.91
Current children cumulated vsize (Kb) 66312

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 16476 0 0 0 41794 92 0 0 25 0 1 0 1843634758 67112960 16232 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 16385 16232 145 145 0 16240 0
[pid=2282] vsize: 65540
Current children cumulated CPU time (s) 418.87
Current children cumulated vsize (Kb) 67664

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 16862 0 0 0 42787 95 0 0 25 0 1 0 1843634758 68685824 16618 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 16769 16618 145 145 0 16624 0
[pid=2282] vsize: 67076
Current children cumulated CPU time (s) 428.83
Current children cumulated vsize (Kb) 69200

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) T 2278 2278 20115 0 -1 0 17389 0 0 0 43778 99 0 0 25 0 1 0 1843634758 70836224 17145 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/2282/statm): 17294 17145 145 145 0 17149 0
[pid=2282] vsize: 69176
Current children cumulated CPU time (s) 438.78
Current children cumulated vsize (Kb) 71300

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 17920 0 0 0 44769 103 0 0 25 0 1 0 1843634758 73003008 17676 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 17823 17676 145 145 0 17678 0
[pid=2282] vsize: 71292
Current children cumulated CPU time (s) 448.73
Current children cumulated vsize (Kb) 73416

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 18414 0 0 0 45761 106 0 0 25 0 1 0 1843634758 75018240 18170 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 18315 18170 145 145 0 18170 0
[pid=2282] vsize: 73260
Current children cumulated CPU time (s) 458.68
Current children cumulated vsize (Kb) 75384

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 18956 0 0 0 46753 110 0 0 25 0 1 0 1843634758 77230080 18712 4294967295 134512640 135094434 3221224448 3221223040 134551692 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 18855 18712 145 145 0 18710 0
[pid=2282] vsize: 75420
Current children cumulated CPU time (s) 468.64
Current children cumulated vsize (Kb) 77544

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 19510 0 0 0 47742 113 0 0 25 0 1 0 1843634758 79495168 19266 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19408 19266 145 145 0 19263 0
[pid=2282] vsize: 77632
Current children cumulated CPU time (s) 478.56
Current children cumulated vsize (Kb) 79756

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 19915 0 0 0 48736 116 0 0 25 0 1 0 1843634758 81145856 19671 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19811 19671 145 145 0 19666 0
[pid=2282] vsize: 79244
Current children cumulated CPU time (s) 488.53
Current children cumulated vsize (Kb) 81368

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 49733 117 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 498.51
Current children cumulated vsize (Kb) 81908

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 50733 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221222928 134781535 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 508.52
Current children cumulated vsize (Kb) 81908

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 51734 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 518.53
Current children cumulated vsize (Kb) 81908

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 52734 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 528.53
Current children cumulated vsize (Kb) 81908

[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 53734 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 538.53
Current children cumulated vsize (Kb) 81908

[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 54734 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 548.53
Current children cumulated vsize (Kb) 81908

[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 55734 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 558.53
Current children cumulated vsize (Kb) 81908

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 56735 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 568.54
Current children cumulated vsize (Kb) 81908

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 57735 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 578.54
Current children cumulated vsize (Kb) 81908

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 58735 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223120 134555821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 588.54
Current children cumulated vsize (Kb) 81908

[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 59735 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 598.54
Current children cumulated vsize (Kb) 81908

[startup+610.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 60735 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 608.54
Current children cumulated vsize (Kb) 81908

[startup+620.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 61735 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 618.54
Current children cumulated vsize (Kb) 81908

[startup+630.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 62736 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 628.55
Current children cumulated vsize (Kb) 81908

[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 63736 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 638.55
Current children cumulated vsize (Kb) 81908

[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20128 0 0 0 64736 118 0 0 25 0 1 0 1843634758 81698816 19807 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 19946 19807 145 145 0 19801 0
[pid=2282] vsize: 79784
Current children cumulated CPU time (s) 648.55
Current children cumulated vsize (Kb) 81908

[startup+660.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 20227 0 0 0 65735 118 0 0 25 0 1 0 1843634758 82104320 19906 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 20045 19906 145 145 0 19900 0
[pid=2282] vsize: 80180
Current children cumulated CPU time (s) 658.54
Current children cumulated vsize (Kb) 82304

[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.98 1/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) T 2278 2278 20115 0 -1 0 20712 0 0 0 66728 121 0 0 25 0 1 0 1843634758 84090880 20391 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/2282/statm): 20530 20391 145 145 0 20385 0
[pid=2282] vsize: 82120
Current children cumulated CPU time (s) 668.5
Current children cumulated vsize (Kb) 84244

[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 21133 0 0 0 67720 124 0 0 25 0 1 0 1843634758 85815296 20812 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 20951 20812 145 145 0 20806 0
[pid=2282] vsize: 83804
Current children cumulated CPU time (s) 678.45
Current children cumulated vsize (Kb) 85928

[startup+690.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 21615 0 0 0 68710 127 0 0 25 0 1 0 1843634758 87789568 21294 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 21433 21294 145 145 0 21288 0
[pid=2282] vsize: 85732
Current children cumulated CPU time (s) 688.38
Current children cumulated vsize (Kb) 87856

[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 22007 0 0 0 69703 131 0 0 25 0 1 0 1843634758 89395200 21686 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 21825 21686 145 145 0 21680 0
[pid=2282] vsize: 87300
Current children cumulated CPU time (s) 698.35
Current children cumulated vsize (Kb) 89424

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 22467 0 0 0 70695 133 0 0 25 0 1 0 1843634758 91279360 22146 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 22285 22146 145 145 0 22140 0
[pid=2282] vsize: 89140
Current children cumulated CPU time (s) 708.29
Current children cumulated vsize (Kb) 91264

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 22818 0 0 0 71689 136 0 0 25 0 1 0 1843634758 92717056 22497 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 22636 22497 145 145 0 22491 0
[pid=2282] vsize: 90544
Current children cumulated CPU time (s) 718.26
Current children cumulated vsize (Kb) 92668

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 23301 0 0 0 72679 140 0 0 25 0 1 0 1843634758 94695424 22980 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 23119 22980 145 145 0 22974 0
[pid=2282] vsize: 92476
Current children cumulated CPU time (s) 728.2
Current children cumulated vsize (Kb) 94600

[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 23743 0 0 0 73671 142 0 0 25 0 1 0 1843634758 96505856 23422 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 23561 23422 145 145 0 23416 0
[pid=2282] vsize: 94244
Current children cumulated CPU time (s) 738.14
Current children cumulated vsize (Kb) 96368

[startup+750.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 24057 0 0 0 74665 144 0 0 25 0 1 0 1843634758 97792000 23736 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 23875 23736 145 145 0 23730 0
[pid=2282] vsize: 95500
Current children cumulated CPU time (s) 748.1
Current children cumulated vsize (Kb) 97624

[startup+760.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 24397 0 0 0 75660 146 0 0 25 0 1 0 1843634758 99184640 24076 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 24215 24076 145 145 0 24070 0
[pid=2282] vsize: 96860
Current children cumulated CPU time (s) 758.07
Current children cumulated vsize (Kb) 98984

[startup+770.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 24765 0 0 0 76654 148 0 0 25 0 1 0 1843634758 100691968 24444 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 24583 24444 145 145 0 24438 0
[pid=2282] vsize: 98332
Current children cumulated CPU time (s) 768.03
Current children cumulated vsize (Kb) 100456

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 25210 0 0 0 77646 151 0 0 25 0 1 0 1843634758 102514688 24889 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 25028 24889 145 145 0 24883 0
[pid=2282] vsize: 100112
Current children cumulated CPU time (s) 777.98
Current children cumulated vsize (Kb) 102236

[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 25635 0 0 0 78639 155 0 0 25 0 1 0 1843634758 104255488 25314 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 25453 25314 145 145 0 25308 0
[pid=2282] vsize: 101812
Current children cumulated CPU time (s) 787.95
Current children cumulated vsize (Kb) 103936

[startup+800.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 26039 0 0 0 79633 157 0 0 25 0 1 0 1843634758 105910272 25718 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 25857 25718 145 145 0 25712 0
[pid=2282] vsize: 103428
Current children cumulated CPU time (s) 797.91
Current children cumulated vsize (Kb) 105552

[startup+810.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 26359 0 0 0 80627 160 0 0 25 0 1 0 1843634758 107220992 26038 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 26177 26038 145 145 0 26032 0
[pid=2282] vsize: 104708
Current children cumulated CPU time (s) 807.88
Current children cumulated vsize (Kb) 106832

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 26689 0 0 0 81619 163 0 0 25 0 1 0 1843634758 108572672 26368 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 26507 26368 145 145 0 26362 0
[pid=2282] vsize: 106028
Current children cumulated CPU time (s) 817.83
Current children cumulated vsize (Kb) 108152

[startup+830.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 27128 0 0 0 82612 166 0 0 25 0 1 0 1843634758 110370816 26807 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 26946 26807 145 145 0 26801 0
[pid=2282] vsize: 107784
Current children cumulated CPU time (s) 827.79
Current children cumulated vsize (Kb) 109908

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 27378 0 0 0 83608 166 0 0 25 0 1 0 1843634758 111394816 27057 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 27196 27057 145 145 0 27051 0
[pid=2282] vsize: 108784
Current children cumulated CPU time (s) 837.75
Current children cumulated vsize (Kb) 110908

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 27732 0 0 0 84603 169 0 0 25 0 1 0 1843634758 112840704 27411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 27549 27411 145 145 0 27404 0
[pid=2282] vsize: 110196
Current children cumulated CPU time (s) 847.73
Current children cumulated vsize (Kb) 112320

[startup+860.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 27989 0 0 0 85598 171 0 0 25 0 1 0 1843634758 113885184 27668 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 27804 27668 145 145 0 27659 0
[pid=2282] vsize: 111216
Current children cumulated CPU time (s) 857.7
Current children cumulated vsize (Kb) 113340

[startup+870.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 28342 0 0 0 86593 173 0 0 25 0 1 0 1843634758 115322880 28021 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 28155 28021 145 145 0 28010 0
[pid=2282] vsize: 112620
Current children cumulated CPU time (s) 867.67
Current children cumulated vsize (Kb) 114744

[startup+880.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 28668 0 0 0 87587 175 0 0 25 0 1 0 1843634758 116654080 28347 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 28480 28347 145 145 0 28335 0
[pid=2282] vsize: 113920
Current children cumulated CPU time (s) 877.63
Current children cumulated vsize (Kb) 116044

[startup+890.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 29025 0 0 0 88581 178 0 0 25 0 1 0 1843634758 118108160 28704 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 28835 28704 145 145 0 28690 0
[pid=2282] vsize: 115340
Current children cumulated CPU time (s) 887.6
Current children cumulated vsize (Kb) 117464

[startup+900.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 29294 0 0 0 89577 180 0 0 25 0 1 0 1843634758 119205888 28973 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 29103 28973 145 145 0 28958 0
[pid=2282] vsize: 116412
Current children cumulated CPU time (s) 897.58
Current children cumulated vsize (Kb) 118536

[startup+910.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 29642 0 0 0 90571 183 0 0 25 0 1 0 1843634758 120623104 29321 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 29449 29321 145 145 0 29304 0
[pid=2282] vsize: 117796
Current children cumulated CPU time (s) 907.55
Current children cumulated vsize (Kb) 119920

[startup+920.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 30033 0 0 0 91565 186 0 0 25 0 1 0 1843634758 122216448 29712 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 29838 29712 145 145 0 29693 0
[pid=2282] vsize: 119352
Current children cumulated CPU time (s) 917.52
Current children cumulated vsize (Kb) 121476

[startup+930.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) T 2278 2278 20115 0 -1 0 30320 0 0 0 92560 187 0 0 25 0 1 0 1843634758 123387904 29999 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/2282/statm): 30124 29999 145 145 0 29979 0
[pid=2282] vsize: 120496
Current children cumulated CPU time (s) 927.48
Current children cumulated vsize (Kb) 122620

[startup+940.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 30620 0 0 0 93554 190 0 0 25 0 1 0 1843634758 124608512 30299 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 30422 30299 145 145 0 30277 0
[pid=2282] vsize: 121688
Current children cumulated CPU time (s) 937.45
Current children cumulated vsize (Kb) 123812

[startup+950.074 s]
Raw data (loadavg): 0.99 0.97 0.98 1/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) T 2278 2278 20115 0 -1 0 30937 0 0 0 94547 193 0 0 25 0 1 0 1843634758 125898752 30616 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/2282/statm): 30737 30616 145 145 0 30592 0
[pid=2282] vsize: 122948
Current children cumulated CPU time (s) 947.41
Current children cumulated vsize (Kb) 125072

[startup+960.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 31242 0 0 0 95542 196 0 0 25 0 1 0 1843634758 127664128 30921 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 31168 30921 145 145 0 31023 0
[pid=2282] vsize: 124672
Current children cumulated CPU time (s) 957.39
Current children cumulated vsize (Kb) 126796

[startup+970.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 31605 0 0 0 96536 198 0 0 25 0 1 0 1843634758 129146880 31284 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 31530 31284 145 145 0 31385 0
[pid=2282] vsize: 126120
Current children cumulated CPU time (s) 967.35
Current children cumulated vsize (Kb) 128244

[startup+980.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 31880 0 0 0 97531 200 0 0 25 0 1 0 1843634758 130265088 31559 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 31803 31559 145 145 0 31658 0
[pid=2282] vsize: 127212
Current children cumulated CPU time (s) 977.32
Current children cumulated vsize (Kb) 129336

[startup+990.078 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 32115 0 0 0 98528 202 0 0 25 0 1 0 1843634758 131223552 31794 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 32037 31794 145 145 0 31892 0
[pid=2282] vsize: 128148
Current children cumulated CPU time (s) 987.31
Current children cumulated vsize (Kb) 130272

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 32381 0 0 0 99523 204 0 0 25 0 1 0 1843634758 132313088 32060 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 32303 32060 145 145 0 32158 0
[pid=2282] vsize: 129212
Current children cumulated CPU time (s) 997.28
Current children cumulated vsize (Kb) 131336

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 32647 0 0 0 100519 206 0 0 25 0 1 0 1843634758 133398528 32326 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 32568 32326 145 145 0 32423 0
[pid=2282] vsize: 130272
Current children cumulated CPU time (s) 1007.26
Current children cumulated vsize (Kb) 132396

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 32955 0 0 0 101514 208 0 0 25 0 1 0 1843634758 134651904 32634 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 32874 32634 145 145 0 32729 0
[pid=2282] vsize: 131496
Current children cumulated CPU time (s) 1017.23
Current children cumulated vsize (Kb) 133620

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 33237 0 0 0 102510 209 0 0 25 0 1 0 1843634758 135802880 32916 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 33155 32916 145 145 0 33010 0
[pid=2282] vsize: 132620
Current children cumulated CPU time (s) 1027.2
Current children cumulated vsize (Kb) 134744

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 33522 0 0 0 103506 211 0 0 25 0 1 0 1843634758 136962048 33201 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 33438 33201 145 145 0 33293 0
[pid=2282] vsize: 133752
Current children cumulated CPU time (s) 1037.18
Current children cumulated vsize (Kb) 135876

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 33852 0 0 0 104499 214 0 0 25 0 1 0 1843634758 138313728 33531 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 33768 33531 145 145 0 33623 0
[pid=2282] vsize: 135072
Current children cumulated CPU time (s) 1047.14
Current children cumulated vsize (Kb) 137196

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 34165 0 0 0 105493 216 0 0 25 0 1 0 1843634758 139591680 33844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 34080 33844 145 145 0 33935 0
[pid=2282] vsize: 136320
Current children cumulated CPU time (s) 1057.1
Current children cumulated vsize (Kb) 138444

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 34494 0 0 0 106488 218 0 0 25 0 1 0 1843634758 140939264 34173 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 34409 34173 145 145 0 34264 0
[pid=2282] vsize: 137636
Current children cumulated CPU time (s) 1067.07
Current children cumulated vsize (Kb) 139760

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 34779 0 0 0 107484 220 0 0 25 0 1 0 1843634758 142098432 34458 4294967295 134512640 135094434 3221224448 3221223040 134557277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 34692 34458 145 145 0 34547 0
[pid=2282] vsize: 138768
Current children cumulated CPU time (s) 1077.05
Current children cumulated vsize (Kb) 140892

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 35090 0 0 0 108477 224 0 0 25 0 1 0 1843634758 143372288 34769 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 35003 34769 145 145 0 34858 0
[pid=2282] vsize: 140012
Current children cumulated CPU time (s) 1087.02
Current children cumulated vsize (Kb) 142136

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 35408 0 0 0 109471 225 0 0 25 0 1 0 1843634758 144670720 35087 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 35320 35087 145 145 0 35175 0
[pid=2282] vsize: 141280
Current children cumulated CPU time (s) 1096.97
Current children cumulated vsize (Kb) 143404

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 35711 0 0 0 110466 228 0 0 25 0 1 0 1843634758 145895424 35390 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 35619 35390 145 145 0 35474 0
[pid=2282] vsize: 142476
Current children cumulated CPU time (s) 1106.95
Current children cumulated vsize (Kb) 144600

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 35989 0 0 0 111461 230 0 0 25 0 1 0 1843634758 147042304 35668 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 35899 35668 145 145 0 35754 0
[pid=2282] vsize: 143596
Current children cumulated CPU time (s) 1116.92
Current children cumulated vsize (Kb) 145720

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 36246 0 0 0 112455 232 0 0 25 0 1 0 1843634758 148082688 35925 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 36153 35925 145 145 0 36008 0
[pid=2282] vsize: 144612
Current children cumulated CPU time (s) 1126.88
Current children cumulated vsize (Kb) 146736

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 36497 0 0 0 113451 234 0 0 25 0 1 0 1843634758 149110784 36176 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 36404 36176 145 145 0 36259 0
[pid=2282] vsize: 145616
Current children cumulated CPU time (s) 1136.86
Current children cumulated vsize (Kb) 147740

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 36685 0 0 0 114447 236 0 0 25 0 1 0 1843634758 149880832 36364 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 36592 36364 145 145 0 36447 0
[pid=2282] vsize: 146368
Current children cumulated CPU time (s) 1146.84
Current children cumulated vsize (Kb) 148492

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 36948 0 0 0 115441 238 0 0 25 0 1 0 1843634758 150949888 36627 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 36853 36627 145 145 0 36708 0
[pid=2282] vsize: 147412
Current children cumulated CPU time (s) 1156.8
Current children cumulated vsize (Kb) 149536

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 37164 0 0 0 116437 240 0 0 25 0 1 0 1843634758 151834624 36843 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 37069 36843 145 145 0 36924 0
[pid=2282] vsize: 148276
Current children cumulated CPU time (s) 1166.78
Current children cumulated vsize (Kb) 150400

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 37413 0 0 0 117433 242 0 0 25 0 1 0 1843634758 152850432 37092 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 37317 37092 145 145 0 37172 0
[pid=2282] vsize: 149268
Current children cumulated CPU time (s) 1176.76
Current children cumulated vsize (Kb) 151392

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 37659 0 0 0 118428 244 0 0 25 0 1 0 1843634758 153849856 37338 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 37561 37338 145 145 0 37416 0
[pid=2282] vsize: 150244
Current children cumulated CPU time (s) 1186.73
Current children cumulated vsize (Kb) 152368

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 37941 0 0 0 119423 247 0 0 25 0 1 0 1843634758 154996736 37620 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 37841 37620 145 145 0 37696 0
[pid=2282] vsize: 151364
Current children cumulated CPU time (s) 1196.71
Current children cumulated vsize (Kb) 153488

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 38136 0 0 0 120419 249 0 0 25 0 1 0 1843634758 155795456 37815 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2282/statm): 38036 37815 145 145 0 37891 0
[pid=2282] vsize: 152144
Current children cumulated CPU time (s) 1206.69
Current children cumulated vsize (Kb) 154268



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 2282
Raw data (/proc/2278/stat): 2278 (minisat+_script) S 2277 2278 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843634753 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2278/statm): 531 226 485 147 0 384 0
[pid=2278] vsize: 2124
Raw data (/proc/2282/stat): 2282 (minisat+_64-bit) R 2278 2278 20115 0 -1 0 38136 0 0 0 120419 249 0 0 25 0 1 0 1843634758 155795456 37815 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2282/statm): 38036 37815 145 145 0 37891 0
[pid=2282] vsize: 152144
Current children cumulated CPU time (s) 1206.69
Current children cumulated vsize (Kb) 154268

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1206.76
CPU user time (s): 1204.2
CPU system time (s): 2.56261
CPU usage (%): 99.7179
Max. virtual memory (cumulated for all children) (Kb): 154268

Verifier Data

ERROR: no interpretation found !