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-3.opb
MD5SUMb95391b071a3986ad670119101f16613
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -43
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.13
Number of variables1534
Total number of constraints126082
Number of constraints which are clauses126082
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 2338

Launcher Data

LAUNCH ON wulflinc1 THE 2005-09-18 19:05:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2724 boxname=wulflinc1 idbench=380 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b95391b071a3986ad670119101f16613  /oldhome/oroussel/tmp/wulflinc1/normalized-frb59-26-3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-frb59-26-3.opb
IDLAUNCH: 2724
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        878248 kB
Buffers:         37940 kB
Cached:          88380 kB
SwapCached:        908 kB
Active:          98032 kB
Inactive:        31112 kB
HighTotal:      131008 kB
HighFree:        46620 kB
LowTotal:       903652 kB
LowFree:        831628 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21600 kB
Committed_AS:    93132 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 19:25:15 (client local time) WITH STATUS 10 IN 1208.06 SECONDS
stats: 2724 7 1208.06 10

Solver Data

c Parsing PB file...
c Converting 126082 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 |  126082   252164 |   42027       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -43
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216998   465444 |   72332       0        0     nan |  0.000 % |
c |       100 |  216440   464274 |   79565      77      692     9.0 |  0.496 % |
c |       250 |  215718   462730 |   87521     178     1363     7.7 |  1.160 % |
c |       475 |  214836   460831 |   96273     357     3111     8.7 |  1.981 % |
c |       813 |  212641   456042 |  105901     592     5851     9.9 |  4.071 % |
c |      1319 |  209385   448854 |  116491     990    12030    12.2 |  7.246 % |
c |      2078 |  205094   439353 |  128140    1507    17185    11.4 | 11.504 % |
c |      3217 |  196864   420718 |  140954    2245    27826    12.4 | 19.808 % |
c |      4926 |  187933   400276 |  155050    3536    41251    11.7 | 29.154 % |
c |      7488 |  174890   370399 |  170555    5163    60601    11.7 | 42.471 % |
c |     11332 |  162083   340109 |  187610    7594    92875    12.2 | 56.282 % |
c |     17099 |  148519   307983 |  206371   10871   135486    12.5 | 71.082 % |
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 |     19471 |  145143   299814 |   48381   12463   157720    12.7 | 71.082 % |
c |     19572 |  145143   299814 |   53219   12564   158110    12.6 | 74.855 % |
c |     19722 |  145143   299814 |   58541   12714   160469    12.6 | 74.855 % |
c |     19947 |  144865   299152 |   64395   12900   164705    12.8 | 75.164 % |
c |     20285 |  144640   298591 |   70834   13140   169632    12.9 | 75.430 % |
c |     20791 |  144145   297400 |   77918   13454   174511    13.0 | 75.987 % |
c |     21550 |  143691   296290 |   85709   14108   190400    13.5 | 76.508 % |
c |     22689 |  143174   295063 |   94280   15003   211362    14.1 | 77.073 % |
c |     24397 |  142110   292541 |  103708   16399   244001    14.9 | 78.248 % |
c |     26959 |  141157   290281 |  114079   18515   320032    17.3 | 79.296 % |
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 |     29178 |  139823   287131 |   46607   20012   367782    18.4 | 79.296 % |
c |     29278 |  139608   286611 |   51267   20026   367537    18.4 | 81.025 % |
c |     29428 |  139550   286467 |   56394   20139   368185    18.3 | 81.091 % |
c |     29653 |  139471   286275 |   62033   20269   375681    18.5 | 81.175 % |
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 |     29811 |  139464   286228 |   46488   20389   388027    19.0 | 81.175 % |
c |     29911 |  139408   286102 |   51136   20451   388814    19.0 | 81.242 % |
c |     30061 |  139192   285577 |   56250   20394   388394    19.0 | 81.489 % |
c |     30287 |  139191   285574 |   61875   20614   390522    18.9 | 81.490 % |
c |     30626 |  139133   285437 |   68063   20890   404382    19.4 | 81.553 % |
c |     31132 |  138976   285056 |   74869   21312   414941    19.5 | 81.729 % |
c |     31891 |  138892   284848 |   82356   22019   435831    19.8 | 81.828 % |
c |     33030 |  138569   284044 |   90591   22926   464026    20.2 | 82.207 % |
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 |     33870 |  138476   283871 |   46158   23604   502946    21.3 | 82.207 % |
c |     33970 |  138311   283468 |   50773   23665   503768    21.3 | 82.539 % |
c |     34120 |  138311   283468 |   55851   23815   513660    21.6 | 82.539 % |
c |     34346 |  138308   283461 |   61436   24031   520109    21.6 | 82.542 % |
c |     34683 |  138149   283085 |   67579   24316   528924    21.8 | 82.713 % |
c |     35189 |  138025   282766 |   74337   24647   538200    21.8 | 82.866 % |
c |     35948 |  138025   282766 |   81771   25406   603192    23.7 | 82.866 % |
c |     37087 |  137588   281684 |   89948   26334   642119    24.4 | 83.372 % |
c |     38795 |  136959   280149 |   98943   27600   711769    25.8 | 84.100 % |
c ==============================================================================
c Found solution: -48
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39995 |  136686   279451 |   45562   28586   771814    27.0 | 84.100 % |
c |     40097 |  136675   279424 |   50118   28671   773626    27.0 | 84.439 % |
c |     40247 |  136675   279424 |   55130   28821   779668    27.1 | 84.439 % |
c |     40472 |  136570   279173 |   60643   28831   782806    27.2 | 84.556 % |
c |     40810 |  136570   279173 |   66707   29169   806748    27.7 | 84.556 % |
c |     41316 |  136521   279056 |   73378   29583   849482    28.7 | 84.611 % |
c |     42075 |  136516   279045 |   80715   30339   884023    29.1 | 84.616 % |
c |     43215 |  136401   278762 |   88787   31387   962003    30.6 | 84.749 % |
c |     44923 |  136232   278358 |   97666   32887  1048554    31.9 | 84.938 % |
c |     47486 |  136149   278147 |  107432   35346  1276312    36.1 | 85.041 % |
c |     51330 |  135674   276982 |  118176   38442  1790167    46.6 | 85.585 % |
c |     57096 |  135612   276826 |  129993   44030  2810947    63.8 | 85.661 % |
c |     65747 |  135576   276739 |  142993   52662  4145672    78.7 | 85.700 % |
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 |     67205 |  135575   276748 |   45191   54070  4291929    79.4 | 85.700 % |
c |     67306 |  135575   276748 |   49710   54171  4295459    79.3 | 85.712 % |
c |     67456 |  135575   276748 |   54681   54321  4300437    79.2 | 85.712 % |
c |     67681 |  135535   276654 |   60149   54440  4305045    79.1 | 85.755 % |
c |     68018 |  135535   276654 |   66164   54777  4342942    79.3 | 85.755 % |
c |     68524 |  135521   276622 |   72780   55207  4364365    79.1 | 85.770 % |
c |     69283 |  135521   276622 |   80058   55966  4413885    78.9 | 85.770 % |
c |     70422 |  135515   276608 |   88064   57102  4537411    79.5 | 85.776 % |
c |     72130 |  135376   276279 |   96870   58658  4750361    81.0 | 85.929 % |
c |     74693 |  135329   276160 |  106558   61096  5113153    83.7 | 85.987 % |
c |     78537 |  135199   275844 |  117213   64712  5460014    84.4 | 86.135 % |
c |     84303 |  135012   275411 |  128935   70321  6502802    92.5 | 86.333 % |
c |     92953 |  134966   275296 |  141828   78769  8516166   108.1 | 86.388 % |
c |    105927 |  134803   274900 |  156011   91584 10845292   118.4 | 86.575 % |
c |    125388 |  134627   274480 |  171612  110465 13789180   124.8 | 86.771 % |
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 |    146490 |  134608   274413 |   44869  131017 18005950   137.4 | 86.771 % |
c |    146590 |  134520   274198 |   49355   22382  2976833   133.0 | 86.897 % |
c |    146740 |  134520   274198 |   54291   22532  2986731   132.6 | 86.897 % |
c |    146965 |  134520   274198 |   59720   22757  2997680   131.7 | 86.897 % |
c |    147302 |  134512   274176 |   65692   23090  3039315   131.6 | 86.908 % |
c |    147808 |  134451   274041 |   72261   23589  3067515   130.0 | 86.968 % |
c |    148567 |  134451   274041 |   79488   24348  3118327   128.1 | 86.968 % |
c |    149706 |  134451   274041 |   87436   25487  3236403   127.0 | 86.968 % |
c |    151416 |  134445   274025 |   96180   27194  3363305   123.7 | 86.976 % |
c |    153979 |  134404   273920 |  105798   29674  3626730   122.2 | 87.028 % |
c |    157823 |  134360   273816 |  116378   33340  4031583   120.9 | 87.076 % |
c |    163589 |  134360   273816 |  128016   39106  5002751   127.9 | 87.076 % |
c |    172238 |  134353   273801 |  140818   47751  6347034   132.9 | 87.082 % |
c |    185212 |  134327   273741 |  154899   60700  8591150   141.5 | 87.110 % |
c |    204674 |  134245   273546 |  170389   80128 11902448   148.5 | 87.200 % |
c |    233867 |  134159   273343 |  187428  109294 17140633   156.8 | 87.290 % |
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 |    238225 |  134187   273424 |   44729  113652 17745327   156.1 | 87.290 % |
c |    238325 |  134187   273424 |   49201   24419  2447777   100.2 | 87.285 % |
c |    238475 |  134187   273424 |   54122   24569  2456904   100.0 | 87.285 % |
c |    238701 |  134187   273424 |   59534   24795  2468989    99.6 | 87.285 % |
c |    239039 |  134110   273222 |   65487   25074  2474764    98.7 | 87.383 % |
c |    239545 |  134110   273222 |   72036   25580  2530061    98.9 | 87.383 % |
c |    240304 |  134102   273204 |   79240   26330  2598566    98.7 | 87.391 % |
c |    241443 |  134102   273204 |   87164   27469  2711977    98.7 | 87.391 % |
c |    243151 |  134102   273204 |   95880   29177  2947946   101.0 | 87.391 % |
c |    245713 |  134102   273204 |  105468   31739  3332683   105.0 | 87.391 % |
c |    249557 |  134097   273193 |  116015   35578  3879118   109.0 | 87.395 % |
c |    255324 |  134064   273108 |  127617   41315  4585248   111.0 | 87.437 % |
c |    263974 |  134031   273025 |  140378   49956  5870587   117.5 | 87.476 % |
c |    276948 |  134005   272961 |  154416   62913  8051620   128.0 | 87.506 % |
c |    296409 |  134000   272950 |  169858   82371 12209581   148.2 | 87.511 % |
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 -C258

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/27284/stat): 27284 (minisat+_script) R 27283 27284 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1728553069 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27284/statm): 174 3 169 147 0 27 0
[pid=27284] 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=27285
New process pid=27286
New process pid=27287
execve syscall for /bin/sed executable
One traced child (pid=27286) 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=27287) exited with status: 0
One traced child (pid=27285) exited with status: 0
New process pid=27288
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-frb59-26-3.opb

[startup+10.0025 s]
Raw data (loadavg): 0.93 0.95 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 940 33 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 9.74
Current children cumulated vsize (Kb) 33892

[startup+20.0034 s]
Raw data (loadavg): 0.94 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 1939 33 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 33892

[startup+30.0041 s]
Raw data (loadavg): 0.95 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 2939 34 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 33892

[startup+40.0049 s]
Raw data (loadavg): 0.95 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 3938 34 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 33892

[startup+50.0057 s]
Raw data (loadavg): 0.96 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 4938 34 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 33892

[startup+60.0055 s]
Raw data (loadavg): 0.97 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 5938 35 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 33892

[startup+70.0063 s]
Raw data (loadavg): 0.97 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 6938 35 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 69.74
Current children cumulated vsize (Kb) 33892

[startup+80.0071 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 7938 35 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 79.74
Current children cumulated vsize (Kb) 33892

[startup+90.0079 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 8938 35 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 33892

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 9937 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 99.74
Current children cumulated vsize (Kb) 33892

[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 10937 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 109.74
Current children cumulated vsize (Kb) 33892

[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 11938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 119.75
Current children cumulated vsize (Kb) 33892

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 12938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 129.75
Current children cumulated vsize (Kb) 33892

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 13938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223120 134553437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 139.75
Current children cumulated vsize (Kb) 33892

[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 14938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 149.75
Current children cumulated vsize (Kb) 33892

[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 15938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223152 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 159.75
Current children cumulated vsize (Kb) 33892

[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 16938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 169.75
Current children cumulated vsize (Kb) 33892

[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 17939 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223152 134558999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 179.76
Current children cumulated vsize (Kb) 33892

[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 18938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 189.75
Current children cumulated vsize (Kb) 33892

[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 7828 0 0 0 19938 36 0 0 25 0 1 0 1728553073 32530432 7815 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 7942 7815 145 145 0 7797 0
[pid=27288] vsize: 31768
Current children cumulated CPU time (s) 199.75
Current children cumulated vsize (Kb) 33892

[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 8117 0 0 0 20934 38 0 0 25 0 1 0 1728553073 33366016 8026 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 8146 8026 145 145 0 8001 0
[pid=27288] vsize: 32584
Current children cumulated CPU time (s) 209.73
Current children cumulated vsize (Kb) 34708

[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 8559 0 0 0 21928 41 0 0 25 0 1 0 1728553073 35299328 8468 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 8618 8468 145 145 0 8473 0
[pid=27288] vsize: 34472
Current children cumulated CPU time (s) 219.7
Current children cumulated vsize (Kb) 36596

[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 9094 0 0 0 22919 44 0 0 25 0 1 0 1728553073 37478400 9003 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 9150 9003 145 145 0 9005 0
[pid=27288] vsize: 36600
Current children cumulated CPU time (s) 229.64
Current children cumulated vsize (Kb) 38724

[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 9821 0 0 0 23906 49 0 0 25 0 1 0 1728553073 40439808 9730 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 9873 9730 145 145 0 9728 0
[pid=27288] vsize: 39492
Current children cumulated CPU time (s) 239.56
Current children cumulated vsize (Kb) 41616

[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 10415 0 0 0 24896 54 0 0 25 0 1 0 1728553073 42860544 10324 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 10464 10324 145 145 0 10319 0
[pid=27288] vsize: 41856
Current children cumulated CPU time (s) 249.51
Current children cumulated vsize (Kb) 43980

[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 11031 0 0 0 25884 59 0 0 25 0 1 0 1728553073 45367296 10940 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 11076 10940 145 145 0 10931 0
[pid=27288] vsize: 44304
Current children cumulated CPU time (s) 259.44
Current children cumulated vsize (Kb) 46428

[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 11616 0 0 0 26874 63 0 0 25 0 1 0 1728553073 47747072 11525 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 11657 11525 145 145 0 11512 0
[pid=27288] vsize: 46628
Current children cumulated CPU time (s) 269.38
Current children cumulated vsize (Kb) 48752

[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 11987 0 0 0 27869 66 0 0 25 0 1 0 1728553073 48939008 11819 4294967295 134512640 135094434 3221224448 3221223088 134562224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 11948 11819 145 145 0 11803 0
[pid=27288] vsize: 47792
Current children cumulated CPU time (s) 279.36
Current children cumulated vsize (Kb) 49916

[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 12353 0 0 0 28863 68 0 0 25 0 1 0 1728553073 50425856 12185 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 12311 12185 145 145 0 12166 0
[pid=27288] vsize: 49244
Current children cumulated CPU time (s) 289.32
Current children cumulated vsize (Kb) 51368

[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 12825 0 0 0 29854 72 0 0 25 0 1 0 1728553073 52346880 12657 4294967295 134512640 135094434 3221224448 3221223060 134563092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 12780 12657 145 145 0 12635 0
[pid=27288] vsize: 51120
Current children cumulated CPU time (s) 299.27
Current children cumulated vsize (Kb) 53244

[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 13134 0 0 0 30848 75 0 0 25 0 1 0 1728553073 53600256 12966 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 13086 12966 145 145 0 12941 0
[pid=27288] vsize: 52344
Current children cumulated CPU time (s) 309.24
Current children cumulated vsize (Kb) 54468

[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 13464 0 0 0 31842 77 0 0 25 0 1 0 1728553073 55205888 13296 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 13478 13296 145 145 0 13333 0
[pid=27288] vsize: 53912
Current children cumulated CPU time (s) 319.2
Current children cumulated vsize (Kb) 56036

[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 14054 0 0 0 32832 81 0 0 25 0 1 0 1728553073 57610240 13886 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 14065 13886 145 145 0 13920 0
[pid=27288] vsize: 56260
Current children cumulated CPU time (s) 329.14
Current children cumulated vsize (Kb) 58384

[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 14579 0 0 0 33822 85 0 0 25 0 1 0 1728553073 59752448 14411 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 14588 14411 145 145 0 14443 0
[pid=27288] vsize: 58352
Current children cumulated CPU time (s) 339.08
Current children cumulated vsize (Kb) 60476

[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 15248 0 0 0 34811 90 0 0 25 0 1 0 1728553073 62484480 15080 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 15255 15080 145 145 0 15110 0
[pid=27288] vsize: 61020
Current children cumulated CPU time (s) 349.02
Current children cumulated vsize (Kb) 63144

[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 15867 0 0 0 35801 93 0 0 25 0 1 0 1728553073 65011712 15699 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 15872 15699 145 145 0 15727 0
[pid=27288] vsize: 63488
Current children cumulated CPU time (s) 358.95
Current children cumulated vsize (Kb) 65612

[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 16280 0 0 0 36794 97 0 0 25 0 1 0 1728553073 66695168 16112 4294967295 134512640 135094434 3221224448 3221223108 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 16283 16112 145 145 0 16138 0
[pid=27288] vsize: 65132
Current children cumulated CPU time (s) 368.92
Current children cumulated vsize (Kb) 67256

[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 16678 0 0 0 37787 101 0 0 25 0 1 0 1728553073 68313088 16510 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 16678 16510 145 145 0 16533 0
[pid=27288] vsize: 66712
Current children cumulated CPU time (s) 378.89
Current children cumulated vsize (Kb) 68836

[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 17380 0 0 0 38776 106 0 0 25 0 1 0 1728553073 71180288 17212 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 17378 17212 145 145 0 17233 0
[pid=27288] vsize: 69512
Current children cumulated CPU time (s) 388.83
Current children cumulated vsize (Kb) 71636

[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 17902 0 0 0 39766 110 0 0 25 0 1 0 1728553073 73306112 17734 4294967295 134512640 135094434 3221224448 3221223120 134556295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 17897 17734 145 145 0 17752 0
[pid=27288] vsize: 71588
Current children cumulated CPU time (s) 398.77
Current children cumulated vsize (Kb) 73712

[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 18218 0 0 0 40760 112 0 0 25 0 1 0 1728553073 74592256 18050 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 18211 18050 145 145 0 18066 0
[pid=27288] vsize: 72844
Current children cumulated CPU time (s) 408.73
Current children cumulated vsize (Kb) 74968

[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 18634 0 0 0 41751 115 0 0 25 0 1 0 1728553073 76288000 18466 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 18625 18466 145 145 0 18480 0
[pid=27288] vsize: 74500
Current children cumulated CPU time (s) 418.67
Current children cumulated vsize (Kb) 76624

[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 18994 0 0 0 42745 118 0 0 25 0 1 0 1728553073 77750272 18826 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 18982 18826 145 145 0 18837 0
[pid=27288] vsize: 75928
Current children cumulated CPU time (s) 428.64
Current children cumulated vsize (Kb) 78052

[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 19390 0 0 0 43738 121 0 0 25 0 1 0 1728553073 79364096 19222 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 19376 19222 145 145 0 19231 0
[pid=27288] vsize: 77504
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 79628

[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.97 1/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) T 27284 27284 17733 0 -1 0 19873 0 0 0 44728 126 0 0 25 0 1 0 1728553073 81330176 19705 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27288/statm): 19856 19705 145 145 0 19711 0
[pid=27288] vsize: 79424
Current children cumulated CPU time (s) 448.55
Current children cumulated vsize (Kb) 81548

[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 20201 0 0 0 45722 129 0 0 25 0 1 0 1728553073 82669568 20033 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 20183 20033 145 145 0 20038 0
[pid=27288] vsize: 80732
Current children cumulated CPU time (s) 458.52
Current children cumulated vsize (Kb) 82856

[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 20589 0 0 0 46714 133 0 0 25 0 1 0 1728553073 84246528 20421 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 20568 20421 145 145 0 20423 0
[pid=27288] vsize: 82272
Current children cumulated CPU time (s) 468.48
Current children cumulated vsize (Kb) 84396

[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 20982 0 0 0 47707 135 0 0 25 0 1 0 1728553073 85848064 20814 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 20959 20814 145 145 0 20814 0
[pid=27288] vsize: 83836
Current children cumulated CPU time (s) 478.43
Current children cumulated vsize (Kb) 85960

[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 21256 0 0 0 48703 137 0 0 25 0 1 0 1728553073 86962176 21088 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 21231 21088 145 145 0 21086 0
[pid=27288] vsize: 84924
Current children cumulated CPU time (s) 488.41
Current children cumulated vsize (Kb) 87048

[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 21607 0 0 0 49697 140 0 0 25 0 1 0 1728553073 88391680 21439 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 21580 21439 145 145 0 21435 0
[pid=27288] vsize: 86320
Current children cumulated CPU time (s) 498.38
Current children cumulated vsize (Kb) 88444

[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 21933 0 0 0 50692 142 0 0 25 0 1 0 1728553073 89718784 21765 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 21904 21765 145 145 0 21759 0
[pid=27288] vsize: 87616
Current children cumulated CPU time (s) 508.35
Current children cumulated vsize (Kb) 89740

[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 22280 0 0 0 51686 144 0 0 25 0 1 0 1728553073 91131904 22112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 22249 22112 145 145 0 22104 0
[pid=27288] vsize: 88996
Current children cumulated CPU time (s) 518.31
Current children cumulated vsize (Kb) 91120

[startup+530.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 22700 0 0 0 52678 147 0 0 25 0 1 0 1728553073 92844032 22532 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 22667 22532 145 145 0 22522 0
[pid=27288] vsize: 90668
Current children cumulated CPU time (s) 528.26
Current children cumulated vsize (Kb) 92792

[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 23043 0 0 0 53673 149 0 0 25 0 1 0 1728553073 94240768 22875 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 23008 22875 145 145 0 22863 0
[pid=27288] vsize: 92032
Current children cumulated CPU time (s) 538.23
Current children cumulated vsize (Kb) 94156

[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 23513 0 0 0 54666 152 0 0 25 0 1 0 1728553073 96157696 23345 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 23476 23345 145 145 0 23331 0
[pid=27288] vsize: 93904
Current children cumulated CPU time (s) 548.19
Current children cumulated vsize (Kb) 96028

[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 23904 0 0 0 55659 155 0 0 25 0 1 0 1728553073 97751040 23736 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 23865 23736 145 145 0 23720 0
[pid=27288] vsize: 95460
Current children cumulated CPU time (s) 558.15
Current children cumulated vsize (Kb) 97584

[startup+570.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 24329 0 0 0 56652 157 0 0 25 0 1 0 1728553073 99483648 24161 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 24288 24161 145 145 0 24143 0
[pid=27288] vsize: 97152
Current children cumulated CPU time (s) 568.1
Current children cumulated vsize (Kb) 99276

[startup+580.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 24866 0 0 0 57644 160 0 0 25 0 1 0 1728553073 101675008 24698 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 24823 24698 145 145 0 24678 0
[pid=27288] vsize: 99292
Current children cumulated CPU time (s) 578.05
Current children cumulated vsize (Kb) 101416

[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 25342 0 0 0 58637 163 0 0 25 0 1 0 1728553073 103616512 25174 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 25297 25174 145 145 0 25152 0
[pid=27288] vsize: 101188
Current children cumulated CPU time (s) 588.01
Current children cumulated vsize (Kb) 103312

[startup+600.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 25809 0 0 0 59628 168 0 0 25 0 1 0 1728553073 105521152 25641 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 25762 25641 145 145 0 25617 0
[pid=27288] vsize: 103048
Current children cumulated CPU time (s) 597.97
Current children cumulated vsize (Kb) 105172

[startup+610.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26231 0 0 0 60620 171 0 0 25 0 1 0 1728553073 107765760 26063 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26310 26063 145 145 0 26165 0
[pid=27288] vsize: 105240
Current children cumulated CPU time (s) 607.92
Current children cumulated vsize (Kb) 107364

[startup+620.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 61620 171 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 617.92
Current children cumulated vsize (Kb) 107760

[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 62618 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 627.91
Current children cumulated vsize (Kb) 107760

[startup+640.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 63618 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 637.91
Current children cumulated vsize (Kb) 107760

[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 64618 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 647.91
Current children cumulated vsize (Kb) 107760

[startup+660.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 65618 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 657.91
Current children cumulated vsize (Kb) 107760

[startup+670.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 66619 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 667.92
Current children cumulated vsize (Kb) 107760

[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 67619 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 677.92
Current children cumulated vsize (Kb) 107760

[startup+690.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 68619 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 687.92
Current children cumulated vsize (Kb) 107760

[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 69619 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 697.92
Current children cumulated vsize (Kb) 107760

[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 70619 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 707.92
Current children cumulated vsize (Kb) 107760

[startup+720.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 71620 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 717.93
Current children cumulated vsize (Kb) 107760

[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 72620 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 727.93
Current children cumulated vsize (Kb) 107760

[startup+740.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 73620 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 737.93
Current children cumulated vsize (Kb) 107760

[startup+750.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 74621 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 747.94
Current children cumulated vsize (Kb) 107760

[startup+760.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 75621 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 757.94
Current children cumulated vsize (Kb) 107760

[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 76621 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 767.94
Current children cumulated vsize (Kb) 107760

[startup+780.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 77621 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 777.94
Current children cumulated vsize (Kb) 107760

[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 78621 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 787.94
Current children cumulated vsize (Kb) 107760

[startup+800.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 79622 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 797.95
Current children cumulated vsize (Kb) 107760

[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 80622 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 807.95
Current children cumulated vsize (Kb) 107760

[startup+820.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 81622 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 817.95
Current children cumulated vsize (Kb) 107760

[startup+830.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 82622 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 827.95
Current children cumulated vsize (Kb) 107760

[startup+840.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 83623 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 837.96
Current children cumulated vsize (Kb) 107760

[startup+850.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 84623 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 847.96
Current children cumulated vsize (Kb) 107760

[startup+860.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 85623 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223072 134557568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 857.96
Current children cumulated vsize (Kb) 107760

[startup+870.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 86623 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 867.96
Current children cumulated vsize (Kb) 107760

[startup+880.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 87623 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 877.96
Current children cumulated vsize (Kb) 107760

[startup+890.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 88624 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 887.97
Current children cumulated vsize (Kb) 107760

[startup+900.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 89624 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 897.97
Current children cumulated vsize (Kb) 107760

[startup+910.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 90624 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 907.97
Current children cumulated vsize (Kb) 107760

[startup+920.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 91624 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 917.97
Current children cumulated vsize (Kb) 107760

[startup+930.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 92625 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223008 134550324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 927.98
Current children cumulated vsize (Kb) 107760

[startup+940.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 93625 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223040 134556823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 937.98
Current children cumulated vsize (Kb) 107760

[startup+950.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 94625 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 947.98
Current children cumulated vsize (Kb) 107760

[startup+960.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26407 0 0 0 95625 172 0 0 25 0 1 0 1728553073 108171264 26162 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26409 26162 145 145 0 26264 0
[pid=27288] vsize: 105636
Current children cumulated CPU time (s) 957.98
Current children cumulated vsize (Kb) 107760

[startup+970.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 96625 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 967.98
Current children cumulated vsize (Kb) 107840

[startup+980.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 97625 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221222912 134781309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 977.98
Current children cumulated vsize (Kb) 107840

[startup+990.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 98626 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 987.99
Current children cumulated vsize (Kb) 107840

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 99626 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 997.99
Current children cumulated vsize (Kb) 107840

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 100626 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1007.99
Current children cumulated vsize (Kb) 107840

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 101626 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1017.99
Current children cumulated vsize (Kb) 107840

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 102626 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1027.99
Current children cumulated vsize (Kb) 107840

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 103627 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1038
Current children cumulated vsize (Kb) 107840

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 104627 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1048
Current children cumulated vsize (Kb) 107840

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 105627 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1058
Current children cumulated vsize (Kb) 107840

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 106627 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1068
Current children cumulated vsize (Kb) 107840

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 107628 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1078.01
Current children cumulated vsize (Kb) 107840

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 108628 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1088.01
Current children cumulated vsize (Kb) 107840

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 109628 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1098.01
Current children cumulated vsize (Kb) 107840

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 110628 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1108.01
Current children cumulated vsize (Kb) 107840

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 111629 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1118.02
Current children cumulated vsize (Kb) 107840

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 112629 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1128.02
Current children cumulated vsize (Kb) 107840

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 113629 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1138.02
Current children cumulated vsize (Kb) 107840

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 114630 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1148.03
Current children cumulated vsize (Kb) 107840

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 115629 172 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1158.02
Current children cumulated vsize (Kb) 107840

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 116628 173 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1168.02
Current children cumulated vsize (Kb) 107840

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 117627 173 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1178.01
Current children cumulated vsize (Kb) 107840

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 118627 173 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1188.01
Current children cumulated vsize (Kb) 107840

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 119627 173 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1198.01
Current children cumulated vsize (Kb) 107840

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 120627 173 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1208.01
Current children cumulated vsize (Kb) 107840



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/58 27288
Raw data (/proc/27284/stat): 27284 (minisat+_script) S 27283 27284 17733 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1728553069 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27284/statm): 531 226 485 147 0 384 0
[pid=27284] vsize: 2124
Raw data (/proc/27288/stat): 27288 (minisat+_64-bit) R 27284 27284 17733 0 -1 0 26427 0 0 0 120628 173 0 0 25 0 1 0 1728553073 108253184 26182 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27288/statm): 26429 26182 145 145 0 26284 0
[pid=27288] vsize: 105716
Current children cumulated CPU time (s) 1208.02
Current children cumulated vsize (Kb) 107840

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.06
CPU user time (s): 1206.28
CPU system time (s): 1.78073
CPU usage (%): 99.8285
Max. virtual memory (cumulated for all children) (Kb): 107840

Verifier Data

ERROR: no interpretation found !