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-2.opb
MD5SUM	fe7ff8b16c276b409b25a87eed31b6f9
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-38
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.09
Number of variables	1150
Total number of constraints	80851
Number of constraints which are clauses	80851
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 5252

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        894232 kB
Buffers:         34460 kB
Cached:          69576 kB
SwapCached:          4 kB
Active:          52696 kB
Inactive:        54240 kB
HighTotal:      131008 kB
HighFree:        57792 kB
LowTotal:       903652 kB
LowFree:        836440 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            28004 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:17:02 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3719 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80851 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 |   80851   161702 |   26950       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2272   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   96575   217899 |   32191       0        0     nan |  0.000 % |
c |       100 |   96530   217744 |   35410      86      912    10.6 |  0.235 % |
c |       250 |   96530   217744 |   38951     236     2369    10.0 |  0.236 % |
c |       475 |   96530   217744 |   42846     461     4424     9.6 |  0.235 % |
c |       812 |   96476   217558 |   47130     784     7600     9.7 |  0.411 % |
c |      1318 |   96461   217507 |   51843    1288    14536    11.3 |  0.469 % |
c |      2077 |   96416   217352 |   57028    2036    23818    11.7 |  0.616 % |
c |      3216 |   96347   217115 |   62731    3155    38834    12.3 |  0.850 % |
c |      4924 |   96146   216424 |   69004    4797    61651    12.9 |  1.527 % |
c |      7486 |   95626   214640 |   75904    7200   114230    15.9 |  3.519 % |
c |     11331 |   94492   210746 |   83495   10714   195145    18.2 |  8.094 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12595 |   94292   210066 |   31430   11914   288772    24.2 |  8.094 % |
c |     12695 |   94292   210066 |   34573   12014   290230    24.2 |  9.030 % |
c |     12845 |   94261   209961 |   38030   12155   292497    24.1 |  9.176 % |
c |     13070 |   94143   209557 |   41833   12333   298017    24.2 |  9.763 % |
c |     13407 |   93983   209003 |   46016   12624   305353    24.2 | 10.554 % |
c |     13913 |   93701   208029 |   50618   13022   316438    24.3 | 11.844 % |
c |     14672 |   93560   207544 |   55680   13691   334609    24.4 | 12.490 % |
c |     15811 |   92887   205223 |   61248   14578   369135    25.3 | 15.919 % |
c |     17520 |   92331   203287 |   67372   16080   427204    26.6 | 18.909 % |
c |     20082 |   92017   202195 |   74110   18385   515070    28.0 | 20.522 % |
c |     23926 |   91683   201043 |   81521   21806   730457    33.5 | 22.222 % |
c |     29692 |   91076   198932 |   89673   26652  1041890    39.1 | 25.332 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35872 |   90899   198324 |   30299   32543  1659153    51.0 | 25.332 % |
c |     35972 |   90878   198253 |   33328   15965   954647    59.8 | 26.407 % |
c |     36122 |   90843   198132 |   36661   16083   959073    59.6 | 26.555 % |
c |     36347 |   90843   198132 |   40327   16308   970015    59.5 | 26.553 % |
c |     36684 |   90799   197980 |   44360   16596   984063    59.3 | 26.729 % |
c |     37192 |   90777   197902 |   48796   17080  1002460    58.7 | 26.848 % |
c |     37951 |   90766   197863 |   53676   17813  1049542    58.9 | 26.906 % |
c |     39090 |   90766   197863 |   59044   18952  1137938    60.0 | 26.905 % |
c |     40799 |   90712   197675 |   64948   20564  1263502    61.4 | 27.169 % |
c |     43361 |   90712   197675 |   71443   23126  1671115    72.3 | 27.169 % |
c |     47206 |   90556   197139 |   78587   26845  1995981    74.4 | 28.019 % |
c |     52972 |   90452   196779 |   86446   32462  2555548    78.7 | 28.546 % |
c |     61621 |   90443   196748 |   95091   41087  3228882    78.6 | 28.576 % |
c |     74596 |   90437   196728 |  104600   54058  5406582   100.0 | 28.606 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81019 |   90400   196603 |   30133   60308  5923549    98.2 | 28.606 % |
c |     81119 |   90400   196603 |   33146   16959  1735968   102.4 | 28.802 % |
c |     81272 |   90400   196603 |   36460   17112  1742298   101.8 | 28.802 % |
c |     81497 |   90400   196603 |   40107   17337  1758374   101.4 | 28.802 % |
c |     81834 |   90400   196603 |   44117   17674  1773405   100.3 | 28.802 % |
c |     82340 |   90394   196583 |   48529   18178  1806222    99.4 | 28.831 % |
c |     83099 |   90310   196297 |   53382   18914  1845740    97.6 | 29.300 % |
c |     84238 |   90310   196297 |   58720   20053  1923995    95.9 | 29.300 % |
c |     85946 |   90287   196218 |   64592   21751  2072819    95.3 | 29.419 % |
c |     88510 |   90287   196218 |   71052   24315  2229531    91.7 | 29.417 % |
c |     92354 |   90262   196131 |   78157   28149  2842855   101.0 | 29.566 % |
c |     98120 |   90157   195766 |   85972   33882  3264321    96.3 | 30.237 % |
c |    106769 |   90157   195766 |   94570   42531  4025877    94.7 | 30.237 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115445 |   90113   195621 |   30037   51200  4941692    96.5 | 30.237 % |
c |    115545 |   90113   195621 |   33040   16931  1211417    71.6 | 30.494 % |
c |    115695 |   90113   195621 |   36344   17081  1224916    71.7 | 30.494 % |
c |    115921 |   90102   195582 |   39979   17299  1243715    71.9 | 30.551 % |
c |    116259 |   90102   195582 |   43977   17637  1253365    71.1 | 30.551 % |
c |    116767 |   90102   195582 |   48374   18145  1282063    70.7 | 30.552 % |
c |    117527 |   90102   195582 |   53212   18905  1322738    70.0 | 30.551 % |
c |    118666 |   90102   195582 |   58533   20044  1440838    71.9 | 30.552 % |
c |    120375 |   90102   195582 |   64386   21753  1585435    72.9 | 30.552 % |
c |    122939 |   90081   195511 |   70825   24306  1893979    77.9 | 30.639 % |
c |    126783 |   90081   195511 |   77908   28150  2316643    82.3 | 30.640 % |
c |    132550 |   90081   195511 |   85699   33917  3324018    98.0 | 30.640 % |
c |    141202 |   90075   195491 |   94268   42565  4397172   103.3 | 30.668 % |
c |    154177 |   90075   195491 |  103695   55540  5805098   104.5 | 30.668 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 41   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    156052 |   90076   195498 |   30025   57415  5968563   104.0 | 30.668 % |
c |    156153 |   90076   195498 |   33027   16879  1322590    78.4 | 30.688 % |
c |    156303 |   90076   195498 |   36330   17029  1333746    78.3 | 30.688 % |
c |    156529 |   90076   195498 |   39963   17255  1342972    77.8 | 30.688 % |
c |    156866 |   90070   195478 |   43959   17589  1359971    77.3 | 30.717 % |
c |    157372 |   90070   195478 |   48355   18095  1381682    76.4 | 30.717 % |
c |    158132 |   90064   195458 |   53191   18851  1428209    75.8 | 30.747 % |
c |    159271 |   90064   195458 |   58510   19990  1518674    76.0 | 30.747 % |
c |    160982 |   90064   195458 |   64361   21701  1715149    79.0 | 30.748 % |
c |    163548 |   90064   195458 |   70797   24267  1955243    80.6 | 30.747 % |
c |    167392 |   90056   195430 |   77877   28107  2278584    81.1 | 30.805 % |
c |    173158 |   90056   195430 |   85664   33873  3075885    90.8 | 30.805 % |
c |    181808 |   90056   195430 |   94231   42523  4867841   114.5 | 30.805 % |
c |    194782 |   90032   195348 |  103654   55490  6214643   112.0 | 30.893 % |
c |    214246 |   90004   195250 |  114019   74906  7834469   104.6 | 31.040 % |
c |    243438 |   90004   195250 |  125421  104098 11772396   113.1 | 31.041 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 42   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    268998 |   90005   195258 |   30001   19242  2538245   131.9 | 31.041 % |
c |    269098 |   90005   195258 |   33001   19342  2542100   131.4 | 31.061 % |
c |    269248 |   90005   195258 |   36301   19492  2545270   130.6 | 31.060 % |
c |    269473 |   89999   195238 |   39931   19713  2555371   129.6 | 31.089 % |
c |    269810 |   89999   195238 |   43924   20050  2569796   128.2 | 31.089 % |
c |    270317 |   89999   195238 |   48316   20557  2583035   125.7 | 31.089 % |
c |    271076 |   89993   195218 |   53148   21312  2614854   122.7 | 31.118 % |
c |    272216 |   89993   195218 |   58463   22452  2690792   119.8 | 31.118 % |
c |    273924 |   89993   195218 |   64309   24160  2842780   117.7 | 31.118 % |
c |    276486 |   89984   195187 |   70740   26706  3006556   112.6 | 31.149 % |
c |    280331 |   89984   195187 |   77814   30551  3388489   110.9 | 31.149 % |
c |    286099 |   89984   195187 |   85596   36319  4006565   110.3 | 31.148 % |
c |    294749 |   89975   195156 |   94155   44968  4911013   109.2 | 31.177 % |
c |    307724 |   89975   195156 |  103571   57943  7097525   122.5 | 31.177 % |
c |    327188 |   89975   195156 |  113928   77407 10294140   133.0 | 31.178 % |
c |    356380 |   89975   195156 |  125321  106599 14224567   133.4 | 31.178 % |
c |    400169 |   89975   195156 |  137853   40814  3001859    73.5 | 31.177 % |
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 15070
Raw data (stat): 15070 (runsolver) R 15069 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479728013 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99966 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 3920 0 0 0 987 11 0 0 25 0 1 0 479728013 17977344 3898 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3898 603 41 0 4348 0
vsize: 17556
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 3920 0 0 0 1987 11 0 0 25 0 1 0 479728013 17977344 3898 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3898 603 41 0 4348 0
vsize: 17556
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 3920 0 0 0 2987 12 0 0 25 0 1 0 479728013 17977344 3898 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3898 603 41 0 4348 0
vsize: 17556
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 3920 0 0 0 3986 12 0 0 25 0 1 0 479728013 17977344 3898 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3898 603 41 0 4348 0
vsize: 17556
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 3920 0 0 0 4986 13 0 0 25 0 1 0 479728013 17977344 3898 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3898 603 41 0 4348 0
vsize: 17556
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 3920 0 0 0 5986 13 0 0 25 0 1 0 479728013 17977344 3898 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3898 603 41 0 4348 0
vsize: 17556
[startup+70.0018 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 4561 0 0 0 6983 16 0 0 25 0 1 0 479728013 20537344 4539 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5014 4539 603 41 0 4973 0
vsize: 20056
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 5153 0 0 0 7981 19 0 0 25 0 1 0 479728013 23093248 5131 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5638 5131 603 41 0 5597 0
vsize: 22552
[startup+90.0025 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 5821 0 0 0 8979 20 0 0 25 0 1 0 479728013 25776128 5799 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6293 5799 603 41 0 6252 0
vsize: 25172
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 6692 0 0 0 9976 23 0 0 25 0 1 0 479728013 29274112 6670 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7147 6670 603 41 0 7106 0
vsize: 28588
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 7426 0 0 0 10973 26 0 0 25 0 1 0 479728013 32354304 7404 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7899 7404 603 41 0 7858 0
vsize: 31596
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 7946 0 0 0 11971 28 0 0 25 0 1 0 479728013 34369536 7924 4294967295 134512640 134672761 3221224560 3221223744 134558880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8391 7924 603 41 0 8350 0
vsize: 33564
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 12971 29 0 0 25 0 1 0 479728013 35512320 8199 4294967295 134512640 134672761 3221224560 3221223744 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8670 8199 603 41 0 8629 0
vsize: 34680
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 13971 29 0 0 25 0 1 0 479728013 35512320 8199 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8670 8199 603 41 0 8629 0
vsize: 34680
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 14970 30 0 0 25 0 1 0 479728013 35512320 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8670 8199 603 41 0 8629 0
vsize: 34680
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 15970 30 0 0 25 0 1 0 479728013 35512320 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8670 8199 603 41 0 8629 0
vsize: 34680
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 16970 30 0 0 25 0 1 0 479728013 35512320 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8670 8199 603 41 0 8629 0
vsize: 34680
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15070
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 17970 30 0 0 25 0 1 0 479728013 35508224 8199 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8669 8199 603 41 0 8628 0
vsize: 34676
[startup+190.004 s]
Raw data (loadavg): 1.15 0.99 0.92 2/54 15123
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 18969 30 0 0 25 0 1 0 479728013 35508224 8199 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 8199 603 41 0 8628 0
vsize: 34676
[startup+200.005 s]
Raw data (loadavg): 1.13 0.99 0.92 2/54 15123
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 19969 30 0 0 25 0 1 0 479728013 35508224 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 8199 603 41 0 8628 0
vsize: 34676
[startup+210.005 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 15123
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 20970 30 0 0 25 0 1 0 479728013 35508224 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 8199 603 41 0 8628 0
vsize: 34676
[startup+220.005 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 15123
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 21970 30 0 0 25 0 1 0 479728013 35508224 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 8199 603 41 0 8628 0
vsize: 34676
[startup+230.006 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 15123
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8221 0 0 0 22970 30 0 0 25 0 1 0 479728013 35508224 8199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 8199 603 41 0 8628 0
vsize: 34676
[startup+240.006 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 15123
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8382 0 0 0 23970 30 0 0 25 0 1 0 479728013 36179968 8360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8833 8360 603 41 0 8792 0
vsize: 35332
[startup+250.006 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8422 0 0 0 24970 30 0 0 25 0 1 0 479728013 36311040 8400 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8400 603 41 0 8824 0
vsize: 35460
[startup+260.006 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8422 0 0 0 25970 30 0 0 25 0 1 0 479728013 36311040 8400 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8400 603 41 0 8824 0
vsize: 35460
[startup+270.007 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8422 0 0 0 26970 30 0 0 25 0 1 0 479728013 36311040 8400 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8400 603 41 0 8824 0
vsize: 35460
[startup+280.008 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8422 0 0 0 27971 30 0 0 25 0 1 0 479728013 36311040 8400 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8400 603 41 0 8824 0
vsize: 35460
[startup+290.007 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8422 0 0 0 28971 30 0 0 25 0 1 0 479728013 36311040 8400 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8400 603 41 0 8824 0
vsize: 35460
[startup+300.008 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8422 0 0 0 29971 30 0 0 25 0 1 0 479728013 36311040 8400 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8400 603 41 0 8824 0
vsize: 35460
[startup+310.008 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8566 0 0 0 30970 31 0 0 25 0 1 0 479728013 36982784 8544 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9029 8544 603 41 0 8988 0
vsize: 36116
[startup+320.009 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 8968 0 0 0 31969 33 0 0 25 0 1 0 479728013 38596608 8946 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9423 8946 603 41 0 9382 0
vsize: 37692
[startup+330.009 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 9317 0 0 0 32968 34 0 0 25 0 1 0 479728013 39944192 9295 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9752 9295 603 41 0 9711 0
vsize: 39008
[startup+340.009 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 9655 0 0 0 33967 35 0 0 25 0 1 0 479728013 41672704 9633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10174 9633 603 41 0 10133 0
vsize: 40696
[startup+350.009 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 9941 0 0 0 34967 36 0 0 25 0 1 0 479728013 42737664 9919 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10434 9919 603 41 0 10393 0
vsize: 41736
[startup+360.009 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 10235 0 0 0 35966 36 0 0 25 0 1 0 479728013 43954176 10213 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10731 10213 603 41 0 10690 0
vsize: 42924
[startup+370.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 10706 0 0 0 36965 37 0 0 25 0 1 0 479728013 45985792 10684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11227 10684 603 41 0 11186 0
vsize: 44908
[startup+380.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 11118 0 0 0 37964 39 0 0 25 0 1 0 479728013 47587328 11096 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11618 11096 603 41 0 11577 0
vsize: 46472
[startup+390.009 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 11462 0 0 0 38964 39 0 0 25 0 1 0 479728013 49053696 11440 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11976 11440 603 41 0 11935 0
vsize: 47904
[startup+400.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 11924 0 0 0 39963 41 0 0 25 0 1 0 479728013 50913280 11902 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12430 11902 603 41 0 12389 0
vsize: 49720
[startup+410.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 12368 0 0 0 40961 42 0 0 25 0 1 0 479728013 52641792 12346 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12852 12346 603 41 0 12811 0
vsize: 51408
[startup+420.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 12807 0 0 0 41960 43 0 0 25 0 1 0 479728013 54505472 12785 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13307 12785 603 41 0 13266 0
vsize: 53228
[startup+430.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 13226 0 0 0 42959 44 0 0 25 0 1 0 479728013 56229888 13204 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13728 13204 603 41 0 13687 0
vsize: 54912
[startup+440.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 13643 0 0 0 43958 46 0 0 25 0 1 0 479728013 57843712 13621 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14122 13621 603 41 0 14081 0
vsize: 56488
[startup+450.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 14034 0 0 0 44957 47 0 0 25 0 1 0 479728013 59445248 14012 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14513 14012 603 41 0 14472 0
vsize: 58052
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 14387 0 0 0 45956 48 0 0 25 0 1 0 479728013 60928000 14365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14365 603 41 0 14834 0
vsize: 59500
[startup+470.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 14709 0 0 0 46956 49 0 0 25 0 1 0 479728013 62271488 14687 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15203 14687 603 41 0 15162 0
vsize: 60812
[startup+480.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 15127 0 0 0 47955 50 0 0 25 0 1 0 479728013 63873024 15105 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15594 15105 603 41 0 15553 0
vsize: 62376
[startup+490.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15125
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 15522 0 0 0 48954 52 0 0 25 0 1 0 479728013 65499136 15500 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15991 15500 603 41 0 15950 0
vsize: 63964
[startup+500.014 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 15861 0 0 0 49953 52 0 0 25 0 1 0 479728013 66957312 15839 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16347 15839 603 41 0 16306 0
vsize: 65388
[startup+510.014 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 16248 0 0 0 50953 53 0 0 25 0 1 0 479728013 68571136 16226 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16741 16226 603 41 0 16700 0
vsize: 66964
[startup+520.015 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 16623 0 0 0 51952 54 0 0 25 0 1 0 479728013 70062080 16601 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17105 16601 603 41 0 17064 0
vsize: 68420
[startup+530.015 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 16985 0 0 0 52951 55 0 0 25 0 1 0 479728013 71528448 16963 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17463 16963 603 41 0 17422 0
vsize: 69852
[startup+540.015 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 17393 0 0 0 53949 57 0 0 25 0 1 0 479728013 73134080 17371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17855 17371 603 41 0 17814 0
vsize: 71420
[startup+550.016 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 17798 0 0 0 54949 58 0 0 25 0 1 0 479728013 74878976 17776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18281 17776 603 41 0 18240 0
vsize: 73124
[startup+560.015 s]
Raw data (loadavg): 1.30 1.07 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18091 0 0 0 55948 59 0 0 25 0 1 0 479728013 76083200 18069 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18575 18069 603 41 0 18534 0
vsize: 74300
[startup+570.016 s]
Raw data (loadavg): 1.25 1.07 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18367 0 0 0 56948 59 0 0 25 0 1 0 479728013 77164544 18345 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18839 18345 603 41 0 18798 0
vsize: 75356
[startup+580.017 s]
Raw data (loadavg): 1.21 1.06 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 57947 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+590.017 s]
Raw data (loadavg): 1.18 1.06 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 58947 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+600.017 s]
Raw data (loadavg): 1.15 1.06 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 59947 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+610.018 s]
Raw data (loadavg): 1.13 1.06 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 60948 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223744 134559665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+620.018 s]
Raw data (loadavg): 1.11 1.05 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 61948 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+630.017 s]
Raw data (loadavg): 1.09 1.05 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 62948 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+640.017 s]
Raw data (loadavg): 1.08 1.05 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 63948 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+650.018 s]
Raw data (loadavg): 1.06 1.05 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 64948 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+660.017 s]
Raw data (loadavg): 1.05 1.05 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 65948 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+670.017 s]
Raw data (loadavg): 1.05 1.04 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18683 0 0 0 66949 60 0 0 25 0 1 0 479728013 78508032 18661 4294967295 134512640 134672761 3221224560 3221223720 134559749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18661 603 41 0 19126 0
vsize: 76668
[startup+680.018 s]
Raw data (loadavg): 1.04 1.04 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18684 0 0 0 67949 60 0 0 25 0 1 0 479728013 78508032 18662 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18662 603 41 0 19126 0
vsize: 76668
[startup+690.017 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18685 0 0 0 68949 60 0 0 25 0 1 0 479728013 78508032 18663 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18663 603 41 0 19126 0
vsize: 76668
[startup+700.018 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18685 0 0 0 69949 60 0 0 25 0 1 0 479728013 78508032 18663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18663 603 41 0 19126 0
vsize: 76668
[startup+710.019 s]
Raw data (loadavg): 1.02 1.04 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18685 0 0 0 70949 60 0 0 25 0 1 0 479728013 78508032 18663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18663 603 41 0 19126 0
vsize: 76668
[startup+720.019 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 71949 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+730.018 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 72950 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+740.018 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 73950 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+750.019 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 74950 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+760.019 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 75950 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+770.018 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 76950 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+780.019 s]
Raw data (loadavg): 1.00 1.03 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 77951 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+790.018 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 78951 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+800.019 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 79951 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+810.02 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 80951 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+820.02 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 81951 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+830.02 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 82952 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+840.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 83952 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+850.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 84951 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+860.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 85952 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+870.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 86952 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+880.022 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18686 0 0 0 87952 60 0 0 25 0 1 0 479728013 78508032 18664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18664 603 41 0 19126 0
vsize: 76668
[startup+890.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18687 0 0 0 88952 60 0 0 25 0 1 0 479728013 78508032 18665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18665 603 41 0 19126 0
vsize: 76668
[startup+900.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18687 0 0 0 89952 60 0 0 25 0 1 0 479728013 78508032 18665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19167 18665 603 41 0 19126 0
vsize: 76668
[startup+910.021 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18809 0 0 0 90952 60 0 0 25 0 1 0 479728013 79032320 18787 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19295 18787 603 41 0 19254 0
vsize: 77180
[startup+920.021 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 18964 0 0 0 91952 60 0 0 25 0 1 0 479728013 79564800 18942 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19425 18942 603 41 0 19384 0
vsize: 77700
[startup+930.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19107 0 0 0 92952 60 0 0 25 0 1 0 479728013 80240640 19085 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19590 19085 603 41 0 19549 0
vsize: 78360
[startup+940.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19254 0 0 0 93952 61 0 0 25 0 1 0 479728013 80777216 19232 4294967295 134512640 134672761 3221224560 3221221948 134566339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19232 603 41 0 19680 0
vsize: 78884
[startup+950.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19254 0 0 0 94952 61 0 0 25 0 1 0 479728013 80777216 19232 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19232 603 41 0 19680 0
vsize: 78884
[startup+960.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19255 0 0 0 95953 61 0 0 25 0 1 0 479728013 80777216 19233 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19233 603 41 0 19680 0
vsize: 78884
[startup+970.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19255 0 0 0 96953 61 0 0 25 0 1 0 479728013 80777216 19233 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19233 603 41 0 19680 0
vsize: 78884
[startup+980.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19255 0 0 0 97953 61 0 0 25 0 1 0 479728013 80777216 19233 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19233 603 41 0 19680 0
vsize: 78884
[startup+990.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 98953 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 99953 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 100953 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223744 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 101953 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 102953 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 103954 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 104954 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 105954 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 106955 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 107955 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 108955 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 109956 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19256 0 0 0 110956 61 0 0 25 0 1 0 479728013 80777216 19234 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19234 603 41 0 19680 0
vsize: 78884
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 111956 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 112956 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 113956 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 114957 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 115957 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 116957 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 117957 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 118957 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 15127
Raw data (stat): 15070 (minisat+) R 15069 10614 10613 0 -1 0 19257 0 0 0 119958 61 0 0 25 0 1 0 479728013 80777216 19235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19721 19235 603 41 0 19680 0
vsize: 78884
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 15127
Raw data (stat): 15070 (minisat+) Z 15069 10614 10613 0 -1 12 19260 0 0 0 119958 64 0 0 25 0 1 0 479728013 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.23
CPU user time (s): 1199.58
CPU system time (s): 0.649901
CPU usage (%): 100.013
Max. virtual memory (Kb): 78884
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####