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-4.opb
MD5SUM	b85a90571dde4fe12541342d5605d680
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.1
Number of variables	1150
Total number of constraints	80258
Number of constraints which are clauses	80258
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 5254

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        839160 kB
Buffers:         34432 kB
Cached:         120648 kB
SwapCached:       2476 kB
Active:          55992 kB
Inactive:       104424 kB
HighTotal:      131008 kB
HighFree:         7336 kB
LowTotal:       903652 kB
LowFree:        831824 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29560 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:20:26 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3721 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80258 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 |   80258   160516 |   26752       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2272   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   95982   216713 |   31994       0        0     nan |  0.000 % |
c |       100 |   95955   216620 |   35193      92      677     7.4 |  0.179 % |
c |       250 |   95955   216620 |   38712     242     2996    12.4 |  0.176 % |
c |       475 |   95937   216558 |   42584     462     5185    11.2 |  0.236 % |
c |       812 |   95937   216558 |   46842     799     8608    10.8 |  0.235 % |
c |      1320 |   95895   216414 |   51526    1298    15699    12.1 |  0.381 % |
c |      2079 |   95832   216197 |   56679    2040    28097    13.8 |  0.589 % |
c |      3218 |   95745   215898 |   62347    3156    40962    13.0 |  0.880 % |
c |      4926 |   95481   214992 |   68581    4759    64921    13.6 |  1.791 % |
c |      7491 |   94938   213127 |   75440    7156   106644    14.9 |  3.873 % |
c |     11337 |   93707   208900 |   82984   10647   192250    18.1 |  9.120 % |
c |     17103 |   92660   205297 |   91282   16082   374087    23.3 | 14.076 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17341 |   92652   205273 |   30884   16317   383261    23.5 | 14.076 % |
c |     17441 |   92652   205273 |   33972   16417   388134    23.6 | 14.131 % |
c |     17593 |   92612   205135 |   37369   16555   390337    23.6 | 14.338 % |
c |     17820 |   92529   204846 |   41106   16729   399733    23.9 | 14.720 % |
c |     18157 |   92518   204807 |   45217   17062   412580    24.2 | 14.776 % |
c |     18664 |   92496   204729 |   49738   17520   432055    24.7 | 14.893 % |
c |     19423 |   92453   204580 |   54712   18264   465183    25.5 | 15.098 % |
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 |     20396 |   92363   204279 |   30787   19188   518931    27.0 | 15.098 % |
c |     20497 |   92287   204013 |   33865   19271   522981    27.1 | 16.004 % |
c |     20647 |   92256   203906 |   37252   19416   527045    27.1 | 16.178 % |
c |     20872 |   92170   203610 |   40977   19610   532633    27.2 | 16.618 % |
c |     21210 |   92058   203222 |   45075   19727   537488    27.2 | 17.145 % |
c |     21716 |   91734   202090 |   49582   20122   554067    27.5 | 18.962 % |
c |     22475 |   91609   201653 |   54541   20823   609384    29.3 | 19.607 % |
c |     23616 |   91297   200569 |   59995   21797   656719    30.1 | 21.309 % |
c |     25324 |   91156   200076 |   65994   23460   744377    31.7 | 22.128 % |
c |     27886 |   90893   199161 |   72594   25732   946995    36.8 | 23.535 % |
c |     31731 |   90699   198493 |   79853   29349  1286724    43.8 | 24.533 % |
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 |     32029 |   90700   198498 |   30233   29647  1300716    43.9 | 24.533 % |
c |     32129 |   90700   198498 |   33256   29747  1303873    43.8 | 24.555 % |
c |     32279 |   90700   198498 |   36581   29897  1312727    43.9 | 24.553 % |
c |     32504 |   90700   198498 |   40240   30122  1322224    43.9 | 24.555 % |
c |     32842 |   90694   198478 |   44264   30414  1339690    44.0 | 24.584 % |
c |     33350 |   90666   198380 |   48690   30854  1400941    45.4 | 24.729 % |
c |     34110 |   90540   197948 |   53559   31329  1456482    46.5 | 25.286 % |
c |     35249 |   90515   197861 |   58915   32446  1542061    47.5 | 25.434 % |
c |     36958 |   90427   197551 |   64807   34114  1705232    50.0 | 25.930 % |
c |     39520 |   90372   197362 |   71287   36569  1884522    51.5 | 26.194 % |
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 |     40881 |   90308   197147 |   30102   37876  1991461    52.6 | 26.194 % |
c |     40981 |   90308   197147 |   33112   17063  1018450    59.7 | 26.596 % |
c |     41132 |   90308   197147 |   36423   17214  1024710    59.5 | 26.596 % |
c |     41357 |   90299   197116 |   40065   17430  1033702    59.3 | 26.626 % |
c |     41694 |   90246   196931 |   44072   17743  1043281    58.8 | 26.920 % |
c |     42200 |   90225   196860 |   48479   18229  1070792    58.7 | 27.008 % |
c |     42960 |   90178   196695 |   53327   18955  1132283    59.7 | 27.270 % |
c |     44099 |   90178   196695 |   58660   20094  1203387    59.9 | 27.271 % |
c |     45807 |   90169   196664 |   64526   21776  1390360    63.8 | 27.299 % |
c |     48369 |   90041   196224 |   70978   24177  1691933    70.0 | 27.914 % |
c |     52213 |   90023   196162 |   78076   27988  1945835    69.5 | 27.973 % |
c |     57979 |   90023   196162 |   85884   33754  2987592    88.5 | 27.975 % |
c |     66630 |   89949   195906 |   94472   42334  4084805    96.5 | 28.356 % |
c |     79604 |   89949   195906 |  103920   55308  5638084   101.9 | 28.356 % |
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 |     92443 |   89851   195572 |   29950   67953  7150158   105.2 | 28.356 % |
c |     92543 |   89851   195572 |   32945   17815  1501845    84.3 | 28.814 % |
c |     92693 |   89845   195552 |   36239   17959  1507433    83.9 | 28.843 % |
c |     92918 |   89799   195396 |   39863   18168  1517363    83.5 | 29.078 % |
c |     93256 |   89799   195396 |   43849   18506  1562246    84.4 | 29.078 % |
c |     93762 |   89799   195396 |   48234   19012  1598518    84.1 | 29.078 % |
c |     94521 |   89799   195396 |   53058   19771  1661105    84.0 | 29.078 % |
c |     95660 |   89756   195245 |   58364   20893  1727614    82.7 | 29.312 % |
c |     97368 |   89715   195104 |   64200   22592  1919032    84.9 | 29.546 % |
c |     99930 |   89698   195045 |   70620   25144  2054574    81.7 | 29.634 % |
c |    103774 |   89698   195045 |   77682   28988  2423827    83.6 | 29.636 % |
c |    109541 |   89698   195045 |   85450   34755  3091055    88.9 | 29.634 % |
c |    118190 |   89687   195006 |   93995   43400  4437168   102.2 | 29.694 % |
c |    131165 |   89687   195006 |  103395   56375  6470910   114.8 | 29.694 % |
c |    150627 |   89571   194602 |  113735   75715  8410819   111.1 | 30.366 % |
c |    179819 |   89571   194602 |  125108  104907 13011218   124.0 | 30.368 % |
c |    223608 |   89571   194602 |  137619   38651  5730501   148.3 | 30.368 % |
c |    289292 |   89548   194523 |  151381  104325 14751835   141.4 | 30.484 % |
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 |    303652 |   89549   194531 |   29849  118685 17237646   145.2 | 30.484 % |
c |    303752 |   89549   194531 |   32833   15828  2323243   146.8 | 30.504 % |
c |    303902 |   89549   194531 |   36117   15978  2332310   146.0 | 30.505 % |
c |    304129 |   89549   194531 |   39729   16205  2336616   144.2 | 30.504 % |
c |    304468 |   89549   194531 |   43701   16544  2356424   142.4 | 30.504 % |
c |    304974 |   89549   194531 |   48072   17050  2371079   139.1 | 30.504 % |
c |    305733 |   89549   194531 |   52879   17809  2391894   134.3 | 30.505 % |
c |    306872 |   89528   194460 |   58167   18941  2454114   129.6 | 30.593 % |
c |    308580 |   89511   194401 |   63983   20636  2537611   123.0 | 30.681 % |
c |    311142 |   89511   194401 |   70382   23198  2699768   116.4 | 30.680 % |
c |    314987 |   89511   194401 |   77420   27043  3031229   112.1 | 30.679 % |
c |    320753 |   89505   194381 |   85162   32800  3370007   102.7 | 30.708 % |
c |    329402 |   89499   194361 |   93678   41446  4109594    99.2 | 30.740 % |
c |    342376 |   89454   194204 |  103046   54377  5169586    95.1 | 30.972 % |
c |    361839 |   89454   194204 |  113351   73840  8097095   109.7 | 30.973 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 43   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    386848 |   89455   194210 |   29818   98849 14250968   144.2 | 30.973 % |
c |    386948 |   89455   194210 |   32799   16735  3745071   223.8 | 30.992 % |
c |    387099 |   89455   194210 |   36079   16886  3753103   222.3 | 30.994 % |
c |    387325 |   89455   194210 |   39687   17112  3758982   219.7 | 30.992 % |
c |    387662 |   89455   194210 |   43656   17449  3768559   216.0 | 30.994 % |
c |    388168 |   89446   194179 |   48022   17951  3783030   210.7 | 31.021 % |
c |    388927 |   89446   194179 |   52824   18710  3829599   204.7 | 31.021 % |
c |    390066 |   89446   194179 |   58106   19849  3978834   200.5 | 31.021 % |
c |    391774 |   89446   194179 |   63917   21557  4080609   189.3 | 31.023 % |
c |    394337 |   89446   194179 |   70309   24120  4414553   183.0 | 31.021 % |
c |    398182 |   89446   194179 |   77340   27965  4726990   169.0 | 31.021 % |
c |    403948 |   89440   194159 |   85074   33727  5062478   150.1 | 31.051 % |
c |    412599 |   89440   194159 |   93581   42378  6278224   148.1 | 31.051 % |
c |    425573 |   89440   194159 |  102939   55352  7411248   133.9 | 31.051 % |
c |    445038 |   89440   194159 |  113233   74817  9761416   130.5 | 31.051 % |
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): 1.11 1.00 0.92 2/54 27270
Raw data (stat): 27270 (runsolver) R 27269 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479748682 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+9.99998 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 27270
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 3892 0 0 0 988 10 0 0 25 0 1 0 479748682 17772544 3870 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4339 3870 603 41 0 4298 0
vsize: 17356
[startup+20.0005 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 27270
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 3892 0 0 0 1987 10 0 0 25 0 1 0 479748682 17772544 3870 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4339 3870 603 41 0 4298 0
vsize: 17356
[startup+30.002 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 27270
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 3892 0 0 0 2987 11 0 0 25 0 1 0 479748682 17772544 3870 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4339 3870 603 41 0 4298 0
vsize: 17356
[startup+40.0021 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27270
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 3892 0 0 0 3985 11 0 0 25 0 1 0 479748682 17772544 3870 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4339 3870 603 41 0 4298 0
vsize: 17356
[startup+50.0018 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 3892 0 0 0 4985 11 0 0 25 0 1 0 479748682 17772544 3870 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4339 3870 603 41 0 4298 0
vsize: 17356
[startup+60.0014 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 4060 0 0 0 5985 12 0 0 25 0 1 0 479748682 18448384 4038 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4504 4038 603 41 0 4463 0
vsize: 18016
[startup+70.0011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 4144 0 0 0 6985 12 0 0 25 0 1 0 479748682 18853888 4122 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4122 603 41 0 4562 0
vsize: 18412
[startup+80.0023 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 5163 0 0 0 7982 15 0 0 25 0 1 0 479748682 23007232 5141 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5617 5141 603 41 0 5576 0
vsize: 22468
[startup+90.0025 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 5887 0 0 0 8980 17 0 0 25 0 1 0 479748682 25960448 5865 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6338 5865 603 41 0 6297 0
vsize: 25352
[startup+100.002 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 6618 0 0 0 9978 19 0 0 25 0 1 0 479748682 28921856 6596 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7061 6596 603 41 0 7020 0
vsize: 28244
[startup+110.003 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 7319 0 0 0 10977 20 0 0 25 0 1 0 479748682 31879168 7297 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7783 7297 603 41 0 7742 0
vsize: 31132
[startup+120.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 7945 0 0 0 11974 23 0 0 25 0 1 0 479748682 34422784 7923 4294967295 134512640 134672761 3221224560 3221223732 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8404 7923 603 41 0 8363 0
vsize: 33616
[startup+130.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 8469 0 0 0 12973 25 0 0 25 0 1 0 479748682 36569088 8447 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8928 8447 603 41 0 8887 0
vsize: 35712
[startup+140.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 8808 0 0 0 13972 26 0 0 25 0 1 0 479748682 37916672 8786 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9257 8786 603 41 0 9216 0
vsize: 37028
[startup+150.005 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9362 0 0 0 14970 28 0 0 25 0 1 0 479748682 40435712 9340 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9872 9340 603 41 0 9831 0
vsize: 39488
[startup+160.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 15970 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+170.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 16970 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+180.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 17970 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+190.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 18970 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+200.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 19970 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+210.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 20970 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+220.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 21971 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+230.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9514 0 0 0 22971 29 0 0 25 0 1 0 479748682 41037824 9492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10019 9492 603 41 0 9978 0
vsize: 40076
[startup+240.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9530 0 0 0 23971 29 0 0 25 0 1 0 479748682 41172992 9508 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10052 9508 603 41 0 10011 0
vsize: 40208
[startup+250.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 9802 0 0 0 24970 30 0 0 25 0 1 0 479748682 42246144 9780 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10314 9780 603 41 0 10273 0
vsize: 41256
[startup+260.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 10214 0 0 0 25969 32 0 0 25 0 1 0 479748682 43859968 10192 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 10192 603 41 0 10667 0
vsize: 42832
[startup+270.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 10664 0 0 0 26968 33 0 0 25 0 1 0 479748682 45752320 10642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11170 10642 603 41 0 11129 0
vsize: 44680
[startup+280.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 11164 0 0 0 27966 35 0 0 25 0 1 0 479748682 47763456 11142 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11661 11142 603 41 0 11620 0
vsize: 46644
[startup+290.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 11559 0 0 0 28964 37 0 0 25 0 1 0 479748682 49373184 11537 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12054 11537 603 41 0 12013 0
vsize: 48216
[startup+300.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 11881 0 0 0 29963 38 0 0 25 0 1 0 479748682 50716672 11859 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12382 11859 603 41 0 12341 0
vsize: 49528
[startup+310.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 12297 0 0 0 30962 39 0 0 25 0 1 0 479748682 52461568 12275 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12808 12275 603 41 0 12767 0
vsize: 51232
[startup+320.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27272
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 12744 0 0 0 31961 40 0 0 25 0 1 0 479748682 54210560 12722 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13235 12722 603 41 0 13194 0
vsize: 52940
[startup+330.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 13194 0 0 0 32959 42 0 0 25 0 1 0 479748682 56074240 13172 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13690 13172 603 41 0 13649 0
vsize: 54760
[startup+340.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 13636 0 0 0 33958 44 0 0 25 0 1 0 479748682 57942016 13614 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14146 13614 603 41 0 14105 0
vsize: 56584
[startup+350.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 14171 0 0 0 34957 45 0 0 25 0 1 0 479748682 60084224 14149 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14669 14149 603 41 0 14628 0
vsize: 58676
[startup+360.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 14676 0 0 0 35956 46 0 0 25 0 1 0 479748682 62087168 14654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15158 14654 603 41 0 15117 0
vsize: 60632
[startup+370.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 15114 0 0 0 36955 47 0 0 25 0 1 0 479748682 63963136 15092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15616 15092 603 41 0 15575 0
vsize: 62464
[startup+380.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 15559 0 0 0 37954 48 0 0 25 0 1 0 479748682 65699840 15537 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16040 15537 603 41 0 15999 0
vsize: 64160
[startup+390.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 15912 0 0 0 38953 49 0 0 25 0 1 0 479748682 67198976 15890 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16406 15890 603 41 0 16365 0
vsize: 65624
[startup+400.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 16148 0 0 0 39952 50 0 0 25 0 1 0 479748682 68165632 16126 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16642 16126 603 41 0 16601 0
vsize: 66568
[startup+410.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 16376 0 0 0 40952 51 0 0 25 0 1 0 479748682 69111808 16354 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16873 16354 603 41 0 16832 0
vsize: 67492
[startup+420.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 16841 0 0 0 41951 52 0 0 25 0 1 0 479748682 70971392 16819 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17327 16819 603 41 0 17286 0
vsize: 69308
[startup+430.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 17323 0 0 0 42949 54 0 0 25 0 1 0 479748682 72966144 17301 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17814 17301 603 41 0 17773 0
vsize: 71256
[startup+440.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 17640 0 0 0 43948 55 0 0 25 0 1 0 479748682 74305536 17618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18141 17618 603 41 0 18100 0
vsize: 72564
[startup+450.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 17988 0 0 0 44948 56 0 0 25 0 1 0 479748682 75644928 17966 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18468 17966 603 41 0 18427 0
vsize: 73872
[startup+460.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18417 0 0 0 45946 58 0 0 25 0 1 0 479748682 77381632 18395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18892 18395 603 41 0 18851 0
vsize: 75568
[startup+470.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18838 0 0 0 46945 58 0 0 25 0 1 0 479748682 79126528 18816 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19318 18816 603 41 0 19277 0
vsize: 77272
[startup+480.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 47945 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+490.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 48945 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+500.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 49945 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+510.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 50946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+520.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 51945 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+530.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 52946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 53946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+550.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 54946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+560.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 55946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+570.004 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 56946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+580.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 57946 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+590.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 58947 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+600.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 59947 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+610.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 60947 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+620.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 61948 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+630.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 62948 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+640.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 63948 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223744 134559618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+650.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 64948 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+660.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 65948 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223744 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+670.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 66949 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+680.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 67949 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+690.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 68949 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+700.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18919 0 0 0 69949 59 0 0 25 0 1 0 479748682 79396864 18897 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18897 603 41 0 19343 0
vsize: 77536
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18920 0 0 0 70949 59 0 0 25 0 1 0 479748682 79396864 18898 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18898 603 41 0 19343 0
vsize: 77536
[startup+720.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18921 0 0 0 71950 59 0 0 25 0 1 0 479748682 79396864 18899 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18899 603 41 0 19343 0
vsize: 77536
[startup+730.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18921 0 0 0 72950 59 0 0 25 0 1 0 479748682 79396864 18899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18899 603 41 0 19343 0
vsize: 77536
[startup+740.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18921 0 0 0 73950 59 0 0 25 0 1 0 479748682 79396864 18899 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18899 603 41 0 19343 0
vsize: 77536
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18921 0 0 0 74949 59 0 0 25 0 1 0 479748682 79396864 18899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19384 18899 603 41 0 19343 0
vsize: 77536
[startup+760.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18921 0 0 0 75949 59 0 0 25 0 1 0 479748682 79396864 18899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19384 18899 603 41 0 19343 0
vsize: 77536
[startup+770.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 18961 0 0 0 76949 59 0 0 25 0 1 0 479748682 79663104 18939 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19449 18939 603 41 0 19408 0
vsize: 77796
[startup+780.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 19415 0 0 0 77948 60 0 0 25 0 1 0 479748682 81539072 19393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19907 19394 603 41 0 19866 0
vsize: 79628
[startup+790.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 19891 0 0 0 78947 61 0 0 25 0 1 0 479748682 83419136 19869 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20366 19869 603 41 0 20325 0
vsize: 81464
[startup+800.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20400 0 0 0 79946 63 0 0 25 0 1 0 479748682 85565440 20378 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20890 20378 603 41 0 20849 0
vsize: 83560
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 80946 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+820.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 81946 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+830.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 82946 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+840.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 83947 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 84947 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+860.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 85947 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+870.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 86947 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+880.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 87947 63 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+890.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 88947 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+900.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 89948 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+910.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 90948 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+920.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 91948 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+930.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 92948 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+940.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 93949 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+950.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 94949 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+960.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 95949 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+970.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 96949 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+980.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 97949 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+990.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 98949 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 99950 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 100950 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 101950 64 0 0 25 0 1 0 479748682 86110208 20526 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 20526 603 41 0 20982 0
vsize: 84092
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 102950 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 103950 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 104951 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 105951 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 106951 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223804 134557468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 107951 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 108951 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 109952 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 110952 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 111952 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 112952 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 113952 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 114953 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 115953 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 116953 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223744 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 117953 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 118953 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27274
Raw data (stat): 27270 (minisat+) R 27269 22612 22611 0 -1 0 20548 0 0 0 119953 64 0 0 25 0 1 0 479748682 85958656 20502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20986 20502 603 41 0 20945 0
vsize: 83944
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 27274
Raw data (stat): 27270 (minisat+) Z 27269 22612 22611 0 -1 12 20551 0 0 0 119954 67 0 0 25 0 1 0 479748682 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.07
CPU time (s): 1200.22
CPU user time (s): 1199.54
CPU system time (s): 0.678896
CPU usage (%): 100.013
Max. virtual memory (Kb): 84092
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####