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/frb45-21-opb/normalized-frb45-21-1.opb
MD5SUM	aa1ea44fce5b7bfbe62733720f941ebb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-33
Optimality of the best value was proved	NO
Number of terms in the objective function	945
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	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	945
Total number of constraints	59186
Number of constraints which are clauses	59186
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 5246

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        852700 kB
Buffers:         40176 kB
Cached:         117380 kB
SwapCached:          0 kB
Active:         108044 kB
Inactive:        52644 kB
HighTotal:      131008 kB
HighFree:        20944 kB
LowTotal:       903652 kB
LowFree:        831756 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15620 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:14:44 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3713 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 59186 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 |   59186   118372 |   19728       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1856   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71835   163600 |   23945       0        0     nan |  0.000 % |
c |       100 |   71817   163538 |   26339      90     1041    11.6 |  0.108 % |
c |       250 |   71808   163507 |   28973     237     2624    11.1 |  0.146 % |
c |       475 |   71799   163476 |   31870     459     5113    11.1 |  0.181 % |
c |       812 |   71772   163383 |   35057     790     8354    10.6 |  0.289 % |
c |      1318 |   71703   163146 |   38563    1264    13374    10.6 |  0.580 % |
c |      2079 |   71562   162661 |   42420    1991    22322    11.2 |  1.156 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 41   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3195 |   71597   162811 |   23865    3042    36759    12.1 |  1.156 % |
c |      3295 |   71567   162709 |   26251    3137    38039    12.1 |  2.391 % |
c |      3445 |   71558   162678 |   28876    3284    40146    12.2 |  2.424 % |
c |      3670 |   71433   162249 |   31764    3475    43166    12.4 |  2.998 % |
c |      4007 |   71346   161950 |   34940    3789    47442    12.5 |  3.351 % |
c |      4513 |   71292   161764 |   38434    4277    55958    13.1 |  3.565 % |
c |      5272 |   71031   160867 |   42278    4969    72483    14.6 |  4.920 % |
c |      6411 |   70722   159812 |   46506    6011   112442    18.7 |  6.524 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7537 |   70283   158305 |   23427    7008   153523    21.9 |  6.524 % |
c |      7637 |   70262   158234 |   25769    7099   155224    21.9 |  8.981 % |
c |      7787 |   70242   158164 |   28346    7243   158580    21.9 |  9.088 % |
c |      8012 |   70187   157979 |   31181    7456   166912    22.4 |  9.444 % |
c |      8349 |   70089   157641 |   34299    7755   173570    22.4 | 10.014 % |
c |      8856 |   69789   156603 |   37729    8163   184828    22.6 | 11.689 % |
c |      9616 |   68849   153347 |   41502    8638   198395    23.0 | 17.391 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10601 |   68755   153020 |   22918    9532   259174    27.2 | 17.391 % |
c |     10701 |   68724   152913 |   25209    9621   261049    27.1 | 18.278 % |
c |     10853 |   68698   152823 |   27730    9765   263726    27.0 | 18.418 % |
c |     11078 |   68591   152448 |   30503    9954   267796    26.9 | 19.202 % |
c |     11415 |   68415   151838 |   33554   10138   273730    27.0 | 20.235 % |
c |     11921 |   68308   151467 |   36909   10584   303814    28.7 | 20.950 % |
c |     12680 |   68040   150531 |   40600   11154   326207    29.2 | 22.800 % |
c |     13819 |   67750   149527 |   44660   12011   359248    29.9 | 24.584 % |
c |     15527 |   67467   148546 |   49126   13523   417548    30.9 | 26.398 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18072 |   67356   148164 |   22452   15965   583615    36.6 | 26.398 % |
c |     18172 |   67356   148164 |   24697   16065   586588    36.5 | 27.208 % |
c |     18323 |   67356   148164 |   27166   16216   593173    36.6 | 27.211 % |
c |     18548 |   67249   147795 |   29883   16303   604402    37.1 | 27.923 % |
c |     18886 |   67181   147555 |   32871   16518   621691    37.6 | 28.422 % |
c |     19393 |   67150   147448 |   36159   16970   644415    38.0 | 28.635 % |
c |     20152 |   67088   147226 |   39775   17633   684001    38.8 | 29.060 % |
c |     21291 |   67036   147044 |   43752   18615   735598    39.5 | 29.309 % |
c |     22999 |   66865   146439 |   48127   20135   794370    39.5 | 30.556 % |
c |     25561 |   66856   146408 |   52940   22669   944421    41.7 | 30.591 % |
c |     29405 |   66693   145843 |   58234   26215  1362566    52.0 | 31.697 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30381 |   66696   145857 |   22232   27191  1419253    52.2 | 31.697 % |
c |     30482 |   66696   145857 |   24455   13697   763033    55.7 | 31.722 % |
c |     30632 |   66696   145857 |   26900   13847   766220    55.3 | 31.719 % |
c |     30857 |   66696   145857 |   29590   14072   777289    55.2 | 31.719 % |
c |     31194 |   66663   145742 |   32549   14387   785978    54.6 | 31.969 % |
c |     31701 |   66636   145647 |   35804   14890   811012    54.5 | 32.185 % |
c |     32461 |   66627   145616 |   39385   15626   855260    54.7 | 32.218 % |
c |     33600 |   66627   145616 |   43323   16765   921009    54.9 | 32.218 % |
c |     35308 |   66621   145596 |   47656   18469  1117833    60.5 | 32.255 % |
c |     37870 |   66574   145425 |   52421   20975  1297631    61.9 | 32.609 % |
c |     41714 |   66486   145121 |   57664   24746  1704724    68.9 | 33.324 % |
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 |     42838 |   66444   144983 |   22148   25804  1784291    69.1 | 33.324 % |
c |     42938 |   66444   144983 |   24362   13002   889594    68.4 | 33.632 % |
c |     43088 |   66393   144798 |   26799   13136   891860    67.9 | 34.093 % |
c |     43313 |   66393   144798 |   29478   13361   901453    67.5 | 34.093 % |
c |     43650 |   66387   144778 |   32426   13694   922265    67.3 | 34.130 % |
c |     44156 |   66387   144778 |   35669   14200   950167    66.9 | 34.128 % |
c |     44916 |   66387   144778 |   39236   14960   989959    66.2 | 34.128 % |
c |     46055 |   66387   144778 |   43160   16099  1057974    65.7 | 34.130 % |
c |     47763 |   66387   144778 |   47476   17807  1139744    64.0 | 34.128 % |
c |     50325 |   66361   144688 |   52223   20354  1346767    66.2 | 34.270 % |
c |     54170 |   66361   144688 |   57446   24199  1661598    68.7 | 34.271 % |
c |     59936 |   66341   144618 |   63190   29939  2489471    83.2 | 34.379 % |
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 |     64031 |   66309   144509 |   22103   33984  3025519    89.0 | 34.379 % |
c |     64131 |   66309   144509 |   24313   15423  1509417    97.9 | 34.616 % |
c |     64281 |   66309   144509 |   26744   15573  1517327    97.4 | 34.616 % |
c |     64506 |   66309   144509 |   29419   15798  1522993    96.4 | 34.616 % |
c |     64843 |   66309   144509 |   32361   16135  1545170    95.8 | 34.616 % |
c |     65349 |   66263   144349 |   35597   16587  1577598    95.1 | 34.972 % |
c |     66108 |   66257   144329 |   39156   17341  1640323    94.6 | 35.005 % |
c |     67247 |   66257   144329 |   43072   18480  1709701    92.5 | 35.005 % |
c |     68956 |   66257   144329 |   47379   20189  1940825    96.1 | 35.005 % |
c |     71518 |   66251   144309 |   52117   22745  2124756    93.4 | 35.041 % |
c |     75364 |   66245   144289 |   57329   26588  2503802    94.2 | 35.076 % |
c |     81130 |   66198   144122 |   63062   32347  3251776   100.5 | 35.432 % |
c |     89779 |   66188   144086 |   69368   40963  3894422    95.1 | 35.541 % |
c |    102753 |   66188   144086 |   76305   53937  6353176   117.8 | 35.541 % |
c |    122214 |   66179   144055 |   83936   73387  7416762   101.1 | 35.577 % |
c |    151406 |   66152   143962 |   92329   34703  2127103    61.3 | 35.681 % |
c |    195195 |   66152   143962 |  101562   78492  5561068    70.8 | 35.683 % |
c |    260879 |   66152   143962 |  111718   57264  8670840   151.4 | 35.681 % |
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 |    292324 |   66153   143967 |   22051   88709 12728837   143.5 | 35.681 % |
c |    292425 |   66153   143967 |   24256   15999  1683350   105.2 | 35.706 % |
c |    292575 |   66153   143967 |   26681   16149  1684998   104.3 | 35.704 % |
c |    292803 |   66153   143967 |   29349   16377  1695820   103.5 | 35.704 % |
c |    293145 |   66153   143967 |   32284   16719  1706066   102.0 | 35.704 % |
c |    293653 |   66153   143967 |   35513   17227  1721782    99.9 | 35.706 % |
c |    294412 |   66153   143967 |   39064   17986  1745171    97.0 | 35.704 % |
c |    295552 |   66153   143967 |   42971   19126  1818958    95.1 | 35.706 % |
c |    297260 |   66145   143939 |   47268   20830  1914585    91.9 | 35.775 % |
c |    299823 |   66145   143939 |   51995   23393  2085795    89.2 | 35.777 % |
c |    303667 |   66145   143939 |   57194   27237  2406490    88.4 | 35.775 % |
c |    309433 |   66145   143939 |   62914   33003  2922875    88.6 | 35.777 % |
c |    318082 |   66145   143939 |   69205   41652  4122573    99.0 | 35.775 % |
c |    331056 |   66145   143939 |   76126   54626  5859143   107.3 | 35.775 % |
c |    350518 |   66145   143939 |   83738   74088  8184027   110.5 | 35.775 % |
c |    379710 |   66145   143939 |   92112   34267  3176986    92.7 | 35.775 % |
c |    423499 |   66139   143919 |  101323   78048  9715672   124.5 | 35.813 % |
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 |    486482 |   66121   143861 |   22040   55443  6481783   116.9 | 35.813 % |
c |    486582 |   66121   143861 |   24244   19229  1883087    97.9 | 36.001 % |
c |    486732 |   66121   143861 |   26668   19379  1886894    97.4 | 36.000 % |
c |    486957 |   66121   143861 |   29335   19604  1892622    96.5 | 35.999 % |
c |    487294 |   66121   143861 |   32268   19941  1904156    95.5 | 36.000 % |
c |    487801 |   66121   143861 |   35495   20448  1930086    94.4 | 36.000 % |
c |    488560 |   66121   143861 |   39045   21207  1962171    92.5 | 35.999 % |
c |    489699 |   66121   143861 |   42949   22346  2067503    92.5 | 36.001 % |
c |    491408 |   66121   143861 |   47244   24055  2142686    89.1 | 35.999 % |
c |    493970 |   66121   143861 |   51969   26617  2348044    88.2 | 35.999 % |
c |    497814 |   66121   143861 |   57166   30461  2536038    83.3 | 35.999 % |
c |    503580 |   66121   143861 |   62882   36227  2918512    80.6 | 35.999 % |
c |    512229 |   66121   143861 |   69170   44876  4249410    94.7 | 36.000 % |
c |    525203 |   66112   143832 |   76088   57848  5541516    95.8 | 36.071 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v 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 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 C466 -C465 -C464 -C463 -C462 -C461 -C460 C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 C421 -C420 C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 C295 C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/56 16734
Raw data (stat): 16734 (runsolver) R 16733 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364633635 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.88 0.94 0.90 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 2937 0 0 0 991 7 0 0 25 0 1 0 364633635 13746176 2915 4294967295 134512640 134672761 3221224560 3221223760 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3356 2915 603 41 0 3315 0
vsize: 13424
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 2937 0 0 0 1991 8 0 0 25 0 1 0 364633635 13746176 2915 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3356 2915 603 41 0 3315 0
vsize: 13424
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.94 0.90 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 2937 0 0 0 2991 8 0 0 25 0 1 0 364633635 13746176 2915 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3356 2915 603 41 0 3315 0
vsize: 13424
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 3039 0 0 0 3991 8 0 0 25 0 1 0 364633635 14151680 3017 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3455 3017 603 41 0 3414 0
vsize: 13820
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.95 0.90 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 3440 0 0 0 4990 9 0 0 25 0 1 0 364633635 15847424 3418 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3418 603 41 0 3828 0
vsize: 15476
[startup+60.003 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 3768 0 0 0 5988 11 0 0 25 0 1 0 364633635 17195008 3746 4294967295 134512640 134672761 3221224560 3221223664 134560390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4198 3746 603 41 0 4157 0
vsize: 16792
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 4747 0 0 0 6985 14 0 0 25 0 1 0 364633635 21327872 4725 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5207 4725 603 41 0 5166 0
vsize: 20828
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 4747 0 0 0 7985 14 0 0 25 0 1 0 364633635 21327872 4725 4294967295 134512640 134672761 3221224560 3221223712 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5207 4725 603 41 0 5166 0
vsize: 20828
[startup+90.0052 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 16734
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 4936 0 0 0 8985 15 0 0 25 0 1 0 364633635 22134784 4914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5404 4914 603 41 0 5363 0
vsize: 21616
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 5481 0 0 0 9983 16 0 0 25 0 1 0 364633635 24289280 5459 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5930 5459 603 41 0 5889 0
vsize: 23720
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 6151 0 0 0 10981 19 0 0 25 0 1 0 364633635 26976256 6129 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6586 6129 603 41 0 6545 0
vsize: 26344
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 6909 0 0 0 11979 21 0 0 25 0 1 0 364633635 30064640 6887 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7340 6887 603 41 0 7299 0
vsize: 29360
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 7697 0 0 0 12977 23 0 0 25 0 1 0 364633635 33402880 7675 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8155 7675 603 41 0 8114 0
vsize: 32620
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 8277 0 0 0 13976 24 0 0 25 0 1 0 364633635 35672064 8255 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8709 8255 603 41 0 8668 0
vsize: 34836
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 8640 0 0 0 14975 25 0 0 25 0 1 0 364633635 37142528 8618 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9068 8618 603 41 0 9027 0
vsize: 36272
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 8976 0 0 0 15974 26 0 0 25 0 1 0 364633635 38477824 8954 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9394 8954 603 41 0 9353 0
vsize: 37576
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 9225 0 0 0 16974 27 0 0 25 0 1 0 364633635 39809024 9203 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9719 9203 603 41 0 9678 0
vsize: 38876
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 9448 0 0 0 17974 27 0 0 25 0 1 0 364633635 40747008 9426 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9948 9426 603 41 0 9907 0
vsize: 39792
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 9682 0 0 0 18974 27 0 0 25 0 1 0 364633635 41689088 9660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10178 9660 603 41 0 10137 0
vsize: 40712
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 9892 0 0 0 19973 28 0 0 25 0 1 0 364633635 42500096 9870 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10376 9870 603 41 0 10335 0
vsize: 41504
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10207 0 0 0 20972 30 0 0 25 0 1 0 364633635 43716608 10185 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10673 10185 603 41 0 10632 0
vsize: 42692
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 21972 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 22972 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 23972 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 24972 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 25973 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 26973 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 27973 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 28973 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 29973 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 30973 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16736
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 31974 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16789
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 32974 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16789
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 33974 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16789
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10232 0 0 0 34974 30 0 0 25 0 1 0 364633635 43851776 10210 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10706 10210 603 41 0 10665 0
vsize: 42824
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16789
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10236 0 0 0 35974 30 0 0 25 0 1 0 364633635 43851776 10214 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10706 10214 603 41 0 10665 0
vsize: 42824
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16789
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10238 0 0 0 36974 30 0 0 25 0 1 0 364633635 43851776 10216 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10706 10216 603 41 0 10665 0
vsize: 42824
[startup+380.011 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 16791
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10241 0 0 0 37974 30 0 0 25 0 1 0 364633635 43851776 10219 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10706 10219 603 41 0 10665 0
vsize: 42824
[startup+390.012 s]
Raw data (loadavg): 1.06 0.99 0.91 2/56 16793
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10468 0 0 0 38973 31 0 0 25 0 1 0 364633635 44781568 10446 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10446 603 41 0 10892 0
vsize: 43732
[startup+400.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 10824 0 0 0 39973 32 0 0 25 0 1 0 364633635 46239744 10802 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11289 10802 603 41 0 11248 0
vsize: 45156
[startup+410.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11179 0 0 0 40972 33 0 0 25 0 1 0 364633635 47726592 11157 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 11157 603 41 0 11611 0
vsize: 46608
[startup+420.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11512 0 0 0 41972 33 0 0 25 0 1 0 364633635 49070080 11490 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11980 11490 603 41 0 11939 0
vsize: 47920
[startup+430.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11721 0 0 0 42971 34 0 0 25 0 1 0 364633635 49926144 11699 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12189 11699 603 41 0 12148 0
vsize: 48756
[startup+440.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11721 0 0 0 43972 34 0 0 25 0 1 0 364633635 49926144 11699 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12189 11699 603 41 0 12148 0
vsize: 48756
[startup+450.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11731 0 0 0 44972 34 0 0 25 0 1 0 364633635 50073600 11709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11709 603 41 0 12184 0
vsize: 48900
[startup+460.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11740 0 0 0 45972 34 0 0 25 0 1 0 364633635 50073600 11718 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11718 603 41 0 12184 0
vsize: 48900
[startup+470.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11741 0 0 0 46972 34 0 0 25 0 1 0 364633635 50073600 11719 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11719 603 41 0 12184 0
vsize: 48900
[startup+480.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11745 0 0 0 47972 34 0 0 25 0 1 0 364633635 50073600 11723 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11723 603 41 0 12184 0
vsize: 48900
[startup+490.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11746 0 0 0 48972 34 0 0 25 0 1 0 364633635 50073600 11724 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11724 603 41 0 12184 0
vsize: 48900
[startup+500.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11748 0 0 0 49973 34 0 0 25 0 1 0 364633635 50073600 11726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11726 603 41 0 12184 0
vsize: 48900
[startup+510.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11750 0 0 0 50973 34 0 0 25 0 1 0 364633635 50073600 11728 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11728 603 41 0 12184 0
vsize: 48900
[startup+520.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11750 0 0 0 51973 34 0 0 25 0 1 0 364633635 50073600 11728 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11728 603 41 0 12184 0
vsize: 48900
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11753 0 0 0 52973 34 0 0 25 0 1 0 364633635 50073600 11731 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11731 603 41 0 12184 0
vsize: 48900
[startup+540.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11755 0 0 0 53973 34 0 0 25 0 1 0 364633635 50073600 11733 4294967295 134512640 134672761 3221224560 3221223736 134559059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11733 603 41 0 12184 0
vsize: 48900
[startup+550.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 11780 0 0 0 54973 34 0 0 25 0 1 0 364633635 50270208 11758 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12273 11758 603 41 0 12232 0
vsize: 49092
[startup+560.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 12040 0 0 0 55972 35 0 0 25 0 1 0 364633635 51212288 12018 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12503 12018 603 41 0 12462 0
vsize: 50012
[startup+570.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 12534 0 0 0 56971 36 0 0 25 0 1 0 364633635 53354496 12512 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13026 12512 603 41 0 12985 0
vsize: 52104
[startup+580.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 13031 0 0 0 57970 37 0 0 25 0 1 0 364633635 55382016 13009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13521 13009 603 41 0 13480 0
vsize: 54084
[startup+590.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 13456 0 0 0 58970 38 0 0 25 0 1 0 364633635 57135104 13434 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13949 13434 603 41 0 13908 0
vsize: 55796
[startup+600.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 13886 0 0 0 59969 39 0 0 25 0 1 0 364633635 58888192 13864 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13864 603 41 0 14336 0
vsize: 57508
[startup+610.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 14256 0 0 0 60968 40 0 0 25 0 1 0 364633635 60383232 14234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14742 14234 603 41 0 14701 0
vsize: 58968
[startup+620.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 14678 0 0 0 61967 42 0 0 25 0 1 0 364633635 62119936 14656 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15166 14656 603 41 0 15125 0
vsize: 60664
[startup+630.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15214 0 0 0 62965 43 0 0 25 0 1 0 364633635 64274432 15192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15692 15192 603 41 0 15651 0
vsize: 62768
[startup+640.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 63965 44 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+650.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 64965 44 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+660.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 65964 45 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+670.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 66965 45 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+680.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 67964 45 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+690.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16795
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 68965 45 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+700.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 69964 45 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+710.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 70964 46 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+720.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 71964 46 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+730.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 72964 46 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+740.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 73964 46 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 74964 46 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 75964 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+770.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 76964 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+780.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 77964 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+790.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 78964 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 79964 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 80964 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+820.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 81965 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+830.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 82965 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+840.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 83965 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+850.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 84965 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+860.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 85965 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+870.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 86966 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+880.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 87966 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+890.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 88966 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+900.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 89966 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+910.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 90966 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+920.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 91966 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+930.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15444 0 0 0 92967 47 0 0 25 0 1 0 364633635 65212416 15422 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15422 603 41 0 15880 0
vsize: 63684
[startup+940.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 93967 47 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+950.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 94967 47 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+960.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 95967 47 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+970.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 96967 47 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+980.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 97967 47 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223696 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+990.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16797
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 98967 47 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 99967 48 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 100966 48 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 101966 48 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 102967 48 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15445 0 0 0 103966 48 0 0 25 0 1 0 364633635 65212416 15423 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15423 603 41 0 15880 0
vsize: 63684
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15650 0 0 0 104966 49 0 0 25 0 1 0 364633635 66146304 15628 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15628 603 41 0 16108 0
vsize: 64596
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 105966 49 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 106966 49 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 107966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 108966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 109966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 110966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 111966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 112967 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 113967 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 114966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 115966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 116966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 117966 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 118967 50 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 16799
Raw data (stat): 16734 (minisat+) R 16733 12452 12451 0 -1 0 15653 0 0 0 119967 51 0 0 25 0 1 0 364633635 66146304 15631 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15631 603 41 0 16108 0
vsize: 64596
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/56 16799
Raw data (stat): 16734 (minisat+) Z 16733 12452 12451 0 -1 12 15656 0 0 0 119967 53 0 0 25 0 1 0 364633635 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.67
CPU system time (s): 0.538918
CPU usage (%): 100.013
Max. virtual memory (Kb): 64596
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####