PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-3.opb
MD5SUM	140696e76e8ed6af142b84a22a9a8f01
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-38
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	1150
Total number of constraints	81068
Number of constraints which are clauses	81068
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 5253

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        843120 kB
Buffers:         34024 kB
Cached:         114740 kB
SwapCached:       3828 kB
Active:          51364 kB
Inactive:       104052 kB
HighTotal:      131008 kB
HighFree:        13944 kB
LowTotal:       903652 kB
LowFree:        829176 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30480 kB
Committed_AS:    63512 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:19:00 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 3720 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 81068 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 |   81068   162136 |   27022       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2272   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   96792   218334 |   32264       0        0     nan |  0.000 % |
c |       100 |   96792   218334 |   35490     100     1055    10.6 |  0.090 % |
c |       250 |   96774   218272 |   39039     245     2486    10.1 |  0.148 % |
c |       475 |   96774   218272 |   42943     470     5214    11.1 |  0.149 % |
c |       813 |   96765   218241 |   47237     806     9774    12.1 |  0.178 % |
c |      1319 |   96702   218024 |   51961    1297    15091    11.6 |  0.381 % |
c |      2078 |   96675   217931 |   57157    2049    24546    12.0 |  0.469 % |
c |      3217 |   96561   217541 |   62873    3162    42500    13.4 |  0.880 % |
c |      4925 |   96346   216802 |   69160    4811    72068    15.0 |  1.644 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6639 |   95920   215347 |   31973    6409   103399    16.1 |  1.644 % |
c |      6739 |   95905   215296 |   35170    6503   105871    16.3 |  3.344 % |
c |      6889 |   95860   215141 |   38687    6639   107959    16.3 |  3.491 % |
c |      7114 |   95735   214712 |   42556    6820   110583    16.2 |  3.958 % |
c |      7451 |   95429   213660 |   46811    7080   115294    16.3 |  5.221 % |
c |      7958 |   95351   213392 |   51492    7542   130121    17.3 |  5.482 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8088 |   95356   213416 |   31785    7672   137453    17.9 |  5.482 % |
c |      8188 |   95347   213385 |   34963    7769   139338    17.9 |  5.539 % |
c |      8338 |   95267   213111 |   38459    7900   141689    17.9 |  5.862 % |
c |      8563 |   95258   213080 |   42305    8122   146411    18.0 |  5.891 % |
c |      8900 |   94973   212097 |   46536    8384   151087    18.0 |  7.122 % |
c |      9406 |   94677   211075 |   51190    8808   160558    18.2 |  8.414 % |
c |     10165 |   94265   209659 |   56309    9447   174265    18.4 | 10.260 % |
c |     11304 |   93970   208642 |   61939   10496   201578    19.2 | 11.637 % |
c |     13012 |   93384   206620 |   68133   12000   241686    20.1 | 14.537 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13390 |   93297   206323 |   31099   12324   259880    21.1 | 14.537 % |
c |     13490 |   93253   206173 |   34208   12404   261435    21.1 | 15.236 % |
c |     13641 |   93244   206142 |   37629   12552   265470    21.1 | 15.265 % |
c |     13867 |   93172   205892 |   41392   12734   270289    21.2 | 15.590 % |
c |     14204 |   93059   205501 |   45532   12996   276908    21.3 | 16.146 % |
c |     14710 |   93034   205414 |   50085   13498   296461    22.0 | 16.292 % |
c |     15470 |   92885   204901 |   55093   14158   317801    22.4 | 17.052 % |
c |     16609 |   92767   204495 |   60603   15185   367172    24.2 | 17.641 % |
c |     18317 |   92387   203173 |   66663   16701   433732    26.0 | 19.719 % |
c |     20879 |   92161   202385 |   73329   19093   525047    27.5 | 20.920 % |
c |     24726 |   91909   201513 |   80662   22650   663179    29.3 | 22.239 % |
c |     30493 |   91538   200222 |   88729   27859   951256    34.1 | 24.114 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39136 |   91319   199474 |   30439   35931  1612032    44.9 | 24.114 % |
c |     39239 |   91319   199474 |   33482   17080   861448    50.4 | 25.132 % |
c |     39389 |   91172   198965 |   36831   17166   864138    50.3 | 26.012 % |
c |     39614 |   91145   198870 |   40514   17389   873624    50.2 | 26.186 % |
c |     39951 |   91145   198870 |   44565   17726   896078    50.6 | 26.186 % |
c |     40457 |   91139   198850 |   49022   18213   930573    51.1 | 26.217 % |
c |     41216 |   91139   198850 |   53924   18972   960748    50.6 | 26.216 % |
c |     42355 |   91139   198850 |   59316   20111  1118898    55.6 | 26.216 % |
c |     44064 |   91091   198686 |   65248   21759  1214864    55.8 | 26.391 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46168 |   90918   198087 |   30306   23689  1339256    56.5 | 26.391 % |
c |     46268 |   90918   198087 |   33336   23789  1343244    56.5 | 27.321 % |
c |     46418 |   90918   198087 |   36670   23939  1345991    56.2 | 27.321 % |
c |     46643 |   90891   197994 |   40337   24146  1366349    56.6 | 27.467 % |
c |     46980 |   90891   197994 |   44371   24483  1383707    56.5 | 27.469 % |
c |     47486 |   90891   197994 |   48808   24989  1421119    56.9 | 27.467 % |
c |     48246 |   90891   197994 |   53688   25749  1486005    57.7 | 27.469 % |
c |     49386 |   90860   197889 |   59057   26876  1560756    58.1 | 27.643 % |
c |     51095 |   90860   197889 |   64963   28585  1783890    62.4 | 27.643 % |
c |     53657 |   90775   197590 |   71459   31078  1946041    62.6 | 28.141 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57089 |   90768   197574 |   30256   34455  2407291    69.9 | 28.141 % |
c |     57189 |   90768   197574 |   33281   16914  1153421    68.2 | 28.222 % |
c |     57339 |   90745   197493 |   36609   17063  1157228    67.8 | 28.368 % |
c |     57565 |   90745   197493 |   40270   17289  1170920    67.7 | 28.367 % |
c |     57902 |   90745   197493 |   44297   17626  1188984    67.5 | 28.367 % |
c |     58408 |   90745   197493 |   48727   18132  1232884    68.0 | 28.367 % |
c |     59169 |   90745   197493 |   53600   18893  1290840    68.3 | 28.367 % |
c |     60309 |   90745   197493 |   58960   20033  1402360    70.0 | 28.367 % |
c |     62017 |   90695   197321 |   64856   21702  1489132    68.6 | 28.571 % |
c |     64579 |   90660   197202 |   71342   24259  1675525    69.1 | 28.747 % |
c |     68424 |   90654   197182 |   78476   28100  2027047    72.1 | 28.779 % |
c |     74190 |   90634   197112 |   86323   33851  2812409    83.1 | 28.864 % |
c |     82839 |   90625   197081 |   94956   42489  3525100    83.0 | 28.893 % |
c |     95814 |   90583   196939 |  104451   55454  5197397    93.7 | 29.158 % |
c |    115276 |   90583   196939 |  114897   74916  7106174    94.9 | 29.159 % |
c |    144468 |   90535   196773 |  126386  104043 12780012   122.8 | 29.420 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 41   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    184673 |   90527   196749 |   30175   32159  5836846   181.5 | 29.420 % |
c |    184774 |   90527   196749 |   33192   15974  2723643   170.5 | 29.472 % |
c |    184924 |   90518   196718 |   36511   16121  2727882   169.2 | 29.500 % |
c |    185149 |   90468   196540 |   40162   16336  2731191   167.2 | 29.852 % |
c |    185486 |   90468   196540 |   44179   16673  2741443   164.4 | 29.851 % |
c |    185992 |   90468   196540 |   48597   17179  2755741   160.4 | 29.853 % |
c |    186751 |   90450   196478 |   53456   17929  2783418   155.2 | 29.911 % |
c |    187890 |   90444   196458 |   58802   19065  2819619   147.9 | 29.939 % |
c |    189598 |   90444   196458 |   64682   20773  3038381   146.3 | 29.940 % |
c |    192161 |   90438   196438 |   71151   23329  3156033   135.3 | 29.970 % |
c |    196005 |   90430   196410 |   78266   27169  3506442   129.1 | 30.026 % |
c |    201773 |   90407   196331 |   86092   32902  3934228   119.6 | 30.145 % |
c |    210423 |   90373   196213 |   94702   41516  4594345   110.7 | 30.320 % |
c |    223398 |   90373   196213 |  104172   54491  5726763   105.1 | 30.319 % |
c |    242859 |   90322   196036 |  114589   73885  7357337    99.6 | 30.582 % |
c |    272052 |   90322   196036 |  126048  103078 11090396   107.6 | 30.584 % |
c |    315841 |   90322   196036 |  138653   34719  7375510   212.4 | 30.584 % |
c |    381526 |   90276   195878 |  152518  100360 13742076   136.9 | 30.818 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 C555 -C554 -C553 -C552 C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C49#### 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.93 0.97 0.91 2/54 32421
Raw data (stat): 32421 (runsolver) R 32420 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479731746 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 32421
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 3936 0 0 0 987 11 0 0 25 0 1 0 479731746 17985536 3914 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4391 3914 603 41 0 4350 0
vsize: 17564
[startup+20.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 32421
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 3936 0 0 0 1986 11 0 0 25 0 1 0 479731746 17985536 3914 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3914 603 41 0 4350 0
vsize: 17564
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 32421
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 3936 0 0 0 2986 11 0 0 25 0 1 0 479731746 17985536 3914 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3914 603 41 0 4350 0
vsize: 17564
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 32421
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 3936 0 0 0 3986 12 0 0 25 0 1 0 479731746 17985536 3914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3914 603 41 0 4350 0
vsize: 17564
[startup+50.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32421
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 3936 0 0 0 4986 12 0 0 25 0 1 0 479731746 17985536 3914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3914 603 41 0 4350 0
vsize: 17564
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32421
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 3936 0 0 0 5986 12 0 0 25 0 1 0 479731746 17985536 3914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3914 603 41 0 4350 0
vsize: 17564
[startup+70.0037 s]
Raw data (loadavg): 1.06 0.99 0.91 3/57 32465
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 4075 0 0 0 6984 13 0 0 25 0 1 0 479731746 18526208 4053 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4523 4053 603 41 0 4482 0
vsize: 18092
[startup+80.0398 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 4493 0 0 0 7987 14 0 0 25 0 1 0 479731746 20213760 4471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4935 4471 603 41 0 4894 0
vsize: 19740
[startup+90.0397 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 4532 0 0 0 8987 14 0 0 25 0 1 0 479731746 20348928 4510 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4968 4510 603 41 0 4927 0
vsize: 19872
[startup+100.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 5259 0 0 0 9985 16 0 0 25 0 1 0 479731746 23310336 5237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5691 5237 603 41 0 5650 0
vsize: 22764
[startup+110.041 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 5793 0 0 0 10984 18 0 0 25 0 1 0 479731746 25591808 5771 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6248 5771 603 41 0 6207 0
vsize: 24992
[startup+120.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 6401 0 0 0 11982 19 0 0 25 0 1 0 479731746 28008448 6379 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6838 6379 603 41 0 6797 0
vsize: 27352
[startup+130.04 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 7176 0 0 0 12980 22 0 0 25 0 1 0 479731746 31236096 7154 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7626 7154 603 41 0 7585 0
vsize: 30504
[startup+140.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32474
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 7698 0 0 0 13978 23 0 0 25 0 1 0 479731746 33382400 7676 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8150 7676 603 41 0 8109 0
vsize: 32600
[startup+150.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 8105 0 0 0 14977 25 0 0 25 0 1 0 479731746 34988032 8083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8542 8083 603 41 0 8501 0
vsize: 34168
[startup+160.041 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 8496 0 0 0 15975 27 0 0 25 0 1 0 479731746 36851712 8474 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8997 8474 603 41 0 8956 0
vsize: 35988
[startup+170.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 8897 0 0 0 16973 29 0 0 25 0 1 0 479731746 38465536 8875 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9391 8875 603 41 0 9350 0
vsize: 37564
[startup+180.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 9289 0 0 0 17972 30 0 0 25 0 1 0 479731746 40079360 9267 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9785 9267 603 41 0 9744 0
vsize: 39140
[startup+190.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 9583 0 0 0 18971 31 0 0 25 0 1 0 479731746 41275392 9561 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10077 9561 603 41 0 10036 0
vsize: 40308
[startup+200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 10004 0 0 0 19970 32 0 0 25 0 1 0 479731746 43028480 9982 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10505 9982 603 41 0 10464 0
vsize: 42020
[startup+210.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 10438 0 0 0 20969 34 0 0 25 0 1 0 479731746 44781568 10416 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10416 603 41 0 10892 0
vsize: 43732
[startup+220.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 11015 0 0 0 21968 35 0 0 25 0 1 0 479731746 47075328 10993 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11493 10993 603 41 0 11452 0
vsize: 45972
[startup+230.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 11592 0 0 0 22967 37 0 0 25 0 1 0 479731746 49491968 11570 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12083 11570 603 41 0 12042 0
vsize: 48332
[startup+240.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 12196 0 0 0 23965 38 0 0 25 0 1 0 479731746 51896320 12174 4294967295 134512640 134672761 3221224560 3221223712 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12174 603 41 0 12629 0
vsize: 50680
[startup+250.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 12821 0 0 0 24963 41 0 0 25 0 1 0 479731746 54452224 12799 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13294 12799 603 41 0 13253 0
vsize: 53176
[startup+260.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 13337 0 0 0 25962 42 0 0 25 0 1 0 479731746 56606720 13315 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13315 603 41 0 13779 0
vsize: 55280
[startup+270.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 13887 0 0 0 26961 44 0 0 25 0 1 0 479731746 58884096 13865 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14376 13865 603 41 0 14335 0
vsize: 57504
[startup+280.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 14423 0 0 0 27959 46 0 0 25 0 1 0 479731746 61034496 14401 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14901 14401 603 41 0 14860 0
vsize: 59604
[startup+290.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 14898 0 0 0 28958 47 0 0 25 0 1 0 479731746 63053824 14876 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15394 14876 603 41 0 15353 0
vsize: 61576
[startup+300.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 15382 0 0 0 29957 48 0 0 25 0 1 0 479731746 64929792 15360 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15852 15360 603 41 0 15811 0
vsize: 63408
[startup+310.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 15693 0 0 0 30956 48 0 0 25 0 1 0 479731746 66293760 15671 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16185 15671 603 41 0 16144 0
vsize: 64740
[startup+320.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 16031 0 0 0 31954 50 0 0 25 0 1 0 479731746 67629056 16009 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16511 16009 603 41 0 16470 0
vsize: 66044
[startup+330.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 16408 0 0 0 32953 51 0 0 25 0 1 0 479731746 69091328 16386 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16868 16386 603 41 0 16827 0
vsize: 67472
[startup+340.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 16799 0 0 0 33952 52 0 0 25 0 1 0 479731746 70696960 16777 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17260 16777 603 41 0 17219 0
vsize: 69040
[startup+350.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 17200 0 0 0 34951 53 0 0 25 0 1 0 479731746 72425472 17178 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17178 603 41 0 17641 0
vsize: 70728
[startup+360.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 17541 0 0 0 35950 54 0 0 25 0 1 0 479731746 73768960 17519 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18010 17519 603 41 0 17969 0
vsize: 72040
[startup+370.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 17843 0 0 0 36950 55 0 0 25 0 1 0 479731746 75018240 17821 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18315 17821 603 41 0 18274 0
vsize: 73260
[startup+380.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 18118 0 0 0 37949 56 0 0 25 0 1 0 479731746 76091392 18096 4294967295 134512640 134672761 3221224560 3221223648 1075352577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18577 18096 603 41 0 18536 0
vsize: 74308
[startup+390.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 18436 0 0 0 38948 57 0 0 25 0 1 0 479731746 77426688 18414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18903 18414 603 41 0 18862 0
vsize: 75612
[startup+400.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 18779 0 0 0 39948 58 0 0 25 0 1 0 479731746 78888960 18757 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19260 18757 603 41 0 19219 0
vsize: 77040
[startup+410.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 19096 0 0 0 40947 59 0 0 25 0 1 0 479731746 80093184 19074 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19554 19074 603 41 0 19513 0
vsize: 78216
[startup+420.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 19426 0 0 0 41946 60 0 0 25 0 1 0 479731746 81432576 19404 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19881 19404 603 41 0 19840 0
vsize: 79524
[startup+430.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 19744 0 0 0 42946 60 0 0 25 0 1 0 479731746 82784256 19722 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20211 19722 603 41 0 20170 0
vsize: 80844
[startup+440.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32476
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20057 0 0 0 43945 61 0 0 25 0 1 0 479731746 84111360 20035 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20535 20035 603 41 0 20494 0
vsize: 82140
[startup+450.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 44945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+460.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 45945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223664 134555126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+470.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 46945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+480.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 47945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+490.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 48945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+500.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 49945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+510.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 50944 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+520.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 51944 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+530.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 52945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+540.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 53945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+550.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 54945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+560.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 55945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+570.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 56945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+580.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 57945 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+590.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 58946 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+600.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 59946 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+610.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 60946 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+620.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 61946 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+630.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 62947 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+640.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 63947 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+650.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 64947 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+660.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 65947 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+670.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 66947 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+680.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 67948 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+690.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 68948 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+700.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 69948 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+710.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 70948 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+720.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 71948 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+730.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 72949 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+740.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 73949 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+750.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 74949 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+760.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 75949 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+770.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 76949 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+780.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 77950 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+790.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 78950 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+800.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 79950 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+810.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 80950 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+820.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 81950 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+830.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 82951 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+840.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20105 0 0 0 83951 62 0 0 25 0 1 0 479731746 84242432 20083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20083 603 41 0 20526 0
vsize: 82268
[startup+850.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 84951 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+860.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 85951 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+870.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 86951 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+880.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 87952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+890.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 88951 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+900.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 89952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+910.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 90952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 91952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+930.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 92952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223744 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+940.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 93952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+950.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 94952 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+960.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 95953 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+970.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 96953 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+980.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 97953 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+990.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 98953 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 99954 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 100954 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 101954 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 102954 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 103954 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 104955 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 105955 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 106955 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20106 0 0 0 107954 62 0 0 25 0 1 0 479731746 84242432 20084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20084 603 41 0 20526 0
vsize: 82268
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 108955 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 109955 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 110955 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 111955 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 112956 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 113956 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223664 134559829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 114956 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 115956 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 116956 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20107 0 0 0 117957 62 0 0 25 0 1 0 479731746 84242432 20085 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20567 20085 603 41 0 20526 0
vsize: 82268
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20110 0 0 0 118957 62 0 0 25 0 1 0 479731746 84766720 20088 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20695 20088 603 41 0 20654 0
vsize: 82780
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32478
Raw data (stat): 32421 (minisat+) R 32420 28546 28545 0 -1 0 20170 0 0 0 119957 62 0 0 25 0 1 0 479731746 85037056 20148 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20761 20148 603 41 0 20720 0
vsize: 83044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32478
Raw data (stat): 32421 (minisat+) Z 32420 28546 28545 0 -1 12 20173 0 0 0 119957 66 0 0 25 0 1 0 479731746 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.11
CPU time (s): 1200.24
CPU user time (s): 1199.58
CPU system time (s): 0.667898
CPU usage (%): 100.011
Max. virtual memory (Kb): 83044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####