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/frb50-23-opb/normalized-frb50-23-2.opb
MD5SUM	fe7ff8b16c276b409b25a87eed31b6f9
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	1150
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	1150
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	1150
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.09
Number of variables	1150
Total number of constraints	80851
Number of constraints which are clauses	80851
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 5629

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 01:03:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4095 boxname=wulflinc19 idbench=335 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fe7ff8b16c276b409b25a87eed31b6f9  /oldhome/oroussel/tmp/wulflinc19/normalized-frb50-23-2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-frb50-23-2.opb /oldhome/oroussel/tmp/wulflinc19/normalized-frb50-23-2.opb
IDLAUNCH: 4095
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        881296 kB
Buffers:         34880 kB
Cached:          84132 kB
SwapCached:         56 kB
Active:          50036 kB
Inactive:        71976 kB
HighTotal:      131008 kB
HighFree:        42812 kB
LowTotal:       903652 kB
LowFree:        838484 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25580 kB
Committed_AS:    63744 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:23:29 (client local time) WITH STATUS 10 IN 1209.47 SECONDS
stats: 4095 7 1209.47 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80851 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 |   80851   161702 |   24255       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   80851   161702 |   32340       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.16437 s)
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  148743   320970 |   44622       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46206          
c   -- var.elim.:  2000/46206          
c   -- var.elim.:  3000/46206          
c   -- var.elim.:  4000/46206          
c   -- var.elim.:  5000/46206          
c   -- var.elim.:  6000/46206          
c   -- var.elim.:  7000/46206          
c   -- var.elim.:  8000/46206          
c   -- var.elim.:  9000/46206          
c   -- var.elim.:  10000/46206          
c   -- var.elim.:  11000/46206          
c   -- var.elim.:  12000/46206          
c   -- var.elim.:  13000/46206          
c   -- var.elim.:  14000/46206          
c   -- var.elim.:  15000/46206          
c   -- var.elim.:  16000/46206          
c   -- var.elim.:  17000/46206          
c   -- var.elim.:  18000/46206          
c   -- var.elim.:  19000/46206          
c   -- var.elim.:  20000/46206          
c   -- var.elim.:  21000/46206          
c   -- var.elim.:  22000/46206          
c   -- var.elim.:  23000/46206          
c   -- var.elim.:  24000/46206          
c   -- var.elim.:  25000/46206          
c   -- var.elim.:  26000/46206          
c   -- var.elim.:  27000/46206          
c   -- var.elim.:  28000/46206          
c   -- var.elim.:  29000/46206          
c   -- var.elim.:  30000/46206          
c   -- var.elim.:  31000/46206          
c   -- var.elim.:  32000/46206          
c   -- var.elim.:  33000/46206          
c   -- var.elim.:  34000/46206          
c   -- var.elim.:  35000/46206          
c   -- var.elim.:  36000/46206          
c   -- var.elim.:  37000/46206          
c   -- var.elim.:  38000/46206          
c   -- var.elim.:  39000/46206          
c   -- var.elim.:  40000/46206          
c   -- var.elim.:  41000/46206          
c   -- var.elim.:  42000/46206          
c   -- var.elim.:  43000/46206          
c   -- var.elim.:  44000/46206          
c   -- var.elim.:  45000/46206          
c   -- var.elim.:  46000/46206          
c   -- var.elim.:  46206/46206          
c   -- var.elim.:  1000/23431          
c   -- var.elim.:  2000/23431          
c   -- var.elim.:  3000/23431          
c   -- var.elim.:  4000/23431          
c   -- var.elim.:  5000/23431          
c   -- var.elim.:  6000/23431          
c   -- var.elim.:  7000/23431          
c   -- var.elim.:  8000/23431          
c   -- var.elim.:  9000/23431          
c   -- var.elim.:  10000/23431          
c   -- var.elim.:  11000/23431          
c   -- var.elim.:  12000/23431          
c   -- var.elim.:  13000/23431          
c   -- var.elim.:  14000/23431          
c   -- var.elim.:  15000/23431          
c   -- var.elim.:  16000/23431          
c   -- var.elim.:  17000/23431          
c   -- var.elim.:  18000/23431          
c   -- var.elim.:  19000/23431          
c   -- var.elim.:  20000/23431          
c   -- var.elim.:  21000/23431          
c   -- var.elim.:  22000/23431          
c   -- var.elim.:  23000/23431          
c   -- var.elim.:  23431/23431          
c   -- var.elim.:  196/196          
c   -- var.elim.:  101/101          
c   -- subsuming                       
c   -- var.elim.:  1000/9293          
c   -- var.elim.:  2000/9293          
c   -- var.elim.:  3000/9293          
c   -- var.elim.:  4000/9293          
c   -- var.elim.:  5000/9293          
c   -- var.elim.:  6000/9293          
c   -- var.elim.:  7000/9293          
c   -- var.elim.:  8000/9293          
c   -- var.elim.:  9000/9293          
c   -- var.elim.:  9293/9293          
c   -- var.elim.:  429/429          
c   -- subsuming                       
c   -- var.elim.:  37/37          
c |         0 |  100826   342123 |      --       0       --      -- |     --   | -47911/21171
c |         0 |  100826   342123 |   40330       0        0     nan |  0.000 % |
c |       100 |  100774   340719 |   44340      98    12944   132.1 | 53.574 % |
c |       250 |  100774   340719 |   48774     248    52242   210.7 | 53.574 % |
c |       475 |  100774   340719 |   53652     473   101548   214.7 | 53.574 % |
c |       812 |  100774   340719 |   59017     810   181621   224.2 | 53.574 % |
c |      1318 |  100712   340174 |   64879    1291   299208   231.8 | 53.690 % |
c |      2077 |  100615   339177 |   71298    2044   445998   218.2 | 53.878 % |
c |      3217 |  100615   339177 |   78428    3184   690953   217.0 | 53.878 % |
c |      4925 |  100615   339177 |   86270    4892  1056987   216.1 | 53.878 % |
c |      7487 |  100306   336108 |   94606    7432  1711084   230.2 | 54.494 % |
c |     11331 |   99933   332799 |  103680   11248  2714739   241.4 | 55.213 % |
c ==============================================================================
c (current CPU-time: 299.677 s)
c ==============================================================================
c [1mFound solution: -39[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 |     13906 |  110528   360708 |   33158   13790  3393586   246.1 | 55.213 % |
c   -- subsuming                       
c   -- var.elim.:  1000/20586          
c   -- var.elim.:  2000/20586          
c   -- var.elim.:  3000/20586          
c   -- var.elim.:  4000/20586          
c   -- var.elim.:  5000/20586          
c   -- var.elim.:  6000/20586          
c   -- var.elim.:  7000/20586          
c   -- var.elim.:  8000/20586          
c   -- var.elim.:  9000/20586          
c   -- var.elim.:  10000/20586          
c   -- var.elim.:  11000/20586          
c   -- var.elim.:  12000/20586          
c   -- var.elim.:  13000/20586          
c   -- var.elim.:  14000/20586          
c   -- var.elim.:  15000/20586          
c   -- var.elim.:  16000/20586          
c   -- var.elim.:  17000/20586          
c   -- var.elim.:  18000/20586          
c   -- var.elim.:  19000/20586          
c   -- var.elim.:  20000/20586          
c   -- var.elim.:  20586/20586          
c   -- var.elim.:  1000/8022          
c   -- var.elim.:  2000/8022          
c   -- var.elim.:  3000/8022          
c   -- var.elim.:  4000/8022          
c   -- var.elim.:  5000/8022          
c   -- var.elim.:  6000/8022          
c   -- var.elim.:  7000/8022          
c   -- var.elim.:  8000/8022          
c   -- var.elim.:  8022/8022          
c   -- var.elim.:  952/952          
c   -- subsuming                       
c   -- var.elim.:  1000/6688          
c   -- var.elim.:  2000/6688          
c   -- var.elim.:  3000/6688          
c   -- var.elim.:  4000/6688          
c   -- var.elim.:  5000/6688          
c   -- var.elim.:  6000/6688          
c   -- var.elim.:  6688/6688          
c   -- var.elim.:  143/143          
c |     13906 |   99880   345947 |      --   13790       --      -- |     --   | -10640/-14744
c |     13906 |   99880   345947 |   39952   13727  3362779   245.0 | 55.213 % |
c |     14006 |   99880   345947 |   43947   13827  3387174   245.0 | 63.389 % |
c |     14156 |   99725   342299 |   48266   13963  3403255   243.7 | 63.649 % |
c |     14381 |   99725   342299 |   53093   14188  3456173   243.6 | 63.649 % |
c |     14718 |   99651   341535 |   58359   14463  3564013   246.4 | 63.779 % |
c |     15224 |   99615   341191 |   64172   14960  3730820   249.4 | 63.842 % |
c |     15983 |   99485   339975 |   70497   15703  3955359   251.9 | 64.067 % |
c |     17122 |   99064   335686 |   77219   16807  4281407   254.7 | 64.805 % |
c |     18830 |   98821   332989 |   84732   18496  4791482   259.1 | 65.230 % |
c |     21393 |   98385   328814 |   92794   20977  5567329   265.4 | 65.996 % |
c |     25237 |   98201   326882 |  101883   24774  6481429   261.6 | 66.320 % |
c |     31003 |   97703   322002 |  111503   30453  8200483   269.3 | 67.192 % |
c ==============================================================================
c (current CPU-time: 488.877 s)
c ==============================================================================
c [1mFound solution: -40[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 |     34859 |   99162   320031 |   29748   34170  9413539   275.5 | 67.192 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11071          
c   -- var.elim.:  2000/11071          
c   -- var.elim.:  3000/11071          
c   -- var.elim.:  4000/11071          
c   -- var.elim.:  5000/11071          
c   -- var.elim.:  6000/11071          
c   -- var.elim.:  7000/11071          
c   -- var.elim.:  8000/11071          
c   -- var.elim.:  9000/11071          
c   -- var.elim.:  10000/11071          
c   -- var.elim.:  11000/11071          
c   -- var.elim.:  11071/11071          
c   -- var.elim.:  1000/1561          
c   -- var.elim.:  1561/1561          
c |     34859 |   96855   311764 |      --   34170       --      -- |     --   | -2289/-4514
c |     34859 |   96855   311764 |   38742   31676  6552194   206.9 | 67.192 % |
c |     34959 |   96855   311764 |   42616   31776  6572159   206.8 | 68.973 % |
c |     35109 |   96855   311764 |   46877   31926  6599356   206.7 | 68.972 % |
c |     35334 |   96855   311764 |   51565   32151  6676759   207.7 | 68.972 % |
c |     35671 |   96804   311314 |   56692   32481  6753435   207.9 | 69.056 % |
c |     36178 |   96722   310508 |   62308   32974  6905627   209.4 | 69.195 % |
c |     36937 |   96722   310508 |   68539   33733  7155602   212.1 | 69.195 % |
c |     38077 |   96688   310183 |   75367   34862  7534777   216.1 | 69.251 % |
c |     39785 |   96453   307860 |   82702   36517  8122041   222.4 | 69.651 % |
c |     42347 |   96328   306606 |   90854   39016  8722406   223.6 | 69.863 % |
c |     46193 |   96197   305344 |   99804   42819  9996960   233.5 | 70.083 % |
c |     51959 |   95909   302501 |  109455   48496 12168583   250.9 | 70.563 % |
c |     60608 |   95589   299521 |  119999   57020 15262719   267.7 | 71.105 % |
c |     73582 |   94855   292156 |  130986   69790 19953787   285.9 | 72.372 % |
c |     93044 |   94572   289515 |  143654   89149 27856970   312.5 | 72.849 % |
c ==============================================================================
c (current CPU-time: 1167.76 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 |    120760 |   95992   291504 |   28797  116699 40093011   343.6 | 72.849 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9240          
c   -- var.elim.:  2000/9240          
c   -- var.elim.:  3000/9240          
c   -- var.elim.:  4000/9240          
c   -- var.elim.:  5000/9240          
c   -- var.elim.:  6000/9240          
c   -- var.elim.:  7000/9240          
c   -- var.elim.:  8000/9240          
c   -- var.elim.:  9000/9240          
c   -- var.elim.:  9240/9240          
c   -- var.elim.:  1000/1745          
c   -- var.elim.:  1745/1745          
c   -- subsuming                       
c   -- var.elim.:  445/445          
c |    120760 |   94292   288083 |      --  116699       --      -- |     --   | -1700/-3420
c |    120760 |   94292   288083 |   37716  111038 35703688   321.5 | 72.849 % |
c |    120860 |   94292   288083 |   41488   24469  5679125   232.1 | 73.559 % |
c |    121011 |   94292   288083 |   45637   24620  5730499   232.8 | 73.559 % |
c |    121236 |   94292   288083 |   50201   24845  5778592   232.6 | 73.559 % |
c |    121573 |   94292   288083 |   55221   25182  5893804   234.0 | 73.559 % |
c |    122079 |   94292   288083 |   60743   25688  6007045   233.8 | 73.559 % |
c |    122839 |   94252   287683 |   66789   26445  6268954   237.1 | 73.628 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 -#### 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.87 0.97 0.91 2/55 27680
Raw data (stat): 27680 (runsolver) R 27679 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480476589 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+9.99945 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9320 0 0 0 955 42 0 0 25 0 1 0 480476589 40964096 8742 4294967295 134512640 134672761 3221224560 3221222800 134566437 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8742 603 41 0 9960 0
vsize: 40004
[startup+20.0009 s]
Raw data (loadavg): 0.90 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9326 0 0 0 1954 44 0 0 25 0 1 0 480476589 40964096 8748 4294967295 134512640 134672761 3221224560 3221223152 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8748 603 41 0 9960 0
vsize: 40004
[startup+30.0011 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9327 0 0 0 2955 44 0 0 25 0 1 0 480476589 40964096 8749 4294967295 134512640 134672761 3221224560 3221222992 134604647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8749 603 41 0 9960 0
vsize: 40004
[startup+40.002 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9328 0 0 0 3953 44 0 0 25 0 1 0 480476589 40964096 8750 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10001 8750 603 41 0 9960 0
vsize: 40004
[startup+50.003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9329 0 0 0 4953 44 0 0 25 0 1 0 480476589 40964096 8751 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8751 603 41 0 9960 0
vsize: 40004
[startup+60.0024 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9330 0 0 0 5953 44 0 0 25 0 1 0 480476589 40964096 8752 4294967295 134512640 134672761 3221224560 3221223008 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8752 603 41 0 9960 0
vsize: 40004
[startup+70.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9336 0 0 0 6953 44 0 0 25 0 1 0 480476589 40964096 8758 4294967295 134512640 134672761 3221224560 3221223056 134644227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8758 603 41 0 9960 0
vsize: 40004
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9338 0 0 0 7954 44 0 0 25 0 1 0 480476589 40964096 8760 4294967295 134512640 134672761 3221224560 3221221984 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10001 8760 603 41 0 9960 0
vsize: 40004
[startup+90.0039 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9344 0 0 0 8954 44 0 0 25 0 1 0 480476589 41095168 8766 4294967295 134512640 134672761 3221224560 3221222480 134566697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10033 8766 603 41 0 9992 0
vsize: 40132
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9377 0 0 0 9954 44 0 0 25 0 1 0 480476589 41357312 8799 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8799 603 41 0 10056 0
vsize: 40388
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27680
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9378 0 0 0 10954 44 0 0 25 0 1 0 480476589 41357312 8800 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8800 603 41 0 10056 0
vsize: 40388
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27682
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9379 0 0 0 11954 44 0 0 25 0 1 0 480476589 41357312 8801 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8801 603 41 0 10056 0
vsize: 40388
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27682
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9382 0 0 0 12954 44 0 0 25 0 1 0 480476589 41357312 8804 4294967295 134512640 134672761 3221224560 3221223088 134607032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8804 603 41 0 10056 0
vsize: 40388
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27682
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9385 0 0 0 13954 44 0 0 25 0 1 0 480476589 41357312 8807 4294967295 134512640 134672761 3221224560 3221223056 134644269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8807 603 41 0 10056 0
vsize: 40388
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27682
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9386 0 0 0 14955 44 0 0 25 0 1 0 480476589 41357312 8808 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8808 603 41 0 10056 0
vsize: 40388
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27682
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9389 0 0 0 15955 44 0 0 25 0 1 0 480476589 41357312 8811 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8811 603 41 0 10056 0
vsize: 40388
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27682
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9391 0 0 0 16955 44 0 0 25 0 1 0 480476589 41357312 8813 4294967295 134512640 134672761 3221224560 3221222816 134621256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 8813 603 41 0 10056 0
vsize: 40388
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9418 0 0 0 17955 45 0 0 25 0 1 0 480476589 41365504 8794 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10099 8794 603 41 0 10058 0
vsize: 40396
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9418 0 0 0 18955 45 0 0 25 0 1 0 480476589 41365504 8794 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10099 8794 603 41 0 10058 0
vsize: 40396
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9418 0 0 0 19955 45 0 0 25 0 1 0 480476589 41365504 8794 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10099 8794 603 41 0 10058 0
vsize: 40396
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9731 0 0 0 20954 46 0 0 25 0 1 0 480476589 42467328 9061 4294967295 134512640 134672761 3221224560 3221223056 134606420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10368 9061 603 41 0 10327 0
vsize: 41472
[startup+220.009 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9731 0 0 0 21955 46 0 0 25 0 1 0 480476589 42467328 9061 4294967295 134512640 134672761 3221224560 3221222896 134603502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10368 9061 603 41 0 10327 0
vsize: 41472
[startup+230.009 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9731 0 0 0 22955 46 0 0 25 0 1 0 480476589 42467328 9061 4294967295 134512640 134672761 3221224560 3221223052 134642887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10368 9061 603 41 0 10327 0
vsize: 41472
[startup+240.009 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9731 0 0 0 23955 46 0 0 25 0 1 0 480476589 42467328 9061 4294967295 134512640 134672761 3221224560 3221223024 134644251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10368 9061 603 41 0 10327 0
vsize: 41472
[startup+250.009 s]
Raw data (loadavg): 1.12 1.00 0.93 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 9731 0 0 0 24955 46 0 0 25 0 1 0 480476589 40972288 8755 4294967295 134512640 134672761 3221224560 3221223008 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10003 8755 603 41 0 9962 0
vsize: 40012
[startup+260.01 s]
Raw data (loadavg): 1.10 1.00 0.93 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 10157 0 0 0 25954 47 0 0 25 0 1 0 480476589 41496576 8890 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10131 8890 603 41 0 10090 0
vsize: 40524
[startup+270.01 s]
Raw data (loadavg): 1.09 1.00 0.93 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 10915 0 0 0 26951 49 0 0 25 0 1 0 480476589 44695552 9648 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10912 9648 603 41 0 10871 0
vsize: 43648
[startup+280.009 s]
Raw data (loadavg): 1.23 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 11559 0 0 0 27950 50 0 0 25 0 1 0 480476589 47333376 10292 4294967295 134512640 134672761 3221224560 3221223432 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11556 10292 603 41 0 11515 0
vsize: 46224
[startup+290.011 s]
Raw data (loadavg): 1.19 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 12247 0 0 0 28948 52 0 0 25 0 1 0 480476589 50065408 10980 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12223 10980 603 41 0 12182 0
vsize: 48892
[startup+300.01 s]
Raw data (loadavg): 1.16 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 12991 0 0 0 29947 54 0 0 25 0 1 0 480476589 53116928 11724 4294967295 134512640 134672761 3221224560 3221223744 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12968 11724 603 41 0 12927 0
vsize: 51872
[startup+310.01 s]
Raw data (loadavg): 1.14 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15233 0 0 0 30925 75 0 0 25 0 1 0 480476589 55984128 12533 4294967295 134512640 134672761 3221224560 3221222996 134606988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13668 12533 603 41 0 13627 0
vsize: 54672
[startup+320.011 s]
Raw data (loadavg): 1.11 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15233 0 0 0 31784 137 0 0 25 0 1 0 480476589 55984128 12533 4294967295 134512640 134672761 3221224560 3221222000 134566687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13668 12533 603 41 0 13627 0
vsize: 54672
[startup+330.011 s]
Raw data (loadavg): 1.10 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15233 0 0 0 32783 138 0 0 25 0 1 0 480476589 55984128 12533 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13668 12533 603 41 0 13627 0
vsize: 54672
[startup+340.011 s]
Raw data (loadavg): 1.08 1.03 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15233 0 0 0 33783 138 0 0 25 0 1 0 480476589 55984128 12533 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13668 12533 603 41 0 13627 0
vsize: 54672
[startup+350.012 s]
Raw data (loadavg): 1.07 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15233 0 0 0 34783 138 0 0 25 0 1 0 480476589 55984128 12533 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13668 12533 603 41 0 13627 0
vsize: 54672
[startup+360.012 s]
Raw data (loadavg): 1.06 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15524 0 0 0 35782 139 0 0 25 0 1 0 480476589 57663488 12824 4294967295 134512640 134672761 3221224560 3221222960 134604081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14078 12824 603 41 0 14037 0
vsize: 56312
[startup+370.012 s]
Raw data (loadavg): 1.05 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15524 0 0 0 36783 139 0 0 25 0 1 0 480476589 57663488 12824 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14078 12824 603 41 0 14037 0
vsize: 56312
[startup+380.012 s]
Raw data (loadavg): 1.04 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15524 0 0 0 37783 139 0 0 25 0 1 0 480476589 55984128 12533 4294967295 134512640 134672761 3221224560 3221223008 134643636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13668 12533 603 41 0 13627 0
vsize: 54672
[startup+390.013 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 15525 0 0 0 38783 139 0 0 25 0 1 0 480476589 55984128 12534 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13668 12534 603 41 0 13627 0
vsize: 54672
[startup+400.012 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 16014 0 0 0 39782 140 0 0 25 0 1 0 480476589 58171392 13023 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14202 13023 603 41 0 14161 0
vsize: 56808
[startup+410.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 16615 0 0 0 40781 141 0 0 25 0 1 0 480476589 60608512 13624 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14797 13624 603 41 0 14756 0
vsize: 59188
[startup+420.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 17163 0 0 0 41780 142 0 0 25 0 1 0 480476589 62840832 14172 4294967295 134512640 134672761 3221224560 3221223696 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15342 14172 603 41 0 15301 0
vsize: 61368
[startup+430.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 17639 0 0 0 42779 143 0 0 25 0 1 0 480476589 64794624 14648 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15819 14648 603 41 0 15778 0
vsize: 63276
[startup+440.014 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 18291 0 0 0 43777 146 0 0 25 0 1 0 480476589 67428352 15300 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16462 15300 603 41 0 16421 0
vsize: 65848
[startup+450.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 18854 0 0 0 44776 147 0 0 25 0 1 0 480476589 69672960 15863 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17010 15863 603 41 0 16969 0
vsize: 68040
[startup+460.014 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 19444 0 0 0 45775 148 0 0 25 0 1 0 480476589 72155136 16453 4294967295 134512640 134672761 3221224560 3221223408 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17616 16453 603 41 0 17575 0
vsize: 70464
[startup+470.015 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 27684
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 19996 0 0 0 46774 150 0 0 25 0 1 0 480476589 74366976 17005 4294967295 134512640 134672761 3221224560 3221223472 134644281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18156 17005 603 41 0 18115 0
vsize: 72624
[startup+480.014 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 20532 0 0 0 47773 151 0 0 25 0 1 0 480476589 76607488 17541 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 17541 603 41 0 18662 0
vsize: 74812
[startup+490.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 21070 0 0 0 48772 152 0 0 25 0 1 0 480476589 78831616 18079 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19246 18079 603 41 0 19205 0
vsize: 76984
[startup+500.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23342 0 0 0 49749 174 0 0 25 0 1 0 480476589 81305600 18627 4294967295 134512640 134672761 3221224560 3221223104 134621199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19850 18627 603 41 0 19809 0
vsize: 79400
[startup+510.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23342 0 0 0 50738 185 0 0 25 0 1 0 480476589 79667200 18335 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19450 18335 603 41 0 19409 0
vsize: 77800
[startup+520.016 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23342 0 0 0 51737 185 0 0 25 0 1 0 480476589 79667200 18335 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19450 18335 603 41 0 19409 0
vsize: 77800
[startup+530.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23342 0 0 0 52736 185 0 0 25 0 1 0 480476589 79667200 18335 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19450 18335 603 41 0 19409 0
vsize: 77800
[startup+540.016 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23344 0 0 0 53736 186 0 0 25 0 1 0 480476589 79667200 18337 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19450 18337 603 41 0 19409 0
vsize: 77800
[startup+550.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23346 0 0 0 54736 186 0 0 25 0 1 0 480476589 79667200 18339 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19450 18339 603 41 0 19409 0
vsize: 77800
[startup+560.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23348 0 0 0 55736 186 0 0 25 0 1 0 480476589 79667200 18341 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19450 18341 603 41 0 19409 0
vsize: 77800
[startup+570.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 23535 0 0 0 56735 187 0 0 25 0 1 0 480476589 80441344 18528 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19639 18528 603 41 0 19598 0
vsize: 78556
[startup+580.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 24057 0 0 0 57735 187 0 0 25 0 1 0 480476589 82644992 19050 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20177 19050 603 41 0 20136 0
vsize: 80708
[startup+590.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 24968 0 0 0 58734 189 0 0 25 0 1 0 480476589 86347776 19961 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21081 19961 603 41 0 21040 0
vsize: 84324
[startup+600.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 25683 0 0 0 59732 191 0 0 25 0 1 0 480476589 89317376 20676 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21806 20676 603 41 0 21765 0
vsize: 87224
[startup+610.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 26192 0 0 0 60730 192 0 0 25 0 1 0 480476589 91308032 21185 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22292 21185 603 41 0 22251 0
vsize: 89168
[startup+620.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 26982 0 0 0 61729 194 0 0 25 0 1 0 480476589 94527488 21975 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23078 21975 603 41 0 23037 0
vsize: 92312
[startup+630.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 27482 0 0 0 62728 195 0 0 25 0 1 0 480476589 96632832 22475 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23592 22475 603 41 0 23551 0
vsize: 94368
[startup+640.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 28274 0 0 0 63727 196 0 0 25 0 1 0 480476589 99811328 23267 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24368 23267 603 41 0 24327 0
vsize: 97472
[startup+650.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 28833 0 0 0 64726 198 0 0 25 0 1 0 480476589 102137856 23826 4294967295 134512640 134672761 3221224560 3221223684 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24936 23826 603 41 0 24895 0
vsize: 99744
[startup+660.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 29193 0 0 0 65725 199 0 0 25 0 1 0 480476589 103579648 24186 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25288 24186 603 41 0 25247 0
vsize: 101152
[startup+670.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 29847 0 0 0 66724 200 0 0 25 0 1 0 480476589 106319872 24840 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25957 24840 603 41 0 25916 0
vsize: 103828
[startup+680.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 30286 0 0 0 67723 201 0 0 25 0 1 0 480476589 108003328 25279 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26368 25279 603 41 0 26327 0
vsize: 105472
[startup+690.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 30741 0 0 0 68722 202 0 0 25 0 1 0 480476589 109953024 25734 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26844 25734 603 41 0 26803 0
vsize: 107376
[startup+700.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 31524 0 0 0 69721 204 0 0 25 0 1 0 480476589 113184768 26517 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27633 26517 603 41 0 27592 0
vsize: 110532
[startup+710.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 31878 0 0 0 70720 204 0 0 25 0 1 0 480476589 114618368 26871 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27983 26871 603 41 0 27942 0
vsize: 111932
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 32378 0 0 0 71719 206 0 0 25 0 1 0 480476589 116674560 27371 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28485 27371 603 41 0 28444 0
vsize: 113940
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 33036 0 0 0 72717 208 0 0 25 0 1 0 480476589 119533568 28029 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29183 28029 603 41 0 29142 0
vsize: 116732
[startup+740.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 33551 0 0 0 73716 209 0 0 25 0 1 0 480476589 121692160 28544 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29710 28544 603 41 0 29669 0
vsize: 118840
[startup+750.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 33928 0 0 0 74715 210 0 0 25 0 1 0 480476589 123260928 28921 4294967295 134512640 134672761 3221224560 3221223704 134616284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30093 28921 603 41 0 30052 0
vsize: 120372
[startup+760.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 34573 0 0 0 75714 211 0 0 25 0 1 0 480476589 125841408 29566 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30723 29566 603 41 0 30682 0
vsize: 122892
[startup+770.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27686
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 35217 0 0 0 76713 213 0 0 25 0 1 0 480476589 128438272 30210 4294967295 134512640 134672761 3221224560 3221223704 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31357 30210 603 41 0 31316 0
vsize: 125428
[startup+780.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 35610 0 0 0 77712 214 0 0 25 0 1 0 480476589 130039808 30603 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31748 30603 603 41 0 31707 0
vsize: 126992
[startup+790.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 36091 0 0 0 78711 215 0 0 25 0 1 0 480476589 132038656 31084 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32236 31084 603 41 0 32195 0
vsize: 128944
[startup+800.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 36283 0 0 0 79711 215 0 0 25 0 1 0 480476589 132763648 31276 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32413 31276 603 41 0 32372 0
vsize: 129652
[startup+810.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 36751 0 0 0 80710 216 0 0 25 0 1 0 480476589 134705152 31744 4294967295 134512640 134672761 3221224560 3221223744 134615764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32887 31744 603 41 0 32846 0
vsize: 131548
[startup+820.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 37458 0 0 0 81709 218 0 0 25 0 1 0 480476589 137572352 32451 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33587 32451 603 41 0 33546 0
vsize: 134348
[startup+830.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 38011 0 0 0 82708 219 0 0 25 0 1 0 480476589 139911168 33004 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34158 33004 603 41 0 34117 0
vsize: 136632
[startup+840.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 38442 0 0 0 83707 220 0 0 25 0 1 0 480476589 141611008 33435 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34573 33435 603 41 0 34532 0
vsize: 138292
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 38839 0 0 0 84706 221 0 0 25 0 1 0 480476589 143314944 33832 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34989 33832 603 41 0 34948 0
vsize: 139956
[startup+860.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 39233 0 0 0 85706 221 0 0 25 0 1 0 480476589 144855040 34226 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35365 34226 603 41 0 35324 0
vsize: 141460
[startup+870.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 39856 0 0 0 86705 223 0 0 25 0 1 0 480476589 147443712 34849 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35997 34849 603 41 0 35956 0
vsize: 143988
[startup+880.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 40473 0 0 0 87704 224 0 0 25 0 1 0 480476589 149934080 35466 4294967295 134512640 134672761 3221224560 3221223432 1075353074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36605 35466 603 41 0 36564 0
vsize: 146420
[startup+890.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 41102 0 0 0 88702 226 0 0 25 0 1 0 480476589 152473600 36095 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37225 36095 603 41 0 37184 0
vsize: 148900
[startup+900.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 41676 0 0 0 89701 227 0 0 25 0 1 0 480476589 154927104 36669 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37824 36669 603 41 0 37783 0
vsize: 151296
[startup+910.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 42298 0 0 0 90698 230 0 0 25 0 1 0 480476589 157409280 37291 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38430 37291 603 41 0 38389 0
vsize: 153720
[startup+920.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 42828 0 0 0 91698 231 0 0 25 0 1 0 480476589 159588352 37821 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38962 37821 603 41 0 38921 0
vsize: 155848
[startup+930.025 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 43092 0 0 0 92697 232 0 0 25 0 1 0 480476589 160600064 38085 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39209 38085 603 41 0 39168 0
vsize: 156836
[startup+940.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 43476 0 0 0 93696 233 0 0 25 0 1 0 480476589 162267136 38469 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39616 38469 603 41 0 39575 0
vsize: 158464
[startup+950.025 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 43822 0 0 0 94696 233 0 0 25 0 1 0 480476589 163667968 38815 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39958 38815 603 41 0 39917 0
vsize: 159832
[startup+960.025 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 44160 0 0 0 95695 234 0 0 25 0 1 0 480476589 165081088 39153 4294967295 134512640 134672761 3221224560 3221223744 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40303 39153 603 41 0 40262 0
vsize: 161212
[startup+970.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 44661 0 0 0 96694 236 0 0 25 0 1 0 480476589 167026688 39654 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40778 39654 603 41 0 40737 0
vsize: 163112
[startup+980.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 44985 0 0 0 97693 237 0 0 25 0 1 0 480476589 168325120 39978 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41095 39978 603 41 0 41054 0
vsize: 164380
[startup+990.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 45428 0 0 0 98692 238 0 0 25 0 1 0 480476589 170139648 40421 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41538 40421 603 41 0 41497 0
vsize: 166152
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 45889 0 0 0 99692 239 0 0 25 0 1 0 480476589 172109824 40882 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42019 40882 603 41 0 41978 0
vsize: 168076
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 46181 0 0 0 100691 239 0 0 25 0 1 0 480476589 173268992 41174 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42302 41174 603 41 0 42261 0
vsize: 169208
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 46699 0 0 0 101690 241 0 0 25 0 1 0 480476589 175349760 41692 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42810 41692 603 41 0 42769 0
vsize: 171240
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 47309 0 0 0 102689 242 0 0 25 0 1 0 480476589 177934336 42302 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43441 42302 603 41 0 43400 0
vsize: 173764
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 47910 0 0 0 103688 243 0 0 25 0 1 0 480476589 180400128 42903 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44043 42903 603 41 0 44002 0
vsize: 176172
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 48208 0 0 0 104687 244 0 0 25 0 1 0 480476589 181559296 43201 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44326 43201 603 41 0 44285 0
vsize: 177304
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 48931 0 0 0 105686 245 0 0 25 0 1 0 480476589 184524800 43924 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45050 43924 603 41 0 45009 0
vsize: 180200
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27688
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 49639 0 0 0 106684 247 0 0 25 0 1 0 480476589 187412480 44632 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45755 44632 603 41 0 45714 0
vsize: 183020
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 50251 0 0 0 107683 249 0 0 25 0 1 0 480476589 189943808 45244 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46373 45244 603 41 0 46332 0
vsize: 185492
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 51047 0 0 0 108681 250 0 0 25 0 1 0 480476589 193175552 46040 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47162 46040 603 41 0 47121 0
vsize: 188648
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 51602 0 0 0 109680 251 0 0 25 0 1 0 480476589 195457024 46595 4294967295 134512640 134672761 3221224560 3221223232 134621164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47719 46595 603 41 0 47678 0
vsize: 190876
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 51836 0 0 0 110680 252 0 0 25 0 1 0 480476589 196370432 46829 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47942 46829 603 41 0 47901 0
vsize: 191768
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 52587 0 0 0 111679 254 0 0 25 0 1 0 480476589 199499776 47580 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48706 47580 603 41 0 48665 0
vsize: 194824
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 53134 0 0 0 112677 255 0 0 25 0 1 0 480476589 201789440 48127 4294967295 134512640 134672761 3221224560 3221223704 134616336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49265 48127 603 41 0 49224 0
vsize: 197060
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 53388 0 0 0 113677 255 0 0 25 0 1 0 480476589 202715136 48381 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49491 48381 603 41 0 49450 0
vsize: 197964
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 53743 0 0 0 114676 257 0 0 25 0 1 0 480476589 204263424 48736 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49869 48736 603 41 0 49828 0
vsize: 199476
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 54238 0 0 0 115675 258 0 0 25 0 1 0 480476589 206270464 49231 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50359 49231 603 41 0 50318 0
vsize: 201436
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 54801 0 0 0 116675 258 0 0 25 0 1 0 480476589 208580608 49794 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50923 49794 603 41 0 50882 0
vsize: 203692
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 57570 0 0 0 117650 282 0 0 25 0 1 0 480476589 217268224 50359 4294967295 134512640 134672761 3221224560 3221223104 134621090 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53044 50359 603 41 0 53003 0
vsize: 212176
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 57834 0 0 0 118642 289 0 0 25 0 1 0 480476589 217055232 50331 4294967295 134512640 134672761 3221224560 3221223272 134643314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52992 50331 603 41 0 52951 0
vsize: 211968
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 58062 0 0 0 119642 290 0 0 25 0 1 0 480476589 215629824 50158 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52644 50158 603 41 0 52603 0
vsize: 210576
[startup+1210.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27690
Raw data (stat): 27680 (minisat+) R 27679 22929 22928 0 -1 0 58062 0 0 0 120641 290 0 0 25 0 1 0 480476589 215629824 50158 4294967295 134512640 134672761 3221224560 3221223684 134566106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52644 50158 603 41 0 52603 0
vsize: 210576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.18 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 27690
Raw data (stat): 27680 (minisat+) Z 27679 22929 22928 0 -1 12 58063 0 0 0 120641 305 0 0 25 0 1 0 480476589 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.18
CPU time (s): 1209.47
CPU user time (s): 1206.41
CPU system time (s): 3.05253
CPU usage (%): 99.9411
Max. virtual memory (Kb): 212176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####