PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-1.opb
MD5SUM	20fc65112f36a5d10cc9eaa82c0beb63
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-38
Optimality of the best value was proved	NO
Number of terms in the objective function	1272
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	1272
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	1272
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.1
Number of variables	1272
Total number of constraints	94227
Number of constraints which are clauses	94227
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5633

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 01:04:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4099 boxname=wulflinc13 idbench=339 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  20fc65112f36a5d10cc9eaa82c0beb63  /oldhome/oroussel/tmp/wulflinc13/normalized-frb53-24-1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-frb53-24-1.opb /oldhome/oroussel/tmp/wulflinc13/normalized-frb53-24-1.opb
IDLAUNCH: 4099
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        892824 kB
Buffers:         34956 kB
Cached:          86576 kB
SwapCached:        392 kB
Active:          56120 kB
Inactive:        68700 kB
HighTotal:      131008 kB
HighFree:        40572 kB
LowTotal:       903652 kB
LowFree:        852252 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11412 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:25:02 (client local time) WITH STATUS 10 IN 1209.51 SECONDS
stats: 4099 7 1209.51 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94227 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   94227   188454 |   28268       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   94227   188454 |   37690       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 5.08823 s)
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  169279   364521 |   50783       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/51085          
c   -- var.elim.:  2000/51085          
c   -- var.elim.:  3000/51085          
c   -- var.elim.:  4000/51085          
c   -- var.elim.:  5000/51085          
c   -- var.elim.:  6000/51085          
c   -- var.elim.:  7000/51085          
c   -- var.elim.:  8000/51085          
c   -- var.elim.:  9000/51085          
c   -- var.elim.:  10000/51085          
c   -- var.elim.:  11000/51085          
c   -- var.elim.:  12000/51085          
c   -- var.elim.:  13000/51085          
c   -- var.elim.:  14000/51085          
c   -- var.elim.:  15000/51085          
c   -- var.elim.:  16000/51085          
c   -- var.elim.:  17000/51085          
c   -- var.elim.:  18000/51085          
c   -- var.elim.:  19000/51085          
c   -- var.elim.:  20000/51085          
c   -- var.elim.:  21000/51085          
c   -- var.elim.:  22000/51085          
c   -- var.elim.:  23000/51085          
c   -- var.elim.:  24000/51085          
c   -- var.elim.:  25000/51085          
c   -- var.elim.:  26000/51085          
c   -- var.elim.:  27000/51085          
c   -- var.elim.:  28000/51085          
c   -- var.elim.:  29000/51085          
c   -- var.elim.:  30000/51085          
c   -- var.elim.:  31000/51085          
c   -- var.elim.:  32000/51085          
c   -- var.elim.:  33000/51085          
c   -- var.elim.:  34000/51085          
c   -- var.elim.:  35000/51085          
c   -- var.elim.:  36000/51085          
c   -- var.elim.:  37000/51085          
c   -- var.elim.:  38000/51085          
c   -- var.elim.:  39000/51085          
c   -- var.elim.:  40000/51085          
c   -- var.elim.:  41000/51085          
c   -- var.elim.:  42000/51085          
c   -- var.elim.:  43000/51085          
c   -- var.elim.:  44000/51085          
c   -- var.elim.:  45000/51085          
c   -- var.elim.:  46000/51085          
c   -- var.elim.:  47000/51085          
c   -- var.elim.:  48000/51085          
c   -- var.elim.:  49000/51085          
c   -- var.elim.:  50000/51085          
c   -- var.elim.:  51000/51085          
c   -- var.elim.:  51085/51085          
c   -- var.elim.:  1000/25894          
c   -- var.elim.:  2000/25894          
c   -- var.elim.:  3000/25894          
c   -- var.elim.:  4000/25894          
c   -- var.elim.:  5000/25894          
c   -- var.elim.:  6000/25894          
c   -- var.elim.:  7000/25894          
c   -- var.elim.:  8000/25894          
c   -- var.elim.:  9000/25894          
c   -- var.elim.:  10000/25894          
c   -- var.elim.:  11000/25894          
c   -- var.elim.:  12000/25894          
c   -- var.elim.:  13000/25894          
c   -- var.elim.:  14000/25894          
c   -- var.elim.:  15000/25894          
c   -- var.elim.:  16000/25894          
c   -- var.elim.:  17000/25894          
c   -- var.elim.:  18000/25894          
c   -- var.elim.:  19000/25894          
c   -- var.elim.:  20000/25894          
c   -- var.elim.:  21000/25894          
c   -- var.elim.:  22000/25894          
c   -- var.elim.:  23000/25894          
c   -- var.elim.:  24000/25894          
c   -- var.elim.:  25000/25894          
c   -- var.elim.:  25894/25894          
c   -- var.elim.:  277/277          
c   -- var.elim.:  133/133          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  1000/9578          
c   -- var.elim.:  2000/9578          
c   -- var.elim.:  3000/9578          
c   -- var.elim.:  4000/9578          
c   -- var.elim.:  5000/9578          
c   -- var.elim.:  6000/9578          
c   -- var.elim.:  7000/9578          
c   -- var.elim.:  8000/9578          
c   -- var.elim.:  9000/9578          
c   -- var.elim.:  9578/9578          
c   -- var.elim.:  745/745          
c |         0 |  114590   370200 |      --       0       --      -- |     --   | -54683/5697
c |         0 |  114590   370200 |   45836       0        0     nan |  0.000 % |
c |       100 |  114590   370200 |   50419     100    17364   173.6 | 56.441 % |
c |       250 |  114590   370200 |   55461     250    42134   168.5 | 56.441 % |
c |       475 |  114590   370200 |   61007     475    79058   166.4 | 56.441 % |
c |       813 |  114590   370200 |   67108     813   153970   189.4 | 56.441 % |
c |      1319 |  114552   369818 |   73794    1315   247993   188.6 | 56.514 % |
c |      2079 |  114524   369569 |   81154    2073   378592   182.6 | 56.569 % |
c |      3218 |  114524   369569 |   89269    3212   616220   191.8 | 56.569 % |
c |      4926 |  114410   368480 |   98099    4908  1012522   206.3 | 56.789 % |
c ==============================================================================
c (current CPU-time: 286.056 s)
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5399 |  118401   379410 |   35520    5376  1112396   206.9 | 56.789 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12910          
c   -- var.elim.:  2000/12910          
c   -- var.elim.:  3000/12910          
c   -- var.elim.:  4000/12910          
c   -- var.elim.:  5000/12910          
c   -- var.elim.:  6000/12910          
c   -- var.elim.:  7000/12910          
c   -- var.elim.:  8000/12910          
c   -- var.elim.:  9000/12910          
c   -- var.elim.:  10000/12910          
c   -- var.elim.:  11000/12910          
c   -- var.elim.:  12000/12910          
c   -- var.elim.:  12910/12910          
c   -- var.elim.:  1000/3192          
c   -- var.elim.:  2000/3192          
c   -- var.elim.:  3000/3192          
c   -- var.elim.:  3192/3192          
c   -- var.elim.:  314/314          
c |      5399 |  114430   372531 |      --    5376       --      -- |     --   | -3962/-4912
c |      5399 |  114430   372531 |   45772    5142   751094   146.1 | 56.789 % |
c |      5499 |  114416   372377 |   50343    5241   761516   145.3 | 59.071 % |
c |      5649 |  114400   372193 |   55369    5385   801051   148.8 | 59.100 % |
c |      5875 |  114376   371952 |   60893    5607   856555   152.8 | 59.144 % |
c |      6212 |  114316   371370 |   66948    5937   927917   156.3 | 59.254 % |
c |      6718 |  114316   371370 |   73642    6443  1024061   158.9 | 59.254 % |
c |      7478 |  114316   371370 |   81007    7203  1190932   165.3 | 59.254 % |
c |      8617 |  114282   371085 |   89081    8333  1413747   169.7 | 59.317 % |
c |     10326 |  114282   371085 |   97989   10042  1841893   183.4 | 59.317 % |
c ==============================================================================
c (current CPU-time: 335.799 s)
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12487 |  125783   401030 |   37734   12174  2385089   195.9 | 59.317 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22024          
c   -- var.elim.:  2000/22024          
c   -- var.elim.:  3000/22024          
c   -- var.elim.:  4000/22024          
c   -- var.elim.:  5000/22024          
c   -- var.elim.:  6000/22024          
c   -- var.elim.:  7000/22024          
c   -- var.elim.:  8000/22024          
c   -- var.elim.:  9000/22024          
c   -- var.elim.:  10000/22024          
c   -- var.elim.:  11000/22024          
c   -- var.elim.:  12000/22024          
c   -- var.elim.:  13000/22024          
c   -- var.elim.:  14000/22024          
c   -- var.elim.:  15000/22024          
c   -- var.elim.:  16000/22024          
c   -- var.elim.:  17000/22024          
c   -- var.elim.:  18000/22024          
c   -- var.elim.:  19000/22024          
c   -- var.elim.:  20000/22024          
c   -- var.elim.:  21000/22024          
c   -- var.elim.:  22000/22024          
c   -- var.elim.:  22024/22024          
c   -- var.elim.:  1000/8548          
c   -- var.elim.:  2000/8548          
c   -- var.elim.:  3000/8548          
c   -- var.elim.:  4000/8548          
c   -- var.elim.:  5000/8548          
c   -- var.elim.:  6000/8548          
c   -- var.elim.:  7000/8548          
c   -- var.elim.:  8000/8548          
c   -- var.elim.:  8548/8548          
c   -- var.elim.:  35/35          
c   -- subsuming                       
c   -- var.elim.:  1000/7202          
c   -- var.elim.:  2000/7202          
c   -- var.elim.:  3000/7202          
c   -- var.elim.:  4000/7202          
c   -- var.elim.:  5000/7202          
c   -- var.elim.:  6000/7202          
c   -- var.elim.:  7000/7202          
c   -- var.elim.:  7202/7202          
c   -- var.elim.:  6/6          
c |     12487 |  114253   381844 |      --   12174       --      -- |     --   | -11516/-19157
c |     12487 |  114253   381844 |   45701   12148  2376721   195.6 | 59.317 % |
c |     12588 |  114223   381547 |   50258   12248  2398562   195.8 | 65.352 % |
c |     12738 |  114193   381290 |   55269   12397  2416152   194.9 | 65.399 % |
c |     12963 |  114191   381266 |   60795   12613  2457350   194.8 | 65.402 % |
c |     13300 |  114191   381266 |   66874   12950  2541089   196.2 | 65.402 % |
c |     13806 |  114159   380935 |   73541   13445  2644862   196.7 | 65.453 % |
c |     14565 |  114111   380437 |   80861   14199  2823848   198.9 | 65.528 % |
c |     15706 |  114081   380138 |   88924   15328  3176171   207.2 | 65.575 % |
c |     17414 |  114079   380115 |   97815   17030  3591428   210.9 | 65.578 % |
c |     19976 |  113756   377099 |  107292   19482  4165661   213.8 | 66.082 % |
c |     23820 |  112808   368036 |  117037   23153  5055736   218.4 | 67.568 % |
c |     29587 |  111931   359524 |  127740   28763  6623240   230.3 | 68.925 % |
c |     38237 |  110954   349876 |  139288   37242  9038729   242.7 | 70.423 % |
c |     51212 |  109734   337765 |  151532   49780 12930258   259.7 | 72.309 % |
c ==============================================================================
c (current CPU-time: 715.699 s)
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     63023 |  110340   332423 |   33101   61160 16708853   273.2 | 72.309 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9816          
c   -- var.elim.:  2000/9816          
c   -- var.elim.:  3000/9816          
c   -- var.elim.:  4000/9816          
c   -- var.elim.:  5000/9816          
c   -- var.elim.:  6000/9816          
c   -- var.elim.:  7000/9816          
c   -- var.elim.:  8000/9816          
c   -- var.elim.:  9000/9816          
c   -- var.elim.:  9816/9816          
c   -- var.elim.:  1000/1916          
c   -- var.elim.:  1916/1916          
c   -- subsuming                       
c   -- var.elim.:  423/423          
c |     63023 |  108695   324780 |      --   61160       --      -- |     --   | -1627/-3491
c |     63023 |  108695   324780 |   43478   53096  9302766   175.2 | 72.309 % |
c |     63123 |  108695   324780 |   47825   53196  9331177   175.4 | 74.209 % |
c |     63274 |  108695   324780 |   52608   53347  9384863   175.9 | 74.209 % |
c |     63499 |  108695   324780 |   57869   53572  9449619   176.4 | 74.209 % |
c |     63836 |  108695   324780 |   63656   53909  9538901   176.9 | 74.209 % |
c |     64343 |  108691   324732 |   70019   54409  9664334   177.6 | 74.216 % |
c |     65102 |  108191   320040 |   76666   55083  9855203   178.9 | 74.969 % |
c |     66243 |  108191   320040 |   84333   56224 10228703   181.9 | 74.969 % |
c |     67951 |  108189   320019 |   92765   57921 10783254   186.2 | 74.972 % |
c |     70513 |  107700   315261 |  101580   60353 11538472   191.2 | 75.703 % |
c |     74357 |  107370   311899 |  111396   64054 12628518   197.2 | 76.206 % |
c ==============================================================================
c (current CPU-time: 812.436 s)
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     74811 |  112264   324029 |   33679   64463 12788936   198.4 | 76.206 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12378          
c   -- var.elim.:  2000/12378          
c   -- var.elim.:  3000/12378          
c   -- var.elim.:  4000/12378          
c   -- var.elim.:  5000/12378          
c   -- var.elim.:  6000/12378          
c   -- var.elim.:  7000/12378          
c   -- var.elim.:  8000/12378          
c   -- var.elim.:  9000/12378          
c   -- var.elim.:  10000/12378          
c   -- var.elim.:  11000/12378          
c   -- var.elim.:  12000/12378          
c   -- var.elim.:  12378/12378          
c   -- var.elim.:  1000/3394          
c   -- var.elim.:  2000/3394          
c   -- var.elim.:  3000/3394          
c   -- var.elim.:  3394/3394          
c   -- subsuming                       
c   -- var.elim.:  1000/3094          
c   -- var.elim.:  2000/3094          
c   -- var.elim.:  3000/3094          
c   -- var.elim.:  3094/3094          
c   -- var.elim.:  65/65          
c |     74811 |  107378   314553 |      --   64463       --      -- |     --   | -4865/-9433
c |     74811 |  107378   314553 |   42951   64463 12788936   198.4 | 76.206 % |
c |     74911 |  107336   314141 |   47227   63582 12483959   196.3 | 77.212 % |
c |     75061 |  107336   314141 |   51950   63732 12532584   196.6 | 77.212 % |
c |     75286 |  107336   314141 |   57145   63957 12663756   198.0 | 77.212 % |
c |     75623 |  107196   312641 |   62778   64279 12717104   197.8 | 77.404 % |
c |     76129 |  107196   312641 |   69056   64785 12861679   198.5 | 77.404 % |
c |     76888 |  107054   311114 |   75861   65450 13032153   199.1 | 77.607 % |
c |     78027 |  106954   310124 |   83369   66578 13374371   200.9 | 77.754 % |
c |     79736 |  106830   308841 |   91599   68216 13860421   203.2 | 77.932 % |
c |     82299 |  106660   307151 |  100599   70699 14553451   205.9 | 78.174 % |
c |     86143 |  106540   305911 |  110534   74453 15753684   211.6 | 78.345 % |
c |     91910 |  106199   302415 |  121199   80007 17410604   217.6 | 78.828 % |
c |    100559 |  105634   296521 |  132609   88324 19978577   226.2 | 79.648 % |
c |    113534 |  105189   292033 |  145256  101051 24372969   241.2 | 80.294 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 C915 -C914 -C913 -C912 -C911 C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C1#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 4527
Raw data (stat): 4527 (runsolver) R 4526 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422272927 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 4527
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10100 0 0 0 960 38 0 0 25 0 1 0 422272927 43872256 9509 4294967295 134512640 134672761 3221224560 3221222324 134566734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10711 9509 603 41 0 10670 0
vsize: 42844
[startup+20.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 4527
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10449 0 0 0 1958 40 0 0 25 0 1 0 422272927 45293568 9858 4294967295 134512640 134672761 3221224560 3221222992 134605456 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11058 9858 603 41 0 11017 0
vsize: 44232
[startup+30.002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10455 0 0 0 2957 41 0 0 25 0 1 0 422272927 45293568 9864 4294967295 134512640 134672761 3221224560 3221221952 134566724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11058 9864 603 41 0 11017 0
vsize: 44232
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10456 0 0 0 3956 41 0 0 25 0 1 0 422272927 45293568 9865 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11058 9865 603 41 0 11017 0
vsize: 44232
[startup+50.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10457 0 0 0 4957 41 0 0 25 0 1 0 422272927 45293568 9866 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11058 9866 603 41 0 11017 0
vsize: 44232
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10458 0 0 0 5957 41 0 0 25 0 1 0 422272927 45293568 9867 4294967295 134512640 134672761 3221224560 3221222992 134604097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11058 9867 603 41 0 11017 0
vsize: 44232
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10459 0 0 0 6957 41 0 0 25 0 1 0 422272927 45293568 9868 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11058 9868 603 41 0 11017 0
vsize: 44232
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10492 0 0 0 7957 41 0 0 25 0 1 0 422272927 45555712 9901 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9901 603 41 0 11081 0
vsize: 44488
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10493 0 0 0 8957 41 0 0 25 0 1 0 422272927 45555712 9902 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9902 603 41 0 11081 0
vsize: 44488
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10494 0 0 0 9957 41 0 0 25 0 1 0 422272927 45555712 9903 4294967295 134512640 134672761 3221224560 3221222156 134566528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9903 603 41 0 11081 0
vsize: 44488
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10495 0 0 0 10958 41 0 0 25 0 1 0 422272927 45555712 9904 4294967295 134512640 134672761 3221224560 3221223008 134643966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9904 603 41 0 11081 0
vsize: 44488
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10498 0 0 0 11958 41 0 0 25 0 1 0 422272927 45555712 9907 4294967295 134512640 134672761 3221224560 3221223088 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9907 603 41 0 11081 0
vsize: 44488
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10499 0 0 0 12958 41 0 0 25 0 1 0 422272927 45555712 9908 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9908 603 41 0 11081 0
vsize: 44488
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10500 0 0 0 13958 41 0 0 25 0 1 0 422272927 45555712 9909 4294967295 134512640 134672761 3221224560 3221223088 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9909 603 41 0 11081 0
vsize: 44488
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10502 0 0 0 14958 41 0 0 25 0 1 0 422272927 45555712 9911 4294967295 134512640 134672761 3221224560 3221222992 134604028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 9911 603 41 0 11081 0
vsize: 44488
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10519 0 0 0 15959 41 0 0 25 0 1 0 422272927 45785088 9928 4294967295 134512640 134672761 3221224560 3221222064 134566727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9928 603 41 0 11137 0
vsize: 44712
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10522 0 0 0 16959 41 0 0 25 0 1 0 422272927 45785088 9931 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9931 603 41 0 11137 0
vsize: 44712
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10525 0 0 0 17959 41 0 0 25 0 1 0 422272927 45785088 9934 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9934 603 41 0 11137 0
vsize: 44712
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10529 0 0 0 18959 42 0 0 25 0 1 0 422272927 45785088 9938 4294967295 134512640 134672761 3221224560 3221222656 134566562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9938 603 41 0 11137 0
vsize: 44712
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10535 0 0 0 19958 42 0 0 25 0 1 0 422272927 45785088 9944 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9944 603 41 0 11137 0
vsize: 44712
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10535 0 0 0 20959 42 0 0 25 0 1 0 422272927 45785088 9944 4294967295 134512640 134672761 3221224560 3221223008 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11178 9944 603 41 0 11137 0
vsize: 44712
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10867 0 0 0 21957 43 0 0 25 0 1 0 422272927 48259072 10276 4294967295 134512640 134672761 3221224560 3221223272 134643102 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10276 603 41 0 11741 0
vsize: 47128
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10867 0 0 0 22958 43 0 0 25 0 1 0 422272927 48259072 10276 4294967295 134512640 134672761 3221224560 3221223024 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10276 603 41 0 11741 0
vsize: 47128
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10867 0 0 0 23958 43 0 0 25 0 1 0 422272927 48259072 10276 4294967295 134512640 134672761 3221224560 3221223056 134606928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10276 603 41 0 11741 0
vsize: 47128
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10867 0 0 0 24958 43 0 0 25 0 1 0 422272927 48259072 10276 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10276 603 41 0 11741 0
vsize: 47128
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10867 0 0 0 25958 43 0 0 25 0 1 0 422272927 45785088 9944 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9944 603 41 0 11137 0
vsize: 44712
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 10877 0 0 0 26958 43 0 0 25 0 1 0 422272927 45785088 9954 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11178 9954 603 41 0 11137 0
vsize: 44712
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 11138 0 0 0 27958 43 0 0 25 0 1 0 422272927 46817280 10215 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11430 10215 603 41 0 11389 0
vsize: 45720
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 13626 0 0 0 28948 53 0 0 25 0 1 0 422272927 51994624 11217 4294967295 134512640 134672761 3221224560 3221223104 134621219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12694 11217 603 41 0 12653 0
vsize: 50776
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 13626 0 0 0 29931 70 0 0 25 0 1 0 422272927 49356800 10885 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12050 10885 603 41 0 12009 0
vsize: 48200
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 13626 0 0 0 30932 70 0 0 25 0 1 0 422272927 49356800 10885 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12050 10885 603 41 0 12009 0
vsize: 48200
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 13627 0 0 0 31931 70 0 0 25 0 1 0 422272927 49356800 10886 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12050 10886 603 41 0 12009 0
vsize: 48200
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 14336 0 0 0 32929 71 0 0 25 0 1 0 422272927 52371456 11595 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12786 11595 603 41 0 12745 0
vsize: 51144
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17162 0 0 0 33915 86 0 0 25 0 1 0 422272927 62914560 12817 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15360 12817 603 41 0 15319 0
vsize: 61440
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17215 0 0 0 34895 107 0 0 25 0 1 0 422272927 60211200 12485 4294967295 134512640 134672761 3221224560 3221222768 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 12485 603 41 0 14659 0
vsize: 58800
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17215 0 0 0 35771 152 0 0 25 0 1 0 422272927 60211200 12485 4294967295 134512640 134672761 3221224560 3221223008 134643574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14700 12485 603 41 0 14659 0
vsize: 58800
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17215 0 0 0 36771 152 0 0 25 0 1 0 422272927 60211200 12485 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 12485 603 41 0 14659 0
vsize: 58800
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17215 0 0 0 37771 152 0 0 25 0 1 0 422272927 60211200 12485 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 12485 603 41 0 14659 0
vsize: 58800
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17215 0 0 0 38771 152 0 0 25 0 1 0 422272927 60211200 12485 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 12485 603 41 0 14659 0
vsize: 58800
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17582 0 0 0 39770 153 0 0 25 0 1 0 422272927 62406656 12852 4294967295 134512640 134672761 3221224560 3221223056 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15236 12852 603 41 0 15195 0
vsize: 60944
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17583 0 0 0 40771 153 0 0 25 0 1 0 422272927 60211200 12485 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 12485 603 41 0 14659 0
vsize: 58800
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 17584 0 0 0 41771 153 0 0 25 0 1 0 422272927 60211200 12486 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 12486 603 41 0 14659 0
vsize: 58800
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 18253 0 0 0 42769 154 0 0 25 0 1 0 422272927 62824448 13155 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15338 13155 603 41 0 15297 0
vsize: 61352
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 18860 0 0 0 43768 156 0 0 25 0 1 0 422272927 65409024 13762 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15969 13762 603 41 0 15928 0
vsize: 63876
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 19446 0 0 0 44766 158 0 0 25 0 1 0 422272927 67751936 14348 4294967295 134512640 134672761 3221224560 3221223372 1075350331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16541 14348 603 41 0 16500 0
vsize: 66164
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 19868 0 0 0 45766 159 0 0 25 0 1 0 422272927 69476352 14770 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16962 14770 603 41 0 16921 0
vsize: 67848
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 20155 0 0 0 46765 159 0 0 25 0 1 0 422272927 70631424 15057 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17244 15057 603 41 0 17203 0
vsize: 68976
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 20727 0 0 0 47764 161 0 0 25 0 1 0 422272927 73011200 15629 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17825 15629 603 41 0 17784 0
vsize: 71300
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 21170 0 0 0 48764 162 0 0 25 0 1 0 422272927 74817536 16072 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18266 16072 603 41 0 18225 0
vsize: 73064
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 21675 0 0 0 49763 163 0 0 25 0 1 0 422272927 76906496 16577 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18776 16577 603 41 0 18735 0
vsize: 75104
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 22125 0 0 0 50762 164 0 0 25 0 1 0 422272927 78712832 17027 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19217 17027 603 41 0 19176 0
vsize: 76868
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 22482 0 0 0 51761 165 0 0 25 0 1 0 422272927 80236544 17384 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19589 17384 603 41 0 19548 0
vsize: 78356
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 23070 0 0 0 52760 166 0 0 25 0 1 0 422272927 82714624 17972 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20194 17972 603 41 0 20153 0
vsize: 80776
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 23513 0 0 0 53759 167 0 0 25 0 1 0 422272927 84545536 18415 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20641 18415 603 41 0 20600 0
vsize: 82564
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 24094 0 0 0 54758 169 0 0 25 0 1 0 422272927 86851584 18996 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21204 18996 603 41 0 21163 0
vsize: 84816
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 24830 0 0 0 55756 170 0 0 25 0 1 0 422272927 89837568 19732 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21933 19732 603 41 0 21892 0
vsize: 87732
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 25194 0 0 0 56756 171 0 0 25 0 1 0 422272927 91398144 20096 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22314 20096 603 41 0 22273 0
vsize: 89256
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 25699 0 0 0 57755 172 0 0 25 0 1 0 422272927 93401088 20601 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22803 20601 603 41 0 22762 0
vsize: 91212
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 26010 0 0 0 58755 172 0 0 25 0 1 0 422272927 94711808 20912 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23123 20912 603 41 0 23082 0
vsize: 92492
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 26479 0 0 0 59754 173 0 0 25 0 1 0 422272927 96645120 21381 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23595 21381 603 41 0 23554 0
vsize: 94380
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 26905 0 0 0 60754 174 0 0 25 0 1 0 422272927 98426880 21807 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24030 21807 603 41 0 23989 0
vsize: 96120
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 27239 0 0 0 61753 175 0 0 25 0 1 0 422272927 99729408 22141 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24348 22141 603 41 0 24307 0
vsize: 97392
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 27757 0 0 0 62752 176 0 0 25 0 1 0 422272927 101810176 22659 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24856 22659 603 41 0 24815 0
vsize: 99424
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 28275 0 0 0 63750 178 0 0 25 0 1 0 422272927 103989248 23177 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25388 23177 603 41 0 25347 0
vsize: 101552
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 28784 0 0 0 64749 179 0 0 25 0 1 0 422272927 106082304 23686 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25899 23686 603 41 0 25858 0
vsize: 103596
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 29214 0 0 0 65749 180 0 0 25 0 1 0 422272927 107786240 24116 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26315 24116 603 41 0 26274 0
vsize: 105260
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 29679 0 0 0 66747 181 0 0 25 0 1 0 422272927 109641728 24581 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26768 24581 603 41 0 26727 0
vsize: 107072
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 29965 0 0 0 67747 182 0 0 25 0 1 0 422272927 110825472 24867 4294967295 134512640 134672761 3221224560 3221223424 1075349729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27057 24867 603 41 0 27016 0
vsize: 108228
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 30592 0 0 0 68745 184 0 0 25 0 1 0 422272927 113385472 25494 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27682 25494 603 41 0 27641 0
vsize: 110728
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 30998 0 0 0 69744 185 0 0 25 0 1 0 422272927 115081216 25900 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28096 25900 603 41 0 28055 0
vsize: 112384
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 31424 0 0 0 70744 186 0 0 25 0 1 0 422272927 116781056 26326 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28511 26326 603 41 0 28470 0
vsize: 114044
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 34873 0 0 0 71717 212 0 0 25 0 1 0 422272927 121151488 27196 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29578 27196 603 41 0 29537 0
vsize: 118312
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 34884 0 0 0 72709 219 0 0 25 0 1 0 422272927 118779904 26838 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28999 26838 603 41 0 28958 0
vsize: 115996
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35253 0 0 0 73709 220 0 0 25 0 1 0 422272927 118636544 26826 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26826 603 41 0 28923 0
vsize: 115856
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35253 0 0 0 74709 220 0 0 25 0 1 0 422272927 118636544 26826 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26826 603 41 0 28923 0
vsize: 115856
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35253 0 0 0 75709 220 0 0 25 0 1 0 422272927 118636544 26826 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26826 603 41 0 28923 0
vsize: 115856
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35253 0 0 0 76709 220 0 0 25 0 1 0 422272927 118636544 26826 4294967295 134512640 134672761 3221224560 3221223744 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26826 603 41 0 28923 0
vsize: 115856
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35254 0 0 0 77710 220 0 0 25 0 1 0 422272927 118636544 26827 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26827 603 41 0 28923 0
vsize: 115856
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35254 0 0 0 78710 220 0 0 25 0 1 0 422272927 118636544 26827 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26827 603 41 0 28923 0
vsize: 115856
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35256 0 0 0 79710 220 0 0 25 0 1 0 422272927 118636544 26829 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26829 603 41 0 28923 0
vsize: 115856
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 35257 0 0 0 80710 220 0 0 25 0 1 0 422272927 118636544 26830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28964 26830 603 41 0 28923 0
vsize: 115856
[startup+820.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 37926 0 0 0 81684 245 0 0 25 0 1 0 422272927 121225216 27325 4294967295 134512640 134672761 3221224560 3221223052 134642872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29596 27325 603 41 0 29555 0
vsize: 118384
[startup+830.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 37926 0 0 0 82666 264 0 0 25 0 1 0 422272927 118644736 26953 4294967295 134512640 134672761 3221224560 3221223008 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28966 26953 603 41 0 28925 0
vsize: 115864
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38298 0 0 0 83665 265 0 0 25 0 1 0 422272927 118644736 26953 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28966 26953 603 41 0 28925 0
vsize: 115864
[startup+850.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38331 0 0 0 84665 265 0 0 25 0 1 0 422272927 118906880 26986 4294967295 134512640 134672761 3221224560 3221223472 134644291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29030 26986 603 41 0 28989 0
vsize: 116120
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38332 0 0 0 85665 265 0 0 25 0 1 0 422272927 118906880 26987 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29030 26987 603 41 0 28989 0
vsize: 116120
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38334 0 0 0 86665 265 0 0 25 0 1 0 422272927 119169024 26989 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26989 603 41 0 29053 0
vsize: 116376
[startup+880.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38335 0 0 0 87665 265 0 0 25 0 1 0 422272927 119169024 26990 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26990 603 41 0 29053 0
vsize: 116376
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38337 0 0 0 88666 265 0 0 25 0 1 0 422272927 119169024 26992 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26992 603 41 0 29053 0
vsize: 116376
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38338 0 0 0 89666 265 0 0 25 0 1 0 422272927 119169024 26993 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26993 603 41 0 29053 0
vsize: 116376
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38339 0 0 0 90666 265 0 0 25 0 1 0 422272927 119169024 26994 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26994 603 41 0 29053 0
vsize: 116376
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38341 0 0 0 91666 265 0 0 25 0 1 0 422272927 119169024 26996 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26996 603 41 0 29053 0
vsize: 116376
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38342 0 0 0 92666 265 0 0 25 0 1 0 422272927 119169024 26997 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26997 603 41 0 29053 0
vsize: 116376
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38343 0 0 0 93667 265 0 0 25 0 1 0 422272927 119169024 26998 4294967295 134512640 134672761 3221224560 3221222464 134566490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 26998 603 41 0 29053 0
vsize: 116376
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38373 0 0 0 94667 265 0 0 25 0 1 0 422272927 119300096 27028 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29126 27028 603 41 0 29085 0
vsize: 116504
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 38676 0 0 0 95666 266 0 0 25 0 1 0 422272927 120619008 27331 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29448 27331 603 41 0 29407 0
vsize: 117792
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 39239 0 0 0 96665 267 0 0 25 0 1 0 422272927 122839040 27894 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29990 27894 603 41 0 29949 0
vsize: 119960
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 39487 0 0 0 97665 267 0 0 25 0 1 0 422272927 123875328 28142 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30243 28142 603 41 0 30202 0
vsize: 120972
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 40006 0 0 0 98665 268 0 0 25 0 1 0 422272927 126062592 28661 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30777 28661 603 41 0 30736 0
vsize: 123108
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 40307 0 0 0 99664 268 0 0 25 0 1 0 422272927 127225856 28962 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31061 28962 603 41 0 31020 0
vsize: 124244
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 40634 0 0 0 100664 269 0 0 25 0 1 0 422272927 128536576 29289 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31381 29289 603 41 0 31340 0
vsize: 125524
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 41045 0 0 0 101663 270 0 0 25 0 1 0 422272927 130248704 29700 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31799 29700 603 41 0 31758 0
vsize: 127196
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 41406 0 0 0 102662 271 0 0 25 0 1 0 422272927 131690496 30061 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32151 30061 603 41 0 32110 0
vsize: 128604
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 41879 0 0 0 103661 272 0 0 25 0 1 0 422272927 133636096 30534 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32626 30534 603 41 0 32585 0
vsize: 130504
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 42315 0 0 0 104660 273 0 0 25 0 1 0 422272927 135479296 30970 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33076 30970 603 41 0 33035 0
vsize: 132304
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 42668 0 0 0 105660 274 0 0 25 0 1 0 422272927 136912896 31323 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33426 31323 603 41 0 33385 0
vsize: 133704
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 42972 0 0 0 106659 275 0 0 25 0 1 0 422272927 138080256 31627 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33711 31627 603 41 0 33670 0
vsize: 134844
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 43382 0 0 0 107659 275 0 0 25 0 1 0 422272927 139739136 32037 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34116 32037 603 41 0 34075 0
vsize: 136464
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 43880 0 0 0 108657 277 0 0 25 0 1 0 422272927 141770752 32535 4294967295 134512640 134672761 3221224560 3221223600 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34612 32535 603 41 0 34571 0
vsize: 138448
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 44737 0 0 0 109656 279 0 0 25 0 1 0 422272927 145297408 33392 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35473 33392 603 41 0 35432 0
vsize: 141892
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 44992 0 0 0 110655 280 0 0 25 0 1 0 422272927 146341888 33647 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35728 33647 603 41 0 35687 0
vsize: 142912
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 45269 0 0 0 111654 281 0 0 25 0 1 0 422272927 147509248 33924 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36013 33924 603 41 0 35972 0
vsize: 144052
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 45482 0 0 0 112654 281 0 0 25 0 1 0 422272927 148439040 34137 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36240 34137 603 41 0 36199 0
vsize: 144960
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 46089 0 0 0 113652 283 0 0 25 0 1 0 422272927 150876160 34744 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36835 34744 603 41 0 36794 0
vsize: 147340
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 46534 0 0 0 114651 284 0 0 25 0 1 0 422272927 152711168 35189 4294967295 134512640 134672761 3221224560 3221223600 134603527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37283 35189 603 41 0 37242 0
vsize: 149132
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 46775 0 0 0 115651 284 0 0 25 0 1 0 422272927 153616384 35430 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37504 35430 603 41 0 37463 0
vsize: 150016
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 46950 0 0 0 116650 285 0 0 25 0 1 0 422272927 154411008 35605 4294967295 134512640 134672761 3221224560 3221223504 134606964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37698 35605 603 41 0 37657 0
vsize: 150792
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 47401 0 0 0 117650 286 0 0 25 0 1 0 422272927 156270592 36056 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38152 36056 603 41 0 38111 0
vsize: 152608
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 47687 0 0 0 118650 286 0 0 25 0 1 0 422272927 157433856 36342 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38436 36342 603 41 0 38395 0
vsize: 153744
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 48038 0 0 0 119648 288 0 0 25 0 1 0 422272927 158887936 36693 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38791 36693 603 41 0 38750 0
vsize: 155164
[startup+1210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4529
Raw data (stat): 4527 (minisat+) R 4526 30701 30700 0 -1 0 48408 0 0 0 120648 289 0 0 25 0 1 0 422272927 160313344 37063 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39139 37063 603 41 0 39098 0
vsize: 156556
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4529
Raw data (stat): 4527 (minisat+) Z 4526 30701 30700 0 -1 12 48409 0 0 0 120648 302 0 0 25 0 1 0 422272927 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.51
CPU user time (s): 1206.48
CPU system time (s): 3.02454
CPU usage (%): 99.9468
Max. virtual memory (Kb): 156556
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####