PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-1.opb
MD5SUM	ed1ca962177baf0f135b785abad8adea
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	1150
Total number of constraints	80072
Number of constraints which are clauses	80072
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6005

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        840520 kB
Buffers:         34832 kB
Cached:         121876 kB
SwapCached:       3160 kB
Active:          71312 kB
Inactive:        91404 kB
HighTotal:      131008 kB
HighFree:         5796 kB
LowTotal:       903652 kB
LowFree:        834724 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25788 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:13:48 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4470 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80072 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80072   160144 |   26690       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  147988   319466 |   49329       0        0     nan |  0.000 % |
c |       100 |  147362   318162 |   54261      77      551     7.2 |  0.736 % |
c |       250 |  146841   317054 |   59688     209     2448    11.7 |  1.369 % |
c |       475 |  145811   314812 |   65656     398     4382    11.0 |  2.680 % |
c |       812 |  144010   310871 |   72222     677     8303    12.3 |  4.995 % |
c |      1318 |  141157   304558 |   79444    1060    12573    11.9 |  8.737 % |
c |      2077 |  136776   294746 |   87389    1627    19630    12.1 | 14.610 % |
c |      3216 |  131215   282210 |   96128    2497    29631    11.9 | 22.142 % |
c |      4924 |  123727   265107 |  105741    3779    49504    13.1 | 32.476 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6427 |  116683   248991 |   38894    4766    61496    12.9 | 32.476 % |
c |      6527 |  116204   247870 |   42783    4831    62291    12.9 | 43.100 % |
c |      6677 |  115663   246594 |   47061    4934    63665    12.9 | 43.849 % |
c |      6902 |  114831   244655 |   51767    5110    65775    12.9 | 44.973 % |
c |      7239 |  113564   241690 |   56944    5351    69474    13.0 | 46.827 % |
c |      7746 |  111539   236942 |   62639    5688    74185    13.0 | 49.645 % |
c |      8505 |  108258   229196 |   68903    6014    79861    13.3 | 54.380 % |
c |      9645 |  106402   224792 |   75793    6813    92319    13.6 | 57.095 % |
c |     11355 |  103049   216804 |   83372    7947   113001    14.2 | 62.021 % |
c |     13917 |   98383   205681 |   91710    9480   147925    15.6 | 68.784 % |
c |     17761 |   94811   197102 |  100881   12081   211420    17.5 | 74.113 % |
c |     23527 |   91940   190193 |  110969   16325   396509    24.3 | 78.405 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26517 |   91505   189103 |   30501   18993   511336    26.9 | 78.405 % |
c |     26617 |   91453   188977 |   33551   19046   513223    26.9 | 79.155 % |
c |     26767 |   91403   188856 |   36906   19147   514654    26.9 | 79.230 % |
c |     26993 |   91347   188722 |   40596   19332   517806    26.8 | 79.308 % |
c |     27330 |   91347   188722 |   44656   19669   531077    27.0 | 79.308 % |
c |     27836 |   91347   188722 |   49122   20175   549790    27.3 | 79.308 % |
c |     28595 |   91336   188697 |   54034   20920   586573    28.0 | 79.323 % |
c |     29734 |   91040   187971 |   59437   21902   671987    30.7 | 79.772 % |
c |     31442 |   91021   187926 |   65381   23576   759400    32.2 | 79.800 % |
c |     34004 |   90924   187692 |   71919   26012   920916    35.4 | 79.947 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37368 |   90426   186513 |   30142   28875  1073664    37.2 | 79.947 % |
c |     37468 |   90272   186133 |   33156   28788  1071210    37.2 | 80.912 % |
c |     37618 |   90272   186133 |   36471   28938  1078094    37.3 | 80.912 % |
c |     37845 |   90055   185604 |   40119   28990  1084507    37.4 | 81.229 % |
c |     38182 |   89765   184919 |   44130   29091  1093267    37.6 | 81.654 % |
c |     38690 |   89677   184699 |   48543   29419  1114490    37.9 | 81.794 % |
c |     39449 |   89637   184597 |   53398   30143  1175417    39.0 | 81.859 % |
c |     40590 |   89554   184394 |   58738   31209  1251534    40.1 | 81.988 % |
c |     42298 |   89419   184073 |   64612   32883  1358367    41.3 | 82.189 % |
c |     44861 |   89408   184048 |   71073   35430  1659938    46.9 | 82.204 % |
c |     48706 |   89194   183528 |   78180   38940  1937517    49.8 | 82.527 % |
c |     54473 |   89111   183331 |   85998   44007  2548488    57.9 | 82.650 % |
c |     63122 |   88944   182914 |   94598   52476  3364323    64.1 | 82.920 % |
c |     76097 |   88814   182580 |  104058   65300  4943713    75.7 | 83.140 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77862 |   88826   182643 |   29608   67005  5167051    77.1 | 83.140 % |
c |     77964 |   88784   182545 |   32568   67090  5171321    77.1 | 83.214 % |
c |     78114 |   88784   182545 |   35825   67240  5180522    77.0 | 83.214 % |
c |     78339 |   88743   182450 |   39408   67391  5196716    77.1 | 83.270 % |
c |     78678 |   88708   182365 |   43349   67686  5220332    77.1 | 83.324 % |
c |     79184 |   88704   182355 |   47683   68174  5263297    77.2 | 83.330 % |
c |     79943 |   88664   182255 |   52452   68714  5301058    77.1 | 83.395 % |
c |     81082 |   88585   182068 |   57697   69580  5394262    77.5 | 83.511 % |
c |     82790 |   88519   181910 |   63467   71223  5554743    78.0 | 83.610 % |
c |     85352 |   88517   181906 |   69814   73749  5848295    79.3 | 83.612 % |
c |     89198 |   88366   181535 |   76795   77183  6388766    82.8 | 83.847 % |
c |     94964 |   88258   181285 |   84475   82844  7485378    90.4 | 83.993 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98263 |   88158   181016 |   29386   85817  7763842    90.5 | 83.993 % |
c |     98364 |   88158   181016 |   32324   22455  2013545    89.7 | 84.158 % |
c |     98514 |   88158   181016 |   35557   22605  2027056    89.7 | 84.158 % |
c |     98740 |   88158   181016 |   39112   22831  2038443    89.3 | 84.158 % |
c |     99077 |   88158   181016 |   43024   23168  2078602    89.7 | 84.158 % |
c |     99583 |   88158   181016 |   47326   23674  2126008    89.8 | 84.158 % |
c |    100342 |   88158   181016 |   52059   24433  2186274    89.5 | 84.158 % |
c |    101484 |   88150   180996 |   57265   25550  2295749    89.9 | 84.170 % |
c |    103195 |   88096   180868 |   62991   27218  2436552    89.5 | 84.250 % |
c |    105757 |   88096   180868 |   69290   29780  2702781    90.8 | 84.250 % |
c |    109601 |   88046   180746 |   76219   33602  3048134    90.7 | 84.328 % |
c |    115367 |   88046   180746 |   83841   39368  3668323    93.2 | 84.328 % |
c |    124016 |   88046   180746 |   92225   48017  4913028   102.3 | 84.328 % |
c |    136990 |   87949   180511 |  101448   60968  6988775   114.6 | 84.476 % |
c |    156451 |   87902   180392 |  111593   80363  9395711   116.9 | 84.553 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    166657 |   87834   180240 |   29278   90507 10717436   118.4 | 84.553 % |
c |    166757 |   87834   180240 |   32205   23788  1691897    71.1 | 84.668 % |
c |    166907 |   87789   180133 |   35426   23933  1702187    71.1 | 84.735 % |
c |    167132 |   87789   180133 |   38969   24158  1720163    71.2 | 84.735 % |
c |    167470 |   87789   180133 |   42865   24496  1758488    71.8 | 84.735 % |
c |    167976 |   87628   179729 |   47152   24984  1795588    71.9 | 84.980 % |
c |    168736 |   87561   179560 |   51867   25707  1847965    71.9 | 85.083 % |
c |    169875 |   87561   179560 |   57054   26846  1997820    74.4 | 85.083 % |
c |    171583 |   87555   179546 |   62759   28551  2143274    75.1 | 85.092 % |
c |    174145 |   87543   179518 |   69035   31109  2357991    75.8 | 85.109 % |
c |    177989 |   87543   179518 |   75939   34953  2874390    82.2 | 85.109 % |
c |    183757 |   87535   179500 |   83533   40698  3596006    88.4 | 85.120 % |
c |    192406 |   87535   179500 |   91886   49347  4807829    97.4 | 85.120 % |
c |    205380 |   87464   179337 |  101075   62280  6436341   103.3 | 85.217 % |
c |    224841 |   87464   179337 |  111183   81741  9073077   111.0 | 85.217 % |
c |    254033 |   87464   179337 |  122301  110933 13542456   122.1 | 85.217 % |
c |    297822 |   87384   179141 |  134531  154625 20442372   132.2 | 85.339 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 C1036 -C1035 C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 C901 -C900 -C899 -C898 -C897 -C896 C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.91 2/54 24009
Raw data (stat): 24009 (runsolver) R 24008 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481141987 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 4911 0 0 0 986 12 0 0 25 0 1 0 481141987 23158784 4889 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5654 4889 603 41 0 5613 0
vsize: 22616
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 4920 0 0 0 1986 12 0 0 25 0 1 0 481141987 23158784 4898 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5654 4898 603 41 0 5613 0
vsize: 22616
[startup+30.001 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 4929 0 0 0 2986 12 0 0 25 0 1 0 481141987 23293952 4907 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5687 4907 603 41 0 5646 0
vsize: 22748
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 4940 0 0 0 3985 12 0 0 25 0 1 0 481141987 23293952 4918 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5687 4918 603 41 0 5646 0
vsize: 22748
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 4954 0 0 0 4985 12 0 0 25 0 1 0 481141987 23433216 4932 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5721 4932 603 41 0 5680 0
vsize: 22884
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 5085 0 0 0 5985 13 0 0 25 0 1 0 481141987 24227840 5063 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5915 5063 603 41 0 5874 0
vsize: 23660
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 5086 0 0 0 6985 13 0 0 25 0 1 0 481141987 24227840 5064 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5064 603 41 0 5874 0
vsize: 23660
[startup+80.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 5086 0 0 0 7984 13 0 0 25 0 1 0 481141987 24227840 5064 4294967295 134512640 134672761 3221224560 3221223776 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5915 5064 603 41 0 5874 0
vsize: 23660
[startup+90.001 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 5131 0 0 0 8984 14 0 0 25 0 1 0 481141987 24498176 5109 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5981 5109 603 41 0 5940 0
vsize: 23924
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 5304 0 0 0 9984 14 0 0 25 0 1 0 481141987 25157632 5282 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6142 5282 603 41 0 6101 0
vsize: 24568
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 5604 0 0 0 10983 15 0 0 25 0 1 0 481141987 26464256 5582 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5582 603 41 0 6420 0
vsize: 25844
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 6064 0 0 0 11981 17 0 0 25 0 1 0 481141987 28209152 6042 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6887 6042 603 41 0 6846 0
vsize: 27548
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 6333 0 0 0 12980 18 0 0 25 0 1 0 481141987 29421568 6311 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7183 6311 603 41 0 7142 0
vsize: 28732
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 6840 0 0 0 13978 20 0 0 25 0 1 0 481141987 31567872 6818 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7707 6818 603 41 0 7666 0
vsize: 30828
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 7318 0 0 0 14977 22 0 0 25 0 1 0 481141987 33439744 7296 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8164 7296 603 41 0 8123 0
vsize: 32656
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 7805 0 0 0 15976 23 0 0 25 0 1 0 481141987 35450880 7783 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8655 7783 603 41 0 8614 0
vsize: 34620
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 8281 0 0 0 16974 25 0 0 25 0 1 0 481141987 37335040 8259 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9115 8259 603 41 0 9074 0
vsize: 36460
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 8712 0 0 0 17973 26 0 0 25 0 1 0 481141987 39215104 8690 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9574 8690 603 41 0 9533 0
vsize: 38296
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 9183 0 0 0 18971 28 0 0 25 0 1 0 481141987 41091072 9161 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10032 9161 603 41 0 9991 0
vsize: 40128
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 9645 0 0 0 19970 29 0 0 25 0 1 0 481141987 42962944 9623 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10489 9623 603 41 0 10448 0
vsize: 41956
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 10154 0 0 0 20969 30 0 0 25 0 1 0 481141987 44961792 10132 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10977 10132 603 41 0 10936 0
vsize: 43908
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 10540 0 0 0 21968 31 0 0 25 0 1 0 481141987 46833664 10518 4294967295 134512640 134672761 3221224560 3221223728 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11434 10518 603 41 0 11393 0
vsize: 45736
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 10755 0 0 0 22968 32 0 0 25 0 1 0 481141987 47702016 10733 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11646 10733 603 41 0 11605 0
vsize: 46584
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 11047 0 0 0 23967 32 0 0 25 0 1 0 481141987 48910336 11025 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11941 11025 603 41 0 11900 0
vsize: 47764
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 11410 0 0 0 24967 33 0 0 25 0 1 0 481141987 50397184 11388 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12304 11388 603 41 0 12263 0
vsize: 49216
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 11794 0 0 0 25966 35 0 0 25 0 1 0 481141987 52002816 11772 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12696 11772 603 41 0 12655 0
vsize: 50784
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 12197 0 0 0 26965 35 0 0 25 0 1 0 481141987 53616640 12175 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13090 12175 603 41 0 13049 0
vsize: 52360
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 12741 0 0 0 27964 37 0 0 25 0 1 0 481141987 55754752 12719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13612 12719 603 41 0 13571 0
vsize: 54448
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13168 0 0 0 28963 38 0 0 25 0 1 0 481141987 57495552 13146 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14037 13146 603 41 0 13996 0
vsize: 56148
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 29962 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 30962 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 31962 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 32962 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223664 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 33962 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 34963 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 35963 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24009
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 36963 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+380.002 s]
Raw data (loadavg): 1.07 0.99 0.92 2/58 24013
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 37963 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+390.003 s]
Raw data (loadavg): 1.14 1.00 0.93 2/54 24062
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 38963 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+400.003 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 24062
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 39963 39 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+410.004 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 24062
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13449 0 0 0 40963 40 0 0 25 0 1 0 481141987 58667008 13427 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14323 13427 603 41 0 14282 0
vsize: 57292
[startup+420.003 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 24062
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13485 0 0 0 41963 40 0 0 25 0 1 0 481141987 58802176 13463 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14356 13463 603 41 0 14315 0
vsize: 57424
[startup+430.003 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 24062
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 13901 0 0 0 42961 41 0 0 25 0 1 0 481141987 60530688 13879 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14778 13879 603 41 0 14737 0
vsize: 59112
[startup+440.004 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 24062
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 14265 0 0 0 43960 43 0 0 25 0 1 0 481141987 61997056 14243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15136 14243 603 41 0 15095 0
vsize: 60544
[startup+450.004 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 14574 0 0 0 44958 46 0 0 25 0 1 0 481141987 63324160 14552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15460 14552 603 41 0 15419 0
vsize: 61840
[startup+460.005 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 14869 0 0 0 45957 46 0 0 25 0 1 0 481141987 64520192 14847 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15752 14847 603 41 0 15711 0
vsize: 63008
[startup+470.005 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 15159 0 0 0 46956 48 0 0 25 0 1 0 481141987 65720320 15137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16045 15137 603 41 0 16004 0
vsize: 64180
[startup+480.005 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 15448 0 0 0 47955 49 0 0 25 0 1 0 481141987 66928640 15426 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16340 15426 603 41 0 16299 0
vsize: 65360
[startup+490.006 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 15788 0 0 0 48954 50 0 0 25 0 1 0 481141987 68259840 15766 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16665 15766 603 41 0 16624 0
vsize: 66660
[startup+500.007 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16068 0 0 0 49953 51 0 0 25 0 1 0 481141987 69341184 16046 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16929 16046 603 41 0 16888 0
vsize: 67716
[startup+510.008 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16420 0 0 0 50952 52 0 0 25 0 1 0 481141987 70811648 16398 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17288 16398 603 41 0 17247 0
vsize: 69152
[startup+520.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 51951 53 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+530.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 52951 54 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+540.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 53951 54 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+550.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 54951 54 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+560.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 55951 55 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+570.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 56951 55 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+580.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 57951 55 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+590.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 58951 56 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+600.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 59951 56 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+610.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 60951 56 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+620.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 61950 56 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+630.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 62950 57 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+640.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 63950 57 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+650.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 64950 58 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+660.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 65950 58 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+670.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 66950 58 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+680.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 67950 59 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+690.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 68950 59 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+700.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 69950 59 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+710.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 70949 60 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+720.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24064
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 71949 60 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+730.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 72949 61 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+740.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16633 0 0 0 73948 61 0 0 25 0 1 0 481141987 71688192 16611 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17502 16611 603 41 0 17461 0
vsize: 70008
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 16839 0 0 0 74948 62 0 0 25 0 1 0 481141987 72486912 16817 4294967295 134512640 134672761 3221224560 3221223664 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17697 16817 603 41 0 17656 0
vsize: 70788
[startup+760.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 17198 0 0 0 75947 63 0 0 25 0 1 0 481141987 73949184 17176 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18054 17176 603 41 0 18013 0
vsize: 72216
[startup+770.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 17524 0 0 0 76946 64 0 0 25 0 1 0 481141987 75284480 17502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18380 17502 603 41 0 18339 0
vsize: 73520
[startup+780.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 17824 0 0 0 77945 65 0 0 25 0 1 0 481141987 76488704 17802 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18674 17802 603 41 0 18633 0
vsize: 74696
[startup+790.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 18138 0 0 0 78944 66 0 0 25 0 1 0 481141987 77828096 18116 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19001 18116 603 41 0 18960 0
vsize: 76004
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 18399 0 0 0 79943 67 0 0 25 0 1 0 481141987 78897152 18377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19262 18377 603 41 0 19221 0
vsize: 77048
[startup+810.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 18667 0 0 0 80943 68 0 0 25 0 1 0 481141987 79958016 18645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19521 18645 603 41 0 19480 0
vsize: 78084
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 18964 0 0 0 81942 69 0 0 25 0 1 0 481141987 81149952 18942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19812 18942 603 41 0 19771 0
vsize: 79248
[startup+830.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 19240 0 0 0 82941 70 0 0 25 0 1 0 481141987 82345984 19218 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 19218 603 41 0 20063 0
vsize: 80416
[startup+840.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 19486 0 0 0 83940 71 0 0 25 0 1 0 481141987 83267584 19464 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20329 19464 603 41 0 20288 0
vsize: 81316
[startup+850.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 19726 0 0 0 84940 72 0 0 25 0 1 0 481141987 84340736 19704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20591 19704 603 41 0 20550 0
vsize: 82364
[startup+860.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 20021 0 0 0 85938 73 0 0 25 0 1 0 481141987 85532672 19999 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20882 19999 603 41 0 20841 0
vsize: 83528
[startup+870.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 20349 0 0 0 86937 74 0 0 25 0 1 0 481141987 86876160 20327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21210 20327 603 41 0 21169 0
vsize: 84840
[startup+880.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 20637 0 0 0 87935 76 0 0 25 0 1 0 481141987 88084480 20615 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21505 20615 603 41 0 21464 0
vsize: 86020
[startup+890.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 20970 0 0 0 88935 76 0 0 25 0 1 0 481141987 89411584 20948 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21829 20948 603 41 0 21788 0
vsize: 87316
[startup+900.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 21290 0 0 0 89934 78 0 0 25 0 1 0 481141987 90742784 21268 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22154 21268 603 41 0 22113 0
vsize: 88616
[startup+910.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 21594 0 0 0 90933 79 0 0 25 0 1 0 481141987 91930624 21572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22444 21572 603 41 0 22403 0
vsize: 89776
[startup+920.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 21895 0 0 0 91932 80 0 0 25 0 1 0 481141987 93122560 21873 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21873 603 41 0 22694 0
vsize: 90940
[startup+930.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 22172 0 0 0 92932 80 0 0 25 0 1 0 481141987 94314496 22150 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23026 22150 603 41 0 22985 0
vsize: 92104
[startup+940.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 22432 0 0 0 93931 81 0 0 25 0 1 0 481141987 95375360 22410 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23285 22410 603 41 0 23244 0
vsize: 93140
[startup+950.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 22691 0 0 0 94930 82 0 0 25 0 1 0 481141987 96440320 22669 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23545 22669 603 41 0 23504 0
vsize: 94180
[startup+960.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 22976 0 0 0 95930 83 0 0 25 0 1 0 481141987 97501184 22954 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23804 22954 603 41 0 23763 0
vsize: 95216
[startup+970.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 23255 0 0 0 96929 84 0 0 25 0 1 0 481141987 98697216 23233 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24096 23233 603 41 0 24055 0
vsize: 96384
[startup+980.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 23487 0 0 0 97928 85 0 0 25 0 1 0 481141987 100159488 23465 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24453 23465 603 41 0 24412 0
vsize: 97812
[startup+990.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 23707 0 0 0 98928 86 0 0 25 0 1 0 481141987 101093376 23685 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24681 23685 603 41 0 24640 0
vsize: 98724
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 23953 0 0 0 99927 86 0 0 25 0 1 0 481141987 102146048 23931 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24938 23931 603 41 0 24897 0
vsize: 99752
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 24186 0 0 0 100926 87 0 0 25 0 1 0 481141987 102961152 24164 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25137 24164 603 41 0 25096 0
vsize: 100548
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 24409 0 0 0 101926 88 0 0 25 0 1 0 481141987 103899136 24387 4294967295 134512640 134672761 3221224560 3221223728 134561136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25366 24387 603 41 0 25325 0
vsize: 101464
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 24639 0 0 0 102925 89 0 0 25 0 1 0 481141987 104960000 24617 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25625 24617 603 41 0 25584 0
vsize: 102500
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 24853 0 0 0 103925 90 0 0 25 0 1 0 481141987 105771008 24831 4294967295 134512640 134672761 3221224560 3221223696 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25823 24831 603 41 0 25782 0
vsize: 103292
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 25085 0 0 0 104924 90 0 0 25 0 1 0 481141987 106696704 25063 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26049 25063 603 41 0 26008 0
vsize: 104196
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 25322 0 0 0 105924 91 0 0 25 0 1 0 481141987 107626496 25300 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26276 25300 603 41 0 26235 0
vsize: 105104
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 25616 0 0 0 106923 92 0 0 25 0 1 0 481141987 108830720 25594 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26570 25594 603 41 0 26529 0
vsize: 106280
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 25860 0 0 0 107922 93 0 0 25 0 1 0 481141987 109903872 25838 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26832 25838 603 41 0 26791 0
vsize: 107328
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 26145 0 0 0 108922 93 0 0 25 0 1 0 481141987 110981120 26123 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27095 26123 603 41 0 27054 0
vsize: 108380
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 26390 0 0 0 109921 95 0 0 25 0 1 0 481141987 112046080 26368 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27355 26368 603 41 0 27314 0
vsize: 109420
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 26599 0 0 0 110921 95 0 0 25 0 1 0 481141987 112848896 26577 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27551 26577 603 41 0 27510 0
vsize: 110204
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 26805 0 0 0 111920 95 0 0 25 0 1 0 481141987 113782784 26783 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27779 26783 603 41 0 27738 0
vsize: 111116
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 27026 0 0 0 112919 97 0 0 25 0 1 0 481141987 114593792 27004 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27977 27004 603 41 0 27936 0
vsize: 111908
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 27253 0 0 0 113918 97 0 0 25 0 1 0 481141987 115523584 27231 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28204 27231 603 41 0 28163 0
vsize: 112816
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 27467 0 0 0 114917 98 0 0 25 0 1 0 481141987 116457472 27445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28432 27445 603 41 0 28391 0
vsize: 113728
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 27680 0 0 0 115917 99 0 0 25 0 1 0 481141987 117256192 27658 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28627 27658 603 41 0 28586 0
vsize: 114508
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 27876 0 0 0 116916 100 0 0 25 0 1 0 481141987 118050816 27854 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28821 27854 603 41 0 28780 0
vsize: 115284
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 28071 0 0 0 117916 101 0 0 25 0 1 0 481141987 118857728 28049 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29018 28049 603 41 0 28977 0
vsize: 116072
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 28263 0 0 0 118916 101 0 0 25 0 1 0 481141987 119656448 28241 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29213 28241 603 41 0 29172 0
vsize: 116852
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 24066
Raw data (stat): 24009 (minisat+) R 24008 18865 18864 0 -1 0 28442 0 0 0 119915 102 0 0 25 0 1 0 481141987 120446976 28420 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29406 28420 603 41 0 29365 0
vsize: 117624
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 24066
Raw data (stat): 24009 (minisat+) Z 24008 18865 18864 0 -1 12 28445 0 0 0 119915 107 0 0 25 0 1 0 481141987 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.24
CPU user time (s): 1199.16
CPU system time (s): 1.07883
CPU usage (%): 100.011
Max. virtual memory (Kb): 117624
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####