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-2.opb
MD5SUM	a931f7e9a55cb6836807387327525e8b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-35
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	58624
Number of constraints which are clauses	58624
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 6375

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        838352 kB
Buffers:         35260 kB
Cached:         123896 kB
SwapCached:       3160 kB
Active:          72512 kB
Inactive:        92660 kB
HighTotal:      131008 kB
HighFree:         3724 kB
LowTotal:       903652 kB
LowFree:        834628 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25736 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:03:04 (client local time) WITH STATUS 10 IN 1200.6 SECONDS
stats: 4842 7 1200.6 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58624 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 |   58624   117248 |   19541       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]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  150265   331770 |   50088       0        0     nan |  0.000 % |
c |       102 |  149621   330304 |   55096      88      622     7.1 |  0.607 % |
c |       252 |  147443   325336 |   60606     190     1194     6.3 |  2.665 % |
c |       477 |  146061   322176 |   66667     391     3388     8.7 |  3.993 % |
c |       814 |  144060   317606 |   73333     669     5363     8.0 |  5.901 % |
c |      1322 |  141016   310653 |   80667    1091     8171     7.5 |  8.798 % |
c |      2081 |  135191   297257 |   88733    1659    13727     8.3 | 14.603 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2688 |  128575   281978 |   42858    1966    15940     8.1 | 14.603 % |
c |      2788 |  127920   280468 |   47143    2043    16739     8.2 | 22.033 % |
c |      2941 |  126198   276502 |   51858    2129    17682     8.3 | 23.867 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2990 |  126052   276204 |   42017    2174    18075     8.3 | 23.867 % |
c |      3090 |  125656   275290 |   46218    2260    18736     8.3 | 24.382 % |
c |      3240 |  123976   271367 |   50840    2360    19479     8.3 | 26.119 % |
c |      3465 |  120499   263265 |   55924    2462    20435     8.3 | 29.717 % |
c |      3802 |  116722   254440 |   61517    2619    22406     8.6 | 33.645 % |
c |      4308 |  111011   241223 |   67668    2784    23694     8.5 | 39.566 % |
c |      5067 |  106769   231359 |   74435    3278    29019     8.9 | 44.116 % |
c |      6206 |   99578   214444 |   81879    4009    36180     9.0 | 51.770 % |
c |      7915 |   93818   200995 |   90067    5332    51600     9.7 | 57.992 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9721 |   85580   181727 |   28526    6194    64671    10.4 | 57.992 % |
c |      9821 |   85580   181727 |   31378    6294    65907    10.5 | 67.285 % |
c |      9972 |   85006   180378 |   34516    6369    67662    10.6 | 67.920 % |
c |     10197 |   83505   176851 |   37968    6440    67749    10.5 | 69.533 % |
c |     10534 |   82104   173546 |   41764    6620    69981    10.6 | 71.091 % |
c |     11040 |   80937   170801 |   45941    6905    72934    10.6 | 72.416 % |
c |     11799 |   78858   165914 |   50535    7322    82563    11.3 | 74.762 % |
c |     12938 |   76694   160811 |   55589    7978   112961    14.2 | 77.208 % |
c |     14646 |   74490   155630 |   61148    9023   141287    15.7 | 79.669 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17100 |   73304   152815 |   24434   10923   243146    22.3 | 79.669 % |
c |     17200 |   72780   151577 |   26877   10818   242510    22.4 | 81.548 % |
c |     17351 |   72437   150772 |   29565   10843   244095    22.5 | 81.944 % |
c |     17576 |   72213   150246 |   32521   10962   247834    22.6 | 82.199 % |
c |     17913 |   72213   150246 |   35773   11299   262481    23.2 | 82.199 % |
c |     18420 |   72195   150203 |   39351   11790   278625    23.6 | 82.221 % |
c |     19179 |   71850   149391 |   43286   12421   318824    25.7 | 82.611 % |
c |     20319 |   71315   148124 |   47614   13307   359412    27.0 | 83.227 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21015 |   71365   148253 |   23788   13999   403427    28.8 | 83.227 % |
c |     21116 |   71365   148253 |   26166   14100   405386    28.8 | 83.202 % |
c |     21266 |   71228   147931 |   28783   14156   408061    28.8 | 83.358 % |
c |     21491 |   71228   147931 |   31661   14381   415357    28.9 | 83.358 % |
c |     21828 |   71228   147931 |   34828   14718   431812    29.3 | 83.358 % |
c |     22334 |   71228   147931 |   38310   15224   461679    30.3 | 83.358 % |
c |     23093 |   71202   147871 |   42141   15967   490430    30.7 | 83.383 % |
c |     24233 |   71196   147857 |   46356   17097   534309    31.3 | 83.390 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24862 |   71152   147729 |   23717   17482   548285    31.4 | 83.390 % |
c |     24962 |   71152   147729 |   26088   17582   551022    31.3 | 83.416 % |
c |     25113 |   71088   147579 |   28697   17700   555556    31.4 | 83.490 % |
c |     25338 |   71050   147491 |   31567   17897   563743    31.5 | 83.528 % |
c |     25675 |   70918   147182 |   34724   18131   569463    31.4 | 83.675 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26090 |   70998   147386 |   23666   18546   607889    32.8 | 83.675 % |
c |     26190 |   70948   147264 |   26032   18612   608354    32.7 | 83.732 % |
c |     26341 |   70876   147090 |   28635   18685   610503    32.7 | 83.824 % |
c |     26566 |   70876   147090 |   31499   18910   627342    33.2 | 83.824 % |
c |     26905 |   70876   147090 |   34649   19249   641026    33.3 | 83.824 % |
c |     27411 |   70659   146586 |   38114   19689   661910    33.6 | 84.056 % |
c |     28171 |   70659   146586 |   41925   20449   698680    34.2 | 84.056 % |
c |     29310 |   70534   146292 |   46118   21417   756833    35.3 | 84.199 % |
c |     31019 |   70435   146059 |   50730   23093   886673    38.4 | 84.316 % |
c |     33581 |   70346   145850 |   55803   25497  1002966    39.3 | 84.418 % |
c |     37425 |   70340   145836 |   61383   29337  1307865    44.6 | 84.424 % |
c |     43192 |   70188   145477 |   67521   34976  1729464    49.4 | 84.596 % |
c |     51843 |   70115   145303 |   74274   43385  2460605    56.7 | 84.688 % |
c |     64817 |   70115   145303 |   81701   56359  4366303    77.5 | 84.688 % |
c |     84278 |   69736   144417 |   89871   75312  6288685    83.5 | 85.114 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93879 |   69704   144320 |   23234   84811  7521407    88.7 | 85.114 % |
c |     93979 |   69704   144320 |   25557   18078  1621853    89.7 | 85.143 % |
c |     94129 |   69704   144320 |   28113   18228  1628210    89.3 | 85.143 % |
c |     94354 |   69700   144311 |   30924   18452  1635894    88.7 | 85.147 % |
c |     94691 |   69700   144311 |   34016   18789  1659233    88.3 | 85.146 % |
c |     95197 |   69700   144311 |   37418   19295  1693089    87.7 | 85.147 % |
c |     95956 |   69494   143830 |   41160   19917  1734076    87.1 | 85.378 % |
c |     97095 |   69494   143830 |   45276   21056  1844300    87.6 | 85.378 % |
c |     98805 |   69416   143646 |   49804   22751  1965716    86.4 | 85.471 % |
c |    101369 |   69392   143589 |   54784   25305  2217487    87.6 | 85.499 % |
c |    105213 |   69277   143309 |   60263   29127  2558867    87.9 | 85.639 % |
c |    110980 |   69111   142920 |   66289   34798  3117212    89.6 | 85.817 % |
c |    119629 |   69093   142877 |   72918   43440  4235069    97.5 | 85.839 % |
c |    132603 |   69093   142877 |   80210   56414  5576869    98.9 | 85.839 % |
c |    152064 |   69065   142810 |   88231   75872  7616650   100.4 | 85.874 % |
c |    181258 |   69065   142810 |   97054  105066 10024052    95.4 | 85.874 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    191395 |   69106   142911 |   23035  115203 10750465    93.3 | 85.874 % |
c |    191495 |   69106   142911 |   25338   20512  1002443    48.9 | 85.846 % |
c |    191646 |   69106   142911 |   27872   20663  1011230    48.9 | 85.846 % |
c |    191871 |   69106   142911 |   30659   20888  1021380    48.9 | 85.846 % |
c |    192209 |   69100   142897 |   33725   21224  1044884    49.2 | 85.853 % |
c |    192715 |   69068   142822 |   37098   21721  1076125    49.5 | 85.888 % |
c |    193474 |   69064   142813 |   40807   22477  1115946    49.6 | 85.891 % |
c |    194613 |   69064   142813 |   44888   23616  1216667    51.5 | 85.891 % |
c |    196322 |   69064   142813 |   49377   25325  1336840    52.8 | 85.891 % |
c |    198884 |   69064   142813 |   54315   27887  1572706    56.4 | 85.891 % |
c |    202730 |   69064   142813 |   59746   31733  1991772    62.8 | 85.891 % |
c |    208496 |   68940   142520 |   65721   37419  2526781    67.5 | 86.040 % |
c |    217145 |   68894   142413 |   72293   46020  3326724    72.3 | 86.087 % |
c |    230120 |   68894   142413 |   79523   58995  4653243    78.9 | 86.088 % |
c |    249581 |   68894   142413 |   87475   78456  6260896    79.8 | 86.088 % |
c |    278775 |   68888   142399 |   96222  107647  8248566    76.6 | 86.094 % |
c |    322565 |   68888   142399 |  105845   45990  2221490    48.3 | 86.094 % |
c |    388249 |   68838   142281 |  116429  111662  8760719    78.5 | 86.151 % |
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 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 25210
Raw data (stat): 25210 (runsolver) R 25209 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481797659 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+9.99954 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3820 0 0 0 986 11 0 0 25 0 1 0 481797659 17629184 3798 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4304 3798 603 41 0 4263 0
vsize: 17216
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3826 0 0 0 1986 11 0 0 25 0 1 0 481797659 17629184 3804 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4304 3804 603 41 0 4263 0
vsize: 17216
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3943 0 0 0 2985 12 0 0 25 0 1 0 481797659 18513920 3921 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4520 3921 603 41 0 4479 0
vsize: 18080
[startup+40.002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3943 0 0 0 3985 12 0 0 25 0 1 0 481797659 18513920 3921 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4520 3921 603 41 0 4479 0
vsize: 18080
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3945 0 0 0 4986 12 0 0 25 0 1 0 481797659 18513920 3923 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4520 3923 603 41 0 4479 0
vsize: 18080
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 4108 0 0 0 5985 13 0 0 25 0 1 0 481797659 19103744 4086 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4664 4086 603 41 0 4623 0
vsize: 18656
[startup+70.0034 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 4490 0 0 0 6984 14 0 0 25 0 1 0 481797659 20709376 4468 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4468 603 41 0 5015 0
vsize: 20224
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 4912 0 0 0 7983 15 0 0 25 0 1 0 481797659 22425600 4890 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5475 4890 603 41 0 5434 0
vsize: 21900
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 5451 0 0 0 8981 17 0 0 25 0 1 0 481797659 24576000 5429 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6000 5429 603 41 0 5959 0
vsize: 24000
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 6019 0 0 0 9979 19 0 0 25 0 1 0 481797659 27111424 5997 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 5997 603 41 0 6578 0
vsize: 26476
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 6517 0 0 0 10978 20 0 0 25 0 1 0 481797659 29122560 6495 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7110 6495 603 41 0 7069 0
vsize: 28440
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 7046 0 0 0 11976 22 0 0 25 0 1 0 481797659 31256576 7024 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7631 7024 603 41 0 7590 0
vsize: 30524
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 7659 0 0 0 12975 24 0 0 25 0 1 0 481797659 33669120 7637 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8220 7637 603 41 0 8179 0
vsize: 32880
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 8252 0 0 0 13973 25 0 0 25 0 1 0 481797659 36188160 8230 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8835 8230 603 41 0 8794 0
vsize: 35340
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 8711 0 0 0 14972 27 0 0 25 0 1 0 481797659 38060032 8689 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9292 8689 603 41 0 9251 0
vsize: 37168
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 9143 0 0 0 15971 28 0 0 25 0 1 0 481797659 39792640 9121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9715 9121 603 41 0 9674 0
vsize: 38860
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 9553 0 0 0 16970 29 0 0 25 0 1 0 481797659 41394176 9531 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10106 9531 603 41 0 10065 0
vsize: 40424
[startup+180.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 9980 0 0 0 17970 30 0 0 25 0 1 0 481797659 43397120 9958 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10595 9958 603 41 0 10554 0
vsize: 42380
[startup+190.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 10225 0 0 0 18970 30 0 0 25 0 1 0 481797659 44474368 10203 4294967295 134512640 134672761 3221224560 3221223744 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10858 10203 603 41 0 10817 0
vsize: 43432
[startup+200.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 10650 0 0 0 19969 31 0 0 25 0 1 0 481797659 46211072 10628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11282 10628 603 41 0 11241 0
vsize: 45128
[startup+210.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11058 0 0 0 20968 33 0 0 25 0 1 0 481797659 47808512 11036 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11672 11036 603 41 0 11631 0
vsize: 46688
[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11437 0 0 0 21967 34 0 0 25 0 1 0 481797659 49278976 11415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12031 11415 603 41 0 11990 0
vsize: 48124
[startup+230.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11824 0 0 0 22967 35 0 0 25 0 1 0 481797659 50880512 11802 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12422 11802 603 41 0 12381 0
vsize: 49688
[startup+240.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 23966 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+250.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 24966 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 25966 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 26967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 27967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 28967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 29967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 30967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 31967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 32968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 33968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 34968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 35968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 36968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12565 11947 603 41 0 12524 0
vsize: 50260
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 12223 0 0 0 37968 36 0 0 25 0 1 0 481797659 52527104 12201 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12824 12201 603 41 0 12783 0
vsize: 51296
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 12534 0 0 0 38968 37 0 0 25 0 1 0 481797659 53850112 12512 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13147 12512 603 41 0 13106 0
vsize: 52588
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 12823 0 0 0 39967 38 0 0 25 0 1 0 481797659 55037952 12801 4294967295 134512640 134672761 3221224560 3221223664 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13437 12801 603 41 0 13396 0
vsize: 53748
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13064 0 0 0 40967 38 0 0 25 0 1 0 481797659 55963648 13042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 13042 603 41 0 13622 0
vsize: 54652
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13348 0 0 0 41966 38 0 0 25 0 1 0 481797659 57147392 13326 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13326 603 41 0 13911 0
vsize: 55808
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13609 0 0 0 42966 39 0 0 25 0 1 0 481797659 58212352 13587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14212 13587 603 41 0 14171 0
vsize: 56848
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13831 0 0 0 43966 40 0 0 25 0 1 0 481797659 59142144 13809 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14439 13809 603 41 0 14398 0
vsize: 57756
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14052 0 0 0 44965 41 0 0 25 0 1 0 481797659 60067840 14030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14665 14030 603 41 0 14624 0
vsize: 58660
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14311 0 0 0 45964 41 0 0 25 0 1 0 481797659 61120512 14289 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14922 14289 603 41 0 14881 0
vsize: 59688
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14526 0 0 0 46964 42 0 0 25 0 1 0 481797659 61911040 14504 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15115 14504 603 41 0 15074 0
vsize: 60460
[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14692 0 0 0 47964 42 0 0 25 0 1 0 481797659 62574592 14670 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15277 14670 603 41 0 15236 0
vsize: 61108
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14870 0 0 0 48963 43 0 0 25 0 1 0 481797659 63365120 14848 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15470 14848 603 41 0 15429 0
vsize: 61880
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15077 0 0 0 49962 44 0 0 25 0 1 0 481797659 64159744 15055 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15664 15055 603 41 0 15623 0
vsize: 62656
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15283 0 0 0 50962 45 0 0 25 0 1 0 481797659 64958464 15261 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15261 603 41 0 15818 0
vsize: 63436
[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15453 0 0 0 51961 46 0 0 25 0 1 0 481797659 65748992 15431 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16052 15431 603 41 0 16011 0
vsize: 64208
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 52961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 53961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 54961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 55961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 56962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 57962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 58962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 59962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 60962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 61963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 62963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 63963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 64963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 65963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 66964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 67964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 68964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 69964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 70965 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 71965 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15642 603 41 0 16195 0
vsize: 64944
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 72965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 73965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 74965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 75965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 76966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 77966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 78966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 79966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15643 603 41 0 16195 0
vsize: 64944
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15667 0 0 0 80966 46 0 0 25 0 1 0 481797659 66502656 15645 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15645 603 41 0 16195 0
vsize: 64944
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15669 0 0 0 81967 46 0 0 25 0 1 0 481797659 66502656 15647 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15647 603 41 0 16195 0
vsize: 64944
[startup+830.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15671 0 0 0 82967 46 0 0 25 0 1 0 481797659 66502656 15649 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15649 603 41 0 16195 0
vsize: 64944
[startup+840.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15673 0 0 0 83967 46 0 0 25 0 1 0 481797659 66502656 15651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16236 15651 603 41 0 16195 0
vsize: 64944
[startup+850.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 84967 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 85967 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 86968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 87968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+890.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 88968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+900.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 89968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223744 134559424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+910.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 90968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 91968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 92968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+940.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 93968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+950.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 94968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223472 1075352323 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+960.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 95968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+970.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 96969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+980.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 97969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+990.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 98969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 99969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 100969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1020.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25210
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 101981 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1030.3 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 25250
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 102994 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1040.31 s]
Raw data (loadavg): 1.22 1.02 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 103995 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1050.41 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 105006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1060.41 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 106006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1070.42 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 107006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1080.42 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 108006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1090.42 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 109007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1100.42 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 25263
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 110007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1110.42 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 111006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1120.42 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 112007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1130.42 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 113007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1140.42 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 114007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1150.42 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 115007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15653 603 41 0 16193 0
vsize: 64936
[startup+1160.42 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15676 0 0 0 116007 47 0 0 25 0 1 0 481797659 66494464 15654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15654 603 41 0 16193 0
vsize: 64936
[startup+1170.42 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15678 0 0 0 117008 47 0 0 25 0 1 0 481797659 66494464 15656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15656 603 41 0 16193 0
vsize: 64936
[startup+1180.42 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15680 0 0 0 118008 47 0 0 25 0 1 0 481797659 66494464 15658 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 15658 603 41 0 16193 0
vsize: 64936
[startup+1190.42 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15683 0 0 0 119008 48 0 0 25 0 1 0 481797659 67018752 15661 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16362 15661 603 41 0 16321 0
vsize: 65448
[startup+1200.42 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25265
Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15754 0 0 0 120008 48 0 0 25 0 1 0 481797659 67284992 15732 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16427 15732 603 41 0 16386 0
vsize: 65708
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.45 s]
Raw data (loadavg): 1.01 1.00 0.93 1/54 25265
Raw data (stat): 25210 (minisat+) Z 25209 18865 18864 0 -1 12 15757 0 0 0 120008 51 0 0 25 0 1 0 481797659 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.45
CPU time (s): 1200.6
CPU user time (s): 1200.09
CPU system time (s): 0.511922
CPU usage (%): 100.012
Max. virtual memory (Kb): 65708
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####