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 5251

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        884188 kB
Buffers:         35308 kB
Cached:          91704 kB
SwapCached:       3276 kB
Active:          69808 kB
Inactive:        63328 kB
HighTotal:      131008 kB
HighFree:        35364 kB
LowTotal:       903652 kB
LowFree:        848824 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11700 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:16:54 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 3718 7 1200.25 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]---> Adder-cost: 2272   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   95794   216334 |   31931       0        0     nan |  0.000 % |
c |       100 |   95776   216272 |   35124      94      919     9.8 |  0.147 % |
c |       250 |   95776   216272 |   38636     244     2964    12.1 |  0.147 % |
c |       475 |   95758   216210 |   42500     463     5135    11.1 |  0.208 % |
c |       812 |   95731   216117 |   46750     789     8168    10.4 |  0.293 % |
c |      1318 |   95695   215993 |   51425    1285    15572    12.1 |  0.412 % |
c |      2077 |   95623   215745 |   56567    2025    24468    12.1 |  0.646 % |
c |      3216 |   95459   215179 |   62224    3111    37942    12.2 |  1.203 % |
c |      4924 |   95298   214626 |   68446    4755    60899    12.8 |  1.789 % |
c |      7486 |   94624   212310 |   75291    7101   103800    14.6 |  4.459 % |
c |     11330 |   92979   206649 |   82820   10432   175986    16.9 | 11.587 % |
c |     17096 |   91142   200294 |   91102   15276   332115    21.7 | 20.974 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25006 |   90070   196579 |   30023   22077   734429    33.3 | 20.974 % |
c |     25106 |   90059   196540 |   33025   22146   735894    33.2 | 26.738 % |
c |     25256 |   90059   196540 |   36327   22296   745397    33.4 | 26.737 % |
c |     25482 |   90002   196347 |   39960   22390   750847    33.5 | 27.060 % |
c |     25819 |   90002   196347 |   43956   22727   763884    33.6 | 27.061 % |
c |     26325 |   89990   196307 |   48352   23165   789366    34.1 | 27.120 % |
c |     27084 |   89990   196307 |   53187   23924   824819    34.5 | 27.118 % |
c |     28223 |   89954   196181 |   58506   24967   889669    35.6 | 27.325 % |
c |     29931 |   89926   196087 |   64356   26615  1027169    38.6 | 27.499 % |
c |     32495 |   89917   196056 |   70792   29136  1322730    45.4 | 27.530 % |
c |     36339 |   89871   195896 |   77871   32827  1621983    49.4 | 27.734 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38896 |   89811   195690 |   29937   35134  1848132    52.6 | 27.734 % |
c |     38996 |   89811   195690 |   32930   15863  1036886    65.4 | 28.021 % |
c |     39146 |   89811   195690 |   36223   16013  1043063    65.1 | 28.021 % |
c |     39371 |   89811   195690 |   39846   16238  1051399    64.7 | 28.019 % |
c |     39708 |   89811   195690 |   43830   16575  1071102    64.6 | 28.019 % |
c |     40215 |   89783   195596 |   48213   17074  1110308    65.0 | 28.195 % |
c |     40975 |   89693   195284 |   53035   17778  1145785    64.4 | 28.576 % |
c |     42114 |   89687   195264 |   58338   18909  1307277    69.1 | 28.605 % |
c |     43822 |   89687   195264 |   64172   20617  1461251    70.9 | 28.605 % |
c |     46385 |   89687   195264 |   70589   23180  1668354    72.0 | 28.605 % |
c |     50229 |   89616   195017 |   77648   26944  1966984    73.0 | 29.017 % |
c |     55996 |   89592   194935 |   85413   32692  2555687    78.2 | 29.103 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60515 |   89561   194837 |   29853   37158  3009584    81.0 | 29.103 % |
c |     60616 |   89561   194837 |   32838   15996  1152012    72.0 | 29.270 % |
c |     60766 |   89552   194806 |   36122   16139  1158616    71.8 | 29.300 % |
c |     60991 |   89552   194806 |   39734   16364  1176318    71.9 | 29.300 % |
c |     61328 |   89537   194755 |   43707   16691  1194385    71.6 | 29.358 % |
c |     61837 |   89522   194704 |   48078   17198  1226550    71.3 | 29.417 % |
c |     62596 |   89522   194704 |   52886   17957  1314214    73.2 | 29.418 % |
c |     63735 |   89522   194704 |   58175   19096  1365869    71.5 | 29.417 % |
c |     65443 |   89522   194704 |   63992   20804  1471012    70.7 | 29.419 % |
c |     68005 |   89470   194524 |   70391   23352  1688624    72.3 | 29.653 % |
c |     71849 |   89470   194524 |   77430   27196  2046357    75.2 | 29.651 % |
c |     77616 |   89464   194504 |   85174   32953  2613348    79.3 | 29.682 % |
c |     86265 |   89458   194484 |   93691   41596  3635234    87.4 | 29.710 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 41   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93621 |   89459   194491 |   29819   48952  4312327    88.1 | 29.710 % |
c |     93721 |   89459   194491 |   32800   16898  1347218    79.7 | 29.732 % |
c |     93871 |   89459   194491 |   36080   17048  1355338    79.5 | 29.732 % |
c |     94096 |   89459   194491 |   39689   17273  1369199    79.3 | 29.731 % |
c |     94433 |   89438   194420 |   43657   17609  1384065    78.6 | 29.818 % |
c |     94941 |   89438   194420 |   48023   18117  1414167    78.1 | 29.818 % |
c |     95700 |   89438   194420 |   52826   18876  1464792    77.6 | 29.818 % |
c |     96840 |   89438   194420 |   58108   20016  1530877    76.5 | 29.821 % |
c |     98548 |   89392   194258 |   63919   21688  1709501    78.8 | 30.111 % |
c |    101111 |   89374   194196 |   70311   24244  1998067    82.4 | 30.170 % |
c |    104955 |   89325   194023 |   77342   28080  2364972    84.2 | 30.463 % |
c |    110722 |   89325   194023 |   85077   33847  3016080    89.1 | 30.463 % |
c |    119372 |   89282   193874 |   93584   42463  3956586    93.2 | 30.669 % |
c |    132348 |   89264   193814 |  102943   55401  5333341    96.3 | 30.758 % |
c |    151809 |   89247   193755 |  113237   74800  7436133    99.4 | 30.844 % |
c |    181001 |   89210   193626 |  124561  103978  9844113    94.7 | 31.078 % |
c |    224792 |   89210   193626 |  137017   36822  6481750   176.0 | 31.078 % |
c |    290476 |   89199   193587 |  150719  102505 17265080   168.4 | 31.137 % |
c |    389005 |   89199   193587 |  165791   64068  8403601   131.2 | 31.138 % |
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.85 0.94 0.90 2/54 17032
Raw data (stat): 17032 (runsolver) R 17031 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421497568 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 3883 0 0 0 987 11 0 0 25 0 1 0 421497568 17715200 3861 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3861 603 41 0 4284 0
vsize: 17300
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 3883 0 0 0 1987 12 0 0 25 0 1 0 421497568 17715200 3861 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3861 603 41 0 4284 0
vsize: 17300
[startup+30.0026 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 3883 0 0 0 2987 12 0 0 25 0 1 0 421497568 17715200 3861 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3861 603 41 0 4284 0
vsize: 17300
[startup+40.0028 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 3883 0 0 0 3986 12 0 0 25 0 1 0 421497568 17715200 3861 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3861 603 41 0 4284 0
vsize: 17300
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 3883 0 0 0 4986 12 0 0 25 0 1 0 421497568 17715200 3861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3861 603 41 0 4284 0
vsize: 17300
[startup+60.004 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 3890 0 0 0 5986 12 0 0 25 0 1 0 421497568 17715200 3868 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3868 603 41 0 4284 0
vsize: 17300
[startup+70.0053 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 4576 0 0 0 6984 14 0 0 25 0 1 0 421497568 20525056 4554 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5011 4554 603 41 0 4970 0
vsize: 20044
[startup+80.0057 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 5107 0 0 0 7982 16 0 0 25 0 1 0 421497568 22736896 5085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5551 5085 603 41 0 5510 0
vsize: 22204
[startup+90.0054 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 5107 0 0 0 8982 16 0 0 25 0 1 0 421497568 22736896 5085 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5551 5085 603 41 0 5510 0
vsize: 22204
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 5107 0 0 0 9982 16 0 0 25 0 1 0 421497568 22736896 5085 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5551 5085 603 41 0 5510 0
vsize: 22204
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 5777 0 0 0 10981 18 0 0 25 0 1 0 421497568 25534464 5755 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5755 603 41 0 6193 0
vsize: 24936
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 6332 0 0 0 11979 19 0 0 25 0 1 0 421497568 27820032 6310 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6792 6310 603 41 0 6751 0
vsize: 27168
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 6522 0 0 0 12979 20 0 0 25 0 1 0 421497568 28495872 6500 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6957 6500 603 41 0 6916 0
vsize: 27828
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 6522 0 0 0 13979 20 0 0 25 0 1 0 421497568 28495872 6500 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6957 6500 603 41 0 6916 0
vsize: 27828
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 6522 0 0 0 14980 20 0 0 25 0 1 0 421497568 28495872 6500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6957 6500 603 41 0 6916 0
vsize: 27828
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 6522 0 0 0 15980 20 0 0 25 0 1 0 421497568 28495872 6500 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6957 6500 603 41 0 6916 0
vsize: 27828
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 6872 0 0 0 16979 21 0 0 25 0 1 0 421497568 29974528 6850 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7318 6850 603 41 0 7277 0
vsize: 29272
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 7517 0 0 0 17977 23 0 0 25 0 1 0 421497568 32653312 7495 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7972 7495 603 41 0 7931 0
vsize: 31888
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17032
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 7926 0 0 0 18976 24 0 0 25 0 1 0 421497568 34271232 7904 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8367 7904 603 41 0 8326 0
vsize: 33468
[startup+200.013 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 8346 0 0 0 19974 26 0 0 25 0 1 0 421497568 36007936 8324 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8791 8324 603 41 0 8750 0
vsize: 35164
[startup+210.012 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 8912 0 0 0 20973 28 0 0 25 0 1 0 421497568 38547456 8890 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9411 8890 603 41 0 9370 0
vsize: 37644
[startup+220.014 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 9345 0 0 0 21971 29 0 0 25 0 1 0 421497568 40431616 9323 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9871 9323 603 41 0 9830 0
vsize: 39484
[startup+230.014 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 9691 0 0 0 22970 30 0 0 25 0 1 0 421497568 41766912 9669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10197 9669 603 41 0 10156 0
vsize: 40788
[startup+240.014 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 10029 0 0 0 23969 32 0 0 25 0 1 0 421497568 43106304 10007 4294967295 134512640 134672761 3221224560 3221223732 134559060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10524 10007 603 41 0 10483 0
vsize: 42096
[startup+250.014 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 10326 0 0 0 24968 33 0 0 25 0 1 0 421497568 44310528 10304 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10818 10304 603 41 0 10777 0
vsize: 43272
[startup+260.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 17085
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 10617 0 0 0 25967 34 0 0 25 0 1 0 421497568 45514752 10595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11112 10595 603 41 0 11071 0
vsize: 44448
[startup+270.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 10861 0 0 0 26965 36 0 0 25 0 1 0 421497568 46571520 10839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11370 10839 603 41 0 11329 0
vsize: 45480
[startup+280.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 11097 0 0 0 27964 38 0 0 25 0 1 0 421497568 47505408 11075 4294967295 134512640 134672761 3221224560 3221223728 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11598 11075 603 41 0 11557 0
vsize: 46392
[startup+290.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 11320 0 0 0 28963 39 0 0 25 0 1 0 421497568 48435200 11298 4294967295 134512640 134672761 3221224560 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11825 11298 603 41 0 11784 0
vsize: 47300
[startup+300.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 11592 0 0 0 29962 40 0 0 25 0 1 0 421497568 49504256 11570 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12086 11570 603 41 0 12045 0
vsize: 48344
[startup+310.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 11855 0 0 0 30961 41 0 0 25 0 1 0 421497568 50569216 11833 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12346 11833 603 41 0 12305 0
vsize: 49384
[startup+320.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 12084 0 0 0 31960 43 0 0 25 0 1 0 421497568 51486720 12062 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12570 12062 603 41 0 12529 0
vsize: 50280
[startup+330.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 12296 0 0 0 32959 43 0 0 25 0 1 0 421497568 52277248 12274 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12763 12274 603 41 0 12722 0
vsize: 51052
[startup+340.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 12522 0 0 0 33959 44 0 0 25 0 1 0 421497568 53223424 12500 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12994 12500 603 41 0 12953 0
vsize: 51976
[startup+350.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 12885 0 0 0 34957 46 0 0 25 0 1 0 421497568 54706176 12863 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13356 12863 603 41 0 13315 0
vsize: 53424
[startup+360.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 13356 0 0 0 35956 47 0 0 25 0 1 0 421497568 56729600 13334 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+370.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 13789 0 0 0 36955 48 0 0 25 0 1 0 421497568 58474496 13767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14276 13767 603 41 0 14235 0
vsize: 57104
[startup+380.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 14225 0 0 0 37954 50 0 0 25 0 1 0 421497568 60211200 14203 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 14203 603 41 0 14659 0
vsize: 58800
[startup+390.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 14579 0 0 0 38953 51 0 0 25 0 1 0 421497568 61685760 14557 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15060 14557 603 41 0 15019 0
vsize: 60240
[startup+400.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 15069 0 0 0 39951 53 0 0 25 0 1 0 421497568 63688704 15047 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15549 15047 603 41 0 15508 0
vsize: 62196
[startup+410.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 15497 0 0 0 40950 54 0 0 25 0 1 0 421497568 65429504 15475 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15974 15475 603 41 0 15933 0
vsize: 63896
[startup+420.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 15915 0 0 0 41948 56 0 0 25 0 1 0 421497568 67158016 15893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16396 15893 603 41 0 16355 0
vsize: 65584
[startup+430.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16340 0 0 0 42947 58 0 0 25 0 1 0 421497568 68771840 16318 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16790 16318 603 41 0 16749 0
vsize: 67160
[startup+440.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16726 0 0 0 43946 59 0 0 25 0 1 0 421497568 70402048 16704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17188 16704 603 41 0 17147 0
vsize: 68752
[startup+450.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 44945 60 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223696 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+460.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 45945 60 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+470.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 46945 60 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+480.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 47945 61 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+490.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 48945 61 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223744 134558853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+500.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17087
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 49944 62 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+510.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 50944 62 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+520.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 51944 62 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+530.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16828 0 0 0 52944 63 0 0 25 0 1 0 421497568 70799360 16806 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16806 603 41 0 17244 0
vsize: 69140
[startup+540.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 53944 63 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+550.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 54944 63 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+560.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 55943 64 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+570.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 56943 64 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+580.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 57943 64 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+590.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 58943 64 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+600.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 59943 65 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+610.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 60943 65 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+620.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 16829 0 0 0 61943 65 0 0 25 0 1 0 421497568 70799360 16807 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17285 16807 603 41 0 17244 0
vsize: 69140
[startup+630.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 17108 0 0 0 62941 68 0 0 25 0 1 0 421497568 72007680 17086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17580 17086 603 41 0 17539 0
vsize: 70320
[startup+640.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 17429 0 0 0 63940 69 0 0 25 0 1 0 421497568 73363456 17407 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17911 17407 603 41 0 17870 0
vsize: 71644
[startup+650.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 17766 0 0 0 64938 70 0 0 25 0 1 0 421497568 74711040 17744 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18240 17744 603 41 0 18199 0
vsize: 72960
[startup+660.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 18126 0 0 0 65937 72 0 0 25 0 1 0 421497568 76181504 18104 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18599 18104 603 41 0 18558 0
vsize: 74396
[startup+670.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 18500 0 0 0 66935 74 0 0 25 0 1 0 421497568 77651968 18478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18958 18478 603 41 0 18917 0
vsize: 75832
[startup+680.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 18898 0 0 0 67934 75 0 0 25 0 1 0 421497568 79384576 18876 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19381 18876 603 41 0 19340 0
vsize: 77524
[startup+690.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 19269 0 0 0 68933 77 0 0 25 0 1 0 421497568 80859136 19247 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19741 19247 603 41 0 19700 0
vsize: 78964
[startup+700.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 19616 0 0 0 69931 78 0 0 25 0 1 0 421497568 82329600 19594 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20100 19594 603 41 0 20059 0
vsize: 80400
[startup+710.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 19957 0 0 0 70930 79 0 0 25 0 1 0 421497568 83668992 19935 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20427 19935 603 41 0 20386 0
vsize: 81708
[startup+720.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 20251 0 0 0 71929 80 0 0 25 0 1 0 421497568 84873216 20229 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20721 20229 603 41 0 20680 0
vsize: 82884
[startup+730.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 20512 0 0 0 72929 81 0 0 25 0 1 0 421497568 85954560 20490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20985 20490 603 41 0 20944 0
vsize: 83940
[startup+740.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 20801 0 0 0 73928 82 0 0 25 0 1 0 421497568 87154688 20779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21278 20779 603 41 0 21237 0
vsize: 85112
[startup+750.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 21016 0 0 0 74927 83 0 0 25 0 1 0 421497568 88096768 20994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21508 20994 603 41 0 21467 0
vsize: 86032
[startup+760.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 21209 0 0 0 75926 85 0 0 25 0 1 0 421497568 88772608 21187 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21673 21187 603 41 0 21632 0
vsize: 86692
[startup+770.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 21507 0 0 0 76925 86 0 0 25 0 1 0 421497568 90103808 21485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21998 21485 603 41 0 21957 0
vsize: 87992
[startup+780.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 21868 0 0 0 77923 88 0 0 25 0 1 0 421497568 91566080 21846 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22355 21846 603 41 0 22314 0
vsize: 89420
[startup+790.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 22246 0 0 0 78921 90 0 0 25 0 1 0 421497568 93036544 22224 4294967295 134512640 134672761 3221224560 3221223664 134560139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22714 22225 603 41 0 22673 0
vsize: 90856
[startup+800.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 22634 0 0 0 79920 91 0 0 25 0 1 0 421497568 94646272 22612 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23107 22612 603 41 0 23066 0
vsize: 92428
[startup+810.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 22959 0 0 0 80919 92 0 0 25 0 1 0 421497568 95977472 22937 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23432 22937 603 41 0 23391 0
vsize: 93728
[startup+820.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 23192 0 0 0 81919 93 0 0 25 0 1 0 421497568 97046528 23170 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23693 23170 603 41 0 23652 0
vsize: 94772
[startup+830.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 23471 0 0 0 82917 95 0 0 25 0 1 0 421497568 98115584 23449 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23954 23449 603 41 0 23913 0
vsize: 95816
[startup+840.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 23821 0 0 0 83916 96 0 0 25 0 1 0 421497568 99590144 23799 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24314 23799 603 41 0 24273 0
vsize: 97256
[startup+850.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 24150 0 0 0 84916 97 0 0 25 0 1 0 421497568 100925440 24128 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24640 24128 603 41 0 24599 0
vsize: 98560
[startup+860.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 24452 0 0 0 85915 98 0 0 25 0 1 0 421497568 102653952 24430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25062 24430 603 41 0 25021 0
vsize: 100248
[startup+870.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 24664 0 0 0 86914 99 0 0 25 0 1 0 421497568 103460864 24642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25259 24642 603 41 0 25218 0
vsize: 101036
[startup+880.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 24923 0 0 0 87914 99 0 0 25 0 1 0 421497568 104521728 24901 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25518 24901 603 41 0 25477 0
vsize: 102072
[startup+890.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 25234 0 0 0 88913 100 0 0 25 0 1 0 421497568 105865216 25212 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25846 25212 603 41 0 25805 0
vsize: 103384
[startup+900.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 25464 0 0 0 89912 102 0 0 25 0 1 0 421497568 106795008 25442 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26073 25442 603 41 0 26032 0
vsize: 104292
[startup+910.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 25754 0 0 0 90911 103 0 0 25 0 1 0 421497568 108007424 25732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26369 25732 603 41 0 26328 0
vsize: 105476
[startup+920.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 26166 0 0 0 91909 105 0 0 25 0 1 0 421497568 109625344 26144 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26764 26144 603 41 0 26723 0
vsize: 107056
[startup+930.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 26586 0 0 0 92908 106 0 0 25 0 1 0 421497568 111345664 26564 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27184 26564 603 41 0 27143 0
vsize: 108736
[startup+940.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 26970 0 0 0 93907 107 0 0 25 0 1 0 421497568 112926720 26948 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27570 26948 603 41 0 27529 0
vsize: 110280
[startup+950.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 27361 0 0 0 94905 109 0 0 25 0 1 0 421497568 114520064 27339 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27959 27339 603 41 0 27918 0
vsize: 111836
[startup+960.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 27676 0 0 0 95904 110 0 0 25 0 1 0 421497568 115736576 27654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28256 27654 603 41 0 28215 0
vsize: 113024
[startup+970.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 27995 0 0 0 96903 111 0 0 25 0 1 0 421497568 117071872 27973 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28582 27973 603 41 0 28541 0
vsize: 114328
[startup+980.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28290 0 0 0 97903 112 0 0 25 0 1 0 421497568 118263808 28268 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28873 28268 603 41 0 28832 0
vsize: 115492
[startup+990.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 98902 113 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 99902 113 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 100902 113 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 101902 114 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 102902 114 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 103902 114 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 104901 115 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 105901 115 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 106901 115 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 107901 116 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 108901 116 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 109901 116 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 110901 116 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 111900 117 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 112900 117 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 113900 118 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 114900 118 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 115900 118 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 116899 119 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 117899 119 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223664 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 118899 119 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 17089
Raw data (stat): 17032 (minisat+) R 17031 10720 10719 0 -1 0 28436 0 0 0 119899 119 0 0 25 0 1 0 421497568 118935552 28414 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 28414 603 41 0 28996 0
vsize: 116148
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 17089
Raw data (stat): 17032 (minisat+) Z 17031 10720 10719 0 -1 12 28439 0 0 0 119900 124 0 0 25 0 1 0 421497568 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.25
CPU user time (s): 1199
CPU system time (s): 1.24981
CPU usage (%): 100.013
Max. virtual memory (Kb): 116148
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####