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 5043

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 21:35:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3002 boxname=wulflinc4 idbench=334 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ed1ca962177baf0f135b785abad8adea  /oldhome/oroussel/tmp/wulflinc4/normalized-frb50-23-1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc4/normalized-frb50-23-1.opb
IDLAUNCH: 3002
/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:        920708 kB
Buffers:         34628 kB
Cached:          59348 kB
SwapCached:          0 kB
Active:          53504 kB
Inactive:        43336 kB
HighTotal:      131008 kB
HighFree:        67844 kB
LowTotal:       903652 kB
LowFree:        852864 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11456 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:55:12 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3002 7 1200.21 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 |  147988   319466 |   49329       0        0     nan |  0.000 % |
c |       100 |  147362   318162 |   54261      77      551     7.2 |  0.736 % |
c |       250 |  146841   317054 |   59688     209     2448    11.7 |  1.369 % |
c |       475 |  145811   314812 |   65656     398     4382    11.0 |  2.680 % |
c |       812 |  144010   310871 |   72222     677     8303    12.3 |  4.995 % |
c |      1318 |  141157   304558 |   79444    1060    12573    11.9 |  8.737 % |
c |      2077 |  136776   294746 |   87389    1627    19630    12.1 | 14.610 % |
c |      3216 |  131215   282210 |   96128    2497    29631    11.9 | 22.142 % |
c |      4924 |  123727   265107 |  105741    3779    49504    13.1 | 32.476 % |
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 |      6427 |  116683   248991 |   38894    4766    61496    12.9 | 32.476 % |
c |      6527 |  116204   247870 |   42783    4831    62291    12.9 | 43.100 % |
c |      6677 |  115663   246594 |   47061    4934    63665    12.9 | 43.849 % |
c |      6902 |  114831   244655 |   51767    5110    65775    12.9 | 44.973 % |
c |      7239 |  113564   241690 |   56944    5351    69474    13.0 | 46.827 % |
c |      7746 |  111539   236942 |   62639    5688    74185    13.0 | 49.645 % |
c |      8505 |  108258   229196 |   68903    6014    79861    13.3 | 54.380 % |
c |      9645 |  106402   224792 |   75793    6813    92319    13.6 | 57.095 % |
c |     11355 |  103049   216804 |   83372    7947   113001    14.2 | 62.021 % |
c |     13917 |   98383   205681 |   91710    9480   147925    15.6 | 68.784 % |
c |     17761 |   94811   197102 |  100881   12081   211420    17.5 | 74.113 % |
c |     23527 |   91940   190193 |  110969   16325   396509    24.3 | 78.405 % |
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 |     26517 |   91505   189103 |   30501   18993   511336    26.9 | 78.405 % |
c |     26617 |   91453   188977 |   33551   19046   513223    26.9 | 79.155 % |
c |     26767 |   91403   188856 |   36906   19147   514654    26.9 | 79.230 % |
c |     26993 |   91347   188722 |   40596   19332   517806    26.8 | 79.308 % |
c |     27330 |   91347   188722 |   44656   19669   531077    27.0 | 79.308 % |
c |     27836 |   91347   188722 |   49122   20175   549790    27.3 | 79.308 % |
c |     28595 |   91336   188697 |   54034   20920   586573    28.0 | 79.323 % |
c |     29734 |   91040   187971 |   59437   21902   671987    30.7 | 79.772 % |
c |     31442 |   91021   187926 |   65381   23576   759400    32.2 | 79.800 % |
c |     34004 |   90924   187692 |   71919   26012   920916    35.4 | 79.947 % |
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 |     37368 |   90426   186513 |   30142   28875  1073664    37.2 | 79.947 % |
c |     37468 |   90272   186133 |   33156   28788  1071210    37.2 | 80.912 % |
c |     37618 |   90272   186133 |   36471   28938  1078094    37.3 | 80.912 % |
c |     37845 |   90055   185604 |   40119   28990  1084507    37.4 | 81.229 % |
c |     38182 |   89765   184919 |   44130   29091  1093267    37.6 | 81.654 % |
c |     38690 |   89677   184699 |   48543   29419  1114490    37.9 | 81.794 % |
c |     39449 |   89637   184597 |   53398   30143  1175417    39.0 | 81.859 % |
c |     40590 |   89554   184394 |   58738   31209  1251534    40.1 | 81.988 % |
c |     42298 |   89419   184073 |   64612   32883  1358367    41.3 | 82.189 % |
c |     44861 |   89408   184048 |   71073   35430  1659938    46.9 | 82.204 % |
c |     48706 |   89194   183528 |   78180   38940  1937517    49.8 | 82.527 % |
c |     54473 |   89111   183331 |   85998   44007  2548488    57.9 | 82.650 % |
c |     63122 |   88944   182914 |   94598   52476  3364323    64.1 | 82.920 % |
c |     76097 |   88814   182580 |  104058   65300  4943713    75.7 | 83.140 % |
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 |     77862 |   88826   182643 |   29608   67005  5167051    77.1 | 83.140 % |
c |     77964 |   88784   182545 |   32568   67090  5171321    77.1 | 83.214 % |
c |     78114 |   88784   182545 |   35825   67240  5180522    77.0 | 83.214 % |
c |     78339 |   88743   182450 |   39408   67391  5196716    77.1 | 83.270 % |
c |     78678 |   88708   182365 |   43349   67686  5220332    77.1 | 83.324 % |
c |     79184 |   88704   182355 |   47683   68174  5263297    77.2 | 83.330 % |
c |     79943 |   88664   182255 |   52452   68714  5301058    77.1 | 83.395 % |
c |     81082 |   88585   182068 |   57697   69580  5394262    77.5 | 83.511 % |
c |     82790 |   88519   181910 |   63467   71223  5554743    78.0 | 83.610 % |
c |     85352 |   88517   181906 |   69814   73749  5848295    79.3 | 83.612 % |
c |     89198 |   88366   181535 |   76795   77183  6388766    82.8 | 83.847 % |
c |     94964 |   88258   181285 |   84475   82844  7485378    90.4 | 83.993 % |
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 |     98263 |   88158   181016 |   29386   85817  7763842    90.5 | 83.993 % |
c |     98364 |   88158   181016 |   32324   22455  2013545    89.7 | 84.158 % |
c |     98514 |   88158   181016 |   35557   22605  2027056    89.7 | 84.158 % |
c |     98740 |   88158   181016 |   39112   22831  2038443    89.3 | 84.158 % |
c |     99077 |   88158   181016 |   43024   23168  2078602    89.7 | 84.158 % |
c |     99583 |   88158   181016 |   47326   23674  2126008    89.8 | 84.158 % |
c |    100342 |   88158   181016 |   52059   24433  2186274    89.5 | 84.158 % |
c |    101484 |   88150   180996 |   57265   25550  2295749    89.9 | 84.170 % |
c |    103195 |   88096   180868 |   62991   27218  2436552    89.5 | 84.250 % |
c |    105757 |   88096   180868 |   69290   29780  2702781    90.8 | 84.250 % |
c |    109601 |   88046   180746 |   76219   33602  3048134    90.7 | 84.328 % |
c |    115367 |   88046   180746 |   83841   39368  3668323    93.2 | 84.328 % |
c |    124016 |   88046   180746 |   92225   48017  4913028   102.3 | 84.328 % |
c |    136990 |   87949   180511 |  101448   60968  6988775   114.6 | 84.476 % |
c |    156451 |   87902   180392 |  111593   80363  9395711   116.9 | 84.553 % |
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 |    166657 |   87834   180240 |   29278   90507 10717436   118.4 | 84.553 % |
c |    166757 |   87834   180240 |   32205   23788  1691897    71.1 | 84.668 % |
c |    166907 |   87789   180133 |   35426   23933  1702187    71.1 | 84.735 % |
c |    167132 |   87789   180133 |   38969   24158  1720163    71.2 | 84.735 % |
c |    167470 |   87789   180133 |   42865   24496  1758488    71.8 | 84.735 % |
c |    167976 |   87628   179729 |   47152   24984  1795588    71.9 | 84.980 % |
c |    168736 |   87561   179560 |   51867   25707  1847965    71.9 | 85.083 % |
c |    169875 |   87561   179560 |   57054   26846  1997820    74.4 | 85.083 % |
c |    171583 |   87555   179546 |   62759   28551  2143274    75.1 | 85.092 % |
c |    174145 |   87543   179518 |   69035   31109  2357991    75.8 | 85.109 % |
c |    177989 |   87543   179518 |   75939   34953  2874390    82.2 | 85.109 % |
c |    183757 |   87535   179500 |   83533   40698  3596006    88.4 | 85.120 % |
c |    192406 |   87535   179500 |   91886   49347  4807829    97.4 | 85.120 % |
c |    205380 |   87464   179337 |  101075   62280  6436341   103.3 | 85.217 % |
c |    224841 |   87464   179337 |  111183   81741  9073077   111.0 | 85.217 % |
c |    254033 |   87464   179337 |  122301  110933 13542456   122.1 | 85.217 % |
c |    297822 |   87384   179141 |  134531  154625 20442372   132.2 | 85.339 % |
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 #### 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.91 0.95 0.92 2/54 9232
Raw data (stat): 9232 (runsolver) R 9231 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421007368 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.99961 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 4933 0 0 0 982 16 0 0 25 0 1 0 421007368 23248896 4911 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5676 4911 603 41 0 5635 0
vsize: 22704
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 4942 0 0 0 1981 16 0 0 25 0 1 0 421007368 23248896 4920 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5676 4920 603 41 0 5635 0
vsize: 22704
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 4951 0 0 0 2980 16 0 0 25 0 1 0 421007368 23384064 4929 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5709 4929 603 41 0 5668 0
vsize: 22836
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 4961 0 0 0 3979 17 0 0 25 0 1 0 421007368 23384064 4939 4294967295 134512640 134672761 3221224640 3221223812 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5709 4939 603 41 0 5668 0
vsize: 22836
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 4975 0 0 0 4980 17 0 0 25 0 1 0 421007368 23523328 4953 4294967295 134512640 134672761 3221224640 3221223856 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 4953 603 41 0 5702 0
vsize: 22972
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 5253 0 0 0 5979 17 0 0 25 0 1 0 421007368 25395200 5231 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5231 603 41 0 6159 0
vsize: 24800
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 5255 0 0 0 6980 17 0 0 25 0 1 0 421007368 25395200 5233 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5233 603 41 0 6159 0
vsize: 24800
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 5255 0 0 0 7980 17 0 0 25 0 1 0 421007368 25395200 5233 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5233 603 41 0 6159 0
vsize: 24800
[startup+90.0042 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 5255 0 0 0 8980 17 0 0 25 0 1 0 421007368 25395200 5233 4294967295 134512640 134672761 3221224640 3221223856 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5233 603 41 0 6159 0
vsize: 24800
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 5364 0 0 0 9980 17 0 0 25 0 1 0 421007368 25931776 5342 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6331 5342 603 41 0 6290 0
vsize: 25324
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 5640 0 0 0 10979 18 0 0 25 0 1 0 421007368 27033600 5618 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6600 5618 603 41 0 6559 0
vsize: 26400
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 6090 0 0 0 11978 20 0 0 25 0 1 0 421007368 28921856 6068 4294967295 134512640 134672761 3221224640 3221223808 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7061 6068 603 41 0 7020 0
vsize: 28244
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 6324 0 0 0 12977 21 0 0 25 0 1 0 421007368 29892608 6302 4294967295 134512640 134672761 3221224640 3221223792 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7298 6302 603 41 0 7257 0
vsize: 29192
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 6867 0 0 0 13975 23 0 0 25 0 1 0 421007368 32186368 6845 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7858 6845 603 41 0 7817 0
vsize: 31432
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 7261 0 0 0 14974 24 0 0 25 0 1 0 421007368 33808384 7239 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8254 7239 603 41 0 8213 0
vsize: 33016
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 7817 0 0 0 15973 25 0 0 25 0 1 0 421007368 36093952 7795 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8812 7795 603 41 0 8771 0
vsize: 35248
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 8240 0 0 0 16971 27 0 0 25 0 1 0 421007368 37711872 8218 4294967295 134512640 134672761 3221224640 3221223776 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9207 8218 603 41 0 9166 0
vsize: 36828
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 8712 0 0 0 17970 28 0 0 25 0 1 0 421007368 39723008 8690 4294967295 134512640 134672761 3221224640 3221223824 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9698 8690 603 41 0 9657 0
vsize: 38792
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 9149 0 0 0 18970 29 0 0 25 0 1 0 421007368 41467904 9127 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10124 9127 603 41 0 10083 0
vsize: 40496
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 9586 0 0 0 19969 30 0 0 25 0 1 0 421007368 43208704 9564 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10549 9564 603 41 0 10508 0
vsize: 42196
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 10107 0 0 0 20968 31 0 0 25 0 1 0 421007368 45342720 10085 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11070 10085 603 41 0 11029 0
vsize: 44280
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 10497 0 0 0 21966 33 0 0 25 0 1 0 421007368 47214592 10475 4294967295 134512640 134672761 3221224640 3221223744 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11527 10475 603 41 0 11486 0
vsize: 46108
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 10812 0 0 0 22966 33 0 0 25 0 1 0 421007368 48402432 10790 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11817 10790 603 41 0 11776 0
vsize: 47268
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 11031 0 0 0 23965 34 0 0 25 0 1 0 421007368 49344512 11009 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12047 11009 603 41 0 12006 0
vsize: 48188
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 11399 0 0 0 24964 35 0 0 25 0 1 0 421007368 50810880 11377 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12405 11377 603 41 0 12364 0
vsize: 49620
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 11683 0 0 0 25963 36 0 0 25 0 1 0 421007368 52015104 11661 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 11661 603 41 0 12658 0
vsize: 50796
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 12128 0 0 0 26963 37 0 0 25 0 1 0 421007368 53751808 12106 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13123 12106 603 41 0 13082 0
vsize: 52492
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 12618 0 0 0 27961 39 0 0 25 0 1 0 421007368 55754752 12596 4294967295 134512640 134672761 3221224640 3221223744 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13612 12596 603 41 0 13571 0
vsize: 54448
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13153 0 0 0 28960 40 0 0 25 0 1 0 421007368 58023936 13131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14166 13131 603 41 0 14125 0
vsize: 56664
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13451 0 0 0 29959 41 0 0 25 0 1 0 421007368 59232256 13429 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14461 13429 603 41 0 14420 0
vsize: 57844
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 30959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 31958 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 32958 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 33959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 34959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223744 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 35959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 36959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 37959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 38959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 39959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 40959 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13568 0 0 0 41960 42 0 0 25 0 1 0 421007368 59637760 13546 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14560 13546 603 41 0 14519 0
vsize: 58240
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 13746 0 0 0 42959 42 0 0 25 0 1 0 421007368 60424192 13724 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14752 13724 603 41 0 14711 0
vsize: 59008
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 14147 0 0 0 43958 44 0 0 25 0 1 0 421007368 62033920 14125 4294967295 134512640 134672761 3221224640 3221223776 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15145 14125 603 41 0 15104 0
vsize: 60580
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 14477 0 0 0 44957 45 0 0 25 0 1 0 421007368 63369216 14455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15471 14455 603 41 0 15430 0
vsize: 61884
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 14784 0 0 0 45956 46 0 0 25 0 1 0 421007368 64700416 14762 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15796 14762 603 41 0 15755 0
vsize: 63184
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 15060 0 0 0 46956 47 0 0 25 0 1 0 421007368 65769472 15038 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16057 15038 603 41 0 16016 0
vsize: 64228
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 15359 0 0 0 47955 48 0 0 25 0 1 0 421007368 66965504 15337 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16349 15337 603 41 0 16308 0
vsize: 65396
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 15649 0 0 0 48954 49 0 0 25 0 1 0 421007368 68173824 15627 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16644 15627 603 41 0 16603 0
vsize: 66576
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 15973 0 0 0 49954 50 0 0 25 0 1 0 421007368 69509120 15951 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16970 15951 603 41 0 16929 0
vsize: 67880
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16267 0 0 0 50953 50 0 0 25 0 1 0 421007368 70709248 16245 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17263 16245 603 41 0 17222 0
vsize: 69052
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16633 0 0 0 51952 51 0 0 25 0 1 0 421007368 72179712 16611 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17622 16611 603 41 0 17581 0
vsize: 70488
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 52952 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223824 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 53952 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223816 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 54953 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 55953 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 56953 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 57953 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 58953 51 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 59953 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 60954 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 61954 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 62954 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 63954 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 64954 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 65954 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 66955 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 67955 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 68955 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 69955 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 70955 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 71955 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 72956 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 73956 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16751 0 0 0 74956 52 0 0 25 0 1 0 421007368 72654848 16729 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17738 16729 603 41 0 17697 0
vsize: 70952
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 16919 0 0 0 75955 52 0 0 25 0 1 0 421007368 73318400 16897 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17900 16897 603 41 0 17859 0
vsize: 71600
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 17272 0 0 0 76955 53 0 0 25 0 1 0 421007368 74780672 17250 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18257 17250 603 41 0 18216 0
vsize: 73028
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 17604 0 0 0 77954 54 0 0 25 0 1 0 421007368 76115968 17582 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18583 17582 603 41 0 18542 0
vsize: 74332
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 17907 0 0 0 78953 55 0 0 25 0 1 0 421007368 77443072 17885 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18907 17885 603 41 0 18866 0
vsize: 75628
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 18212 0 0 0 79953 56 0 0 25 0 1 0 421007368 78651392 18190 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19202 18190 603 41 0 19161 0
vsize: 76808
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 18476 0 0 0 80952 57 0 0 25 0 1 0 421007368 79716352 18454 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19462 18454 603 41 0 19421 0
vsize: 77848
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 18749 0 0 0 81952 57 0 0 25 0 1 0 421007368 80777216 18727 4294967295 134512640 134672761 3221224640 3221223808 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 18727 603 41 0 19680 0
vsize: 78884
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 19027 0 0 0 82951 58 0 0 25 0 1 0 421007368 81977344 19005 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20014 19005 603 41 0 19973 0
vsize: 80056
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 19316 0 0 0 83951 59 0 0 25 0 1 0 421007368 83169280 19294 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20305 19294 603 41 0 20264 0
vsize: 81220
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 19565 0 0 0 84950 59 0 0 25 0 1 0 421007368 84226048 19543 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20563 19543 603 41 0 20522 0
vsize: 82252
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 19827 0 0 0 85949 60 0 0 25 0 1 0 421007368 85295104 19805 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20824 19805 603 41 0 20783 0
vsize: 83296
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 20075 0 0 0 86948 61 0 0 25 0 1 0 421007368 86237184 20053 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21054 20053 603 41 0 21013 0
vsize: 84216
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 20407 0 0 0 87947 62 0 0 25 0 1 0 421007368 87576576 20385 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21381 20385 603 41 0 21340 0
vsize: 85524
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 20701 0 0 0 88947 63 0 0 25 0 1 0 421007368 88784896 20679 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21676 20679 603 41 0 21635 0
vsize: 86704
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 21019 0 0 0 89946 64 0 0 25 0 1 0 421007368 90124288 20997 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22003 20997 603 41 0 21962 0
vsize: 88012
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 21348 0 0 0 90946 64 0 0 25 0 1 0 421007368 91451392 21326 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22327 21326 603 41 0 22286 0
vsize: 89308
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 21656 0 0 0 91945 65 0 0 25 0 1 0 421007368 92647424 21634 4294967295 134512640 134672761 3221224640 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22619 21634 603 41 0 22578 0
vsize: 90476
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 21958 0 0 0 92945 65 0 0 25 0 1 0 421007368 93970432 21936 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22942 21936 603 41 0 22901 0
vsize: 91768
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 22231 0 0 0 93945 66 0 0 25 0 1 0 421007368 95027200 22209 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23200 22209 603 41 0 23159 0
vsize: 92800
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 22493 0 0 0 94944 67 0 0 25 0 1 0 421007368 96092160 22471 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23460 22471 603 41 0 23419 0
vsize: 93840
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 22757 0 0 0 95944 67 0 0 25 0 1 0 421007368 97153024 22735 4294967295 134512640 134672761 3221224640 3221223808 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23719 22735 603 41 0 23678 0
vsize: 94876
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 23036 0 0 0 96943 69 0 0 25 0 1 0 421007368 98349056 23014 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24011 23014 603 41 0 23970 0
vsize: 96044
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 23326 0 0 0 97942 69 0 0 25 0 1 0 421007368 99540992 23304 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24302 23304 603 41 0 24261 0
vsize: 97208
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 23558 0 0 0 98942 70 0 0 25 0 1 0 421007368 101007360 23536 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24660 23536 603 41 0 24619 0
vsize: 98640
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 23778 0 0 0 99941 71 0 0 25 0 1 0 421007368 101937152 23756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24887 23756 603 41 0 24846 0
vsize: 99548
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 24023 0 0 0 100940 72 0 0 25 0 1 0 421007368 102858752 24001 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25112 24001 603 41 0 25071 0
vsize: 100448
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 24250 0 0 0 101940 72 0 0 25 0 1 0 421007368 103804928 24228 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25343 24228 603 41 0 25302 0
vsize: 101372
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 24472 0 0 0 102940 73 0 0 25 0 1 0 421007368 104742912 24450 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25572 24450 603 41 0 25531 0
vsize: 102288
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 24707 0 0 0 103939 73 0 0 25 0 1 0 421007368 105664512 24685 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25797 24685 603 41 0 25756 0
vsize: 103188
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 24922 0 0 0 104939 74 0 0 25 0 1 0 421007368 106586112 24900 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26022 24900 603 41 0 25981 0
vsize: 104088
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 25167 0 0 0 105938 75 0 0 25 0 1 0 421007368 107515904 25145 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26249 25145 603 41 0 26208 0
vsize: 104996
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 25383 0 0 0 106938 75 0 0 25 0 1 0 421007368 108449792 25361 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26477 25361 603 41 0 26436 0
vsize: 105908
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 25654 0 0 0 107937 76 0 0 25 0 1 0 421007368 109514752 25632 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26737 25632 603 41 0 26696 0
vsize: 106948
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 25921 0 0 0 108937 77 0 0 25 0 1 0 421007368 110718976 25899 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27031 25899 603 41 0 26990 0
vsize: 108124
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 26178 0 0 0 109936 78 0 0 25 0 1 0 421007368 111648768 26156 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27258 26156 603 41 0 27217 0
vsize: 109032
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 26453 0 0 0 110935 79 0 0 25 0 1 0 421007368 112844800 26431 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27550 26432 603 41 0 27509 0
vsize: 110200
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 26654 0 0 0 111935 79 0 0 25 0 1 0 421007368 113639424 26632 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27744 26632 603 41 0 27703 0
vsize: 110976
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 26860 0 0 0 112935 80 0 0 25 0 1 0 421007368 114442240 26838 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27940 26838 603 41 0 27899 0
vsize: 111760
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 27069 0 0 0 113935 80 0 0 25 0 1 0 421007368 115376128 27047 4294967295 134512640 134672761 3221224640 3221223808 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28168 27047 603 41 0 28127 0
vsize: 112672
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 27289 0 0 0 114933 81 0 0 25 0 1 0 421007368 116174848 27267 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28363 27267 603 41 0 28322 0
vsize: 113452
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 27516 0 0 0 115933 81 0 0 25 0 1 0 421007368 117104640 27494 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28590 27494 603 41 0 28549 0
vsize: 114360
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 27721 0 0 0 116932 82 0 0 25 0 1 0 421007368 118042624 27699 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28819 27699 603 41 0 28778 0
vsize: 115276
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 27926 0 0 0 117932 83 0 0 25 0 1 0 421007368 118837248 27904 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29013 27904 603 41 0 28972 0
vsize: 116052
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 28120 0 0 0 118931 83 0 0 25 0 1 0 421007368 119635968 28098 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29208 28098 603 41 0 29167 0
vsize: 116832
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 9232
Raw data (stat): 9232 (minisat+) R 9231 5897 5896 0 -1 0 28316 0 0 0 119931 84 0 0 25 0 1 0 421007368 120434688 28294 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29403 28294 603 41 0 29362 0
vsize: 117612
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 9232
Raw data (stat): 9232 (minisat+) Z 9231 5897 5896 0 -1 12 28319 0 0 0 119931 89 0 0 25 0 1 0 421007368 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.09
CPU time (s): 1200.21
CPU user time (s): 1199.32
CPU system time (s): 0.897863
CPU usage (%): 100.01
Max. virtual memory (Kb): 117612
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####