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-5.opb
MD5SUM	54f6acf3ab92bda8abb11350f74de20e
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	80035
Number of constraints which are clauses	80035
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 5255

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        831496 kB
Buffers:         35840 kB
Cached:         129456 kB
SwapCached:         12 kB
Active:          54736 kB
Inactive:       113432 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        831244 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29352 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:20:27 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 3722 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80035 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 |   80035   160070 |   26678       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]---> Adder-cost: 2272   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   95757   216260 |   31919       0        0     nan |  0.000 % |
c |       100 |   95748   216229 |   35110      98      886     9.0 |  0.120 % |
c |       250 |   95748   216229 |   38621     248     2584    10.4 |  0.117 % |
c |       476 |   95748   216229 |   42484     474     5577    11.8 |  0.117 % |
c |       813 |   95704   216075 |   46732     800     8582    10.7 |  0.265 % |
c |      1321 |   95671   215962 |   51405    1299    14396    11.1 |  0.383 % |
c |      2080 |   95626   215807 |   56546    2046    23585    11.5 |  0.557 % |
c |      3219 |   95521   215446 |   62201    3153    37994    12.1 |  0.880 % |
c |      4927 |   95401   215034 |   68421    4833    64551    13.4 |  1.292 % |
c |      7489 |   94711   212668 |   75263    7192   104948    14.6 |  3.931 % |
c |     11333 |   93403   208178 |   82789   10622   181338    17.1 |  9.447 % |
c |     17100 |   91483   201532 |   91068   15468   342981    22.2 | 18.774 % |
c |     25751 |   90573   198376 |  100175   23112  1041916    45.1 | 23.614 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36024 |   90330   197544 |   30110   32929  2545155    77.3 | 23.614 % |
c |     36124 |   90324   197524 |   33121   15248  1603747   105.2 | 24.802 % |
c |     36274 |   90324   197524 |   36433   15398  1613143   104.8 | 24.802 % |
c |     36499 |   90324   197524 |   40076   15623  1619390   103.7 | 24.802 % |
c |     36837 |   90324   197524 |   44084   15961  1649984   103.4 | 24.802 % |
c |     37345 |   90299   197437 |   48492   16451  1681168   102.2 | 24.949 % |
c |     38104 |   90171   196987 |   53341   17172  1711875    99.7 | 25.742 % |
c |     39243 |   90162   196956 |   58675   18309  1766036    96.5 | 25.772 % |
c |     40951 |   90096   196728 |   64543   19974  1865469    93.4 | 26.094 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43392 |   89988   196352 |   29996   22286  2009643    90.2 | 26.094 % |
c |     43493 |   89988   196352 |   32995   22387  2016945    90.1 | 26.700 % |
c |     43643 |   89988   196352 |   36295   22537  2020149    89.6 | 26.700 % |
c |     43868 |   89979   196321 |   39924   22757  2032316    89.3 | 26.729 % |
c |     44206 |   89928   196140 |   43917   23083  2054536    89.0 | 27.054 % |
c |     44712 |   89928   196140 |   48308   23589  2091982    88.7 | 27.053 % |
c |     45471 |   89869   195937 |   53139   24273  2171793    89.5 | 27.286 % |
c |     46610 |   89869   195937 |   58453   25412  2248162    88.5 | 27.286 % |
c |     48318 |   89850   195870 |   64299   27102  2372117    87.5 | 27.403 % |
c |     50880 |   89832   195810 |   70728   29629  2537384    85.6 | 27.491 % |
c |     54724 |   89764   195576 |   77801   33435  2802390    83.8 | 27.815 % |
c |     60490 |   89749   195521 |   85582   39200  3356968    85.6 | 27.933 % |
c |     69140 |   89670   195252 |   94140   47774  4236435    88.7 | 28.341 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72483 |   89666   195245 |   29888   51094  4457120    87.2 | 28.341 % |
c |     72583 |   89637   195142 |   32876   17594  1147761    65.2 | 28.597 % |
c |     72733 |   89637   195142 |   36164   17744  1156352    65.2 | 28.597 % |
c |     72959 |   89637   195142 |   39780   17970  1169220    65.1 | 28.597 % |
c |     73298 |   89637   195142 |   43759   18309  1183737    64.7 | 28.597 % |
c |     73805 |   89609   195048 |   48134   18794  1216478    64.7 | 28.774 % |
c |     74564 |   89609   195048 |   52948   19553  1255025    64.2 | 28.774 % |
c |     75703 |   89571   194916 |   58243   20676  1361070    65.8 | 28.979 % |
c |     77411 |   89565   194896 |   64067   22363  1527613    68.3 | 29.007 % |
c |     79973 |   89565   194896 |   70474   24925  1842543    73.9 | 29.007 % |
c |     83819 |   89565   194896 |   77521   28771  2349288    81.7 | 29.009 % |
c |     89586 |   89565   194896 |   85273   34538  2975234    86.1 | 29.009 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 41   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91082 |   89566   194903 |   29855   36034  3124415    86.7 | 29.009 % |
c |     91185 |   89551   194852 |   32840   15728  1347419    85.7 | 29.086 % |
c |     91335 |   89545   194832 |   36124   15872  1352145    85.2 | 29.115 % |
c |     91560 |   89536   194801 |   39737   16093  1367631    85.0 | 29.146 % |
c |     91897 |   89536   194801 |   43710   16430  1391858    84.7 | 29.145 % |
c |     92403 |   89510   194711 |   48081   16914  1417210    83.8 | 29.262 % |
c |     93163 |   89493   194652 |   52889   17670  1466421    83.0 | 29.350 % |
c |     94302 |   89493   194652 |   58178   18809  1640884    87.2 | 29.352 % |
c |     96010 |   89493   194652 |   63996   20517  1742838    84.9 | 29.352 % |
c |     98572 |   89493   194652 |   70396   23079  2036210    88.2 | 29.352 % |
c |    102416 |   89493   194652 |   77436   26923  2550849    94.7 | 29.350 % |
c |    108182 |   89485   194624 |   85179   32685  3475789   106.3 | 29.410 % |
c |    116832 |   89470   194573 |   93697   41311  4140191   100.2 | 29.469 % |
c |    129806 |   89470   194573 |  103067   54285  5674618   104.5 | 29.467 % |
c |    149268 |   89470   194573 |  113374   73747  9395930   127.4 | 29.467 % |
c |    178460 |   89470   194573 |  124711  102939 13661947   132.7 | 29.469 % |
c |    222250 |   89383   194274 |  137182   39883  5262662   132.0 | 29.965 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 42   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    261105 |   89300   193986 |   29766   78711  9953841   126.5 | 29.965 % |
c |    261205 |   89300   193986 |   32742   16244  2224197   136.9 | 30.512 % |
c |    261355 |   89300   193986 |   36016   16394  2227188   135.9 | 30.514 % |
c |    261580 |   89288   193946 |   39618   16611  2232954   134.4 | 30.573 % |
c |    261917 |   89288   193946 |   43580   16948  2242054   132.3 | 30.571 % |
c |    262424 |   89288   193946 |   47938   17455  2260887   129.5 | 30.571 % |
c |    263184 |   89280   193918 |   52732   18212  2288276   125.6 | 30.631 % |
c |    264323 |   89280   193918 |   58005   19351  2344262   121.1 | 30.631 % |
c |    266033 |   89280   193918 |   63806   21061  2446736   116.2 | 30.631 % |
c |    268596 |   89245   193797 |   70186   23613  2571155   108.9 | 30.835 % |
c |    272442 |   89228   193738 |   77205   27431  2847584   103.8 | 30.925 % |
c |    278208 |   89222   193718 |   84925   33188  3464781   104.4 | 30.953 % |
c |    286859 |   89213   193687 |   93418   41819  4013853    96.0 | 30.982 % |
c |    299835 |   89213   193687 |  102760   54795  5649003   103.1 | 30.981 % |
c |    319296 |   89213   193687 |  113036   74256  7442481   100.2 | 30.981 % |
c |    348488 |   89202   193648 |  124339  103436 11762379   113.7 | 31.040 % |
c |    392282 |   89202   193648 |  136773   38793  7376133   190.1 | 31.040 % |
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.92 0.97 0.91 2/54 31624
Raw data (stat): 31624 (runsolver) R 31623 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479741359 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 31624
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 3879 0 0 0 987 11 0 0 25 0 1 0 479741359 17715200 3857 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4325 3857 603 41 0 4284 0
vsize: 17300
[startup+20 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 31624
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 3879 0 0 0 1985 12 0 0 25 0 1 0 479741359 17715200 3857 4294967295 134512640 134672761 3221224560 3221223724 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3857 603 41 0 4284 0
vsize: 17300
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 31624
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 3879 0 0 0 2985 12 0 0 25 0 1 0 479741359 17715200 3857 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4325 3857 603 41 0 4284 0
vsize: 17300
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31624
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 3879 0 0 0 3983 12 0 0 25 0 1 0 479741359 17715200 3857 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3857 603 41 0 4284 0
vsize: 17300
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 4510 0 0 0 4982 14 0 0 25 0 1 0 479741359 20398080 4488 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4488 603 41 0 4939 0
vsize: 19920
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 4510 0 0 0 5981 15 0 0 25 0 1 0 479741359 20398080 4488 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4980 4488 603 41 0 4939 0
vsize: 19920
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 4684 0 0 0 6980 16 0 0 25 0 1 0 479741359 21204992 4662 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5177 4662 603 41 0 5136 0
vsize: 20708
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 5326 0 0 0 7977 19 0 0 25 0 1 0 479741359 23756800 5304 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5800 5304 603 41 0 5759 0
vsize: 23200
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 5902 0 0 0 8975 20 0 0 25 0 1 0 479741359 26034176 5880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6356 5880 603 41 0 6315 0
vsize: 25424
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6524 0 0 0 9973 23 0 0 25 0 1 0 479741359 28585984 6502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6979 6502 603 41 0 6938 0
vsize: 27916
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6645 0 0 0 10973 23 0 0 25 0 1 0 479741359 29093888 6623 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7103 6623 603 41 0 7062 0
vsize: 28412
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6645 0 0 0 11973 23 0 0 25 0 1 0 479741359 29093888 6623 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7103 6623 603 41 0 7062 0
vsize: 28412
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6645 0 0 0 12974 23 0 0 25 0 1 0 479741359 29089792 6623 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7102 6623 603 41 0 7061 0
vsize: 28408
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6645 0 0 0 13974 23 0 0 25 0 1 0 479741359 29089792 6623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7102 6623 603 41 0 7061 0
vsize: 28408
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6645 0 0 0 14974 23 0 0 25 0 1 0 479741359 29089792 6623 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7102 6623 603 41 0 7061 0
vsize: 28408
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6645 0 0 0 15974 23 0 0 25 0 1 0 479741359 29089792 6623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7102 6623 603 41 0 7061 0
vsize: 28408
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 6797 0 0 0 16974 23 0 0 25 0 1 0 479741359 29757440 6775 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7265 6775 603 41 0 7224 0
vsize: 29060
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 7284 0 0 0 17973 25 0 0 25 0 1 0 479741359 31780864 7262 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7759 7262 603 41 0 7718 0
vsize: 31036
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 7841 0 0 0 18971 26 0 0 25 0 1 0 479741359 33939456 7819 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7819 603 41 0 8245 0
vsize: 33144
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 8452 0 0 0 19970 28 0 0 25 0 1 0 479741359 36466688 8430 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8903 8430 603 41 0 8862 0
vsize: 35612
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 9206 0 0 0 20968 30 0 0 25 0 1 0 479741359 39534592 9184 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9652 9184 603 41 0 9611 0
vsize: 38608
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 9861 0 0 0 21966 32 0 0 25 0 1 0 479741359 42205184 9839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10304 9839 603 41 0 10263 0
vsize: 41216
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 10458 0 0 0 22965 33 0 0 25 0 1 0 479741359 44998656 10436 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10986 10436 603 41 0 10945 0
vsize: 43944
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 11023 0 0 0 23964 34 0 0 25 0 1 0 479741359 47276032 11001 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11542 11001 603 41 0 11501 0
vsize: 46168
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 11635 0 0 0 24962 37 0 0 25 0 1 0 479741359 49676288 11613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12128 11613 603 41 0 12087 0
vsize: 48512
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 12060 0 0 0 25961 38 0 0 25 0 1 0 479741359 51417088 12038 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12553 12038 603 41 0 12512 0
vsize: 50212
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 12517 0 0 0 26960 39 0 0 25 0 1 0 479741359 53284864 12495 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13009 12495 603 41 0 12968 0
vsize: 52036
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 13006 0 0 0 27960 39 0 0 25 0 1 0 479741359 55291904 12984 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13499 12984 603 41 0 13458 0
vsize: 53996
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 13298 0 0 0 28958 41 0 0 25 0 1 0 479741359 56504320 13276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13795 13276 603 41 0 13754 0
vsize: 55180
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 13733 0 0 0 29957 43 0 0 25 0 1 0 479741359 58253312 13711 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14222 13711 603 41 0 14181 0
vsize: 56888
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 14159 0 0 0 30956 44 0 0 25 0 1 0 479741359 59998208 14137 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14648 14137 603 41 0 14607 0
vsize: 58592
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 14625 0 0 0 31954 46 0 0 25 0 1 0 479741359 61870080 14603 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15105 14603 603 41 0 15064 0
vsize: 60420
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31626
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 15089 0 0 0 32953 47 0 0 25 0 1 0 479741359 63746048 15067 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15563 15067 603 41 0 15522 0
vsize: 62252
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 15428 0 0 0 33952 48 0 0 25 0 1 0 479741359 65216512 15406 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15922 15406 603 41 0 15881 0
vsize: 63688
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 15778 0 0 0 34951 49 0 0 25 0 1 0 479741359 66551808 15756 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16248 15756 603 41 0 16207 0
vsize: 64992
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 16153 0 0 0 35950 50 0 0 25 0 1 0 479741359 68141056 16131 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16636 16131 603 41 0 16595 0
vsize: 66544
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 16493 0 0 0 36949 52 0 0 25 0 1 0 479741359 69480448 16471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16963 16471 603 41 0 16922 0
vsize: 67852
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 16880 0 0 0 37947 53 0 0 25 0 1 0 479741359 71081984 16858 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17354 16858 603 41 0 17313 0
vsize: 69416
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 17320 0 0 0 38946 55 0 0 25 0 1 0 479741359 72953856 17298 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17811 17298 603 41 0 17770 0
vsize: 71244
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 17741 0 0 0 39946 55 0 0 25 0 1 0 479741359 74571776 17719 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18206 17719 603 41 0 18165 0
vsize: 72824
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 18168 0 0 0 40945 57 0 0 25 0 1 0 479741359 76308480 18146 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18630 18146 603 41 0 18589 0
vsize: 74520
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 18637 0 0 0 41943 58 0 0 25 0 1 0 479741359 78327808 18615 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19123 18615 603 41 0 19082 0
vsize: 76492
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 19070 0 0 0 42943 59 0 0 25 0 1 0 479741359 80052224 19048 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19544 19048 603 41 0 19503 0
vsize: 78176
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 19505 0 0 0 43942 60 0 0 25 0 1 0 479741359 81784832 19483 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19967 19483 603 41 0 19926 0
vsize: 79868
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 19934 0 0 0 44941 61 0 0 25 0 1 0 479741359 83673088 19912 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20428 19912 603 41 0 20387 0
vsize: 81712
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20080 0 0 0 45940 62 0 0 25 0 1 0 479741359 84209664 20058 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20559 20058 603 41 0 20518 0
vsize: 82236
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20276 0 0 0 46940 62 0 0 25 0 1 0 479741359 85012480 20254 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20755 20254 603 41 0 20714 0
vsize: 83020
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20549 0 0 0 47939 63 0 0 25 0 1 0 479741359 86093824 20527 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21019 20527 603 41 0 20978 0
vsize: 84076
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20792 0 0 0 48939 64 0 0 25 0 1 0 479741359 87171072 20770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21282 20770 603 41 0 21241 0
vsize: 85128
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 49939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 50939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 51939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 52939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 53939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 54938 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 55938 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 56939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 57939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 58939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 59939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 60939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 61939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 62939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 63939 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 64940 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 65940 64 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 66940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 67939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 68939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 69939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 70939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 71939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 72939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 73939 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 74940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 75940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 76940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 77940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 78940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 79940 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 80941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 81941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 82941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 83941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 84941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 85941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 86941 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 87942 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 88942 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 89942 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 90942 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 91942 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 92943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 93943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 94943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 95943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 96943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 97944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+990.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 98944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223744 134558859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 99944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 100944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134564752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 101943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 102943 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 103944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 104944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 105944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 106944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 107944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 108944 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 109945 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 110945 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 111945 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 112945 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 113945 65 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20854 0 0 0 114944 66 0 0 25 0 1 0 479741359 87306240 20832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20832 603 41 0 21274 0
vsize: 85260
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20855 0 0 0 115945 66 0 0 25 0 1 0 479741359 87306240 20833 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20833 603 41 0 21274 0
vsize: 85260
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20855 0 0 0 116945 66 0 0 25 0 1 0 479741359 87306240 20833 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20833 603 41 0 21274 0
vsize: 85260
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20856 0 0 0 117945 66 0 0 25 0 1 0 479741359 87306240 20834 4294967295 134512640 134672761 3221224560 3221223744 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20834 603 41 0 21274 0
vsize: 85260
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20860 0 0 0 118945 66 0 0 25 0 1 0 479741359 87306240 20838 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20838 603 41 0 21274 0
vsize: 85260
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31628
Raw data (stat): 31624 (minisat+) R 31623 27222 27221 0 -1 0 20861 0 0 0 119945 66 0 0 25 0 1 0 479741359 87306240 20839 4294967295 134512640 134672761 3221224560 3221223664 134555098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21315 20839 603 41 0 21274 0
vsize: 85260
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31628
Raw data (stat): 31624 (minisat+) Z 31623 27222 27221 0 -1 12 20864 0 0 0 119946 69 0 0 25 0 1 0 479741359 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.06
CPU time (s): 1200.16
CPU user time (s): 1199.46
CPU system time (s): 0.698893
CPU usage (%): 100.009
Max. virtual memory (Kb): 85260
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####