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-1.opb
MD5SUM	ed1ca962177baf0f135b785abad8adea
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
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.08
Number of variables	1150
Total number of constraints	80072
Number of constraints which are clauses	80072
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 6379

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        888512 kB
Buffers:         36408 kB
Cached:          89528 kB
SwapCached:          0 kB
Active:          59192 kB
Inactive:        69612 kB
HighTotal:      131008 kB
HighFree:        37688 kB
LowTotal:       903652 kB
LowFree:        850824 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11792 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:05:24 (client local time) WITH STATUS 10 IN 1200.48 SECONDS
stats: 4846 7 1200.48 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80072 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80072   160144 |   26690       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216544   479415 |   72181       0        0     nan |  0.000 % |
c |       100 |  216234   478712 |   79399      92      431     4.7 |  0.195 % |
c |       250 |  214581   474947 |   87339     198     1287     6.5 |  1.233 % |
c |       475 |  212245   469573 |   96072     364     2406     6.6 |  2.838 % |
c |       812 |  209920   464239 |  105680     663     6217     9.4 |  4.313 % |
c |      1318 |  203848   450322 |  116248    1046     8686     8.3 |  8.287 % |
c |      2077 |  197613   435978 |  127873    1667    14213     8.5 | 12.451 % |
c |      3217 |  187846   413432 |  140660    2537    23795     9.4 | 19.267 % |
c |      4925 |  166557   364082 |  154726    3559    34615     9.7 | 34.052 % |
c |      7488 |  146666   317494 |  170199    5338    58917    11.0 | 48.199 % |
c |     11332 |  124147   264883 |  187218    7562    94083    12.4 | 64.633 % |
c |     17098 |  109769   231059 |  205940   10844   143010    13.2 | 75.418 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18634 |  107086   224758 |   35695   11382   154515    13.6 | 75.418 % |
c |     18734 |  106961   224461 |   39264   11447   156371    13.7 | 77.530 % |
c |     18884 |  106812   224111 |   43190   11539   157870    13.7 | 77.638 % |
c |     19109 |  105873   221893 |   47510   11297   155272    13.7 | 78.346 % |
c |     19447 |  105210   220321 |   52261   11389   155647    13.7 | 78.850 % |
c |     19953 |  105025   219879 |   57487   11798   164220    13.9 | 78.997 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20645 |  104748   219269 |   34916   12289   186417    15.2 | 78.997 % |
c |     20745 |  104748   219269 |   38407   12389   188652    15.2 | 79.295 % |
c |     20895 |  104728   219223 |   42248   12532   190249    15.2 | 79.308 % |
c |     21121 |  104342   218313 |   46473   12558   190398    15.2 | 79.606 % |
c |     21458 |  101824   212419 |   51120   12493   190725    15.3 | 81.468 % |
c |     21966 |   99733   207526 |   56232   12501   193616    15.5 | 83.024 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22577 |   99702   207446 |   33234   13058   213708    16.4 | 83.024 % |
c |     22677 |   99642   207305 |   36557   13096   214603    16.4 | 83.085 % |
c |     22827 |   99642   207305 |   40213   13246   218078    16.5 | 83.085 % |
c |     23052 |   99642   207305 |   44234   13471   222745    16.5 | 83.085 % |
c |     23389 |   99257   206397 |   48657   13662   226785    16.6 | 83.391 % |
c |     23895 |   98990   205766 |   53523   13810   237520    17.2 | 83.607 % |
c |     24655 |   98854   205449 |   58876   14480   270331    18.7 | 83.708 % |
c |     25794 |   98206   203930 |   64763   15013   311922    20.8 | 84.196 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27181 |   98161   203838 |   32720   16309   397772    24.4 | 84.196 % |
c |     27281 |   98155   203824 |   35992   16404   399643    24.4 | 84.266 % |
c |     27432 |   98147   203805 |   39591   16554   408173    24.7 | 84.272 % |
c |     27657 |   98032   203541 |   43550   16762   421659    25.2 | 84.348 % |
c |     27994 |   97980   203418 |   47905   17051   443524    26.0 | 84.387 % |
c |     28500 |   97916   203263 |   52695   17498   474476    27.1 | 84.443 % |
c |     29259 |   97420   202104 |   57965   17671   487620    27.6 | 84.809 % |
c |     30398 |   97267   201746 |   63762   18667   534031    28.6 | 84.924 % |
c |     32107 |   97055   201246 |   70138   20218   598665    29.6 | 85.088 % |
c |     34669 |   96681   200354 |   77152   22351   721144    32.3 | 85.375 % |
c |     38513 |   96062   198908 |   84867   25576   923235    36.1 | 85.834 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40821 |   95787   198238 |   31929   27537  1059909    38.5 | 85.834 % |
c |     40921 |   95787   198238 |   35121   27637  1062305    38.4 | 86.031 % |
c |     41071 |   95787   198238 |   38634   27787  1076225    38.7 | 86.031 % |
c |     41297 |   95373   197277 |   42497   27633  1075858    38.9 | 86.324 % |
c |     41634 |   95373   197277 |   46747   27970  1091796    39.0 | 86.324 % |
c |     42140 |   95367   197263 |   51421   28454  1140179    40.1 | 86.328 % |
c |     42899 |   95290   197077 |   56564   29205  1182083    40.5 | 86.399 % |
c |     44038 |   95290   197077 |   62220   30344  1295278    42.7 | 86.399 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45153 |   95161   196792 |   31720   31411  1353110    43.1 | 86.399 % |
c |     45253 |   95161   196792 |   34892   31511  1354596    43.0 | 86.534 % |
c |     45404 |   95157   196783 |   38381   31661  1362528    43.0 | 86.536 % |
c |     45629 |   95157   196783 |   42219   31886  1381701    43.3 | 86.536 % |
c |     45966 |   95149   196765 |   46441   32203  1387373    43.1 | 86.540 % |
c |     46473 |   95145   196756 |   51085   32707  1422262    43.5 | 86.542 % |
c |     47232 |   95145   196756 |   56193   33466  1497764    44.8 | 86.542 % |
c |     48372 |   95145   196756 |   61813   34606  1567475    45.3 | 86.542 % |
c |     50080 |   95145   196756 |   67994   36314  1773209    48.8 | 86.542 % |
c |     52643 |   95145   196756 |   74794   38877  2064876    53.1 | 86.542 % |
c |     56487 |   95145   196756 |   82273   42721  2544626    59.6 | 86.542 % |
c |     62255 |   94805   195957 |   90500   47637  3113253    65.4 | 86.803 % |
c |     70904 |   94805   195957 |   99550   56286  4461051    79.3 | 86.803 % |
c |     83878 |   94805   195957 |  109506   69260  6454334    93.2 | 86.803 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84429 |   94777   195885 |   31592   69577  6485052    93.2 | 86.803 % |
c |     84529 |   94777   195885 |   34751   69677  6493777    93.2 | 86.821 % |
c |     84679 |   94777   195885 |   38226   69827  6498086    93.1 | 86.821 % |
c |     84905 |   94777   195885 |   42048   70053  6518206    93.0 | 86.821 % |
c |     85243 |   94777   195885 |   46253   70391  6548612    93.0 | 86.821 % |
c |     85751 |   94777   195885 |   50879   70899  6574743    92.7 | 86.821 % |
c |     86510 |   94777   195885 |   55967   71658  6668099    93.1 | 86.821 % |
c |     87649 |   94777   195885 |   61563   72797  6797960    93.4 | 86.821 % |
c |     89358 |   94777   195885 |   67720   74506  6963133    93.5 | 86.821 % |
c |     91920 |   94668   195627 |   74492   77041  7230129    93.8 | 86.909 % |
c |     95765 |   94668   195627 |   81941   80886  7848278    97.0 | 86.909 % |
c |    101531 |   94668   195627 |   90135   86652  8431403    97.3 | 86.909 % |
c |    110182 |   94668   195627 |   99149   95303  9836963   103.2 | 86.909 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    113160 |   94558   195377 |   31519   98257 10261196   104.4 | 86.909 % |
c |    113260 |   94558   195377 |   34670   20721  2009892    97.0 | 87.011 % |
c |    113410 |   94558   195377 |   38137   20871  2015283    96.6 | 87.011 % |
c |    113635 |   94558   195377 |   41951   21096  2033040    96.4 | 87.011 % |
c |    113972 |   94558   195377 |   46146   21433  2055707    95.9 | 87.011 % |
c |    114481 |   94502   195244 |   50761   21939  2091084    95.3 | 87.056 % |
c |    115240 |   94502   195244 |   55837   22698  2129616    93.8 | 87.056 % |
c |    116379 |   94189   194506 |   61421   23814  2226664    93.5 | 87.304 % |
c |    118089 |   94013   194095 |   67563   25517  2478561    97.1 | 87.429 % |
c |    120651 |   93884   193793 |   74320   28053  2646068    94.3 | 87.525 % |
c |    124496 |   93856   193726 |   81752   31889  2954397    92.6 | 87.549 % |
c |    130262 |   93856   193726 |   89927   37655  3680714    97.7 | 87.549 % |
c |    138912 |   93673   193307 |   98920   46294  4616789    99.7 | 87.674 % |
c |    151888 |   93450   192781 |  108812   59186  6163179   104.1 | 87.846 % |
c |    171350 |   93444   192767 |  119693   78645  8596912   109.3 | 87.850 % |
c ==============================================================================
c [1mFound solution: -46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192366 |   93320   192446 |   31106   99608 10930004   109.7 | 87.850 % |
c |    192466 |   93320   192446 |   34216   22473  1378694    61.3 | 87.939 % |
c |    192617 |   93320   192446 |   37638   22624  1388775    61.4 | 87.939 % |
c |    192843 |   93320   192446 |   41402   22850  1408024    61.6 | 87.939 % |
c |    193180 |   93320   192446 |   45542   23187  1443514    62.3 | 87.939 % |
c |    193686 |   93320   192446 |   50096   23693  1480427    62.5 | 87.939 % |
c |    194445 |   93320   192446 |   55106   24452  1568040    64.1 | 87.939 % |
c |    195584 |   93320   192446 |   60616   25591  1676159    65.5 | 87.939 % |
c |    197292 |   93320   192446 |   66678   27299  1874143    68.7 | 87.939 % |
c |    199854 |   93168   192089 |   73346   29792  2097985    70.4 | 88.053 % |
c |    203699 |   93162   192075 |   80680   33634  2489952    74.0 | 88.057 % |
c |    209465 |   93162   192075 |   88749   39400  3083959    78.3 | 88.057 % |
c |    218114 |   93134   192010 |   97623   48031  4097694    85.3 | 88.076 % |
c |    231088 |   93042   191798 |  107386   60994  5691126    93.3 | 88.134 % |
c |    250549 |   93034   191779 |  118124   80452  8710141   108.3 | 88.141 % |
c |    279741 |   93028   191765 |  129937  109641 11050373   100.8 | 88.145 % |
c |    323531 |   93016   191737 |  142931  153427 14810729    96.5 | 88.154 % |
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 -C634 -C633 -C632 C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 C509 -C508 -C507 -C506 -C505 C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C#### 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.92 0.98 0.92 2/54 13524
Raw data (stat): 13524 (runsolver) R 13523 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423588789 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5248 0 0 0 982 15 0 0 25 0 1 0 423588789 24330240 5226 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5940 5226 603 41 0 5899 0
vsize: 23760
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5254 0 0 0 1981 15 0 0 25 0 1 0 423588789 24330240 5232 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5940 5232 603 41 0 5899 0
vsize: 23760
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5262 0 0 0 2981 15 0 0 25 0 1 0 423588789 24330240 5240 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5940 5240 603 41 0 5899 0
vsize: 23760
[startup+40.002 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5265 0 0 0 3980 15 0 0 25 0 1 0 423588789 24330240 5243 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5940 5243 603 41 0 5899 0
vsize: 23760
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5271 0 0 0 4980 16 0 0 25 0 1 0 423588789 24330240 5249 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5940 5249 603 41 0 5899 0
vsize: 23760
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5278 0 0 0 5981 16 0 0 25 0 1 0 423588789 24477696 5256 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5976 5256 603 41 0 5935 0
vsize: 23904
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5288 0 0 0 6981 16 0 0 25 0 1 0 423588789 24477696 5266 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5976 5266 603 41 0 5935 0
vsize: 23904
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5297 0 0 0 7981 16 0 0 25 0 1 0 423588789 24477696 5275 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5976 5275 603 41 0 5935 0
vsize: 23904
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5318 0 0 0 8981 16 0 0 25 0 1 0 423588789 24616960 5296 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6010 5296 603 41 0 5969 0
vsize: 24040
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5612 0 0 0 9980 17 0 0 25 0 1 0 423588789 26611712 5590 4294967295 134512640 134672761 3221224560 3221223760 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6497 5590 603 41 0 6456 0
vsize: 25988
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 5761 0 0 0 10980 18 0 0 25 0 1 0 423588789 27336704 5739 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6674 5739 603 41 0 6633 0
vsize: 26696
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 6048 0 0 0 11979 18 0 0 25 0 1 0 423588789 28405760 6026 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6935 6026 603 41 0 6894 0
vsize: 27740
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 6430 0 0 0 12978 20 0 0 25 0 1 0 423588789 30019584 6408 4294967295 134512640 134672761 3221224560 3221223664 134559824 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7329 6408 603 41 0 7288 0
vsize: 29316
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 6818 0 0 0 13976 21 0 0 25 0 1 0 423588789 31531008 6796 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7698 6796 603 41 0 7657 0
vsize: 30792
[startup+150.006 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 7315 0 0 0 14975 22 0 0 25 0 1 0 423588789 33685504 7293 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8224 7293 603 41 0 8183 0
vsize: 32896
[startup+160.006 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 7919 0 0 0 15974 24 0 0 25 0 1 0 423588789 36220928 7897 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8843 7897 603 41 0 8802 0
vsize: 35372
[startup+170.006 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 8383 0 0 0 16972 25 0 0 25 0 1 0 423588789 38096896 8361 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9301 8361 603 41 0 9260 0
vsize: 37204
[startup+180.006 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 8818 0 0 0 17971 26 0 0 25 0 1 0 423588789 39845888 8796 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9728 8796 603 41 0 9687 0
vsize: 38912
[startup+190.007 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 9358 0 0 0 18970 28 0 0 25 0 1 0 423588789 42102784 9336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10279 9336 603 41 0 10238 0
vsize: 41116
[startup+200.007 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 9892 0 0 0 19969 29 0 0 25 0 1 0 423588789 44232704 9870 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9870 603 41 0 10758 0
vsize: 43196
[startup+210.008 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 10423 0 0 0 20968 30 0 0 25 0 1 0 423588789 46358528 10401 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11318 10401 603 41 0 11277 0
vsize: 45272
[startup+220.007 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 10882 0 0 0 21967 31 0 0 25 0 1 0 423588789 48226304 10860 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11774 10860 603 41 0 11733 0
vsize: 47096
[startup+230.008 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 11345 0 0 0 22966 33 0 0 25 0 1 0 423588789 50085888 11323 4294967295 134512640 134672761 3221224560 3221223664 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12228 11323 603 41 0 12187 0
vsize: 48912
[startup+240.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 11760 0 0 0 23965 34 0 0 25 0 1 0 423588789 52064256 11738 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12711 11738 603 41 0 12670 0
vsize: 50844
[startup+250.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 12148 0 0 0 24965 35 0 0 25 0 1 0 423588789 53665792 12126 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13102 12126 603 41 0 13061 0
vsize: 52408
[startup+260.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 12459 0 0 0 25964 36 0 0 25 0 1 0 423588789 54947840 12437 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13415 12437 603 41 0 13374 0
vsize: 53660
[startup+270.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 12857 0 0 0 26962 37 0 0 25 0 1 0 423588789 56561664 12835 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13809 12835 603 41 0 13768 0
vsize: 55236
[startup+280.018 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 13196 0 0 0 27962 38 0 0 25 0 1 0 423588789 57892864 13174 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 13174 603 41 0 14093 0
vsize: 56536
[startup+290.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 13676 0 0 0 28962 39 0 0 25 0 1 0 423588789 59904000 13654 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14625 13654 603 41 0 14584 0
vsize: 58500
[startup+300.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 14010 0 0 0 29962 40 0 0 25 0 1 0 423588789 61243392 13988 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14952 13988 603 41 0 14911 0
vsize: 59808
[startup+310.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 14349 0 0 0 30961 41 0 0 25 0 1 0 423588789 62574592 14327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15277 14327 603 41 0 15236 0
vsize: 61108
[startup+320.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 14727 0 0 0 31960 42 0 0 25 0 1 0 423588789 64184320 14705 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15670 14705 603 41 0 15629 0
vsize: 62680
[startup+330.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 15161 0 0 0 32959 43 0 0 25 0 1 0 423588789 65908736 15139 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16091 15139 603 41 0 16050 0
vsize: 64364
[startup+340.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 15605 0 0 0 33958 44 0 0 25 0 1 0 423588789 67768320 15583 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16545 15583 603 41 0 16504 0
vsize: 66180
[startup+350.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 15968 0 0 0 34957 45 0 0 25 0 1 0 423588789 69251072 15946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 15946 603 41 0 16866 0
vsize: 67628
[startup+360.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 35957 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+370.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 36957 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+380.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 37957 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+390.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 38957 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223696 134560645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+400.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 39957 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+410.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 40957 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+420.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 41958 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+430.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 42958 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+440.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 43958 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+450.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 44958 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+460.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 45959 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+470.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 46959 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+480.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 47959 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+490.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 48959 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+500.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 49959 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+510.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 50959 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+520.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 51960 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+530.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 52960 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+540.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 53960 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+550.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 54960 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+560.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16268 0 0 0 55960 46 0 0 25 0 1 0 423588789 70377472 16246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16246 603 41 0 17141 0
vsize: 68728
[startup+570.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16477 0 0 0 56960 47 0 0 25 0 1 0 423588789 71315456 16455 4294967295 134512640 134672761 3221224560 3221223744 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17411 16455 603 41 0 17370 0
vsize: 69644
[startup+580.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16724 0 0 0 57960 47 0 0 25 0 1 0 423588789 72253440 16702 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17640 16702 603 41 0 17599 0
vsize: 70560
[startup+590.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 16968 0 0 0 58959 48 0 0 25 0 1 0 423588789 73314304 16946 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17899 16946 603 41 0 17858 0
vsize: 71596
[startup+600.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 59959 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+610.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 60960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+620.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 61960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+630.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 62960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+640.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 63960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+650.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 64960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+660.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 65960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+670.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 66960 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+680.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 67961 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+690.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 68961 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+700.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 69961 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+710.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 70961 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+720.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 71961 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+730.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 72962 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+740.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 73962 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+750.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 74962 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+760.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 75962 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+770.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 76962 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223736 134559059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+780.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 77962 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+790.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 78963 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+800.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 79963 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+810.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 80963 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+820.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 81963 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+830.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 82963 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+840.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17244 0 0 0 83964 48 0 0 25 0 1 0 423588789 74362880 17222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17222 603 41 0 18114 0
vsize: 72620
[startup+850.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17246 0 0 0 84964 48 0 0 25 0 1 0 423588789 74362880 17224 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17224 603 41 0 18114 0
vsize: 72620
[startup+860.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17249 0 0 0 85964 48 0 0 25 0 1 0 423588789 74362880 17227 4294967295 134512640 134672761 3221224560 3221223664 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18155 17227 603 41 0 18114 0
vsize: 72620
[startup+870.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17386 0 0 0 86964 48 0 0 25 0 1 0 423588789 74903552 17364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18287 17364 603 41 0 18246 0
vsize: 73148
[startup+880.131 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13524
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17551 0 0 0 87973 49 0 0 25 0 1 0 423588789 75571200 17529 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18450 17529 603 41 0 18409 0
vsize: 73800
[startup+890.407 s]
Raw data (loadavg): 1.08 1.02 0.93 2/56 13564
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17740 0 0 0 88970 55 0 0 25 0 1 0 423588789 76361728 17718 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18643 17718 603 41 0 18602 0
vsize: 74572
[startup+900.407 s]
Raw data (loadavg): 1.15 1.03 0.94 2/54 13577
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 17913 0 0 0 89971 55 0 0 25 0 1 0 423588789 77156352 17891 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18837 17891 603 41 0 18796 0
vsize: 75348
[startup+910.52 s]
Raw data (loadavg): 1.12 1.03 0.94 2/54 13577
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 18136 0 0 0 90981 56 0 0 25 0 1 0 423588789 77950976 18114 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19031 18114 603 41 0 18990 0
vsize: 76124
[startup+920.52 s]
Raw data (loadavg): 1.10 1.03 0.94 2/54 13577
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 18366 0 0 0 91980 57 0 0 25 0 1 0 423588789 79007744 18344 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19289 18344 603 41 0 19248 0
vsize: 77156
[startup+930.52 s]
Raw data (loadavg): 1.09 1.03 0.94 2/54 13577
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 18579 0 0 0 92980 57 0 0 25 0 1 0 423588789 79826944 18557 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19489 18557 603 41 0 19448 0
vsize: 77956
[startup+940.521 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 13577
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 18796 0 0 0 93980 58 0 0 25 0 1 0 423588789 80748544 18774 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19714 18774 603 41 0 19673 0
vsize: 78856
[startup+950.521 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 13577
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 19036 0 0 0 94980 58 0 0 25 0 1 0 423588789 81719296 19014 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19951 19014 603 41 0 19910 0
vsize: 79804
[startup+960.521 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 19262 0 0 0 95980 58 0 0 25 0 1 0 423588789 82653184 19240 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20179 19240 603 41 0 20138 0
vsize: 80716
[startup+970.521 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 19468 0 0 0 96979 60 0 0 25 0 1 0 423588789 83439616 19446 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20371 19446 603 41 0 20330 0
vsize: 81484
[startup+980.522 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 19659 0 0 0 97978 60 0 0 25 0 1 0 423588789 84230144 19637 4294967295 134512640 134672761 3221224560 3221223664 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20564 19637 603 41 0 20523 0
vsize: 82256
[startup+990.522 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 19850 0 0 0 98978 61 0 0 25 0 1 0 423588789 85549056 19828 4294967295 134512640 134672761 3221224560 3221223712 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20886 19828 603 41 0 20845 0
vsize: 83544
[startup+1000.52 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 20016 0 0 0 99977 62 0 0 25 0 1 0 423588789 86212608 19994 4294967295 134512640 134672761 3221224560 3221223744 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21048 19994 603 41 0 21007 0
vsize: 84192
[startup+1010.52 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 20155 0 0 0 100977 62 0 0 25 0 1 0 423588789 86736896 20133 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21176 20133 603 41 0 21135 0
vsize: 84704
[startup+1020.52 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 20302 0 0 0 101976 63 0 0 25 0 1 0 423588789 87404544 20280 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21339 20280 603 41 0 21298 0
vsize: 85356
[startup+1030.52 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 20439 0 0 0 102976 63 0 0 25 0 1 0 423588789 87932928 20417 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20417 603 41 0 21427 0
vsize: 85872
[startup+1040.52 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 20665 0 0 0 103976 64 0 0 25 0 1 0 423588789 88866816 20643 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21696 20643 603 41 0 21655 0
vsize: 86784
[startup+1050.52 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 20845 0 0 0 104976 64 0 0 25 0 1 0 423588789 89530368 20823 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21858 20823 603 41 0 21817 0
vsize: 87432
[startup+1060.53 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21027 0 0 0 105975 65 0 0 25 0 1 0 423588789 90341376 21005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22056 21005 603 41 0 22015 0
vsize: 88224
[startup+1070.52 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21184 0 0 0 106975 65 0 0 25 0 1 0 423588789 90996736 21162 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22216 21162 603 41 0 22175 0
vsize: 88864
[startup+1080.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21332 0 0 0 107975 66 0 0 25 0 1 0 423588789 91525120 21310 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22345 21310 603 41 0 22304 0
vsize: 89380
[startup+1090.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21492 0 0 0 108975 66 0 0 25 0 1 0 423588789 92188672 21470 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22507 21470 603 41 0 22466 0
vsize: 90028
[startup+1100.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21671 0 0 0 109974 67 0 0 25 0 1 0 423588789 92856320 21649 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22670 21649 603 41 0 22629 0
vsize: 90680
[startup+1110.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21796 0 0 0 110973 67 0 0 25 0 1 0 423588789 93384704 21774 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22799 21774 603 41 0 22758 0
vsize: 91196
[startup+1120.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 21945 0 0 0 111972 68 0 0 25 0 1 0 423588789 94048256 21923 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22961 21923 603 41 0 22920 0
vsize: 91844
[startup+1130.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 22148 0 0 0 112972 68 0 0 25 0 1 0 423588789 94842880 22126 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23155 22126 603 41 0 23114 0
vsize: 92620
[startup+1140.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 22338 0 0 0 113972 69 0 0 25 0 1 0 423588789 95637504 22316 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23349 22316 603 41 0 23308 0
vsize: 93396
[startup+1150.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 22530 0 0 0 114971 70 0 0 25 0 1 0 423588789 96432128 22508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23543 22508 603 41 0 23502 0
vsize: 94172
[startup+1160.53 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 22707 0 0 0 115971 70 0 0 25 0 1 0 423588789 97095680 22685 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23705 22685 603 41 0 23664 0
vsize: 94820
[startup+1170.53 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 22861 0 0 0 116971 70 0 0 25 0 1 0 423588789 97763328 22839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23868 22839 603 41 0 23827 0
vsize: 95472
[startup+1180.53 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 23021 0 0 0 117971 71 0 0 25 0 1 0 423588789 98422784 22999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24029 22999 603 41 0 23988 0
vsize: 96116
[startup+1190.53 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 23172 0 0 0 118971 71 0 0 25 0 1 0 423588789 98983936 23150 4294967295 134512640 134672761 3221224560 3221223744 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24166 23150 603 41 0 24125 0
vsize: 96664
[startup+1200.53 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 13579
Raw data (stat): 13524 (minisat+) R 13523 5897 5896 0 -1 0 23338 0 0 0 119970 72 0 0 25 0 1 0 423588789 99774464 23316 4294967295 134512640 134672761 3221224560 3221223744 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24359 23316 603 41 0 24318 0
vsize: 97436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.58 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 13579
Raw data (stat): 13524 (minisat+) Z 13523 5897 5896 0 -1 12 23341 0 0 0 119970 76 0 0 25 0 1 0 423588789 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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): 1200.58
CPU time (s): 1200.48
CPU user time (s): 1199.71
CPU system time (s): 0.766883
CPU usage (%): 99.9913
Max. virtual memory (Kb): 97436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####