PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        892912 kB
Buffers:         34928 kB
Cached:          84792 kB
SwapCached:       2272 kB
Active:          56908 kB
Inactive:        67956 kB
HighTotal:      131008 kB
HighFree:        42308 kB
LowTotal:       903652 kB
LowFree:        850604 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11292 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:16:41 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4474 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80035 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80035   160070 |   26678       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  147951   319392 |   49317       0        0     nan |  0.000 % |
c |       100 |  147312   318040 |   54248      57     1282    22.5 |  0.772 % |
c |       251 |  146773   316900 |   59673     187     2917    15.6 |  1.422 % |
c |       476 |  145213   313544 |   65640     368     5352    14.5 |  3.429 % |
c |       813 |  143505   309796 |   72205     621     8354    13.5 |  5.644 % |
c |      1320 |  139677   301273 |   79425    1008    13306    13.2 | 10.638 % |
c |      2079 |  135693   292365 |   87368    1543    19391    12.6 | 15.964 % |
c |      3218 |  129784   278974 |   96104    2359    29829    12.6 | 24.035 % |
c |      4926 |  122432   262085 |  105715    3616    48944    13.5 | 34.279 % |
c |      7488 |  111938   237654 |  116286    5258    69109    13.1 | 49.006 % |
c |     11332 |  101310   212553 |  127915    7785   111547    14.3 | 64.438 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14084 |   96816   201835 |   32272    9412   143299    15.2 | 64.438 % |
c |     14184 |   96772   201727 |   35499    9499   144028    15.2 | 71.052 % |
c |     14334 |   96570   201231 |   39049    9550   144833    15.2 | 71.359 % |
c |     14560 |   96295   200569 |   42954    9703   147277    15.2 | 71.772 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14788 |   96036   200007 |   32012    9819   147145    15.0 | 71.772 % |
c |     14888 |   96036   200007 |   35213    9919   148330    15.0 | 72.243 % |
c |     15038 |   96036   200007 |   38734   10069   149721    14.9 | 72.243 % |
c |     15263 |   96036   200007 |   42607   10294   154570    15.0 | 72.243 % |
c |     15600 |   95761   199378 |   46868   10569   160536    15.2 | 72.625 % |
c |     16106 |   95153   197892 |   51555   10886   169202    15.5 | 73.553 % |
c |     16865 |   94758   196946 |   56711   11525   181628    15.8 | 74.144 % |
c |     18004 |   94310   195868 |   62382   12430   205545    16.5 | 74.813 % |
c |     19713 |   94001   195126 |   68620   13894   265668    19.1 | 75.275 % |
c |     22276 |   92381   191245 |   75482   15687   319719    20.4 | 77.691 % |
c |     26120 |   91522   189173 |   83030   19074   495885    26.0 | 78.980 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27853 |   91077   188149 |   30359   20461   588458    28.8 | 78.980 % |
c |     27953 |   91077   188149 |   33394   20561   590686    28.7 | 79.629 % |
c |     28103 |   91026   188021 |   36734   20631   592469    28.7 | 79.706 % |
c |     28328 |   91026   188021 |   40407   20856   599678    28.8 | 79.706 % |
c |     28665 |   91026   188021 |   44448   21193   622260    29.4 | 79.706 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28969 |   90731   187263 |   30243   21322   628608    29.5 | 79.706 % |
c |     29069 |   90722   187240 |   33267   21414   632006    29.5 | 80.173 % |
c |     29219 |   90593   186934 |   36594   21396   633325    29.6 | 80.358 % |
c |     29445 |   90536   186795 |   40253   21617   652375    30.2 | 80.447 % |
c |     29782 |   90499   186706 |   44278   21904   668251    30.5 | 80.503 % |
c |     30289 |   90299   186216 |   48706   22108   682253    30.9 | 80.809 % |
c |     31048 |   90231   186060 |   53577   22782   711877    31.2 | 80.904 % |
c |     32187 |   89778   184940 |   58935   23599   766824    32.5 | 81.598 % |
c |     33896 |   89773   184929 |   64828   25280   869667    34.4 | 81.605 % |
c |     36458 |   89601   184511 |   71311   27781  1104154    39.7 | 81.868 % |
c |     40303 |   89001   183057 |   78442   30883  1452224    47.0 | 82.782 % |
c |     46069 |   88653   182193 |   86286   36261  1909440    52.7 | 83.326 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53577 |   88651   182222 |   29550   43705  2561808    58.6 | 83.326 % |
c |     53677 |   88651   182222 |   32505   43805  2563789    58.5 | 83.359 % |
c |     53827 |   88622   182151 |   35755   43811  2568576    58.6 | 83.404 % |
c |     54052 |   88622   182151 |   39331   44036  2589935    58.8 | 83.404 % |
c |     54389 |   88537   181938 |   43264   44316  2602581    58.7 | 83.542 % |
c |     54895 |   88502   181851 |   47590   44743  2640960    59.0 | 83.598 % |
c |     55654 |   88489   181818 |   52349   45410  2688658    59.2 | 83.620 % |
c |     56795 |   88255   181245 |   57584   46245  2798146    60.5 | 83.970 % |
c |     58504 |   88255   181245 |   63343   47954  2931810    61.1 | 83.970 % |
c |     61066 |   88117   180910 |   69677   50021  3189748    63.8 | 84.181 % |
c |     64910 |   88088   180842 |   76645   53834  3616238    67.2 | 84.220 % |
c |     70676 |   88083   180831 |   84309   59598  4123646    69.2 | 84.226 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76602 |   87920   180446 |   29306   64994  4731142    72.8 | 84.226 % |
c |     76704 |   87920   180446 |   32236   65096  4739491    72.8 | 84.488 % |
c |     76855 |   87920   180446 |   35460   65247  4745429    72.7 | 84.488 % |
c |     77080 |   87920   180446 |   39006   65472  4759519    72.7 | 84.488 % |
c |     77417 |   87920   180446 |   42906   65809  4783089    72.7 | 84.488 % |
c |     77924 |   87920   180446 |   47197   66316  4834519    72.9 | 84.488 % |
c |     78684 |   87915   180435 |   51917   67073  4915209    73.3 | 84.494 % |
c |     79823 |   87782   180128 |   57109   67701  5020176    74.2 | 84.681 % |
c |     81531 |   87629   179763 |   62820   69363  5207979    75.1 | 84.907 % |
c |     84093 |   87629   179763 |   69102   71925  5462668    75.9 | 84.907 % |
c |     87937 |   87629   179763 |   76012   75769  5852613    77.2 | 84.907 % |
c |     93703 |   87615   179727 |   83613   81487  6335995    77.8 | 84.931 % |
c |    102352 |   87615   179727 |   91974   90136  7289858    80.9 | 84.931 % |
c |    115328 |   87613   179723 |  101172  103111  8798918    85.3 | 84.933 % |
c |    134790 |   87540   179550 |  111289  122522 11000809    89.8 | 85.040 % |
c |    163982 |   87270   178893 |  122418  150898 14231492    94.3 | 85.455 % |
c |    207771 |   87197   178706 |  134660   54694  5876777   107.4 | 85.578 % |
c |    273455 |   87182   178671 |  148126  120376 10322069    85.7 | 85.599 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 C946 -C945 -C944 -C943 -C942 -C941 C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 28950
Raw data (stat): 28950 (runsolver) R 28949 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422940631 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4907 0 0 0 984 14 0 0 25 0 1 0 422940631 23158784 4885 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5654 4885 603 41 0 5613 0
vsize: 22616
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4916 0 0 0 1984 14 0 0 25 0 1 0 422940631 23158784 4894 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5654 4894 603 41 0 5613 0
vsize: 22616
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4927 0 0 0 2983 14 0 0 25 0 1 0 422940631 23293952 4905 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5687 4905 603 41 0 5646 0
vsize: 22748
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4938 0 0 0 3983 14 0 0 25 0 1 0 422940631 23293952 4916 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5687 4916 603 41 0 5646 0
vsize: 22748
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4953 0 0 0 4983 14 0 0 25 0 1 0 422940631 23433216 4931 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5721 4931 603 41 0 5680 0
vsize: 22884
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4959 0 0 0 5983 14 0 0 25 0 1 0 422940631 23433216 4937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5721 4937 603 41 0 5680 0
vsize: 22884
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 4975 0 0 0 6984 14 0 0 25 0 1 0 422940631 23433216 4953 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5721 4953 603 41 0 5680 0
vsize: 22884
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 5008 0 0 0 7984 15 0 0 25 0 1 0 422940631 23568384 4986 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5754 4986 603 41 0 5713 0
vsize: 23016
[startup+90.0025 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 5153 0 0 0 8984 15 0 0 25 0 1 0 422940631 24498176 5131 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5981 5131 603 41 0 5940 0
vsize: 23924
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 5269 0 0 0 9983 15 0 0 25 0 1 0 422940631 25034752 5247 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6112 5247 603 41 0 6071 0
vsize: 24448
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 5611 0 0 0 10982 16 0 0 25 0 1 0 422940631 26435584 5589 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6454 5589 603 41 0 6413 0
vsize: 25816
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 5895 0 0 0 11980 18 0 0 25 0 1 0 422940631 27598848 5873 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6738 5873 603 41 0 6697 0
vsize: 26952
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 6473 0 0 0 12979 20 0 0 25 0 1 0 422940631 30007296 6451 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7326 6451 603 41 0 7285 0
vsize: 29304
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 6871 0 0 0 13977 21 0 0 25 0 1 0 422940631 31735808 6849 4294967295 134512640 134672761 3221224560 3221223664 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7748 6849 603 41 0 7707 0
vsize: 30992
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 7259 0 0 0 14975 22 0 0 25 0 1 0 422940631 33218560 7237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8110 7237 603 41 0 8069 0
vsize: 32440
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 7764 0 0 0 15974 24 0 0 25 0 1 0 422940631 35246080 7742 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8605 7742 603 41 0 8564 0
vsize: 34420
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 8022 0 0 0 16973 25 0 0 25 0 1 0 422940631 36323328 8000 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8868 8000 603 41 0 8827 0
vsize: 35472
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 8466 0 0 0 17972 26 0 0 25 0 1 0 422940631 38187008 8444 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9323 8444 603 41 0 9282 0
vsize: 37292
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 8941 0 0 0 18970 28 0 0 25 0 1 0 422940631 40062976 8919 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9781 8919 603 41 0 9740 0
vsize: 39124
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28950
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 9329 0 0 0 19970 29 0 0 25 0 1 0 422940631 41680896 9307 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10176 9307 603 41 0 10135 0
vsize: 40704
[startup+210.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 28997
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 9763 0 0 0 20967 31 0 0 25 0 1 0 422940631 43429888 9741 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10603 9741 603 41 0 10562 0
vsize: 42412
[startup+220.014 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 29003
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 10053 0 0 0 21966 33 0 0 25 0 1 0 422940631 44642304 10031 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10899 10031 603 41 0 10858 0
vsize: 43596
[startup+230.013 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 29003
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 10387 0 0 0 22965 34 0 0 25 0 1 0 422940631 46235648 10365 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11288 10365 603 41 0 11247 0
vsize: 45152
[startup+240.013 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 29003
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 10685 0 0 0 23964 35 0 0 25 0 1 0 422940631 47443968 10663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11583 10663 603 41 0 11542 0
vsize: 46332
[startup+250.013 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 29003
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 11025 0 0 0 24963 36 0 0 25 0 1 0 422940631 48787456 11003 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11911 11003 603 41 0 11870 0
vsize: 47644
[startup+260.013 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 29003
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 11334 0 0 0 25962 37 0 0 25 0 1 0 422940631 50118656 11312 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12236 11312 603 41 0 12195 0
vsize: 48944
[startup+270.013 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 29003
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 11607 0 0 0 26961 38 0 0 25 0 1 0 422940631 51187712 11585 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12497 11585 603 41 0 12456 0
vsize: 49988
[startup+280.013 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 11927 0 0 0 27959 40 0 0 25 0 1 0 422940631 52518912 11905 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12822 11905 603 41 0 12781 0
vsize: 51288
[startup+290.013 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 12211 0 0 0 28958 41 0 0 25 0 1 0 422940631 53596160 12189 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13085 12189 603 41 0 13044 0
vsize: 52340
[startup+300.013 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 12525 0 0 0 29958 42 0 0 25 0 1 0 422940631 54923264 12503 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13409 12503 603 41 0 13368 0
vsize: 53636
[startup+310.012 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 12918 0 0 0 30957 43 0 0 25 0 1 0 422940631 56508416 12896 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13796 12896 603 41 0 13755 0
vsize: 55184
[startup+320.013 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 13237 0 0 0 31956 45 0 0 25 0 1 0 422940631 57847808 13215 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14123 13215 603 41 0 14082 0
vsize: 56492
[startup+330.013 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 13599 0 0 0 32954 46 0 0 25 0 1 0 422940631 59310080 13577 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14480 13577 603 41 0 14439 0
vsize: 57920
[startup+340.012 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 13925 0 0 0 33953 48 0 0 25 0 1 0 422940631 60641280 13903 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14805 13903 603 41 0 14764 0
vsize: 59220
[startup+350.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 14207 0 0 0 34952 49 0 0 25 0 1 0 422940631 61698048 14185 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15063 14185 603 41 0 15022 0
vsize: 60252
[startup+360.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 14492 0 0 0 35951 49 0 0 25 0 1 0 422940631 62889984 14470 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15354 14470 603 41 0 15313 0
vsize: 61416
[startup+370.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 14732 0 0 0 36951 50 0 0 25 0 1 0 422940631 63823872 14710 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15582 14710 603 41 0 15541 0
vsize: 62328
[startup+380.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 15044 0 0 0 37950 51 0 0 25 0 1 0 422940631 65163264 15022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15909 15022 603 41 0 15868 0
vsize: 63636
[startup+390.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 15302 0 0 0 38950 52 0 0 25 0 1 0 422940631 66236416 15280 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16171 15280 603 41 0 16130 0
vsize: 64684
[startup+400.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 15631 0 0 0 39949 53 0 0 25 0 1 0 422940631 67567616 15609 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16496 15609 603 41 0 16455 0
vsize: 65984
[startup+410.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 15946 0 0 0 40948 54 0 0 25 0 1 0 422940631 68763648 15924 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16788 15924 603 41 0 16747 0
vsize: 67152
[startup+420.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 16228 0 0 0 41947 55 0 0 25 0 1 0 422940631 69959680 16206 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17080 16206 603 41 0 17039 0
vsize: 68320
[startup+430.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 16465 0 0 0 42947 55 0 0 25 0 1 0 422940631 70881280 16443 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17305 16443 603 41 0 17264 0
vsize: 69220
[startup+440.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 16719 0 0 0 43946 56 0 0 25 0 1 0 422940631 71946240 16697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 16697 603 41 0 17524 0
vsize: 70260
[startup+450.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 16954 0 0 0 44945 57 0 0 25 0 1 0 422940631 72880128 16932 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17793 16932 603 41 0 17752 0
vsize: 71172
[startup+460.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 17220 0 0 0 45945 58 0 0 25 0 1 0 422940631 73957376 17198 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18056 17198 603 41 0 18015 0
vsize: 72224
[startup+470.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 17405 0 0 0 46944 59 0 0 25 0 1 0 422940631 74760192 17383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18252 17383 603 41 0 18211 0
vsize: 73008
[startup+480.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 17566 0 0 0 47943 60 0 0 25 0 1 0 422940631 75436032 17544 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18417 17544 603 41 0 18376 0
vsize: 73668
[startup+490.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 17818 0 0 0 48943 61 0 0 25 0 1 0 422940631 76365824 17796 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18644 17796 603 41 0 18603 0
vsize: 74576
[startup+500.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 18167 0 0 0 49942 62 0 0 25 0 1 0 422940631 78352384 18145 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19129 18145 603 41 0 19088 0
vsize: 76516
[startup+510.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 18450 0 0 0 50941 62 0 0 25 0 1 0 422940631 79429632 18428 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19392 18428 603 41 0 19351 0
vsize: 77568
[startup+520.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 18742 0 0 0 51941 63 0 0 25 0 1 0 422940631 80633856 18720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19686 18720 603 41 0 19645 0
vsize: 78744
[startup+530.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29005
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 19025 0 0 0 52940 64 0 0 25 0 1 0 422940631 81842176 19003 4294967295 134512640 134672761 3221224560 3221223684 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19981 19003 603 41 0 19940 0
vsize: 79924
[startup+540.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 19312 0 0 0 53940 65 0 0 25 0 1 0 422940631 83030016 19290 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20271 19290 603 41 0 20230 0
vsize: 81084
[startup+550.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 19589 0 0 0 54939 65 0 0 25 0 1 0 422940631 84094976 19567 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20531 19567 603 41 0 20490 0
vsize: 82124
[startup+560.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 19780 0 0 0 55938 66 0 0 25 0 1 0 422940631 84893696 19758 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20726 19758 603 41 0 20685 0
vsize: 82904
[startup+570.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 19920 0 0 0 56938 66 0 0 25 0 1 0 422940631 85426176 19898 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20856 19898 603 41 0 20815 0
vsize: 83424
[startup+580.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 20117 0 0 0 57938 67 0 0 25 0 1 0 422940631 86224896 20095 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21051 20095 603 41 0 21010 0
vsize: 84204
[startup+590.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 20328 0 0 0 58938 68 0 0 25 0 1 0 422940631 87171072 20306 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21282 20306 603 41 0 21241 0
vsize: 85128
[startup+600.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 20516 0 0 0 59937 68 0 0 25 0 1 0 422940631 87977984 20494 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21479 20494 603 41 0 21438 0
vsize: 85916
[startup+610.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 20722 0 0 0 60936 69 0 0 25 0 1 0 422940631 88780800 20700 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21675 20700 603 41 0 21634 0
vsize: 86700
[startup+620.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 20935 0 0 0 61936 69 0 0 25 0 1 0 422940631 89591808 20913 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21873 20913 603 41 0 21832 0
vsize: 87492
[startup+630.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 21130 0 0 0 62935 70 0 0 25 0 1 0 422940631 90402816 21108 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22071 21108 603 41 0 22030 0
vsize: 88284
[startup+640.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 21357 0 0 0 63935 71 0 0 25 0 1 0 422940631 91332608 21335 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22298 21335 603 41 0 22257 0
vsize: 89192
[startup+650.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 21629 0 0 0 64934 71 0 0 25 0 1 0 422940631 92401664 21607 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22559 21607 603 41 0 22518 0
vsize: 90236
[startup+660.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 21897 0 0 0 65934 72 0 0 25 0 1 0 422940631 93466624 21875 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22819 21875 603 41 0 22778 0
vsize: 91276
[startup+670.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22152 0 0 0 66934 72 0 0 25 0 1 0 422940631 94523392 22130 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23077 22130 603 41 0 23036 0
vsize: 92308
[startup+680.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 67934 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+690.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 68934 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223824 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+700.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 69934 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+710.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 70934 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+720.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 71934 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+730.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 72935 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+740.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 73935 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+750.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 74935 72 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+760.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 75935 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+770.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 76934 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+780.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 77935 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+790.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 78935 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+800.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 79935 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+810.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 80935 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223744 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+820.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 81935 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+830.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 82936 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+840.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 83936 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+850.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 84936 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+860.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 85936 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+870.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 86936 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+880.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 87937 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+890.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 88937 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+900.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 89937 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+910.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 90937 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+920.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 91937 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+930.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 92937 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+940.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 93938 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+950.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 94938 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+960.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 95938 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+970.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 96938 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+980.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 97938 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+990.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 98939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 99939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.98 0.91 3/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 100939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 101939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 102939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 103939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 104940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 105940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 106940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 107939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 108939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 109938 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 110939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 111939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 112939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 113939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 114939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 115939 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 116940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 117940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223736 134559059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 118940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 29007
Raw data (stat): 28950 (minisat+) R 28949 24215 24214 0 -1 0 22165 0 0 0 119940 73 0 0 25 0 1 0 422940631 94654464 22143 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22143 603 41 0 23068 0
vsize: 92436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 29007
Raw data (stat): 28950 (minisat+) Z 28949 24215 24214 0 -1 12 22168 0 0 0 119940 77 0 0 25 0 1 0 422940631 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.19
CPU user time (s): 1199.41
CPU system time (s): 0.776881
CPU usage (%): 100.01
Max. virtual memory (Kb): 92436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####